Home Intuitionistic Logic ExplorerTheorem List (p. 71 of 133) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 7001-7100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfinct 7001* A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)

Theoremomct 7002 is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)

Theoremctfoex 7003* A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)

2.6.36  Omniscient sets

Syntaxcomni 7004 Extend class definition to include the class of omniscient sets.
Omni

Syntaxxnninf 7005 Set of nonincreasing sequences in .

Definitiondf-omni 7006* An omniscient set is one where we can decide whether a predicate (here represented by a function ) holds (is equal to ) for all elements or fails to hold (is equal to ) for some element. Definition 3.1 of [Pierik], p. 14.

In particular, Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)

Omni

Definitiondf-nninf 7007* Define the set of nonincreasing sequences in . Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 9041 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used or , but the former allows us to take advantage of (df2o3 6327) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)

Theoremisomni 7008* The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
Omni

Theoremisomnimap 7009* The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
Omni

Theoremenomnilem 7010 Lemma for enomni 7011. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
Omni Omni

Theoremenomni 7011 Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either Omni or Omni. The former is a better match to conventional notation in the sense that df2o3 6327 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.)
Omni Omni

Theoremfinomni 7012 A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.)
Omni

Theoremexmidomniim 7013 Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7014. (Contributed by Jim Kingdon, 29-Jun-2022.)
EXMID Omni

Theoremexmidomni 7014 Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
EXMID Omni

Theoremexmidlpo 7015 Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.)
EXMID Omni

Theoremfodjuomnilemdc 7016* Lemma for fodjuomni 7021. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
DECID inl

Theoremfodjuf 7017* Lemma for fodjuomni 7021 and fodjumkv 7034. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
inl

Theoremfodjum 7018* Lemma for fodjuomni 7021 and fodjumkv 7034. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
inl

Theoremfodju0 7019* Lemma for fodjuomni 7021 and fodjumkv 7034. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
inl

Theoremfodjuomnilemres 7020* Lemma for fodjuomni 7021. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.)
Omni              inl

Theoremfodjuomni 7021* A condition which ensures is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.)
Omni

Theoreminfnninf 7022 The point at infinity in ℕ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.)

Theoremnnnninf 7023* Elements of ℕ corresponding to natural numbers. The natural number corresponds to a sequence of ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 7022. Remark/TODO: the theorem still holds if , that is, the antecedent could be weakened to . (Contributed by Jim Kingdon, 14-Jul-2022.)

Theoremctssexmid 7024* The decidability condition in ctssdc 6998 is needed. More specifically, ctssdc 6998 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.)
Omni

2.6.37  Markov's principle

Syntaxcmarkov 7025 Extend class definition to include the class of Markov sets.
Markov

Definitiondf-markov 7026* A Markov set is one where if a predicate (here represented by a function ) on that set does not hold (where hold means is equal to ) for all elements, then there exists an element where it fails (is equal to ). Generalization of definition 2.5 of [Pierik], p. 9.

In particular, Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)

Markov

Theoremismkv 7027* The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.)
Markov

Theoremismkvmap 7028* The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.)
Markov

Theoremismkvnex 7029* The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.)
Markov

Theoremomnimkv 7030 An omniscient set is Markov. In particular, the case where is means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
Omni Markov

Theoremexmidmp 7031 Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.)
EXMID Markov

Theoremmkvprop 7032* Markov's Principle expressed in terms of propositions (or more precisely, the case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.)
Markov DECID

Theoremfodjumkvlemres 7033* Lemma for fodjumkv 7034. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
Markov              inl

Theoremfodjumkv 7034* A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.)
Markov

2.6.38  Cardinal numbers

Syntaxccrd 7035 Extend class definition to include the cardinal size function.

Definitiondf-card 7036* Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)

Theoremcardcl 7037* The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)

Theoremisnumi 7038 A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)

Theoremfinnum 7039 Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremonenon 7040 Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)

Theoremcardval3ex 7041* The value of . (Contributed by Jim Kingdon, 30-Aug-2021.)

Theoremoncardval 7042* The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)

Theoremcardonle 7043 The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)

Theoremcard0 7044 The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)

Theoremcarden2bex 7045* If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)

Theorempm54.43 7046 Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)

Theorempr2nelem 7047 Lemma for pr2ne 7048. (Contributed by FL, 17-Aug-2008.)

