Home | Intuitionistic Logic Explorer Theorem List (p. 133 of 133) | < Previous Wrap > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nninff 13201 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nnsf 13202* | Domain and range of . Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | peano4nninf 13203* | The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | peano3nninf 13204* | The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfalllemn 13205* | Lemma for nninfall 13207. Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfalllem1 13206* | Lemma for nninfall 13207. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfall 13207* | Given a decidable predicate on ℕ∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which is a decidable predicate is that it assigns a value of either or (which can be thought of as false and true) to every element of ℕ∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfex 13208 | ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfsellemdc 13209* | Lemma for nninfself 13212. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ DECID | ||
Theorem | nninfsellemcl 13210* | Lemma for nninfself 13212. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfsellemsuc 13211* | Lemma for nninfself 13212. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfself 13212* | Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | nninfsellemeq 13213* | Lemma for nninfsel 13216. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsellemqall 13214* | Lemma for nninfsel 13216. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsellemeqinf 13215* | Lemma for nninfsel 13216. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsel 13216* | is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ ℕ∞ | ||
Theorem | nninfomnilem 13217* | Lemma for nninfomni 13218. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ ℕ∞ Omni | ||
Theorem | nninfomni 13218 | ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ Omni | ||
Theorem | nninffeq 13219* | Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 4-Aug-2023.) |
ℕ∞ ℕ∞ | ||
Theorem | exmidsbthrlem 13220* | Lemma for exmidsbthr 13221. (Contributed by Jim Kingdon, 11-Aug-2022.) |
ℕ∞ EXMID | ||
Theorem | exmidsbthr 13221* | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
EXMID | ||
Theorem | exmidsbth 13222* |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6855) is the
proof of the Schroeder-Bernstein Theorem from the Metamath Proof
Explorer database (in which excluded middle holds), but adapted to use
EXMID as an antecedent rather than being unconditionally
true, as in
the non-intuitionist proof at
https://us.metamath.org/mpeuni/sbth.html 6855.
The reverse direction (exmidsbthr 13221) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.) |
EXMID | ||
Theorem | sbthomlem 13223 | Lemma for sbthom 13224. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
Omni ⊔ | ||
Theorem | sbthom 13224 | Schroeder-Bernstein is not possible even for . We know by exmidsbth 13222 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.) |
Omni EXMID | ||
Theorem | qdencn 13225* | The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 10977 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
Theorem | refeq 13226* | Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.) |
Theorem | triap 13227 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
DECID # | ||
Theorem | isomninnlem 13228* | Lemma for isomninn 13229. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
frec Omni | ||
Theorem | isomninn 13229* | Omniscience stated in terms of natural numbers. Similar to isomnimap 7009 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 30-Aug-2023.) |
Omni | ||
Theorem | cvgcmp2nlemabs 13230* | Lemma for cvgcmp2n 13231. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting as the sum of and a term which gets smaller as gets large. (Contributed by Jim Kingdon, 25-Aug-2023.) |
Theorem | cvgcmp2n 13231* | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
Theorem | trilpolemclim 13232* | Lemma for trilpo 13239. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
Theorem | trilpolemcl 13233* | Lemma for trilpo 13239. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemisumle 13234* | Lemma for trilpo 13239. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
Theorem | trilpolemgt1 13235* | Lemma for trilpo 13239. The case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemeq1 13236* | Lemma for trilpo 13239. The case. This is proved by noting that if any is zero, then the infinite sum is less than one based on the term which is zero. We are using the fact that the sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemlt1 13237* | Lemma for trilpo 13239. The case. We can use the distance between and one (that is, ) to find a position in the sequence where terms after that point will not add up to as much as . By finomni 7012 we know the terms up to either contain a zero or are all one. But if they are all one that contradicts the way we constructed , so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemres 13238* | Lemma for trilpo 13239. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpo 13239* |
Real number trichotomy implies the Limited Principle of Omniscience
(LPO). We expect that we'd need some form of countable choice to prove
the converse.
Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 13237 (which means the sequence contains a zero), trilpolemeq1 13236 (which means the sequence is all ones), and trilpolemgt1 13235 (which is not possible). (Contributed by Jim Kingdon, 23-Aug-2023.) |
Omni | ||
Theorem | supfz 13240 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
Theorem | inffz 13241 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
inf | ||
Theorem | taupi 13242 | Relationship between and . This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
Theorem | ax1hfs 13243 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) |
Theorem | dftest 13244 |
A proposition is testable iff its negative or double-negative is true.
See Chapter 2 [Moschovakis] p. 2.
We do not formally define testability with a new token, but instead use DECID before the formula in question. For example, DECID corresponds to " is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) For statements about testable propositions, search for the keyword "testable" in the comments of statements, for instance using the Metamath command "MM> SEARCH * "testable" / COMMENTS". (New usage is discouraged.) |
DECID | ||
These are definitions and proofs involving an experimental "allsome" quantifier (aka "all some"). In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like do not imply that is ever true, leading to vacuous truths. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem. The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines. I do not expect this to be used much in metamath, because in metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it. The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow ! , and when restricted (applied to a class) we allow ! . The first symbol after the setvar variable must always be if it is the form applied to a class, and since cannot begin a wff, it is unambiguous. The looks like it would be a problem because or might include implications, but any implication arrow within any wff must be surrounded by parentheses, so only the implication arrow of ! can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html I hope that others will eventually agree that allsome is awesome. | ||
Syntax | walsi 13245 | Extend wff definition to include "all some" applied to a top-level implication, which means is true whenever is true, and there is at least least one where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Syntax | walsc 13246 | Extend wff definition to include "all some" applied to a class, which means is true for all in , and there is at least one in . (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Definition | df-alsi 13247 | Define "all some" applied to a top-level implication, which means is true whenever is true and there is at least one where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Definition | df-alsc 13248 | Define "all some" applied to a class, which means is true for all in and there is at least one in . (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Theorem | alsconv 13249 | There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.) |
! ! | ||
Theorem | alsi1d 13250 | Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Theorem | alsi2d 13251 | Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Theorem | alsc1d 13252 | Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! | ||
Theorem | alsc2d 13253 | Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
! |
< Previous Wrap > |
Copyright terms: Public domain | < Previous Wrap > |