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]. The one exception to the statement that we use IZF is that a few sections develop set theory using Constructive ZermeloFraenkel (CZF), also described in Crosilla. These sections start at wbd (including the section header right before it) and the biggest complication is the machinery to classify formulas as bounded formulas, for purposes of the Axiom of Restricted Separation axbdsep.
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 , necon4d , 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  
mt4d  mt2d  
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  If the proposition being eliminated is decidable (for example due to nndceq, zdceq, zdcle, zdclt, eluzdc, or fzdcel), then case elimination will work using theorems such as exmiddc and mpjaodan  
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, dfordc  
imor , imori  imorr, imorri, imordc  
pm4.63  pm3.2im  
iman  imanim, imanst  
annim  annimim  
oran , pm4.57  oranim, orandc  
ianor  pm3.14, ianordc  
pm4.14  pm4.14dc, pm3.37  
pm5.17  xorbin  The combination of dfxor and xorbin is the forward direction of pm5.17  
biluk  bilukdc  
ecase  none  This is a form of case elimination.  
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, dfrex2dc  
nfrexd  nfrexdxy, nfrexdya  
nfral  nfralxy, nfralya  
nfra2  nfra1, nfralya  
nfrex  nfrexxy, nfrexya  
r19.30  none  
r19.35  r19.351  
ralcom2  ralcom  
2reuswap  2reuswapdc  
dfpss and all proper subclass theorems  none  In set.mm, "A is a proper subclass of B" is defined to be (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) and this definition is almost always used in conjunction with excluded middle. A more natural definition might be (𝐴 ⊆ 𝐵 ∧ ∃𝑥𝑥 ∈ (𝐵 ∖ 𝐴)), if we need proper subclass at all.  
nss  nssr  
ddif  ddifnel, ddifss  
dfss4  ssddif, dfss4st  
n0f  n0rf  
n0  n0r, notm0, fin0, fin0or  
neq0  neq0r  
reximdva0  reximdva0m  
ssdif0  ssdif0im  
inssdif0  inssdif0im  
abn0  abn0r, abn0m  
rabn0  rabn0m, rabn0r  
undif1  undif1ss  
undif2  undif2ss  
inundif  inundifss  
undif  undifss  subset rather than equality, for any sets  
undiffi  where both container and subset are finite  
undifdc  where the container has decidable equality and the subset is finite  
undifdcss  when membership in the subset is decidable  
for any sets  implies excluded middle as shown at undifexmid  
ssundif  ssundifim  
uneqdifeq  uneqdifeqim  
r19.2z  r19.2m  
r19.9rzv  r19.9rmv  
r19.45zv  r19.45mv  
r19.44zv  r19.44mv  
dfif2  dfif  
ifsb  ifsbdc  
dfif4  none  Unused in set.mm  
dfif5  none  Unused in set.mm  
ifeq1da  ifeq1dadc  
ifnot  none  
ifan  none  
ifor  none  
ifeq2da  none  
ifclda  ifcldadc  
ifeqda  none  
elimif , ifid , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD  none  
ifbothda  ifbothdadc  
ifboth  ifbothdc  
eqif  eqifdc  
ifcl , ifcld  ifcldcd, ifcldadc  
dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
ifex , ifexg  ifcldcd, ifcldadc  
ifpr  none  Should be provable if the condition is decidable.  
difsnid  difsnss  One direction, for any set  
nndifsnid  for a natural number  
dcdifsnid  for a set with decidable equality  
fidifsnid  for a finite set  
sssn  sssnr, sssnm  
pwsn  pwsnss  Also see exmidpw  
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  
axrep  axcoll  There are a lot of ways to state replacement and most/all of them hold, for example zfrep6 or funimaexg.  
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  
reuxfr2d , reuxfr2 , reuxfrd , reuxfr  none  The set.mm proof of reuxfr2d relies on 2reuswap  
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. We conjecture that the set.mm snex ({𝐴} ∈ V with no condition on whether 𝐴 is a set) is not provable. The axioms of set theory allow us to construct rank levels from others, but not to construct something from nothing (except the 0 rank and stuff you can bootstrap from there). A class provides no "data" about where it lives, because it is spread out over the whole universe  you only get the ability to ask yesno(maybe) questions about set membership in the class. An assertion that a class exists is a piece of data that gives you a bound on the rank of this set, which can be used to build other existing things like unions and powersets of this class and so on. Anything with unbounded rank cannot be proven to exist. So snex, which starts from an arbitrary class and produces evidence that { A } exists, cannot be provable, because the bound here can't depend on A and cannot be upper bounded by anything independent of A either  there are singletons at every rank. However, we can refute a singleton being a proper class  see notnotsnex. 

