Intuitionistic Logic Explorer Home Page  First > Last > 

Mirrors > Home > ILE Home > Th. List > Recent 
Intuitionistic Logic (Wikipedia [accessed 19Jul2015], Stanford Encyclopedia of Philosophy [accessed 19Jul2015]) can be thought of as a constructive logic in which we must build and exhibit concrete examples of objects before we can accept their existence. Unproved statements in intuitionistic logic are not given an intermediate truth value, instead, they remain of unknown truth value until they are either proved or disproved. Intuitionist logic can also be thought of as a weakening of classical logic such that the law of excluded middle (LEM), (φ ∨ ¬ φ), doesn't always hold. Specifically, it holds if we have a proof for φ or we have a proof for ¬ φ, but it doesn't necessarily hold if we don't have a proof of either one. There is also no rule for double negation elimination. Brouwer observed in 1908 that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections.
Contents of this page  Related pages External links 
(Placeholder for future use)
(By Gérard Lang, 7May2018)
Mario Carneiro's work (Metamath database) "iset.mm" provides in Metamath a development of "set.mm" whose eventual aim is to show how many of the theorems of set theory and mathematics that can be derived from classical first order logic can also be derived from a weaker system called "intuitionistic logic." To achieve this task, iset.mm adds (or substitutes) intuitionistic axioms for a number of the classical logical axioms of set.mm.
Among these new axioms, the first six (axia1, axia2, axia3, axio, axin1, and axin2), when added to ax1, ax2, and axmp, allow for the development of intuitionistic propositional logic. We omit the classical axiom ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) (which is ax3 in set.mm). Each of our new axioms is a theorem of classical propositional logic, but ax3 cannot be derived from them. Similarly, other basic classical theorems, like the third middle excluded or the equivalence of a proposition with its double negation, cannot be derived in intuitionistic propositional calculus. Glivenko showed that a proposition φ is a theorem of classical propositional calculus if and only if ¬¬φ is a theorem of intuitionistic propositional calculus.
The next 4 new axioms (axial, axi5r, axie1, and axie2) together with the set.mm axioms ax4, ax5, ax7, and axgen do not mention equality or distinct variables.
The axi9 axiom is just a slight variation of the classical ax9. The classical axiom ax12 is strengthened into first axi12 and then axbndl (two results which would be fairly readily equivalent to ax12 classically but which do not follow from ax12, at least not in an obvious way, in intuitionistic logic). The substitution of axi9, axi12, and axbndl for ax9 and ax12 and the inclusion of ax8, ax10, ax11, ax13, ax14, and ax17 allow for the development of the intuitionistic predicate calculus.
Each of the new axioms is a theorem of classical first order logic with equality. But some axioms of classical first order logic with equality, like ax3, cannot be derived in the intuitionistic predicate calculus.
One of the major interests of the intuitionistic predicate calculus is that its use can be considered as a realization of the program of the constructivist philosophical view of mathematics.
As with the classical axioms we have propositional logic and predicate logic.
The axioms of intuitionistic propositional logic consist of some of the axioms from classical propositional logic, plus additional axioms for the operation of the 'and', 'or' and 'not' connectives.
Axiom Simp  ax1  ⊢ (φ → (ψ → φ)) 
Axiom Frege  ax2  ⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) 
Rule of Modus Ponens  axmp  ⊢ φ & ⊢ φ → ψ ⇒ ⊢ ψ 
Left 'and' elimination  axia1  ⊢ ((φ ∧ ψ) → φ) 
Right 'and' elimination  axia2  ⊢ ((φ ∧ ψ) → ψ) 
'And' introduction  axia3  ⊢ (φ → (ψ → (φ ∧ ψ))) 
Definition of 'or'  axio  ⊢ (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ))) 
'Not' introduction  axin1  ⊢ ((φ → ¬ φ) → ¬ φ) 
'Not' elimination  axin2  ⊢ (¬ φ → (φ → ψ)) 
Unlike in classical propositional logic, 'and' and 'or' are not readily defined in terms of implication and 'not'. In particular, φ ∨ ψ is not equivalent to ¬ φ → ψ, nor is φ → ψ equivalent to ¬ φ ∨ ψ, nor is φ ∧ ψ equivalent to ¬ (φ → ¬ ψ).
The axin1 axiom is a form of proof by contradiction which does hold intuitionistically. That is, if φ implies a contradiction (such as its own negation), then one can conclude ¬ φ. By contrast, assuming ¬ φ and then deriving a contradiction only serves to prove ¬ ¬ φ, which in intuitionistic logic is not the same as φ.
The biconditional can be defined as the conjunction of two implications, as in dfbi2 and dfbi.
Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (forall) and ∃ (thereexists). Unlike in classical logic, ∃ cannot be defined in terms of ∀. As in classical logic, we also add = for equality (which is key to how we handle substitution in metamath) and ∈ (which for current purposes can just be thought of as an arbitrary predicate, but which will later come to mean set membership).
Our axioms are based on the classical set.mm predicate logic axioms, but adapted for intuitionistic logic, chiefly by adding additional axioms for ∃ and also changing some aspects of how we handle negations.
Axiom of Specialization  ax4  ⊢ (∀xφ → φ) 
Axiom of Quantified Implication  ax5  ⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ)) 
The converse of ax5o  axi5r  ⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ψ)) 
Axiom of Quantifier Commutation  ax7  ⊢ (∀x∀yφ → ∀y∀xφ) 
Rule of Generalization  axgen  ⊢ φ => ⊢ ∀xφ 
x is bound in ∀xφ  axial  ⊢ (∀xφ → ∀x∀xφ) 
x is bound in ∃xφ  axie1  ⊢ (∃xφ → ∀x∃xφ) 
Define existential quantification  axie2  ⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ))) 
Axiom of Equality  ax8  ⊢ (x = y → (x = z → y = z)) 
Axiom of Existence  axi9  ⊢ ∃x x = y 
Axiom of Quantifier Substitution  ax10  ⊢ (∀x x = y → ∀y y = x) 
Axiom of Variable Substitution  ax11  ⊢ (x = y → (∀yφ → ∀x(x = y → φ))) 
Axiom of Quantifier Introduction  axi12  ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y))) 
Axiom of Bundling  axbndl  ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀x∀z(x = y → ∀z x = y))) 
Left Membership Equality  ax13  ⊢ (x = y → (x ∈ z → y ∈ z)) 
Right Membership Equality  ax14  ⊢ (x = y → (z ∈ x → z ∈ y)) 
Distinctness  ax17  ⊢ (φ → ∀xφ), where x does not occur in φ 
Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets." A set can be an element of another set, and this relationship is indicated by the symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. These axioms were developed in response to Russell's Paradox, a discovery that revolutionized the foundations of mathematics and logic.
In the IZF axioms that follow, all set variables are assumed to be distinct. If you click on their links you will see the explicit distinct variable conditions.
Axiom of Extensionality  axext  ⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y) 
Axiom of Collection  axcoll  ⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ) 
Axiom of Separation  axsep  ⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ)) 
Axiom of Power Sets  axpow  ⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y) 
Axiom of Pairing  axpr  ⊢ ∃z∀w((w = x ∨ w = y) → w ∈ z) 
Axiom of Union  axun  ⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y) 
Axiom of Set Induction  axsetind  ⊢ (∀𝑎(∀y ∈ 𝑎 [y / 𝑎]φ → φ) → ∀𝑎φ) 
Axiom of Infinity  axiinf  ⊢ ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x)) 
We develop set theory based on the Intuitionistic ZermeloFraenkel (IZF) system, mostly following the IZF axioms as laid out in [Crosilla]. Constructive ZermeloFraenkel (CZF), also described in Crosilla, is not as easy to formalize in metamath because the Axiom of Restricted Separation would require us to develop the ability to classify formulas as bounded formulas, similar to the machinery we have built up for asserting on whether variables are free in formulas.
Listed here are some examples of starting points for your journey through the maze. Some are stated just as they would be in a nonconstructive context; others are here to highlight areas which look different constructively. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory.
The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic CrossReference useful.
Propositional calculus Predicate calculus Set theory Real and complex numbers 
For the student or master of classical mathematics, constructive mathematics can be baffling. One can get over some of the intial hurdles of understanding how constructive mathematics works and why it might be interesting by reading [Bauer] but that work does little to explain in concrete terms how to write proofs in intuitionistic logic. Fortunately, metamath helps with one of the biggest hurdles: noticing when one is even using the law of the excluded middle or the axiom of choice. But suppose you have a classical proof from the Metamath Proof Explorer and it fails to verify when you copy it over to the Intuitionistic Logic Explorer. What then? Here are some rules of thumb in converting classical proofs to intuitionistic ones.
This is a list of theorems from the Metamath Proof Explorer (which assumes the law of the excluded middle throughout) which we do not have in the Intuitionistic Logic Explorer (generally because they are not provable without the law of the excluded middle, although some could be proved but aren't for a variety of reasons), together with the closest replacements.
set.mm  iset.mm  notes  

ax3 , con4d , con34b , necon4bd  con3  The form of contraposition which removes negation does not hold in intutionistic logic.  
pm2.18  pm2.01  See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.  
pm2.18d  pm2.01d  See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.  
notnotrd , notnotri , notnot2 , notnot  notnot1  Double negation introduction holds but not double negation elimination.  
mt3d  mtod  
nyl2  nsyl  
pm2.61 , pm2.61d , pm2.61d1 , pm2.61d2 , pm2.61i , pm2.61ii , pm2.61nii , pm2.61iii , pm2.61ian , pm2.61dan , pm2.61ddan , pm2.61dda , pm2.61ine , pm2.61ne , pm2.61dne , pm2.61dane , pm2.61da2ne , pm2.61da3ne , pm2.61iine  none  
impcon4bid, con4bid, notbi, con1bii, con4bii, con2bii  con3, condc  
xor3 , nbbn  xorbin, xornbi, xor3dc, nbbndc  
biass  biassdc  
dfor , pm4.64 , pm2.54 , orri , orrd  pm2.53, ori, ord  
pm4.63  pm3.2im  
iman  imanim  
annim  annimim  
oran  oranim  
ianor  pm3.14  
biluk  bilukdc  
ecase3d  none  This is a form of case elimination.  
dedlem0b  dedlemb  
3ianor  3ianorr  
dfex  exalim  
alex  alexim  
exnal  exnalim  
alexn  alexnim  
exanali  exanaliim  
19.35  19.351  
19.30  none  
19.36  19.361  
19.37  19.371  
19.32  19.32r  
19.31  19.31r  
exdistrf  exdistrfor  
exmo  exmonim  
mo2  mo2r, mo3  
nne  nner, nnedc  
exmidne  dcne  
neor  pm2.53, ori, ord  
neorian  pm3.14  
nnel  none  The reverse direction could be proved; the forward direction is double negation elimination.  
nfrald  nfraldxy, nfraldya  
rexnal  rexnalim  
rexanali  none  
nrexralim  none  
dfral2  ralexim  
dfrex2  rexalim  
nfrexd  nfrexdxy, nfrexdya  
nfral  nfralxy, nfralya  
nfra2  nfra1, nfralya  
nfrex  nfrexxy, nfrexya  
r19.30  none  
r19.35  r19.351  
ralcom2  ralcom  
sspss  sspssr  
n0f  n0rf  
n0  n0r  
neq0  neq0r  
reximdva0  reximdva0m  
rabn0  rabn0m, rabn0r  
ssdif0  ssdif0im  
inssdif0  inssdif0im  
undif2  undif2ss  
uneqdifeq  uneqdifeqim  
r19.45zv  r19.45mv  
dfif2  dfif  
ifsb  none  
dfif4  none  Unused in set.mm  
dfif5  none  Unused in set.mm  
ifnot  none  
ifan  none  
ifor  none  
ifeq1da, ifeq2da  none  
ifclda  none  
ifeqda  none  
elimif , ifbothda , ifboth , ifid , eqif , ifval , elif , ifel , ifcl , ifcld , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD  none  
dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel , ifex , ifexg  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
iundif2  iundif2ss  
trintss  trintssm  
trint0  trint0m  
csbexg , csbex  csbexga, csbexa  set.mm uses case elimination to remove the A ∈ V condition.  
intabs  none  Lightly used in set.mm, and the set.mm proof is not intuitionistic  
moabex  euabex  In general, most of the set.mm ∃! theorems still hold, but a decent number of the ∃* ones get caught up on "there are two cases: the set exists or it does not"  
snex  snexg, snex  The iset.mm version of snex has an additional hypothesis  
opex  opexg, opex  The iset.mm version of opex has additional hypotheses  
dfso  dfiso  Although we define Or to describe a weakly linear order (such as real numbers), there are some orders which are also trichotomous, for example nntri3or, pitri3or, and nqtri3or.  
sotric  sotricim  One direction, for any weak linear order.  
sotritric  For a trichotomous order.  
nntri2  For the specific order E Or 𝜔  
pitric  For the specific order <_{N} Or N  
nqtric  For the specific order <_{Q} Or Q  
sotrieq  sotritrieq  For a trichotomous order  
sotrieq2  see sotrieq and then apply ioran  
issoi  issod, ispod  Many of the set.mm usages of issoi don't carry over, so there is less need for this convenience theorem.  
isso2i  issod  Presumably this could be proved if we need it.  
dffr and all theorems using Fr  none  Right now iset.mm does not have a wellfounded predicate
( Presumably if we were to add This definition has some problems when A is a proper class. As such, axsetind has to be stated as a schema instead: ∀x(∀y(y ∈ x → y ∈ 𝑆) → x ∈ 𝑆) → 𝑆 = V There are two ways to say no infinite descending sequence, using ∃¬ or ¬ ∀, which are not intuitionistically equivalent. Furthermore there are some trivial commutations that are not intuitionistically valid. So I think that makes the following definition possibilities: R Fr A ↔ ∀𝑠(∀x(∀y(y𝑅x → y ∈ 𝑠) → x ∈ 𝑠) → A ⊆ 𝑠) R Fr2 A ↔ ∀𝑠(𝑠 ⊆ A → (∀x ∈ 𝑠∃y ∈ 𝑠y𝑅x → 𝑠 = ∅)) R Fr3 A ↔ ∀𝑠(𝑠 ⊆ A → (∃xx ∈ 𝑠 → ∃x ∈ 𝑠∀y ∈ 𝑠¬ y𝑅x)) The set.mm definition is roughly Fr3 (but it uses nonempty in place of inhabited). We can probably just focus on the first definition, but ideally we'd prove it in set.mm (to show that given excluded middle it is equivalent to the definition of Fr in set.mm). If we adopted wellfoundedness along these lines, we'd be able to add wellfoundedness to the definition of an ordinal and prove many of the ordinal theorems without axsetind. The proof of ordirr would be similar to the current proof of elirr except that axsetind would be replaced by E Fr A and V throughout the elirr proof would be replaced by A. Likewise for en2lp. These theorems (for ordinals) would then not rely on axsetind. 

dfwe (and all theorems using We)  none  Ordering is moderately different in constructive logic, so if there is anything along these lines worth doing it will be different from set.mm.  
tz7.7  none  
ordelssne  none  
ordelpss  none  
ordsseleq  onelss, eqimss  Taken together, onelss and eqimss represent the reverse direction of the biconditional from ordsseleq  
ordtri3or  nntri3or  Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid.  
ordtri2  nntri2  ordtri2 for all ordinals presumably implies excluded middle although we don't have a specific proof analogous to ordtriexmid.  
ordtri3 , ordtri4 , ordtri2or2 , ordtri2or3 , dford2  none  Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid. We don't have similar proofs for every variation of of trichotomy but most of them are presumably powerful enough to imply excluded middle.  
ordtri1 , ontri1 , onssneli , onssnel2i  ssnel, nntri1  ssnel is a trichotomylike theorem which does hold, although it is an implication whereas ordtri1 is a biconditional. nntri1 is biconditional, but just for natural numbers.  
ordtr2 , ontr2  none  See also ordelpss in set.mm  
ordtr3  none  This is weak linearity of ordinals, which presumably implies excluded middle by ordsoexmid.  
ordtri2or  none  Implies excluded middle as shown at ordtri2orexmid.  
ord0eln0 , on0eln0  ne0i, nn0eln0  
nsuceq0  nsuceq0g  
ordsssuc  trsucss  
ordequn  none  If you know which ordinal is larger, you can achieve a similar result via theorems such as oneluni or ssequn1.  
ordun  onun2  
dmxpid  dmxpm  
relimasn  imasng  
opswap  opswapg  
cnvso  cnvsom  
iotaex  iotacl, euiotaex  
dffun3  dffun5r  
dffun5  dffun5r  
fvex  funfvex  when evaluating a function within its domain  
fvexg, fvex  when the function is a set and is evaluated at a set  
relrnfvex  when evaluating a relation whose range is a set  
mptfvex  when the function is defined via mapsto, yields a set for all inputs, and is evaluated at a set  
1stexg, 2ndexg  for the functions 1^{st} and 2^{nd}  
ndmfv  ndmfvg  The ¬ A ∈ V case is fvprc.  
elfvdm  relelfvdm  
elfvex  relelfvdm  
f0cli  ffvelrn  
funiunfv  fniunfv, funiunfvdm  
funiunfvf  funiunfvdmf  
eluniima  eluniimadm  
riotaex  riotacl, riotaexg  
nfriotad  nfriotadxy  
csbriota , csbriotagOLD  csbriotag  
riotaxfrd  none  Although it may be intuitionizable, it is lightly used in set.mm.  
ovex  fnovex  when the operation is a function evaluated within its domain.  
fvexg, fvex  when the operation is a set and is evaluated at a set  
relrnfvex  when the operation is a relation whose range is a set  
mpt2fvex  When the operation is defined via mapsto, yields a set on any inputs, and is being evaluated at two sets.  
fnov  fnovim  
ov3  ovi3  Although set.mm's ov3 could be proved, it is only used a few places in set.mm, and in iset.mm those places need the modified form found in ovi3.  
oprssdm  none  
ndmovg , ndmov  ndmfvg  These theorems are generally used in set.mm for case elimination which is why we just have the general ndmfvg rather than an operationspecific version.  
ndmovcl , ndmovcom , ndmovass , ndmovdistr , ndmovord , and ndmovordi  none  These theorems are generally used in set.mm for case elimination and the most straightforward way to avoid them is to add conditions that we are evaluating functions within their domains.  
ndmovrcl  elmpt2cl, relelfvdm  
caov4  caov4d  Note that caov4d has a closure hypothesis.  
caov411  caov411d  Note that caov411d has a closure hypothesis.  
caov42  caov42d  Note that caov42d has a closure hypothesis.  
caovdir  caovdird  caovdird adds some constraints about where the operations are evaluated.  
caovdilem  caovdilemd  
caovlem2  caovlem2d  
caovmo  caovimo  
ofval  fnofval  
offn , offveq , caofid0l , caofid0r , caofid1 , caofid2  none  Assuming we really need to add conditions that the operations are functions being evaluated within their domains, there would be a fair bit of intuitionizing.  
ordeleqon  none  
ssonprc  none  not provable (we conjecture), but interesting enough to intuitionize anyway. ∪ A = On → A ∉ 𝑉 is provable, and (B ∈ On ∧ ∪ A ⊆ B) → A ∈ 𝑉 is provable. (Why isn't dfpss stated so that the set difference is inhabited? If so, you could prove ∪ A ⊊ On → A ∈ 𝑉.)  
onint  none  Conjectured to not be provable without excluded middle. If you apply onint to a pair you can derive totality of the order.  
onint0  none  Thought to be "trivially not intuitionistic", and it is not clear if there is an alternate way to state it that is true. If the empty set is in A then of course ^ A = (/), but the converse seems difficult. I don't know so much about the structure of the ordinals without linearity,  
onssmin, onminesb, onminsb  none  Conjectured to not be provable without excluded middle, for the same reason as onint.  
oninton  none yet  This one (with nonempty changed to inhabited) I think can still be salvaged though. From the fact that it is inhabited you get that it exists, and is a subset of an ordinal x. It is an intersection of transitive sets so it is transitive, and of course all its members are members of x so they are transitive too. And E. Fr A falls to subsets.  
onintrab, onintrab2  none yet  The set.mm proof uses oninton.  
oneqmin  none  Falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.  
onminex  none yet  falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.  
onmindif2  none  Conjectured to not be provable without excluded middle.  
onmindif2  none  Conjectured to not be provable without excluded middle.  
ordpwsuc  ordpwsucss  See the ordpwsucss comment for discussion of the succcessorlike properites of (𝒫 A ∩ On). Full ordpwsuc implies excluded middle as seen at ordpwsucexmid.  
ordsucelsuc  onsucelsucr, nnsucelsuc  The converse of onsucelsucr implies excluded middle, as shown at onsucelsucexmid.  
ordsucsssuc  onsucsssucr, nnsucsssuc  The converse of onsucsssucr implies excluded middle, as shown at onsucsssucexmid.  
ordsucuniel  sucunielr  Full ordsucuniel implies excluded middle, as shown at ordsucunielexmid.  
ordsucun  none yet  Conjectured to be provable in the reverse direction, but not the forward direction (implies some order totality).  
ordunpr  none  Presumably not provable without excluded middle.  
ordunel  none  Conjectured to not be provable (ordunel implies ordsucun).  
onsucuni, ordsucuni  none  Conjectured to not be provable without excluded middle.  
orduniorsuc  none  Presumably not provable.  
ordunisuc  onunisuci, unisuc, unisucg  
orduniss2  onuniss2  
onsucuni2  none yet  Conjectured to be provable.  
0elsuc  none yet  Conjectured to be provable.  
onuniorsuci  none  Conjectured to not be provable without excluded middle.  
onuninsuci, ordununsuc  none  Conjectured to be provable in the forward direction but not the reverse one.  
onsucssi  none yet  Conjectured to be provable.  
nlimsucg  none yet  Conjectured to be provable.  
ordunisuc2  ordunisuc2r  The forward direction is conjectured to imply excluded middle. Here is a sketch of the proposed proof. Let om' be the set of all finite iterations of suc' A = (𝒫 A ∩ On) on ∅. (We can formalize this proof but not until we have om and at least finite induction.) Then om' = U. om' because if x e. om' then x = suc'^n (/) for some n, and then x C_ suc'^n (/) implies x e. suc'^(n+1) (/) e. om' so x e. U. om'.
Now supposing the theorem, we know that A. x e. om' suc x e. om', so in particular 2o e. om', that is, 2o = suc'^n (/) for some n. (Note that 1o = suc' (/)  see pw0.) For n = 0 and n = 1 this is clearly false, and for n = m+3 we have 1o e. suc' suc' (/) , so 2o C_ suc' suc' (/), so 2o e. suc' suc' suc' (/) C_ suc' suc' suc' suc'^m (/) = 2o, contradicting ordirr. Thus 2o = suc' suc' (/) = suc' 1o. Applying this to X = {x ∈ {∅} ∣ φ} we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ordtriexmidlem2 for 𝑋 = ∅ and rabsnt as seen in the onsucsssucexmid proof for 𝑋 = 1_{𝑜}). 

ordzsl, onzsl, dflim3, nlimon  none  
dflim4  dfilim  We conjecture that dflim4 is not equivalent to dfilim.  
limsuc  none yet  Conjectured to be provable.  
limsssuc  none yet  Conjectured to be provable.  
tfinds  tfis3  
findsg  uzind4  findsg presumably could be proved, but there hasn't been a need for it.  
xpexr2  xpexr2m  
1stval  1stvalg  
2ndval  2ndvalg  
1stnpr  none  May be intuitionizable, but very lightly used in set.mm.  
2ndnpr  none  May be intuitionizable, but very lightly used in set.mm.  
brtpos  brtposg  
ottpos  ottposg  
ovtpos  ovtposg  
pwuninel  pwuninel2  The set.mm proof of pwuninel uses case elimination.  
iunonOLD  iunon  
smofvon2  smofvon2dm  
tfr1  tfri1  
tfr2  tfri2  
tfr3  tfri3  
tfr2b , recsfnon , recsval  none  These transfinite recursion theorems are lightly used in set.mm.  
dfrdg  dfirdg  This definition combines the successor and limit cases (rather than specifying them as separate cases in a way which relies on excluded middle). In the words of [Crosilla], p. "Settheoretic principles incompatible with intuitionistic logic", "we can still define many of the familiar settheoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit."  
rdgfnon  rdgifnon  
ordge1n0  ordge1n0im, ordgt0ge1  
ondif1  dif1o  In set.mm, ondif1 is used for Cantor Normal Form  
ondif2 , dif20el  none  The set.mm proof is not intuitionistic  
brwitnlem  none  The set.mm proof is not intuitionistic  
om0r  om0, nnm0r  
om00  nnm00  
om00el  none  
suc11reg  suc11g  
frfnom  frecfnom  frecfnom adopts the frec notation and adds conditions on the characteristic function and initial value.  
fr0g  frec0g  frec0g adopts the frec notation and adds a condition on the characteristic function.  
frsuc  frecsuc  frecsuc adopts the frec notation and adds conditions on the characteristic function and initial value.  
om0x  om0  
oaord1  none yet  
oaword  oawordi  The other direction presumably could be proven but isn't yet.  
omwordi  nnmword  The set.mm proof of omwordi relies on case elimination.  
omword1  nnmword  
nnawordex  nnaordex  nnawordex is only used a few places in set.mm  
swoso  none  Unused in set.mm.  
ecdmn0  ecdmn0m  
erdisj, qsdisj, qsdisj2, uniinqs  none  These could presumably be restated to be provable, but they are lightly used in set.mm  
xpider  xpiderm  
iiner  iinerm  
riiner  riinerm  
brecop2  none  This is a form of reverse closure and uses excluded middle in its proof.  
erov , erov2  none  Unused in set.mm.  
eceqoveq  none  Unused in set.mm.  
dfsdom , relsdom , brsdom , dfdom2 , sdomdom , sdomnen , brdom2 , bren2 , domdifsn  none  Many aspects of strict dominance as developed in set.mm rely on excluded middle and a different definition would be needed if we wanted strict dominance to have the expected properties.  
en1b  en1bg  
mapsnen , map1 , pw2f1olem , pw2f1o , pw2eng , pw2en  none  We have not added set exponentiation to iset.mm yet.  
snfi  snfig  
difsnen  none  The set.mm proof uses excluded middle.  
undom  none  The set.mm proof uses undif2 and we just have undif2ss  
xpdom3  xpdom3m  
domunsncan  none  The set.mm proof relies on difsnen  
omxpenlem , omxpen , omf1o  none  The set.mm proof relies on omwordi  
enfixsn  none  The set.mm proof relies on difsnen  
sbth and its lemmas, sbthb , sbthcl  none  The SchroederBernstein Theorem implies excluded middle  
2pwuninel  2pwuninelg  
onomeneq , onfin , onfin2  none  The set.mm proofs rely on excluded middle  
nndomo  none  Should be provable but the set.mm proof wouldn't work  
nnsdomo , sucdom2 , sucdom , 0sdom1dom , 1sdom2 , sdom1  none  iset.mm doesn't yet have strict dominance  
modom , modom2  none  The set.mm proofs rely on excluded middle  
1sdom , unxpdom , unxpdom2 , sucxpdom  none  iset.mm doesn't yet have strict dominance  
pssinf  none  The set.mm proof relies on sdomnen  
fisseneq  none  The set.mm proof relies on excluded middle  
ominf  none  Although this theorem presumably could be proved, it would probably need a very different proof than the set.mm one  
isinf  none  The set.mm proof uses the converse of ssdif0im  
fineqv  none  The set.mm proof relies on theorems we don't have, and even for the theorems we do have, we'd need to carefully look at what axioms they rely on.  
pssnn  none  The set.mm proof uses excluded middle.  
ssnnfi  none  The proof in ssfiexmid would apply to this as well as to ssfi , since {∅} ∈ 𝜔  
ssfi  ssfiexmid  
domfi  none  The set.mm proof is in terms of ssfi  
xpfir  none  Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi  
infi  none  Presumably the proof of ssfiexmid could be adapted to show this implies excluded middle  
rabfi  none  Presumably the proof of ssfiexmid could be adapted to show this implies excluded middle  
finresfin  none  The set.mm proof is in terms of ssfi  
f1finf1o  none  The set.mm proof is not intuitionistic  
nfielex  none  The set.mm proof relies on neq0  
en1eqsn , en1eqsnbi  none  The set.mm proof relies on fisseneq  
diffi  none  The set.mm proof is in terms of ssfi  
dif1en  none  The set.mm proof relies on diffi  
axreg , axreg2 , zfregcl  axsetind  axreg implies excluded middle as seen at regexmid  
addcompi  addcompig  
addasspi  addasspig  
mulcompi  mulcompig  
mulasspi  mulasspig  
distrpi  distrpig  
addcanpi  addcanpig  
mulcanpi  mulcanpig  
addnidpi  addnidpig  
ltapi  ltapig  
ltmpi  ltmpig  
nlt1pi  nlt1pig  
dfnq  dfnqqs  
dfnq  dfnqqs  
dferq  none  Not needed given dfnqqs  
dfplq  dfplqqs  
dfmq  dfmqqs  
df1nq  df1nqqs  
dfltnq  dfltnqqs  
elpqn  none  Not needed given dfnqqs  
ordpipq  ordpipqqs  
addnqf  dmaddpq, addclnq  It should be possible to prove that +_{Q} is a function, but so far there hasn't been a need to do so.  
addcomnq  addcomnqg  
mulcomnq  mulcomnqg  
mulassnq  mulassnqg  
recmulnq  recmulnqg  
ltanq  ltanqg  
ltmnq  ltmnqg  
ltexnq  ltexnqq  
archnq  archnqq  
dfnp  dfinp  
df1p  dfi1p  
dfplp  dfiplp  
dfltp  dfiltp  
elnp , elnpi  elinp  
prn0  prml, prmu  
prpssnq  prssnql, prssnqu  
elprnq  elprnql, elprnqu  
prcdnq  prcdnql, prcunqu  
prub  prubl  
prnmax  prnmaxl  
npomex  none  
prnmadd  prnmaddl  
genpv  genipv  
genpcd  genpcdl  
genpnmax  genprndl  
ltrnq  ltrnqg, ltrnqi  
genpcl  addclpr, mulclpr  
genpass  genpassg  
addclprlem1  addnqprllem, addnqprulem  
addclprlem2  addnqprl, addnqpru  
plpv  plpvlu  
mpv  mpvlu  
mulclprlem  mulnqprl, mulnqpru  
addcompr  addcomprg  
addasspr  addassprg  
mulcompr  mulcomprg  
mulasspr  mulassprg  
distrlem1pr  distrlem1prl, distrlem1pru  
distrlem4pr  distrlem4prl, distrlem4pru  
distrlem5pr  distrlem5prl, distrlem5pru  
distrpr  distrprg  
ltprord  ltprordil  There hasn't yet been a need to investigate versions which are biconditional or which involve proper subsets.  
psslinpr  ltsopr  
prlem934  prarloc2  
ltaddpr2  ltaddpr  
ltexprlem1 , ltexprlem2 , ltexprlem3 , ltexprlem4  none  See the lemmas for ltexpri generally.  
ltexprlem5  ltexprlempr  
ltexprlem6  ltexprlemfl, ltexprlemfu  
ltexprlem7  ltexprlemrl, ltexprlemru  
ltapr  ltaprg  
addcanpr  addcanprg  
prlem936  prmuloc2  
reclem2pr  recexprlempr  
reclem3pr  recexprlem1ssl, recexprlem1ssu  
reclem4pr  recexprlemss1l, recexprlemss1u, recexprlemex  
supexpr , suplem1pr , suplem2pr  none  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.  
mulcmpblnrlem  mulcmpblnrlemg  
ltsrpr  ltsrprg  
dmaddsr , dmmulsr  none  Although these presumably could be proved in a way similar to dmaddpq and dmmulpq (in fact dmaddpqlem would seem to be easily generalizable to anything of the form ((𝑆 × 𝑇) / 𝑅)), we haven't yet had a need to do so.  
addcomsr  addcomsrg  
addasssr  addasssrg  
mulcomsr  mulcomsrg  
mulasssr  mulasssrg  
distrsr  distrsrg  
ltasr  ltasrg  
sqgt0sr  mulgt0sr, apsqgt0  
recexsr  recexsrlem  This would follow from sqgt0sr (as in the set.mm proof of recexsr), but "not equal to zero" would need to be changed to "apart from zero".  
mappsrpr , ltpsrpr , map2psrpr  none  Although variants of these theorems could be intuitionized, in set.mm they are only used for supremum theorems, so we can consider this in more detail when we tackle what kind of supremum theorems to prove.  
supsrlem , supsr  none  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.  
axaddf , axaddf , axmulf , axmulf  none  Because these are described as deprecated in set.mm, we haven't figured out what would be involved in proving them for iset.mm.  
ax1ne0 , ax1ne0  ax0lt1, ax0lt1, 1ap0, 1ne0  
axrrecex , axrrecex  axprecex, axprecex  
axprelttri , axprelttri  axpreltirr, axpreltwlin, axpreltirr, axpreltwlin  
axpresup , axpresup , axsup  none yet  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. If we want a set of axioms for real numbers which allows us to avoid constructiondependent theorems beyond this point, we'll need a modified Least Upper Bound property, a statement concerning Dedekind cuts or something similar, or some other axiom(s).  
elimne0  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
xrltnle  xrlenlt  
ssxr  dfxr  Lightly used in set.mm  
ltnle , ltnlei , ltnled  lenlt, zltnle  
lttri2 , lttri4  ztri3or  Real number trichotomy is not provable.  
leloe , eqlelt , leloei , leloed , eqleltd  none  
leltne , leltned  none  
ltneOLD  ltne  
letric , letrii , letrid  zletric  
ltlen , ltleni , ltlend  ltleap, zltlen  
ne0gt0  none  We presumably could prove this if we changed "not equal to zero" to "apart from zero".  
lecasei , ltlecasei  none  These are real number trichotomy  
lelttric  zlelttric  
lttri2i  none  This can be read as "two real numbers are nonequal if and only if they are apart" which relies on excluded middle  
ne0gt0d , lttrid , lttri2d , lttri4d  none  These are real number trichotomy  
dedekind , dedekindle  none  
mul02lem1  none  The one use in set.mm is not needed in iset.mm.  
negex  negcl  
msqgt0 , msqgt0i , msqgt0d  apsqgt0  "Not equal to zero" is changed to "apart from zero"  
relin01  none  Relies on real number trichotomy.  
ltordlem , ltord1 , leord1 , eqord1 , ltord2 , leord2 , eqord2  none  These depend on real number trichotomy and are not used until later in set.mm.  
wloglei , wlogle  none  These depend on real number trichotomy and are not used until later in set.mm.  
recex  recexap  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
mulcand, mulcan2d  mulcanapd, mulcanap2d  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
mulcanad , mulcan2ad  mulcanapad, mulcanap2ad  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
mulcan , mulcan2 , mulcani  mulcanap, mulcanap2, mulcanapi  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
mul0or , mul0ori , mul0ord  none  Remark 2.19 of [Geuvers] says that this does not hold in general and has a counterexample.  
mulne0b , mulne0bd , mulne0bad , mulne0bbd  mulap0b, mulap0bd, mulap0bad, mulap0bbd  
mulne0 , mulne0i , mulne0d  mulap0, mulap0i, mulap0d  
receu  receuap  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
mulnzcnopr  none  
msq0i , msq0d  none  This probably could be proved in terms of tightness of apartness and A # 0 ∧ B # 0 → (A · B) # 0, but is unused in set.mm.  
mulcan1g , mulcan2g  various cancellation theorems  Presumably this is unavailable for the same reason that mul0or is unavailable.  
1div0  none  This could be proved, but the set.mm proof does not work asis.  
divval  divvalap  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
divmul , divmul2 , divmul3  divmulap, divmulap2, divmulap3  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
divcl , reccl  divclap, recclap  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
divcan1 , divcan2  divcanap1, divcanap2  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
diveq0  diveqap0  In theorems involving reciprocals or division, not equal to zero changes to apart from zero.  
divne0b , divne0  divap0b, divap0  
recne0  recap0  
recid , recid2  recidap, recidap2  
divrec  divrecap  
divrec2  divrecap2  
divass  divassap  
div23 , div32 , div13 , div12  div23ap, div32ap, div13ap, div12ap  
divdir , divcan3 , divcan4  divdirap, divcanap3, divcanap4  
div11 , divid , div0  div11ap, dividap, div0ap  
diveq1 , divneg , divsubdir  diveqap1, divnegap, divsubdirap  
recrec , rec11 , rec11r  recrecap, rec11ap, rec11rap  
divmuldiv , divdivdiv , divcan5  divmuldivap, divdivdivap, divcanap5  
divmul13 , divmul24 , divmuleq  divmul13ap, divmul24ap, divmuleqap  
recdiv , divcan6 , divdiv32 , divcan7  recdivap, divcanap6, divdiv32ap, divcanap7  
dmdcan , divdiv1 , divdiv2 , recdiv2  dmdcanap, divdivap1, divdivap2, recdivap2  
ddcan , divadddiv , divsubdiv  ddcanap, divadddivap, divsubdivap  
ddcan , divadddiv , divsubdiv  ddcanap, divadddivap, divsubdivap  
conjmul , rereccl, redivcl  conjmulap, rerecclap, redivclap  
div2neg , divneg2  div2negap, divneg2ap  
recclzi , recne0zi , recidzi  recclapzi, recap0apzi, recidapzi  
reccli , recidi , recreci  recclapi, recidapi, recrecapi  
dividi , div0i  dividapi, div0api  
divclzi , divcan1zi , divcan2zi  divclapzi, divcanap1zi, divcanap2zi  
divreczi , divcan3zi , divcan4zi  divrecapzi, divcanap3zi, divcanap4zi  
rec11i , rec11ii  rec11api, rec11apii  
divcli , divcan2i , divcan1i , divreci , divcan3i , divcan4i  divclapi, divcanap2i, divcanap1i, divrecapi, divcanap3i, divcanap4i  
div0i  divap0i  
divasszi , divmulzi , divdirzi , divdiv23zi  divassapzi, divmulapzi, divdirapzi, divdiv23apzi  
divmuli , divdiv32i  divmulapi, divdiv32api  
divassi , divdiri , div23i , div11i  divassapi, divdirapi, div23api, div11api  
divmuldivi, divmul13i, divadddivi, divdivdivi  divmuldivapi, divmul13api, divadddivapi, divdivdivapi  
rerecclzi , rereccli , redivclzi , redivcli  rerecclapzi, rerecclapi, redivclapzi, redivclapi  
reccld , rec0d , recidd , recid2d , recrecd , dividd , div0d  recclapd, recap0d, recidapd, recidap2d, recrecapd, dividapd, div0apd  
divcld , divcan1d , divcan2d , divrecd , divrec2d , divcan3d , divcan4d  divclapd, divcanap1d, divcanap2d, divrecapd, divrecap2d, divcanap3d, divcanap4d  
diveq0d , diveq1d , diveq1ad , diveq0ad , divne1d , div0bd , divnegd , divneg2d , div2negd  diveqap0d, diveqap1d, diveqap1ad, diveqap0ad, divap1d, divap0bd, divnegapd, divneg2apd, div2negapd  
divne0d , recdivd , recdiv2d , divcan6d , ddcand , rec11d  divap0d, recdivapd, recdivap2d, divcanap6d, ddcanapd, rec11apd  
divmuld , div32d , div13d , divdiv32d , divcan5d , divcan5rd , divcan7d , dmdcand , dmdcan2d , divdiv1d , divdiv2d  divmulapd, div32apd, div13apd, divdiv32apd, divcanap5d, divcanap5rd, divcanap7d, dmdcanapd, dmdcanap2d, divdivap1d, divdivap2d  
divmul2d, divmul3d, divassd, div12d, div23d, divdird, divsubdird, div11d  divmulap2d, divmulap3d, divassapd, div12apd, div23apd, divdirapd, divsubdirapd, div11apd  
rereccld , redivcld  rerecclapd, redivclapd  
mvllmuld  mvllmulapd  
elimgt0 , elimge0  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
mulge0b , mulle0b , mulsuble0b  none  Presumably unprovable for reasons analogous to mul0or.  
ledivp1i , ltdivp1i  none  Presumably could be proved, but unused in set.mm.  
crne0  crap0  
ofsubeq0 , ofnegsub , ofsubge0  none  Depend on ofval and/or offn .  
dfnn  dfnn2  
dfnn3  dfnn2  Presumably could be proved, as it is a slight variation of dfnn2  
avgle  none  
nnunb  none  Presumably provable from arch but unused in set.mm.  
frnnn0supp , frnnn0fsupp  nn0supp  iset.mm does not yet have either the notation, or in some cases the theorems, related to the support of a function or a fintely supported function.  
suprzcl  none  
zriotaneg  none  Lightly used in set.mm  
suprfinzcl  none  
decex  deccl  
uzwo , uzwo2 , nnwo , nnwof , nnwos  none  Presumably would imply excluded middle, unless there is something which makes this different from nnregexmid.  
uzinfmi , nninfm , nn0infm , infmssuzle , infmssuzcl  none  We do not yet have a supremum notation, or most supremum theorems, in iset.mm  
negn0  negm  
supminf  none  We do not yet have a supremum notation, or most supremum theorems, in iset.mm  
zsupss , suprzcl2 , suprzub , uzsupss  none  We do not yet have a supremum notation, or most supremum theorems, in iset.mm  
rpneg  rpnegap  
xrlttri , xrlttri2  none  A generalization of real trichotomy.  
xrleloe , xrleltne , dfle2  none  Consequences of real trichotomy.  
xrltlen  none  We presumably could prove an analogue to ltleap but we have not yet defined apartness for extended reals (# is for complex numbers).  
dflt2  none  
xrletri  none  
xrmax1 , xrmax2 , xrmin1 , xrmin2 , xrmaxeq , xrmineq , xrmaxlt , xrltmin , xrmaxle , xrlemin , max1 , max2 , min1 , min2 , maxle , lemin , maxlt , ltmin , max0sub , ifle  none  
qbtwnre , qbtwnxr  none yet  These should be provable, but the set.mm proof relies on zbtwnre (which in turn is proved using the least upper bound property). The most straightforward solution is to use a constructiondependent proof in terms of dfiltp (the only complicated part of which is connecting Q and ℚ). This is the solution adopted by Theorem 11.2.6 of [HoTT].  
qsqueeze  none yet  Once we have qbtwnre , we should be able to prove this as a consequence of squeeze0.  
qextltlem , qextlt , qextle  none  The set.mm proof is not intuitionistic.  
xralrple , alrple  none yet  If we had qbtwnxr , it looks like the set.mm proof would work with minor changes.  
xnegex  xnegcl  
xaddval , xaddf , xmulval , xaddpnf1 , xaddpnf2 , xaddmnf1 , xaddmnf2 , pnfaddmnf , mnfaddpnf , rexadd , rexsub , xaddnemnf , xaddnepnf , xnegid , xaddcl , xaddcom , xaddid1 , xaddid2 , xnegdi , xaddass , xaddass2 , xpncan , xnpcan , xleadd1a , xleadd2a , xleadd1 , xltadd1 , xltadd2 , xaddge0 , xle2add , xlt2add , xsubge0 , xposdif , xlesubadd , xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xaddcld , xmulcld , xadd4d  none  There appears to be no fundamental obstacle to proving these, because disjunctions can arise from elxr rather than excluded middle. However, _{𝑒}, +_{𝑒}, and ·_{e} are lightly used in set.mm, and the set.mm proofs would require significant changes.  
ixxub , ixxlb  none  
iccen  none  
supicc , supiccub , supicclub , supicclub2  none  
ixxun , ixxin  none  
ioo0  none  Once we have qbtwnxr , it may be possible to rearrange the logic from set.mm so that this proof works (via rabeq0, ralnex, and xrlenlt perhaps).  
ioon0  none  Presumably nonempty would need to be changed to inhabited, see also discussion at ioo0  
iooid  iooidg  
ndmioo  none  See discussion at ndmov but set.mm uses excluded middle, both in proving this and in using it.  
lbioo , ubioo  lbioog, ubioog  
iooin  none  
ico0 , ioc0  none  Possibly similar to ioo0 ; see discussion there.  
icc0  icc0r  
ioorebas  ioorebasg  
ge0xaddcl , ge0xmulcl  none  Rely on xaddcl and xmulcl ; see discussion in this list for those theorems.  
icoun , snunioo , snunico , snunioc , prunioo  none  
ioojoin  none  
difreicc  none  
iccsplit  none  This depends, apparently in an essential way, on real number trichotomy.  
xov1plusxeqvd  none  This presumably could be proved if not equal is changed to apart, but is lightly used in set.mm.  
fzn0  fzm  
fz0  none  Although it would be possible to prove a version of this with the additional conditions that 𝑀 ∈ V and 𝑁 ∈ V, the theorem is lightly used in set.mm.  
fzon0  fzom  
fzo0n0  fzo0m  
ssfzoulel  none  Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.  
fzonfzoufzol  none  Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.  
elfznelfzo , elfznelfzob , injresinjlem , injresinj  none  Some or all of this presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.  
dffl , dfceil , and other floor and ceiling theoerms.  none  Most of the theorems in this section are conjectured to imply excluded middle. Imagine a real number which is around 2.99995 or 3.00001 . In order to determine whether its floor is 2 or 3, it would be necessary to compute the number to arbitrary precision. For similarity to the Metamath Proof Explorer, it may be desirable to define floor and ceiling, but only provide most of the theorems where the argument is a rational number.  
dfmod and other modulus theoerms.  none  As with dffl it may be feasible to define this for rational numbers rather than reals.  
om2uz0i  frec2uz0d  
om2uzsuci  frec2uzsucd  
om2uzuzi  frec2uzuzd  
om2uzlti  frec2uzltd  
om2uzlt2i  frec2uzlt2d  
om2uzrani  frec2uzrand  
om2uzf1oi  frec2uzf1od  
om2uzisoi  frec2uzisod  
om2uzoi , ltweuz , ltwenn , ltwefz  none  We do not have a syntax for well ordering and based on theorems like nnregexmid, there is probably little room for this concept.  
om2uzrdg  frec2uzrdg  
uzrdglem  frecuzrdglem  
uzrdgfni  frecuzrdgfn  
uzrdg0i  frecuzrdg0  
uzrdgsuci  frecuzrdgsuc  
uzinf  none  See ominf  
uzrdgxfr  none  Presumably could be proved if restated in terms of frec (a la frec2uz0d). However, it is lightly used in set.mm.  
fzennn  frecfzennn  
fzen2  frecfzen2  
cardfz  none  Cardinality does not work the same way without excluded middle and iset.mm has few cardinality related theorems.  
hashgf1o  frechashgf1o  
fzfi  fzfig  
fzfid  fzfigd  
fzofi  fzofig  
fsequb  none  Seems like it might be provable, but unused in set.mm  
fsequb2  none  The set.mm proof does not work asis  
fseqsupcl , fseqsupubi  none  iset.mm does not have the "sup" syntax and lacks most supremum theorems from set.mm.  
uzindi  none  This could presumably be proved, perhaps from uzind4, but is lightly used in set.mm  
axdc4uz  none  Although some versions of constructive mathematics accept dependent choice, we have not yet developed it in iset.mm  
ssnn0fi , rabssnn0fi  none  Conjectured to imply excluded middle along the lines of nnregexmid or ssfiexmid  
dfseq  dfiseq  
seqex  iseqcl  
seqeq1 , seqeq2 , seqeq3 , seqeq1d , seqeq2d , seqeq3d , seqeq123d  iseqeq1, iseqeq2, iseqeq3  
nfseq  nfiseq  
seqval  iseqval  
seqfn  iseqfn  
seq1 , seq1i  iseq1  
seqp1 , seqp1i  iseqp1  
seqcl  iseqcl  
seqfveq2  iseqfveq2  
seqfeq2  iseqfeq2  
seqfveq  iseqfveq  
dfexp  dfiexp  The difference is that seq in iset.mm takes three arguments compared with two in set.mm.  
expval  expival  
expnnval  expinnval  
expneg  expnegap0  The set.mm theorem does not exclude the case of dividing by zero.  
expneg2  expineg2  
expn1  expn1ap0  
expcl2lem  expcl2lemap  
reexpclz  reexpclzap  
expclzlem  expclzaplem  
expclz  expclzap  
expne0  expap0  
expne0i  expap0i  
expnegz  expnegzap  
mulexpz  mulexpzap  
exprec  exprecap  
expaddzlem , expaddz  expaddzaplem, expaddzap  
expmulz  expmulzap  
expsub  expsubap  
expp1z  expp1zap  
expm1  expm1ap  
expdiv  expdivap  
expcan , expcand  none  Presumably provable, but the set.mm proof uses eqord1 and the theorem is lightly used in set.mm  
ltexp2 , leexp2 , leexp2 , ltexp2d , leexp2d  none  Presumably provable, but the set.mm proof uses ltord1  
ltexp2r , ltexp2rd  none  Presumably provable, but the set.mm proof uses ltexp2  
sqdiv  sqdivap  
sqgt0  sqgt0ap  
iexpcyc  none yet  See discussion under dfmod ; modulus for integers would suffice so issues with modulus for reals would not be an impediment.  
sqrecii , sqrecd  exprecap  
sqdivi  sqdivapi  
sqgt0i  sqgt0api  
sqlecan  lemul1  Unused in set.mm  
sqeqori  none  The reverse direction is oveq1 together with sqneg. The forward direction is presumably not provable, see mul0or for more discussion.  
subsq0i , sqeqor  none  Variations of sqeqori .  
sq01  none  Lightly used in set.mm. Presumably not provable as stated, for reasons analogous to mul0or .  
crreczi  none  Presumably could be proved if notequal is changed to apart, but unused in set.mm.  
expmulnbnd  none  Should be possible to prove this or something similar, but the set.mm proof relies on case elimination based on whether 0 ≤ A or not.  
digit2 , digit1  none  Depends on modulus and floor, and unused in set.mm.  
modexp  none  Depends on modulus. Presumably it, or something similar, can be made to work as it is mostly about integers rather than reals.  
discr1 , discr  none  The set.mm proof uses real number trichotomy.  
sqrecd  sqrecapd  
expclzd  expclzapd  
exp0d  expap0d  
expnegd  expnegapd  
exprecd  exprecapd  
expp1zd  expp1zapd  
expm1d  expm1apd  
expsubd  expsubapd  
sqdivd  sqdivapd  
expdivd  expdivapd  
reexpclzd  reexpclzapd  
sqgt0d  sqgt0apd  
mulre  mulreap  
rediv  redivap  
imdiv  imdivap  
cjdiv  cjdivap  
sqeqd  none  The set.mm proof is not intuitionistic, and this theorem is unused in set.mm.  
cjdivi  cjdivapi  
cjdivd  cjdivapd  
redivd  redivapd  
imdivd  imdivapd  
dfsqrt  dfrsqrt  See discussion of complex square roots in the comment of dfrsqrt  
sqrtval  sqrtrval  See discussion of complex square roots in the comment of dfrsqrt  
01sqrex and its lemmas  none  We have not yet defined real number completeness enough to prove the existence of these square roots, but we expect we'll eventually be able to prove this theorem from cauappcvgpr or similar theorems.  
cnpart  none  See discussion of complex square roots in the comment of dfrsqrt  
resqrex  none yet  This will be provable once completeness is better developed  
sqrmo  none  See discussion of complex square roots in the comment of dfrsqrt  
resqreu  none yet  Once completeness is better developed, it should be possible to adjust this to reflect sqrtrval  
resqrtcl  none yet  Once completeness is better developed, this will be provable via resqrex  
resqrtth , remsqsqrt  none yet  These will be provable once completeness is better developed  
sqrtge0 , sqrtgt0  none yet  These will be provable once completeness is better developed  
sqrtmul , sqrtle , sqrtlt , sqrt11 , sqrt00  none yet  These should be provable once completeness is better developed  
rpsqrtcl  none yet  This is a variation of sqrtgt0  
sqrtdiv  none yet  Should be provable once completeness is better developed  
sqrtneg  none  Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of dfrsqrt  
sqrtsq2  none yet  Should be provable once completeness is better developed  
sqrt2gt1lt2  none yet  Should be provable once completeness is better developed  
sqrtm1  none  Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of dfrsqrt  
abscl  none yet  Should be easy once we get resqrtcl  
absvalsq , absvalsq2 , sqabsadd , sqabssub  none yet  Should be easy once we prove resqrtth  
absge0  none yet  Should be easy once we prove sqrtge0  
absrpcl  none yet  Should be provable once we have proved completeness and more of the square root theorems. Not equal presumably will need to be changed to apart.  
abs00 , abs00ad  none yet  Should be provable once we have proved completeness and more of the square root theorems. We will presumably also be able to prove ((abs‘A) # 0 ↔ A # 0 which is stronger and is something we'd likely want.  
absreimsq , absreim  none yet  Should be provable once we have proved absvalsq2  
absmul  none yet  Should be provable once we have proved sqrtmul  
absdiv  none yet  Should be provable once we have proved completeness and more of the square root theorems. Not equal will need to be changed to apart.  
leabs  none  The set.mm proof relies on real number trichotomy. Here is a sketch of a proof which might work once absge0 is proved. Suppose (abs‘A) < A. By sowlin, (abs‘A) < 0 ∨ 0 < A. But absge0 tells us that (abs‘A) < 0 is not possible, and 0 < A implies (abs‘A) = A via absid. This is a contradiction so ¬ (abs‘A) < A, which by lenlt implies A ≤ (abs‘A).  
absor  none  We could prove this for rationals if we wanted  
absresq  none yet  This will follow once we have proved absvalsq  
absmod0  none  See dfmod ; we may want to supply this for rationals or integers  
absexp  none yet  Should be provable once we have proved absmul  
absexpz  none yet  Should be provable, with not equal changed to apart, once we have proved absexp  
abssq , sqabs  none yet  Should be provable once we have absexp or other completeness related results  
absrele , absimle  none yet  Should be provable once we have proved sqrtle  
max0add  none  Relies on real number trichotomy  
absz  none  Although this is presumably provable, the set.mm proof is not intuitionistic and it is lightly used in set.mm 
This
page was last updated on 15Aug2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 