Theorempr2ne 7048 If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)

Theoremexmidonfinlem 7049* Lemma for exmidonfin 7050. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
DECID

Theoremexmidonfin 7050 If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6766 and nnon 4523. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
EXMID

Theoremen2eleq 7051 Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)

Theoremen2other2 7052 Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)

Theoremdju1p1e2 7053 Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)

Theoreminfpwfidom 7054 The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption because this theorem also implies that is a set if is.) (Contributed by Mario Carneiro, 17-May-2015.)

Theoremexmidfodomrlemeldju 7055 Lemma for exmidfodomr 7060. A variant of djur 6954. (Contributed by Jim Kingdon, 2-Jul-2022.)
inl inr

Theoremexmidfodomrlemreseldju 7056 Lemma for exmidfodomrlemrALT 7059. A variant of eldju 6953. (Contributed by Jim Kingdon, 9-Jul-2022.)
inl inr

Theoremexmidfodomrlemim 7057* Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
EXMID

Theoremexmidfodomrlemr 7058* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
EXMID

TheoremexmidfodomrlemrALT 7059* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7058. In particular, this proof uses eldju 6953 instead of djur 6954 and avoids djulclb 6940. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
EXMID

Theoremexmidfodomr 7060* Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.)
EXMID

2.6.39  Axiom of Choice equivalents

Syntaxwac 7061 Formula for an abbreviation of the axiom of choice.
CHOICE

Definitiondf-ac 7062* The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49.

There are some decisions about how to write this definition especially around whether ax-setind 4452 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)

CHOICE

Theoremacfun 7063* A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
CHOICE

Theoremexmidaclem 7064* Lemma for exmidac 7065. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
CHOICE EXMID

Theoremexmidac 7065 The axiom of choice implies excluded middle. See acexmid 5773 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
CHOICE EXMID

2.6.40  Cardinal number arithmetic

Theoremendjudisj 7066 Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)

Theoremdjuen 7067 Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)

Theoremdjuenun 7068 Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)

Theoremdju1en 7069 Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremdju0en 7070 Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremxp2dju 7071 Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremdjucomen 7072 Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremdjuassen 7073 Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremxpdjuen 7074 Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremdjudoml 7075 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)

Theoremdjudomr 7076 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)

PART 3  CHOICE PRINCIPLES

We have already introduced the full Axiom of Choice df-ac 7062 but since it implies excluded middle as shown at exmidac 7065, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.

3.1  Countable Choice and Dependent Choice

3.1.1  Introduce Countable Choice

Syntaxwacc 7077 Formula for an abbreviation of countable choice.
CCHOICE

Definitiondf-cc 7078* The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7062 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
CCHOICE

Theoremccfunen 7079* Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
CCHOICE

PART 4  REAL AND COMPLEX NUMBERS

This section derives the basics of real and complex numbers.

To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6370 and similar theorems ), going from there to positive integers (df-ni 7112) and then positive rational numbers (df-nqqs 7156) does not involve a major change in approach compared with the Metamath Proof Explorer.

It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle. With excluded middle, it is natural to define the cut as the lower set only (as Metamath Proof Explorer does), but we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero".

4.1  Construction and axiomatization of real and complex numbers

4.1.1  Dedekind-cut construction of real and complex numbers

Syntaxcnpi 7080 The set of positive integers, which is the set of natural numbers with 0 removed.

Note: This is the start of the Dedekind-cut construction of real and complex numbers.

Syntaxcmi 7082 Positive integer multiplication.

Syntaxclti 7083 Positive integer ordering relation.

Syntaxcmpq 7085 Positive pre-fraction multiplication.

Syntaxcltpq 7086 Positive pre-fraction ordering relation.

Syntaxceq 7087 Equivalence class used to construct positive fractions.

Syntaxcnq 7088 Set of positive fractions.

Syntaxc1q 7089 The positive fraction constant 1.

Syntaxcmq 7091 Positive fraction multiplication.

Syntaxcrq 7092 Positive fraction reciprocal operation.

Syntaxcltq 7093 Positive fraction ordering relation.

Syntaxceq0 7094 Equivalence class used to construct nonnegative fractions.
~Q0

Syntaxcnq0 7095 Set of nonnegative fractions.
Q0

Syntaxc0q0 7096 The nonnegative fraction constant 0.
0Q0