nssss  nssssr  
rmorabex  euabex  See discussion under moabex  
nnullss  mss  
opex  opexg, opex  The iset.mm version of opex has additional hypotheses  
otex  otexg  
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  dffrind  
fri , dffr2 , frc  none  That any subset of the base set has an element which is minimal accordng to a wellfounded relation presumably implies excluded middle (or is otherwise unprovable).  
frss  freq2  Because the definition of Fr is different than set.mm, the proof would need to be different.  
frirr  frirrg  We do not yet have a lot of theorems for the case where 𝐴 is a proper class.  
fr2nr  none  Shouldn't be hard to prove if we need it (using a proof similar to frirrg and en2lp).  
frminex  none  Presumably unprovable.  
efrn2lp  none  Should be easy but lightly used in set.mm  
dfepfr , epfrc  none  Presumably unprovable.  
dfwe  dfwetr  
wess  none  See frss entry. Holds for E (see for example wessep).  
weso  wepo  
wecmpep  none  We does not imply trichotomy in iset.mm  
wefrc , wereu , wereu2  none  Presumably not provable  
dmxp  dmxpm  
dmxpid  dmxpm  
relimasn  imasng  
rnxp  rnxpm  
opswap  opswapg  
cnvso  cnvsom  
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.  
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.  
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  
ordtri2or  none  Implies excluded middle as shown at ordtri2orexmid.  
ordtri2or2  nntri2or2  ordtri2or2 implies excluded middle as shown at ordtri2or2exmid.  
onsseli  none  See entry for ordsseleq  
unizlim  none  The reverse direction is basically uni0 plus limuni  
on0eqel  0elnn  The full on0eqel is conjectured to imply excluded middle by an argument similar to ordtriexmid  
snsn0non  none  Presumably would be provable (by first proving ¬ ∅ ∈ {{∅}} as in the set.mm proof, and then using that to show that {{∅}} is not a transitive set).  
onxpdisj  none  Unused in set.mm  
onnev  none  Presumably provable (see snsn0non entry)  
iotaex  iotacl, euiotaex  
dffun3  dffun5r  
dffun5  dffun5r  
resasplit  resasplitss  
fresaun  none  The set.mm proof relies on resasplit  
fresaunres2 , fresaunres1  none  The set.mm proof relies on resasplit  
fint  fintm  
foconst  none  Although it presumably holds if nonempty is changed to inhabited, it would need a new proof and it is unused in set.mm.  
f1oprswap  none  The 𝐴 ≠ 𝐵 case is handled (basically) by f1oprg. If there is a proof of the original f1oprswap which does not rely on case elimination, it would look very different from the set.mm proof.  
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}  
fvif  fvifdc  
ndmfv  ndmfvg  The ¬ 𝐴 ∈ V case is fvprc.  
elfvdm  relelfvdm  
elfvex  relelfvdm  
fvmpti  fvmptg  The set.mm proof relies on case elimination on 𝐶 ∈ V  
fvmpt2i  fvmpt2  The set.mm proof relies on case elimination on 𝐶 ∈ V  
fvmptss  fvmptssdm  
fvmptex  none  The set.mm proof relies on case elimination  
fvmptnf  none  The set.mm proof relies on case elimination  
fvmptn  none  The set.mm proof relies on case elimination  
fvmptss2  fvmpt  What fvmptss2 adds is the cases where this is a proper class, or we are out of the domain.  
fvopab4ndm  none  
fndmdifeq0  none  Although it seems like this might be intuitionizable, it is lightly used in set.mm.  
f0cli  ffvelrn  
dff3  dff3im  
dff4  dff4im  
fvunsn  fvunsng  
fnsnsplit  none  Although it should be possible to prove subset rather than equality (using difsnss instead of difsnid ), this theorem is lightly used in set.mm.  
funiunfv  fniunfv, funiunfvdm  
funiunfvf  funiunfvdmf  
eluniima  eluniimadm  
dff14a , dff14b  none  The set.mm proof depends, in an apparently essential way, on excluded middle.  
fveqf1o  none  The set.mm proof relies on f1oprswap , which we don't have  
soisores  isoresbr  
soisoi  none  The set.mm proof relies on trichotomy  
isocnv3  none  It seems possible that one direction of the biconditional could be proved.  
isomin  none  
riotaex  riotacl, riotaexg  
nfriotad  nfriotadxy  
csbriota , csbriotagOLD  csbriotag  
riotaxfrd  none  Although it may be intuitionizable, it is lightly used in set.mm. The set.mm proof relies on reuxfrd .  
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.  
ovrcl  elmpt2cl, relelfvdm  
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. (One thing we presumably could prove is (∪ 𝐴 ⊆ On ∧ ∃𝑥𝑥 ∈ (On ∖ ∪ 𝐴)) → 𝐴 ∈ 𝑉 which might be easier to understand if we define (or think of) proper subset as meaning that the set difference is inhabited.)  
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, nnsucuniel  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_{o}). 

