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.18i  pm2.01d  See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.  
notnotrd , notnotri , notnotr , notnotb  notnot  Double negation introduction holds but not double negation elimination.  
mt3d  mtod  
nsyl2  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  
dfbi1 , dfbi3  dfbi, dfbi2  
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  
imor , imori  imorr, imorri, imordc  
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  
pm4.42  pm4.42r  
3ianor  3ianorr  
dfnan and other theorems using NAND (Sheffer stroke) notation  none  A quick glance at the internet shows this mostly being used in the presence of excluded middle; in any case it is not currently present in iset.mm  
dfxor  dfxor  Although the definition of exclusive or is called dfxor in both set.mm and iset.mm (at least currently), the definitions are not equivalent (in the absence of excluded middle).  
xnor  none  The set.mm proof uses theorems not in iset.mm.  
xorass  none  The set.mm proof uses theorems not in iset.mm.  
xor2  xoranor, xor2dc  
xornan  xor2dc  
xornan2  none  See discussion under dfnan  
xorneg2 , xorneg1 , xorneg  none  The set.mm proofs use theorems not in iset.mm.  
xorexmid  none  A form of excluded middle  
dfex  exalim  
alex  alexim  
exnal  exnalim  
alexn  alexnim  
exanali  exanaliim  
19.35 , 19.35ri  19.351  
19.30  none  
19.39  i19.39  
19.24  i19.24  
19.36 , 19.36v  19.361  
19.37 , 19.37v  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  
nss  nssr  
sspss  sspssr  
n0f  n0rf  
n0  n0r, fin0  
neq0  neq0r  
reximdva0  reximdva0m  
rabn0  rabn0m, rabn0r  
ssdif0  ssdif0im  
inssdif0  inssdif0im  
undif1  undif1ss  
undif2  undif2ss  
inundif  inundifss  
undif  undifss  
ssundif  ssundifim  
uneqdifeq  uneqdifeqim  
r19.2z  r19.2m  
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 , ifid , eqif , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD  none  
ifboth  ifbothdc  
ifcl , ifcld  ifcldcd  
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.  
difsnid  difsnss  One direction, for any set  
nndifsnid  for a natural number  
fidifsnid  for a finite set  
iundif2  iundif2ss  
iindif2  iindif2m  
iinin2  iinin2m  
iinin1  iinin1m  
iinvdif  iindif2m  Unused in set.mm  
riinn0  riinm  
riinrab  iinrabm  
iinuni  iinuniss  
iununi  iununir  
rintn0  rintm  
trintss  trintssm  
trint0  trint0m  
csbexg , csbex  csbexga, csbexa  set.mm uses case elimination to remove the 𝐴 ∈ V condition.  
intex  inteximm, intexr  inteximm is the forward direction (but for inhabited rather than nonempty classes) and intexr is the reverse direction.  
intexab  intexabim  
intexrab  intexrabim  
iinexg  iinexgm  Changes not empty to inhabited  
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  
nssss  nssssr  
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: ∀𝑥(∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝑆 = 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 ↔ ∀𝑠(∀𝑥(∀𝑦(𝑦𝑅𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠) → 𝐴 ⊆ 𝑠) R Fr2 A ↔ ∀𝑠(𝑠 ⊆ 𝐴 → (∀𝑥 ∈ 𝑠∃𝑦 ∈ 𝑠𝑦𝑅𝑥 → 𝑠 = ∅)) R Fr3 A ↔ ∀𝑠(𝑠 ⊆ 𝐴 → (∃𝑥𝑥 ∈ 𝑠 → ∃𝑥 ∈ 𝑠∀𝑦 ∈ 𝑠¬ 𝑦𝑅𝑥)) 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 𝐴 and V throughout the elirr proof would be replaced by 𝐴. Likewise for en2lp. These theorems (for ordinals) would then not rely on axsetind. For more on axioms which might be adopted which are incompatible with axsetind (that is, Nonwellfounded Set Theory but in the absence of excluded middle), see Chapter 20 of [AczelRathjen], p. 183. 

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 , onsseleq  onelss, eqimss, nnsseleq  Taken together, onelss and eqimss represent the reverse direction of the biconditional from ordsseleq . For natural numbers the biconditional is provable.  
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 , 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.  
ordtri2or2  nntri2or2  ordtri2or2 implies excluded middle as shown at ordtri2or2exmid.  
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  Implies excluded middle as shown at ontr2exmid  
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  
dffv3  dffv3g  
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 ¬ 𝐴 ∈ V case is fvprc.  
elfvdm  relelfvdm  
elfvex  relelfvdm  
f0cli  ffvelrn  
dff3  dff3im  
dff4  dff4im  
fvunsn  fvunsng  
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.  
ovexg  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. ∪ 𝐴 = On → 𝐴 ∉ 𝑉 is provable, and (𝐵 ∈ On ∧ ∪ 𝐴 ⊆ 𝐵) → 𝐴 ∈ 𝑉 is provable. (Why isn't dfpss stated so that the set difference is inhabited? If so, you could prove ∪ 𝐴 ⊊ On → 𝐴 ∈ 𝑉.)  
onint  onintss  onint implies excluded middle as shown in onintexmid.  
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  onintonm  
onintrab  none  The set.mm proof relies on the converse of inteximm.  
onintrab2  onintrab2im  The converse would appear to need the converse of inteximm.  
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  
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 (𝒫 𝐴 ∩ 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  
0elsuc  none  This theorem may appear to be innocuous but it implies excluded middle as shown at 0elsucexmid.  
onuniorsuci  none  Conjectured to not be provable without excluded middle.  
onuninsuci, orduninsuc  none  Conjectured to be provable in the forward direction but not the reverse one.  
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 = (𝒫 𝐴 ∩ 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 = {𝑥 ∈ {∅} ∣ 𝜑} 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  fidifsnen  
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  fisbth  The SchroederBernstein Theorem implies excluded middle  
2pwuninel  2pwuninelg  
php  phpm  
snnen2o  snnen2og, snnen2oprc  
onomeneq , onfin , onfin2  none  The set.mm proofs rely on excluded middle  
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  none  Implies excluded middle as shown at 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  diffisn, diffifi  diffi is not provable, as shown at diffitest  
enp1ilem , enp1i , en2 , en3 , en4  none  The set.mm proof relies on excluded middle and undif1  
findcard3  none  The set.mm proof is in terms of strict dominance.  
unfi  none  Not provable according to Remark 8.1.17 of [AczelRathjen].  
axreg , axreg2 , zfregcl  axsetind  axreg implies excluded middle as seen at regexmid  
dfrank and all theorems realted to the rank function  none  One possible definition is Definition 9.3.4 of [AczelRathjen], p. 91  
dfaleph and all theorems involving aleph  none  
dfcf and all theorems involving cofinality  none  
dfacn and all theorems using this definition  none  
cardf2 , cardon , isnum2  cardcl, isnumi  It would also be easy to prove Fun card if there is a need.  
ennum  none  The set.mm proof relies on isnum2  
tskwe  none  Relies on dfsdom  
xpnum  none  The set.mm proof relies on isnum2  
cardval3  cardval3ex  
cardid2  none  The set.mm proof relies on onint  
isnum3  none  
oncardid  none  The set.mm proof relies on cardid2  
cardidm  none  Presumably this would need a condition on 𝐴 but even with that, the set.mm proof relies on cardid2  
oncard  none  The set.mm proof relies on theorems we don't have, and this theorem is unused in set.mm.  
ficardom  none  Both the set.mm proof, and perhaps some possible alternative proofs, rely on onomeneq and perhaps other theorems we don't have currently.  
ficardid  none  The set.mm proof relies on cardid2  
cardnn  none  The set.mm proof relies on a variety of theorems we don't have currently.  
cardnueq0  none  The set.mm proof relies on cardid2  
cardne  none  The set.mm proof relies on ordinal trichotomy (and if that can be solved there might be some more minor problems which require revisions to the theorem)  
carden2a  none  The set.mm proof relies on excluded middle.  
carden2b  carden2bex  
card1 , cardsn  none  Rely on a variety of theorems we don't currently have. Lightly used in set.mm.  
carddomi2  none  The set.mm proof relies on excluded middle.  
sdomsdomcardi  none  Relies on a variety of theorems we don't currently have.  
entri3  fientri3  Because full entri3 is equivalent to the axiom of choice, it implies excluded middle.  
dfwina , dfina , dftsk , dfgru , axgroth and all theorems related to inaccessibles and large cardinals  none  For an introduction to inaccessibles and large set properties see Chapter 18 of [AczelRathjen], p. 165 (including why "large set properties" is more apt terminology than "large cardinal properties" in the absence of excluded middle).  
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  
nqpr  nqprlu  
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  caucvgprpr  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences.  
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  prsrpos, prsrlt, srpospr  
supsrlem , supsr  caucvgsr  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences.  
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  axcaucvg, axcaucvg, caucvgre  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences.  
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  leltap, leltapd  
ltneOLD  ltne, ltap  
letric , letrii , letrid  zletric  
ltlen , ltleni , ltlend  ltleap, zltlen  
ne0gt0 , ne0gt0d  ap0gt0, ap0gt0d  
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  
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  sqeq0, sqeq0i  These slight restatements of sqeq0 are 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  
divmuldivd  divmuldivapd  
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  iseqex  The only difference is the differing syntax of seq.  
seqeq1 , seqeq2 , seqeq3 , seqeq1d , seqeq2d , seqeq3d , seqeq123d  iseqeq1, iseqeq2, iseqeq3  
nfseq  nfiseq  
seqval  iseqval  
seqfn  iseqfn  
seq1 , seq1i  iseq1  
seqp1 , seqp1i  iseqp1  
seqm1  iseqm1  
seqcl2  none yet  Presumably could prove this (with adjustments analogous to iseqp1). The third argument to seq in iset.mm would correspond to 𝐶 rather than 𝐷 (some of the other seq related theorems do not allow 𝐶 and 𝐷 to be different, but seqcl2 does).  
seqf2  none yet  Presumably could prove this, analogously to seqcl2.  
seqcl  iseqcl  iseqcl requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seqcl . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqf  iseqf  
seqfveq2  iseqfveq2  
seqfeq2  iseqfeq2  
seqfveq  iseqfveq  
seqfeq  iseqfeq  
seqshft2  iseqshft2  
seqres  none  Should be intuitionizable as with the other seq theorems, but unused in set.mm  
serf  iserf  
serfre  iserfre  
sermono  isermono  isermono requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in sermono . Given that the intention is to use this for infinite series, there may be no need to look into whether this requirement can be relaxed.  
seqsplit  iseqsplit  iseqsplit requires that 𝐹 be defined on (ℤ_{≥}‘𝐾) not merely (𝐾...𝑁) as in seqsplit . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seq1p  iseq1p  iseq1p requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seq1p . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqcaopr3  iseqcaopr3  iseqcaopr3 requires that 𝐹, 𝐺, and 𝐻 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seqcaopr3 . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqcaopr2  iseqcaopr2  iseqcaopr2 requires that 𝐹, 𝐺, and 𝐻 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seqcaopr2 . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqcaopr  iseqcaopr  iseqcaopr requires that 𝐹, 𝐺, and 𝐻 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seqcaopr . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqf1o  none  May be adaptable with sufficient attention to issues such as whether the operation + is closed with respect to 𝐶 as well as 𝑆, and perhaps other issues.  
seradd  iseradd  iseradd requires that 𝐹, 𝐺, and 𝐻 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in seradd . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
sersub  isersub  isersub requires that 𝐹, 𝐺, and 𝐻 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in sersub . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqid3  iseqid3, iseqid3s  iseqid3 and iseqid3s differ with respect to which entries in 𝐹 need to be zero. Further refinements to the hypotheses including where 𝐹 needs to be defined and the like might be possible (with a greater amount of work), but perhaps these are sufficient.  
seqid  iseqid  
seqid2  none yet  It should be possible to come up with a (presumably modified) versiona of this, but we have not done so yet.  
seqhomo  iseqhomo  
seqz , seqfeq4 , seqfeq3  none yet  It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet.  
seqdistr  iseqdistr  
ser0  iser0  The only difference is the syntax of seq.  
ser0f  iser0f  The only difference is the syntax of seq.  
serge0  serige0  This theorem uses ℂ as the final argument to seq which probably will be more convenient even if all the values are elements of a subset of ℂ.  
serle  serile  This theorem uses ℂ as the final argument to seq which probably will be more convenient even if all the values are elements of a subset of ℂ.  
ser1const , seqof , seqof2  none yet  It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet.  
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 ≤ 𝐴 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  
seqshft  none currently  need to figure out how to adjust this for the differences between set.mm and iset.mm concerning seq.  
dfsgn and theorems related to the sgn function  none  To choose a value near zero requires knowing the argument with unlimited precision. It would be possible to define for rational numbers, or real numbers apart from zero.  
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. Here's one possibility if we do want to define square roots on (some) complex numbers: It should be possible to define the complex square root function on all complex numbers satisfying (ℑ‘𝑥) # 0 ∨ 0 ≤ (ℜ‘𝑥), using a similar construction to the one used in set.mm. You need the real square root as a basis for the construction, but then there is a trick using the complex number x + x (see sqreu) that yields the complex square root whenever it is apart from zero (you need to divide by it at one point IIRC), which is exactly on the negative real line. You can either live with this constraint, which gives you the complex square root except on the negative real line (which puts a hole at zero), or you can extend it by continuity to zero as well by joining it with the real square root. The disjunctive domain of the resulting function might not be so useful though.  
sqrtval  sqrtrval  See discussion of complex square roots in the comment of dfrsqrt  
01sqrex and its lemmas  resqrex  Both set.mm and iset.mm prove resqrex although via different mechanisms so there is no need for 01sqrex.  
cnpart  none  See discussion of complex square roots in the comment of dfrsqrt  
sqrmo  rsqrmo  See discussion of complex square roots in the comment of dfrsqrt  
resqreu  rersqreu  Although the set.mm theorem is primarily about real square roots, the iset.mm equivalent removes some complex number related parts.  
sqrtneg , sqrtnegd  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  
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  
absrpcl , absrpcld  absrpclap, absrpclapd  
absdiv , absdivzi , absdivd  absdivap, absdivapzi, absdivapd  
absor , absori , absord  none  We could prove this for rationals, or real numbers apart from zero, if we wanted  
absmod0  none  See dfmod ; we may want to supply this for rationals or integers  
absexpz  absexpzap  
max0add  none  This would hold if we defined the maximum of two real numbers and recast this theoerem in terms of that (rather than using if in a way which 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  
recval  recvalap  
absgt0 , absgt0i  absgt0ap, absgt0api  
absmax  none  The right hand side of this theorem (which is in terms of absolute value) could serve as a definition of maximum, but the left hand side (in terms of if) is not well behaved in the absence of trichotomy.  
abs1m  none  Because this theorem provides (∗‘𝐴) / (abs‘𝐴) as the answer if 𝐴 ≠ 0 and 𝑖 as the answer if 𝐴 = 0, and uses excluded middle to combine those cases, it is presumably not provable as stated. We could prove the theorem with the additional condition that 𝐴 # 0, but it is unused in set.mm.  
abslem2  none  Although this could presumably be proved if not equal were changed to apart, it is lightly used in set.mm.  
rddif , absrdbnd  none  As described under dffl , floor is problematic without excluded middle.  
rexanre  none yet  May be feasible once we've added maximum for real numbers  
rexfiuz  none  Relies on findcard2  
rexuzre  none  Presumably could be intuitionized although it would be easier after we add maximum for real numbers. It is unused in set.mm for whatever that is worth.  
rexico  none  May be feasible once we've added maximum for real numbers  
caubnd  none  The caubnd proof uses theorems related to finite sets and maximums which are not present in iset.mm, so this will need developing those areas and/or a different approach than set.mm.  
sqreulem , sqreu , sqrtcl , sqrtcld , sqrtthlem , sqrtf , sqrtth , sqsqrtd , msqsqrtd , sqr00d , sqrtrege0 , sqrtrege0d , eqsqrtor , eqsqrtd , eqsqrt2d  rersqreu, resqrtcl, resqrtcld, resqrtth  As described at dfrsqrt, square roots of complex numbers are in set.mm defined with the help of excluded middle.  
dflimsup and all superior limit theorems  none  This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.  
dfrlim and theorems related to limits of partial functions on the reals  none  This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to convergence.  
dfo1 and theorems related to eventually bounded functions  none  This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.  
dflo1 and theorems related to eventually upper bounded functions  none  This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.  
serclim0  iserclim0  The only difference is the syntax of seq.  
reccn2  none yet  Will need to be revamped to deal with negated equality versus apartness and perhaps other issues.  
clim2ser  clim2iser  The only difference is the syntax of seq.  
clim2ser2  clim2iser2  The only difference is the syntax of seq.  
iserex  iiserex  The only difference is the syntax of seq.  
isermulc2  iisermulc2  The only difference is the syntax of seq.  
iserle  iserile  The only difference is the syntax of seq.  
iserge0  iserige0  The only difference is the syntax of seq.  
climserle  climserile  The only difference is the syntax of seq.  
isershft  none yet  Relies on seqshft  
isercoll and its lemmas, isercoll2  none yet  The set.mm proof would need modification  
climsup  none  To even show convergence would presumably require a hypothesis related to the rate of convergence. Not to mention the lack of much in the way of supremum notation or theorems in iset.mm.  
climbdd  none  Presumably could be proved but the current proof of caubnd would need at least some minor adjustments.  
caurcvg2  climrecvg1n  
caucvg  climcvg1n  
caucvgb  climcaucn, climcvg1n  Without excluded middle, there are additional complications related to the rate of convergence.  
serf0  serif0  The only difference is the syntax of seq.  
iseralt  none  The set.mm proof relies on caurcvg2 which does not specify a rate of convergence.  
sumex  none  This will need to replaced by suitable closure theorems.  
sumeq2w  sumeq2  Presumably could be proved, and perhaps also would rely only on extensionality (and logical axioms). But unused in set.mm.  
seq1st  none  The second argument to seq, at least as handled in theorems such as iseqfn, must be defined on all integers greater than or equal to 𝑀, not just at 𝑀 itself. It may be possible to patch this up, but seq1st is unused in set.mm.  
algr0  ialgr0  Several hypotheses are tweaked or added to reflect differences in how seq works  
algrf  ialgrf  Several hypotheses are tweaked or added to reflect differences in how seq works  
algrp1  ialgrp1  Several hypotheses are tweaked or added to reflect differences in how seq works  
alginv  ialginv  Two hypotheses are tweaked or added to reflect differences in how seq works  
algcvg  ialgcvg  seq as defined in dfiseq has a third argument  
algcvga  ialgcvga  Two hypotheses are tweaked or added to reflect differences in how seq works  
algfx  ialgfx  Two hypotheses are tweaked or added to reflect differences in how seq works 
This
page was last updated on 15Aug2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 