ordzsl, onzsl, dflim3, nlimon  none  
dflim4  dfilim  We conjecture that dflim4 is not equivalent to dfilim.  
limsuc  none  This would be trivial if dflim4 were the definition of a limit ordinal. With dflim2 as the definition, limsuc might need ordunisuc2 (which we believe is not provable, see its entry in this list).  
limsssuc  none  Conjectured to be provable (is this also based on dflim4 being the definition of limit ordinal or is it unrelated?).  
tfinds , tfindsg  tfis3  We are unable to separate limit and successor ordinals using case elimination.  
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  
omopth2  none  The set.mm proof relies on ordinal trichotomy.  
omeulem1 , omeu  none  The set.mm proof relies on ordinal trichotomy, omopth2 , oaord , and other theorems we don't have.  
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  
oa0r  none  The set.mm proof distinguishes between limit and successor cases using case elimination.  
oaordi  nnaordi  The set.mm proof of oaordi relies on being able to distinguish between limit ordinals and successor ordinals via case elimination.  
oaord  nnaord  The set.mm proof of oaord relies on ordinal trichotomy.  
oawordri  none  Implies excluded middle as shown at oawordriexmid  
oaword  oawordi  The other direction presumably could be proven but isn't yet.  
oaord1  none yet  
oaword2  none  The set.mm proof relies on oawordri and oa0r  
oawordeu  none  The set.mm proof relies on a number of things we don't have  
oawordex  nnawordex  The set.mm proof relies on oawordeu  
omwordi  nnmword  The set.mm proof of omwordi relies on case elimination.  
omword1  nnmword  
oawordex  nnawordex  
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.  
ralxpmap  none  Lightly used in set.mm. The set.mm proof relies on fnsnsplit and undif .  
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  
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 , oaord , om0r , and other theorems we do not have  
pw2f1o , pw2eng , pw2en  none  Presumably would require some kind of decidability hypothesis. Discussions of this sort tend to get into how many truth values there are and sets like {𝑠 ∣ 𝑠 ⊆ 1_{o}} (relatively undeveloped so far except for a few results like exmid01 and uni0b).  
enfixsn  none  The set.mm proof relies on difsnen  
sbth and its lemmas, sbthb , sbthcl  fisbth  The SchroederBernstein Theorem is equivalent to excluded middle by exmidsbth  
fodomr  none  Equivalent to excluded middle per exmidfodomr  
mapdom1  mapdom1g  
2pwuninel  2pwuninelg  
mapunen  none  The set.mm proof relies on fresaunres1 and fresaunres2 .  
map2xp  none  The set.mm proof relies on mapunen  
mapdom2 , mapdom3  none  The set.mm proof relies on case elimination and undif . At a minimum, it would appear that nonempty would need to be changed to inhabited.  
pwen  none  The set.mm proof relies on pw2eng  
limenpsi  none  The set.mm proof relies on sbth  
limensuci , limensuc  none  The set.mm proof relies on undif  
infensuc  none  The set.mm proof relies on limensuc  
php  phpm  
snnen2o  snnen2og, snnen2oprc  
onomeneq , onfin , onfin2  none  The set.mm proofs rely on excluded middle  
nnsdomo , sucdom2 , sucdom , 0sdom1dom , sdom1  none  iset.mm doesn't yet have strict dominance  
1sdom2  1nen2  Although the presence of 1nen2 might make it look like a natural definition for strict dominance would be 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵, that definition may be more suitable for finite sets than all sets, so at least for now we only define ≈ and express certain theorems (such as this one) in terms of equinumerosity which in set.mm are expressed in terms of 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  
isinf  isinfinf  
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  ssfirab  when the subset is defined by a decidable property  
ssfidc  when membership in the subset is decidable  
for the general case  Implies excluded middle as shown at ssfiexmid  
domfi  none  Implies excluded middle as shown at domfiexmid  
xpfir  none  Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi  
infi  none  Implies excluded middle as shown at infiexmid. It is conjectured that we could prove the special case (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∪ 𝐵) ∈ Fin) → (𝐴 ∩ 𝐵) ∈ Fin  
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  
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.  
frfi  none  Not known whether this can be proved (either with the current dffrind or any other possible concept analogous to Fr).  
fimax2g , fimaxg  none  The set.mm proof relies on frfi and fri  
fisupg  none  The set.mm proof relies on excluded middle and presumably this theorem would need to be modified to be provable.  
unfi  unsnfi  For the union of a set and a singleton whose element is not a member of that set  
unfidisj  For the union of two disjoint sets  
unfiin  When the intersection is known to be finite  
for any two finite sets  Implies excluded middle as shown at unfiexmid.  
prfi  prfidisj  for two unequal sets  
in general  The set.mm proof depends on unfi and it would appear that mapping {𝐴, 𝐵} to a natural number would decide whether 𝐴 and 𝐵 are equal and thus imply excluded middle.  
fodomfi  none  Might be provable, for example via ac6sfi or induction directly. The set.mm proof does use undom in addition to induction.  
dmfi  fundmfi  
resfnfinfin  resfnfinfinss  
residfi  none  Presumably provable, but lightly used in set.mm  
cnvfi  relcnvfi  
rnfi  funrnfi  
fofi  f1ofi  Presumably precluded by an argument similar to domfiexmid (the set.mm proof relies on domfi).  
pwfi  none  The set.mm proof uses domfi and other theorems we don't have  
abrexfi  none  At first glance it would appear that the mapping would need to be one to one or some other condition.  
dfsup2  none  The set.mm proof uses excluded middle in several places and the theorem is lightly used in set.mm.  
supmo  supmoti  The conditions on the order are different.  
supexd , supex  none  The set.mm proof uses rmorabex  
supeu  supeuti  
supval2  supval2ti  
eqsup  eqsupti  
eqsupd  eqsuptid  
supcl  supclti  
supub  supubti  
suplub  suplubti  
suplub2  suplub2ti  
supnub  none  Presumably provable, although the set.mm proof relies on excluded middle and it is not used until later in set.mm.  
sup0riota , sup0 , infempty  none  Suitably modified verions may be provable, but they are unused in set.mm.  
supmax  supmaxti  
fisup2g , fisupcl  none  Other variations may be possible, but the set.mm proof will not work asis or with small modifications.  
supgtoreq  none  The set.mm proof uses fisup2g and also trichotomy.  
suppr  none  The formulation using if would seem to require a trichotomous order. For real numbers, supremum on a pair does yield the maximum of two numbers: see maxcl, maxle1, maxle2, maxleast, and maxleb.  
supiso  supisoti  
infexd , infex  none  See supexd  
eqinf , eqinfd  eqinfti, eqinftid  
infval  infvalti  
infcllem  cnvinfex  infcllem has an unnecessary hypothesis; other than that these are the same  
infcl  infclti  
inflb  inflbti  
infglb  infglbti  
infglbb  none  Presumably provable with additional conditions (see suplub2)  
infnlb  infnlbti  
infmin  infminti  
infmo  infmoti  
infeu  infeuti  
fimin2g , fiming  none  The set.mm proof relies on frfi and fri  
fiinfg , fiinf2g  none  The set.mm proof relies on fiming  
fiinfcl  none  See fisupcl  
infltoreq  none  The set.mm proof depends on supgtoreq and fiinfcl  
infpr  none  See suppr  
infsn  infsnti  
infiso  infisoti  
axreg , axreg2 , zfregcl  axsetind  axreg implies excluded middle as seen at regexmid  
dfrank and all theorems related 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.  
prdom2  none  The set.mm proof would only work in the case where 𝐴 = 𝐵 is decidable. If we can prove fodomfi , that would appear to imply prsomd2 fairly quickly.  
dif1card  none  The set.mm proof relies on cardennn  
leweon  none  We lack the well ordering related theorems this relies on, and it isn't clear they are provable.  
r0weon  none  We lack the well ordering related theorems this relies on, and it isn't clear they are provable.  
infxpen  none  The set.mm proof relies on well ordering related theorems that we don't have (and may not be able to have), and it isn't clear that infxpen is provable.  
infxpidm2  none  Depends on cardinality theorems we don't have.  
infxpenc  none  Relies on notations and theorems we don't have.  
infxpenc2  none  Relies on theorems we don't have.  
dfac8a  none  The set.mm proof does not work asis and numerability may not be able to work the same way.  
dfac8b  none  We are lacking much of what this proof relies on and we may not be able to make numerability and wellordering work as in set.mm.  
dfac8c  none  The set.mm proof does not work asis and wellordering may not be able to work the same way.  
ac10ct  none  The set.mm proof does not work asis and wellordering may not be able to work the same way.  
ween  none  The set.mm proof does not work asis and wellordering and numerability may not be able to work the same way.  
ac5num , ondomen , numdom , ssnum , onssnum , indcardi  none  Numerability (or cardinality in general) is not well developed and to a certain extent cannot be.  
fodom , fodomnum  none  Presumably not provable as stated  
fodomb  none  That the reverse direction is equivalent to excluded middle is exmidfodomr. The forward direction is presumably also not provable.  
entri3  fientri3  Because full entri3 is equivalent to the axiom of choice, it implies excluded middle.  
infinf  infnfi  Defining "A is infinite" as ω ≼ 𝐴 follows definition 8.1.4 of [AczelRathjen], p. 71. It can presumably not be shown to be equivalent to ¬ 𝐴 ∈ Fin in the absence of excluded middle (see inffiexmid which isn't exactly about ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 but which is close).  
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 , lttri2i , lttri2d  qlttri2  Real number trichotomy is not provable.  
lttri4  ztri3or, qtri3or  Real number trichotomy is not provable.  
leloe , eqlelt , leloei , leloed , eqleltd  none  
leltne , leltned  leltap, leltapd  
ltneOLD  ltne, ltap  
letric , letrii , letrid  zletric, qletric  
ltlen , ltleni , ltlend  ltleap, zltlen, qltlen  
ne0gt0 , ne0gt0d  ap0gt0, ap0gt0d  
lecasei , ltlecasei  none  These are real number trichotomy  
lelttric  zlelttric, qlelttric  
lttrid , lttri4d  none  These are real number trichotomy  
leneltd  leltapd  
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  Although these presumably could be proved using theorems like letri3 and lenlt, at least for now we have chosen to just invoke those other theorems directly (example: expcan and its lemma expcanlem) which avoids some extra set variables and produces proofs which are almost as short.  
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  
divmulass  divmulassap  
divmulasscom  divmulasscomap  
divdir , divcan3 , divcan4  divdirap, divcanap3, divcanap4  
div11 , divid , div0  div11ap, dividap, div0ap  
diveq1 , divneg  diveqap1, divnegap  
muldivdir  muldivdirap  
divsubdir  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 , mulsuble0b  none  Presumably unprovable for reasons analogous to mul0or.  
mulle0b  mulle0r  The converse of mulle0r is presumably unprovable for reasons analogous to mul0or.  
ledivp1i , ltdivp1i  none  Presumably could be proved, but unused in set.mm.  
fimaxre  fimaxre2  When applied to a pair this could show which of two unequal real numbers is larger, so perhaps not provable for that reason. (see fin0 for inhabited versus nonempty).  
fimaxre3  none  The set.mm proof relies on abrexfi .  
fiminre  none  See fimaxre  
sup2 , sup3 , sup3ii  none  We won't be able to have the least upper bound property for all nonempty bounded sets. In cases where we can show that the supremum exists, we might be able to prove slightly different ways of stating there is a supremum.  
infm3  none  See sup3  
suprcl , suprcld , suprclii  supclti  
suprub , suprubd , suprubii  suprubex  
suprlub , suprlubii  suprlubex  
suprnub , suprnubii  suprnubex  
suprleub , suprleubii  suprleubex  
supaddc , supadd  none  Presumably provable with suitable conditions for the existence of the supremums  
supmul1 , supmul  none  Presumably provable with suitable conditions for the existence of the supremums  
riotaneg  none  The theorem is unused in set.mm and the set.mm proof relies on reuxfrd  
infrecl  infclti  
infrenegsup  infrenegsupex  
infregelb  none yet  Presumably could be handled in a way analogous to suprleubex  
infrelb  none yet  Presumably could be handled in a way analogous to suprubex  
supfirege  suprubex  The question here is whether results like maxle1 can be generalized (presumably by induction) from pairs to finite sets.  
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  qavgle  
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  suprzclex  
zriotaneg  none  Lightly used in set.mm  
suprfinzcl  none  
decex  deccl  
halfthird  none  Presumably will be easy to intuitionize  
5recm6rec  none  Presumably will be easy to intuitionize  
uzwo , uzwo2 , nnwo , nnwof , nnwos  none  Presumably would imply excluded middle, unless there is something which makes this different from nnregexmid.  
negn0  negm  
uzinfi, nninf, nn0inf  none  Presumably provable  
infssuzle  infssuzledc  
infssuzcl  infssuzcldc  
supminf  supminfex  
zsupss , suprzcl2  zsupcl, suprzclex  
suprzub  none  Presumably could prove something like this with different conditions for the existence of the supremum (see infssuzledc for something along these lines).  
uzsupss  zsupcl  
uzwo3 , zmin  none  Proved in terms of supremum theorems and presumably not possible without excluded middle.  
zbtwnre  none  Proved in terms of supremum theorems and presumably not possible without excluded middle.  
rebtwnz  qbtwnz  
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 , max0sub , ifle  none  
max1  maxle1  
max2  maxle2  
2resupmax  none  Proved from real trichotomy. We express maximum in iset.mm using sup({𝐴, 𝐵}, ℝ, < ) rather than if(𝐴 ≤ 𝐵, 𝐵, 𝐴). The former has the expected maximum properties such as maxcl, maxle1, maxle2, maxleast, and maxleb.  
min1  min1inf  
min2  min2inf  
maxle  maxleastb  
lemin  lemininf  
maxlt  maxltsup  
ltmin  ltmininf  
qsqueeze  none yet  Presumably provable from qbtwnre and squeeze0, but unused in set.mm.  
qextltlem , qextlt , qextle  none  The set.mm proof is not intuitionistic.  
xralrple , alrple  none yet  Now that we have 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  
ioon0  ioom  Nonempty is changed to inhabited  
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  
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.  
flcl , reflcl , flcld  flqcl, flqcld  
fllelt  flqlelt  
flle  flqle  
flltp1 , fllep1  flqltp1  
fraclt1 , fracle1  qfraclt1  
fracge0  qfracge0  
flge  flqge  
fllt  flqlt  
flflp1  none  The set.mm proof relies on case elimination.  
flidm  flqidm  
flidz  flqidz  
flltnz  flqltnz  
flwordi  flqwordi  
flword2  flqword2  
flval2 , flval3  none  Unused in set.mm  
flbi  flqbi  
flbi2  flqbi2  
ico01fl0  none  Presumably could be proved for rationals, but lightly used in set.mm.  
flge0nn0  flqge0nn0  
flge1nn  flqge1nn  
refldivcl  flqcl  
fladdz  flqaddz  
flzadd  flqzadd  
flmulnn0  flqmulnn0  
fldivle  flqle  
ltdifltdiv  none  Unused in set.mm.  
fldiv4lem1div2uz2 , fldiv4lem1div2  none  Presumably provable, but lightly used in set.mm.  
ceilval  ceilqval  The set.mm ceilval, with a real argument and no additional conditions, is probably provable if there is a need.  
dfceil2 , ceilval2  none  Unused in set.mm.  
ceicl  ceiqcl  
ceilcl  ceilqcl  
ceilge  ceilqge  
ceige  ceiqge  
ceim1l  ceiqm1l  
ceilm1lt  ceilqm1lt  
ceile  ceiqle  
ceille  ceilqle  
ceilidz  ceilqidz  
flleceil  flqleceil  
fleqceilz  flqeqceilz  
quoremz , quoremnn0 , quoremnn0ALT  none  Unused in set.mm.  
intfrac2  intqfrac2  
fldiv  flqdiv  
fldiv2  none  Presumably would be provable if real is changed to rational.  
fznnfl  none  Presumably would be provable if real is changed to rational.  
uzsup , ioopnfsup , icopnfsup , rpsup , resup , xrsup  none  As with most theorems involving supremums, these would likely need significant changes  
modval  modqval  As with theorems such as flqcl, we prove most of the modulo related theorems for rationals, although other conditions on real arguments other than whether they are rational would be possible in the future.  
modvalr  modqvalr  
modcl , modcld  modqcl, modqcld  
flpmodeq  flqpmodeq  
mod0  modq0  
mulmod0  mulqmod0  
negmod0  negqmod0  
modge0  modqge0  
modlt  modqlt  
modelico  modqelico  
moddiffl  modqdiffl  
moddifz  modqdifz  
modfrac  modqfrac  
flmod  flqmod  
intfrac  intqfrac  
modmulnn  modqmulnn  
modvalp1  modqvalp1  
modid  modqid  
modid0  modqid0  
modid2  modqid2  
0mod  q0mod  
1mod  q1mod  
modabs  modqabs  
modabs2  modqabs2  
modcyc  modqcyc  
modcyc2  modqcyc2  
modadd1  modqadd1  
modaddabs  modqaddabs  
modaddmod  modqaddmod  
muladdmodid  mulqaddmodid  
modmuladd  modqmuladd  
modmuladdim  modqmuladdim  
modmuladdnn0  modqmuladdnn0  
negmod  qnegmod  
modadd2mod  modqadd2mod  
modm1p1mod0  modqm1p1mod0  
modltm1p1mod  modqltm1p1mod  
modmul1  modqmul1  
modmul12d  modqmul12d  
modnegd  modqnegd  
modadd12d  modqadd12d  
modsub12d  modqsub12d  
modsubmod  modqsubmod  
modsubmodmod  modqsubmodmod  
2txmodxeq0  q2txmodxeq0  
2submod  q2submod  
modmulmod  modqmulmod  
modmulmodr  modqmulmodr  
modaddmulmod  modqaddmulmod  
moddi  modqdi  
modsubdir  modqsubdir  
modeqmodmin  modqeqmodmin  
modirr  none  A version of this (presumably modified) may be possible, but it is unused in set.mm  
om2uz0i  frec2uz0d  
om2uzsuci  frec2uzsucd  
om2uzuzi  frec2uzuzd  
om2uzlti  frec2uzltd  
om2uzlt2i  frec2uzlt2d  
om2uzrani  frec2uzrand  
om2uzf1oi  frec2uzf1od  
om2uzisoi  frec2uzisod  
om2uzoi , ltweuz , ltwenn , ltwefz  none  Based on theorems like nnregexmid it is not clear what, if anything, along these lines is possible.  
om2uzrdg  frec2uzrdg  
uzrdglem  frecuzrdglem  
uzrdgfni  frecuzrdgtcl  
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  none  The set.mm proof relies on fisupcl and it is not clear whether this supremum theorem or anything similar can be proved.  
fseqsupubi  none  The set.mm proof relies on fsequb2 and suprub and it is not clear whether this supremum theorem or anything similar can be proved.  
uzindi  none  This could presumably be proved, perhaps from uzsinds, 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  iseqfcl  
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  iseqfcl  
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  iseqid2  
seqhomo  iseqhomo  
seqz  iseqz  
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  
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  
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  
expne0d  expap0d  
expnegd  expnegapd  
exprecd  exprecapd  
expp1zd  expp1zapd  
expm1d  expm1apd  
expsubd  expsubapd  
sqdivd  sqdivapd  
expdivd  expdivapd  
reexpclzd  reexpclzapd  
sqgt0d  sqgt0apd  
mulsubdivbinom2  none  Presumably provable if not equal is changed to apart.  
muldivbinom2  none  Presumably provable if not equal is changed to apart.  
nn0le2msqi  nn0le2msqd  Although nn0le2msqi could be proved, having a version in deduction form will be more useful.  
nn0opthlem1  nn0opthlem1d  Although nn0opthlem1 could be proved, having a version in deduction form will be more useful.  
nn0opthlem2  nn0opthlem2d  Although nn0opthlem2 could be proved, having a version in deduction form will be more useful.  
nn0opthi  nn0opthd  Although nn0opthi could be proved, having a version in deduction form will be more useful.  
nn0opth2i  nn0opth2d  Although nn0opth2i could be proved, having a version in deduction form will be more useful.  
facmapnn  faccl  Presumably provable now that iset.mm has dfmap. But faccl would be sufficient for the uses in set.mm.  
faclbnd4 , faclbnd5 , and lemmas  none  Presumably provable; unused in set.mm.  
bcval5  ibcval5  
dfhash  dfihash  
hashkf , hashgval , hashginv  none  Due to the differences between dfhash in set.mm and dfihash here, there's no particular need for these as stated  
hashinf  hashinfom  The condition that 𝐴 is infinite is changed from ¬ 𝐴 ∈ Fin to ω ≼ 𝐴.  
hashbnd  none  The set.mm proof is not intuitionistic.  
hashfxnn0 , hashf , hashxnn0 , hashresfn , dmhashres , hashnn0pnf  none  Although dfihash is defined for finite sets and infinite sets, it is not clear we would be able to show this definition (or another definition) is defined for all sets.  
hashnnn0genn0  none  Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize.  
hashnemnf  none  Presumably provable but the set.mm proof relies on hashnn0pnf  
hashv01gt1  hashfiv01gt1  It is not clear there would be any way to combine the finite and infinite cases.  
hasheni  hashen, hashinfom  It is not clear there would be any way to combine the finite and infinite cases.  
hasheqf1oi  fihasheqf1oi  It is not clear there would be any way to combine the finite and infinite cases.  
hashf1rn  fihashf1rn  It is not clear there would be any way to combine the finite and infinite cases.  
hasheqf1od  fihasheqf1od  It is not clear there would be any way to combine the finite and infinite cases.  
hashcard  none  Cardinality is not well developed in iset.mm  
hashxrcl  none  It is not clear there would be any way to combine the finite and infinite cases.  
hashclb  none  Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize.  
nfile  filtinf  It is not clear there would be any way to combine the case where 𝐴 is finite and the case where it is infinite.  
hashvnfin  none  This is a form of reverse closure, presumably not provable.  
hashnfinnn0  hashinfom  
isfinite4  isfinite4im  
hasheq0  fihasheq0  It is not clear there would be any way to combine the finite and infinite cases.  
hashneq0 , hashgt0n0  fihashneq0  
hashen1  fihashen1  
hashrabrsn  none  Presumably would need conditions around the existence of 𝐴 and decidability of 𝜑 but unused in set.mm.  
hashrabsn01  none  Presumably would need conditions around the existence of 𝐴 and decidability of 𝜑 but unused in set.mm.  
hashrabsn1  none  The set.mm proof uses excluded middle and this theorem is unused in set.mm.  
hashfn  fihashfn  There is an added condition that the domain be finite.  
hashgadd  omgadd  
hashgval2  none  Presumably provable, when restated as (♯ ↾ ω) = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0), but lightly used in set.mm.  
hashdom  fihashdom  There is an added condition that 𝐵 is finite.  
hashdomi  fihashdom  It is presumably not possible to extend fihashdom beyond the finite set case.  
hashun2  none  The set.mm proof relies on undif2 (we just have undif2ss) and diffi (we just have diffifi)  
hashun3  none  The set.mm proof relies on various theorems we do not have  
hashinfxadd  none  
hashunx  none  It is not clear there would be any way to combine the finite and infinite cases.  
hashge0  hashcl  It is not clear there would be any way to combine the finite and infinite cases.  
hashgt0 , hashge1  hashnncl  It is not clear there would be any way to combine the finite and infinite cases.  
hashnn0n0nn  hashnncl  To the extent this is reverse closure, we probably can't prove it. For inhabited versus nonempty, see fin0  
elprchashprn2  hashsng  Given either 𝑁 ∈ V or ¬ 𝑁 ∈ V this could be proved (as (♯‘{𝑀, 𝑁}) reduces to hashsng or hash0 respectively), but is not clear we can combine the cases (even 1domsn may not be enough).  
hashprb  hashprg  
hashprdifel  none  This would appear to be a form of reverse closure.  
hashle00  fihasheq0  
hashgt0elex , hashgt0elexb  fihashneq0  See fin0 for inhabited versus nonempty. It isn't clear it would be possible to also include the infinite case as hashgt0elex does.  
hashss  fihashss  
prsshashgt1  fiprsshashgt1  
hashin  none  Presumably additional conditions would be needed (see infi entry).  
hashssdif  fihashssdif  
hashdif  none  Modified versions presumably would be provable, but this is unused in set.mm.  
hashsn01  none  Presumably not provable  
hashsnle1  none  At first glance this would appear to be the same as 1domsn but to apply fihashdom would require that the singleton be finite, which might imply that we cannot improve on hashsng.  
hashsnlei  none  Presumably not provable  
hash1snb , euhash1 , hash1n0 , hashgt12el , hashgt12el2  none  Conjectured to be provable in the finite set case  
hashunlei  none  Not provable per unfiexmid (see also entry for hashun2)  
hashsslei  fihashss  Would be provable if we transfered 𝐵 ∈ Fin from the conclusion to the hypothesis but as written falls afoul of ssfiexmid.  
hashmap  none  Probably provable but the set.mm proof relies on a number of theorems which we don't have.  
hashpw  none  Unlike pw2en this is only for finite sets, so it presumably is provable. The set.mm proof may be usable.  
hashfun  none  Presumably provable but the set.mm proof relies on excluded middle and undif.  
hashres , hashreshashfun  none  Presumably would need to add 𝐵 ∈ Fin or similar conditions.  
hashimarn , hashimarni  none  Presumably would need an additional condition such as 𝐹 ∈ Fin but unused in set.mm.  
fnfz0hashnn0  none  Presumably would need an additional condition such as 𝑁 ∈ ℕ_{0} but unused in set.mm.  
fnfzo0hashnn0  none  Presumably would need an additional condition such as 𝑁 ∈ ℕ_{0} but unused in set.mm.  
hashbc  none  The set.mm proof uses pwfi and ssfi .  
hashf1  none  The set.mm proof uses ssfi , excluded middle, abn0 , diffi and perhaps other theorems we don't have.  
hashfac  none  The set.mm proof uses hashf1 .  
leiso , leisorel  none  The set.mm proof uses isocnv3 .  
fz1iso  none  The set.mm proof depends on OrdIso  
ishashinf  none  May be possible with the antecedent changed from ¬ 𝐴 ∈ Fin to ω ≼ 𝐴 but the set.mm proof does not work as is.  
seqcoll , seqcoll2  none  Presumably will require significant modifications.  
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  qabsor  It also would be possible to prove this for 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  max0addsup  
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  maxabs  
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  If there is a need, we could prove these for rationals or real numbers apart from any rational. Alternately, we could prove a result with a slightly larger bound for any real number.  
rexuzre  none  Unless the real number 𝑗 is known to be apart from an integer, it isn't clear there would be any way to prove this (see the steps in the set.mm proof which rely on the floor of a real number). It is unused in set.mm for whatever that is worth.  
caubnd  none  If we can prove fimaxre3 it would appear that the set.mm proof would work with small changes (in the case of the maximum of two real numbers, using maxle1, maxle2, and maxcl).  
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 show convergence would presumably require a hypothesis related to the rate of convergence.  
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.  
dfsum  dfisum  Although this defintion is intended to function similarly to the set.mm one, a lot of details have to be changed, especially around decidability, to make sum work.  
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.  
sumeq2ii  sumeq2d  
sumrblem  isumrblem  
fsumcvg  fisumcvg  
sumrb  isumrb  
dfprod and theorems using it  none  To define this, will need to tackle all the issues with dfisum plus some more around, for example, not equal to zero versus apart from zero  
znnen  none  Corollary 8.1.23 of [AczelRathjen] and thus presumably provable. The set.mm proof would not work asis or with small changes, however.  
qnnen  none  Corollary 8.1.23 of [AczelRathjen] and thus presumably provable. The set.mm proof would not work asis or with small changes, however.  
dvdsaddre2b  none  Something along these lines (perhaps with real changed to rational) may be possible  
fsumdvds , 3dvds  none  May be possible when summation is well enough developed  
sumeven , sumodd , evensumodd , oddsumodd , pwp1fsum , oddpwp1fsum  none  Presumably possible when summation is well enough developed  
divalglem0 and other divalg lemmas  divalglemnn and other lemmas  Since the end result divalg is the same, we don't list all the differences in lemmas here.  
gcdcllem1 , gcdcllem2 , gcdcllem3  gcdn0cl, gcddvds, dvdslegcd  These are lemmas which are part of the proof of theorems that iset.mm proves a somewhat different way  
seq1st  none  The second argument to seq, at least as handled in theorems such as iseqfcl, 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  
eucalg  eucialg  Tweaked for the different seq syntax  
dflcmf and theorems using it  none  Although this could be defined, most of the theorems would need decidability conditions analogous to zsupcl  
absproddvds , absprodnn  none  Needs product to be developed, but once that is done seems like it might be possible.  
fissn0dvds , fissn0dvdsn0  none  Possibly could be proved using findcard2 or the like.  
coprmprod , coprmproddvds  none  Can investigate once product is better developed.  
isprm5  none  Presumably provable, but the set.mm proof relies on excluded middle in multiple places.  
isprm7  none  The set.mm proof relies on isprm5  
maxprmfct  none  Presumably provable with suitable adjustments to the condition for the existence of the supremum  
ncoprmlnprm  none  Presumably provable but the set.mm proof uses excluded middle  
zsqrtelqelz  nn0sqrtelqelz  We don't yet have much on the square root of a negative number  
dfodz and all theorems concerning the order function on the class of integers mod N  none  Presumably could be defined, but would require changes to how we show the infimum exists. Lightly used in set.mm.  
eulerth  none  The lemma eulerthlem2 relies on seqf1o  
fermltl  none  Relies on eulerth  
prmdiv  none  Relies on eulerth  
prmdiveq  none  Relies on prmdiv  
prmdivdiv  none  Relies on prmdiveq  
phisum  none  May be provable once summation is better developed 
This
page was last updated on 15Aug2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 