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  
nsyl4  con1dc  
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  
pm4.52  pm4.52im  
pm4.53  pm4.53r  
pm5.17  xorbin  The combination of dfxor and xorbin is the forward direction of pm5.17  
biluk  bilukdc  
biadan  biadani  The set.mm proof of biadan depends on biluk  
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  
dfmo  dfmo  The definitions are different although they currently share the same name.  
exmo  exmonim  
mof  mo2r, mo3  
dfeu , dfeu  eu5  Although this is a definition in set.mm and a theorem in iset.mm it is otherwise the same (with a different name).  
eu6  dfeu  Although this is a definition in iset.mm and a theorem in set.mm it is otherwise the same (with a different name).  
nfabd2  nfabd  
nne  nner, nnedc  
exmidne  dcne  
necon1ad  necon1addc  
necon1bd  necon1bddc  
necon4ad  necon4addc  
necon4bd  necon4bddc  
necon1d  necon1ddc  
necon4d  necon4ddc  
necon1ai  necon1aidc  
necon1bi  necon1bidc  
necon4ai  necon4aidc  
necon1i  necon1idc  
necon4i  necon4idc  
necon4abid  necon4abiddc  
necon4bbid  necon4bbiddc  
necon4bid  necon4biddc, apcon4bid  
necon1abii  necon1abiidc  
necon1bbii  necon1bbiidc  
necon1abid  necon1abiddc  
necon1bbid  necon1bbiddc  
necon2abid  necon2abiddc  
necon2bbid  necon2bbiddc  
necon2abii  necon2abiidc  
necon2bbii  necon2bbiidc  
nebi  nebidc  
pm2.61ne, pm2.61ine, pm2.61dne, pm2.61dane, pm2.61da2ne, pm2.61da3ne  pm2.61dc  
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  
rmo2  rmo2i  
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  
dfsymdif , dfsymdif2  symdifxor  The symmetric difference notation and a number of the theorems could be brought over from set.mm.  
dfss4  ssddif, dfss4st  
dfun3  unssin  
dfin3  inssun  
dfin4  inssddif  
unineq  none  
difindi  difindiss  
difdif2  difdif2ss  
indm  indmss  
undif3  undif3ss  
n0f  n0rf  
n0  n0r, notm0, fin0, fin0or  
neq0  neq0r  
reximdva0  reximdva0m  
ssdif0  ssdif0im  
inssdif0  inssdif0im  
abn0  abn0r, abn0m  
rabn0  rabn0m, rabn0r  
csb0  csbconstg, csbprc  The set.mm proof uses excluded middle to combine the 𝐴 ∈ V and ¬ 𝐴 ∈ V cases.  
sbcel12  sbcel12g  
sbcne12  sbcne12g  
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  
forward direction only, for any sets  still implies excluded middle as shown at exmidundifim  
ssundif  ssundifim  
uneqdifeq  uneqdifeqim  
r19.2z  r19.2m  
r19.3rz  r19.3rm  
r19.28z  r19.28m  
r19.9rzv  r19.9rmv  
r19.37zv  r19.3rmv  
r19.45zv  r19.45mv  
r19.44zv  r19.44mv  
r19.27z  r19.27m  
r19.36zv  r19.36av  
dfif2  dfif  
ifsb  ifsbdc  
dfif4  none  Unused in set.mm  
dfif5  none  Unused in set.mm  
ifeq1da  ifeq1dadc  
ifnot  none  
ifor  none  
ifeq2da  none  
ifclda  ifcldadc  
ifeqda  none  
elimif , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD  none  
ifbothda  ifbothdadc  
ifboth  ifbothdc  
ifid  ifiddc  
eqif  eqifdc  
ifcl , ifcld  ifcldcd, ifcldadc  
ifan  ifandc  
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  
pwpw0  pwpw0ss  that pwpw0 is equivalent to excluded middle follows from exmidpw or exmid01  
sssn  sssnr  One direction, for any classes.  
sssnm  When the subset is inhabited.  
for all sets  Equivalent to excluded middle by exmidsssn.  
ssunsn2 , ssunsn  none  
eqsn  eqsnm  
ssunpr  none  
sspr  ssprr  
sstp  sstpr  
prnebg  none  
pwsn  pwsnss  Also see exmidpw  
pwpr  pwprss  
pwtp  pwtpss  
pwpwpw0  pwpwpw0ss  
iundif2  iundif2ss  
iindif2  iindif2m  
iinin2  iinin2m  
iinin1  iinin1m  
iinvdif  iindif2m  Unused in set.mm  
riinn0  riinm  
riinrab  iinrabm  
iunxdif3  none  the set.mm proof relies on inundif  
iinuni  iinuniss  
iununi  iununir  
rintn0  rintm  
disjor  disjnim  
disjors  disjnims  
disji  none  
disjprg , disjxiun , disjxun  none  
disjss3  none  Might need to be restated or have decidability conditions added  
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  
opnz  opm, opnzi  
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  
relimasn  imasng  
xpnz  xpm  
xpeq0  xpeq0r, sqxpeq0  
difxp  none  The set.mm proof relies on ianor  
rnxp  rnxpm  
ssxpb  ssxpbm  
xp11  xp11m  
xpcan  xpcanm  
xpcan2  xpcan2m  
xpima2  xpima2m  
sossfld , sofld , soex  none  the set.mm proofs rely on trichotomy  
csbrn  csbrng  
dmsnn0  dmsnm  
rnsnn0  rnsnm  
relsn2  relsn2m  
dmsnopss  dmsnopg  The domain is empty in the ¬ 𝐵 ∈ V case which follows readily from opprc2 and dmsn0. But we presumably cannot combine the 𝐵 ∈ V and ¬ 𝐵 ∈ V cases (set.mm uses excluded middle to do so).  
dmsnsnsn  dmsnsnsng  
opswap  opswapg  
unixp  unixpm  
cnvso  cnvsom  
unixp0  unixp0im  
unixpid  none  We could prove the theorem for the case where A is inhabited  
cnviin  cnviinm  
xpco  xpcom  
xpcoid  xpcom  
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  nntr2  ontr2 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, nnsssuc  
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)  
nfiotad  nfiotadw  
nfiota  nfiotaw  
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}  
slotex  for a slot of an extensible structure  
fvexi , fvexd  see fvex  
fvif  fvifdc  
fvrn0  none  The set.mm proof uses case elimination on whether (𝐹‘𝑋) is the empty set.  
fvssunirn  fvssunirng, relfvssunirn  
ndmfv  ndmfvg  The ¬ 𝐴 ∈ V case is fvprc.  
elfvdm  relelfvdm  
elfvex , elfvexd  relelfvdm, mptrcl  
dffn5  dffn5im  
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  
fmptsng , fmptsnd  none  presumably provable  
fvunsn  fvunsng  
fnsnsplit  fnsnsplitss  Subset rather than equality, for a function on any set.  
fnsnsplitdc  For a function on a set with decidable equality.  
fsnunf2  none  Apparently would need decidable equality on 𝑆 or some other condition.  
funresdfunsn  funresdfunsnss  Subset rather than equality, for a function on any set.  
funresdfunsndc  For a function on a set with decidable equality.  
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  
mpofvex  When the operation is defined via mapsto, yields a set on any inputs, and is being evaluated at two sets.  
addcl, expcl, etc  If there is a closure theorem for a particular operation, that is often the way to intuitionize ovex (check for your particular operation, as these are just a few examples).  
ovrcl  elmpocl, relelfvdm  
opabresex2d  none  it should be possible to update iset.mm to reflect set.mm in this area and related theorems  
ovif12  none  would be provable under the condition that 𝜑 is decidable  
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  oprssdmm  
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  elmpocl, 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  
mpondm0  none  could be proved, but usually is used in conjunction with excluded middle  
elovmporab  none  could be proved, but unused in set.mm  
elovmporab1  none  could be proved  
2mpo0  none  Possibly provable, but an inhabited set version would be more likely to be helpful (if anything is).  
relmptopab  none  Presumably would need a condition that 𝐵 ∈ dom 𝐹  
ofval  ofvalg  
offn  off  the set.mm proof of offn uses ovex and it isn't clear whether anything can be proved with weaker hypotheses than off  
offveq  offeq  
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 , tfindsg2 , tfindes , tfinds2 , tfinds3  tfis3  We are unable to separate limit and successor ordinals using case elimination.  
dfom  dfiom  
findsg  uzind4  findsg presumably could be proved, but there hasn't been a need for it.  
xpexr  none  
xpexr2  xpexr2m  
xpexcnv  none  would be provable if nonempty is changed to inhabited  
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.  
mptmpoopabbrd  none  it should be possible to update iset.mm to reflect set.mm in this area and related theorems  
mptmpoopabovd  none  it should be possible to update iset.mm to reflect set.mm in this area and related theorems  
el2mpocsbcl  none  the set.mm proof uses excluded middle  
el2mpocl  none  the set.mm proof uses el2mpocsbcl  
ovmptss  none  The set.mm proof relies on fvmptss  
mposn  none  presumably provable  
relmpoopab  none  The set.mm proof relies on ovmptss  
mpoxeldm  none  presumably provable  
mpoxneldm  none  presumably provable  
mpoxopynvov0g  none  presumably provable  
mpoxopxnop0  none  presumably provable  
mpoxopx0ov0  none  presumably provable  
mpoxopxprcov0  none  presumably provable  
mpoxopynvov0  none  
mpoxopoveqd  none  unused in set.mm  
brovmpoex  none  unused in set.mm  
sprmpod  none  unused in set.mm  
brtpos  brtposg  
ottpos  ottposg  
ovtpos  ovtposg  
dfcur , dfunc and all theorems using the curry and uncurry syntaxes  none  presumably could be added with only the usual issues around nonempty versus inhabited and the like  
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  
oarec  none  the set.mm proof relies on tfinds3  
oaf1o  none  the set.mm proof uses ontri1 and oawordeu  
oacomf1o , oacomf1olem  none  the set.mm proof relies on oarec and oaf1o  
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  
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 .  
nfixp  nfixpxy, nfixp1  set.mm (indirectly) uses excluded middle to combine the cases where 𝑥 and 𝑦 are distinct and where they are not.  
ixpexg  ixpexgg  
ixpiin  ixpiinm  
ixpint  ixpintm  
ixpn0  ixpm  
undifixp  none  The set.mm proof relies on undif  
resixpfo  none  The set.mm proof relies on membership in 𝐵 being decidable and would need to have nonempty changed to inhabited, but might be adaptable with those conditions added. However, this theorem is currently only used in the proof of Tychonoff's Theorem, which we do not expect to be able to prove.  
boxriin  none  Would seem to need a condition that 𝐼 has decidable equality.  
boxcutc  none  Would seem to need a condition that 𝐴 has decidable equality.  
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  none  Not possible because they would imply onfin2  
onfin2  none  Implies excluded middle as shown as exmidonfin  
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  fimax2gtri  
fimaxg  none  The set.mm proof of fimaxg relies on fimax2g which 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.  
unbnn  none  the impossibility proof at exmidunben should apply here as well  
unbnn2  none  the impossibility proof at exmidunben should apply here as well  
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.  
difinf  difinfinf  
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 any set has decidable equality.  
tpfi  tpfidisj  
fiint  fiintim  
fodomfi  none  Might be provable, for example via ac6sfi or induction directly. The set.mm proof does use undom in addition to induction.  
fofinf1o  none  The set.mm proof uses excluded middle in several places.  
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).  
iunfi  iunfidisj  for a disjoint collection  
in general  Presumably not possible for the same reasons as in unfiexmid  
unifi  none  Presumably the issues are similar to iunfi  
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.  
fisuppfi  preimaf1ofi  The set.mm proof of fisuppfi uses ssfi  
intrnfi  none  presumably not provable; the set.mm proof uses fofi  
iinfi  none  presumably not provable; the set.mm proof uses intrnfi  
inelfi  none  may need a condition such as 𝐴 ≠ 𝐵; the set.mm proof uses prfi  
fiin  none  presumably needs a condition analogous to those in unfidisj or unfiin; the set.mm proof uses unfi  
dffi2  none  the set.mm proof uses fiin and other theorems we do not have  
inficl  none  the set.mm proof uses fiin and dffi2 (see also inelfi which might be relevant)  
fipwuni  none  would need a 𝐴 ∈ V condition but even with that, the set.mm proof uses inficl  
fisn  none  presumably would be provable (with an 𝐴 ∈ V condition added), but the set.mm proof uses inficl  
fipwss  fipwssg  adds the condition that 𝐴 is a set  
elfiun  none  the set.mm proof uses ssfi , fiin , and excluded middle  
dffi3  none  might be possible (perhaps using dffrec notation), but the set.mm proof does not work asis  
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  
axinf , zfinf , axinf2 , axinf  axiinf, zfinf2  probably most of the variations of the axiom of infinity in set.mm could be shown to be equivalent to each other in iset.mm as well  
inf5  none  as this is in terms of proper subset it is unlikely to work well in iset.mm  
elom3 , dfom4 , dfom5  none  the set.mm theorems depend on theorems we do not have  
oancom  none  presumably provable but the set.mm proof does not work asis  
isfinite  fict  
omenps , omensuc  none  presumably provable but the set.mm proofs do not work asis  
infdifsn  none  possibly provable with added ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴DECID 𝑥 = 𝑦 and 𝐵 ∈ 𝐴 conditions, for example via a technique analogous to difinfsn  
infdiffi  none  if we can prove a version of infdifsn it should carry over from singletons to finite sets, much the way difinfinf follows from difinfsn  
unbnn3  none  the impossibility proof at exmidunben should apply here as well  
noinfep  none  the set.mm proof uses fri  
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  Presumably not possible for the same reasons as onfin2  
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.  
undjudom  none  The set.mm proof relies on undom  
dju1dif  none  presumably provable  
mapdjuen  none  the set.mm proof relies on mapunen  
pwdjuen  none  the set.mm proof relies on mapdjuen  
djudom1  none  the set.mm proof relies on undom  
djudom2  none  the set.mm proof relies on djudom1  
djuxpdom  none  presumably provable if having cardinality greater than one is expressed as 2_{o} ≼ 𝐴 instead  
djufi  none  we should be able to prove (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ⊔ 𝐵) ∈ Fin  
cdainflem , djuinf  none  the set.mm proof is not easily adapted  
infdju1  none  the set.mm proof relies on infdifsn  
pwdju1  none  the set.mm proof relies on pwdjuen and pwpw0  
pwdjuidm  none  the set.mm proof relies on infdju1 and pwdju1  
djulepw  none  
onadju  none  the set.mm proof uses oacomf1olem and oarec  
cardadju  none  the set.mm proof uses cardon , onadju , and cardid2  
djunum  none  the set.mm proof uses cardon and cardadju  
unnum  none  the set.mm proof uses djunum , numdom , and undjudom  
nnadju  none  depends on various cardinality theorems we don't have  
ficardun  none  depends on various cardinality theorems we don't have  
ficardun2  none  depends on various cardinality theorems we don't have  
pwsdompw  none  depends on various cardinality theorems we don't have  
unctb  unct  
infdjuabs  none  the set.mm proof uses sbth and other theorems we don't have  
infunabs  none  the set.mm proof uses undjudom and infdjuabs  
infdju  none  the set.mm proof uses sbth and other theorems we don't have  
infdif  none  the set.mm proof uses sbth and other theorems we don't have  
pwdjudom  none  
axcc  cc1  
axcc2  cc2  
axcc3  cc3  
axcc4  cc4  
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).  
dfwun and all weak universe theorems  none  
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  suplocexpr  also see caucvgprpr but completeness cannot be formulated as in set.mm without changes  
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  mappsrprg  
ltpsrpr  ltpsrprg  
map2psrpr  map2psrprg  
supsr  suplocsr  also see caucvgsr  
ax1ne0 , ax1ne0  ax0lt1, ax0lt1, 1ap0, 1ne0  
axrrecex , axrrecex  axprecex, axprecex  
axprelttri , axprelttri  axpreltirr, axpreltwlin, axpreltirr, axpreltwlin  
axpresup , axpresup  axpresuploc, axpresuploc  
axsup  axsuploc  
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  dedekindeu  various details are different including that in dedekindeu the lower and upper cuts have to be open (and thus the real corresponding to the Dedekind cut is not contained in either the lower or upper cut)  
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.  
ltord1 , leord1 , ltord2 , leord2  none  The set.mm proof relies on real number trichotomy.  
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  mul0eqap  Remark 2.19 of [Geuvers] says that (𝐴 · 𝐵) = 0 → (𝐴 = 0 ∨ 𝐵 = 0) 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  
diveq1bd  diveqap1bd  
div2sub , div2subd  div2subap, div2subapd  
subrec , subreci , subrecd  subrecap, subrecapi, subrecapd  
mvllmuld  mvllmulapd  
mvllmuli  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  fimaxq, fimaxre2  When applied to a pair fimaxre 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  none  Presumably provable (with a locatedness condition added) but most likely not as interesting as sup3 in the absence of leloe  
sup3 , sup3ii  none  We won't be able to have the least upper bound property for all inhabited bounded sets, as shown at sup3exmid.  
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  
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  
mul2lt0bi  mul2lt0np, mul2lt0pn  The set.mm proof of the forward direction of mul2lt0bi is not intuitionistic.  
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  xrmax1sup  
xrmax2  xrmax2sup  
xrmin1 , xrmin2  xrmin1inf, xrmin2inf  
xrmaxeq  xrmaxleim  
xrmineq  xrmineqinf  
xrmaxlt  xrmaxltsup  
xrltmin  xrltmininf  
xrmaxle  xrmaxlesup  
xrlemin  xrlemininf  
max0sub , ifle  none  
max1  maxle1  
max2  maxle2  
2resupmax  2zsupmax  for integers  
in general  The set.mm proof uses real trichotomy in an apparently essential way. 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.  
ssfzunsnext  none  Presumably provable using 2zsupmax and similar theorems.  
min1  min1inf  
min2  min2inf  
maxle  maxleastb  
lemin  lemininf  
maxlt  maxltsup  
ltmin  ltmininf  
lemaxle  maxle2  
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  
xmulval  none  The set.mm definition would appear to only function if comparing a real number with zero is decidable (which we will not be able to show in general)  
xnn0xaddcl  none  presumably provable  
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 , xmulcld  none  Although a few of these contain hypotheses that arguments are apart from zero (and thus could be proved with the current definition of ·_{e}), in general extended real multiplication will not work as in set.mm using that definition.  
xrsupss  none  the set.mm proof relies on sup3 which implies excluded middle by sup3exmid  
supxrcl  none  the set.mm proof relies on xrsupss  
infxrcl  none  presumably not provable for all the usual sup3exmid reasons  
ixxub , ixxlb  none  
supicc , supiccub , supicclub , supicclub2  suplociccreex, suplociccex  
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  iooinsup  
icc0  icc0r  
ioorebas  ioorebasg  
ge0xmulcl  none  Relies on xmulcl ; see discussion in this list for that 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  dfseqfrec  
seqval  seq3val  
seqfn  seqf  
seq1 , seq1i  seq31  
seqp1 , seqp1i  seq3p1  
seqm1  seq3m1  
seqcl2  seqf2  seqf2 requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
seqcl  seqf, seq3clss  seqf requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁). This requirement is relaxed somewhat in seq3clss.  
seqfveq2  seq3fveq2  
seqfeq2  seq3feq2  
seqfveq  seq3fveq  
seqfeq  seq3feq  
seqshft2  seq3shft2  
seqres  none  Should be intuitionizable as with the other seq theorems, but unused in set.mm  
sermono  ser3mono  ser3mono requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁) as in sermono .  
seqsplit  seq3split  seq3split requires that 𝐹 be defined on (ℤ_{≥}‘𝐾) not merely (𝐾...𝑁) as in seqsplit . This is not a problem when used on infinite sequences; finite sums may find it easier to use fsumsplit instead.  
seq1p  seq31p  Requires that 𝐹 be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁). This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.  
seqcaopr3  seq3caopr3  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
seqcaopr2  seq3caopr2  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
seqcaopr  seq3caopr  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
seqf1o  seq3f1o  The functions 𝐺 and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁). Also, a single set 𝑆 takes the place of 𝐶 and 𝑆 because that is sufficient flexibility at least for now.  
seradd  ser3add  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
sersub  ser3sub  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
seqid3  seq3id3  
seqid  seq3id  
seqid2  seq3id2  
seqhomo  seq3homo  
seqz  seq3z  The sequence has to be defined on (ℤ_{≥}‘𝑀) not just (𝑀...𝑁)  
seqfeq4  seqfeq3  The sequence has to be defined on (ℤ_{≥}‘𝑀) not just (𝑀...𝑁)  
seqdistr  seq3distr  
serge0  ser3ge0  The sequence has to be defined on (ℤ_{≥}‘𝑀) not just (𝑀...𝑁)  
serle  ser3le  Changes several hypotheses from (𝑀...𝑁) to (ℤ_{≥}‘𝑀)  
ser1const  fsumconst  Finite summation in iset.mm is easier to express using Σ rather than seq directly.  
seqof , seqof2  none  It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet.  
expval  exp3val  The set.mm theorem does not exclude the case of dividing by zero.  
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. For the nonnegative real case see sq11.  
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.  
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  
hashelne0d  none  would be easy to prove if 𝐴 ∈ 𝑉 is changed to 𝐴 ∈ Fin  
hashen1  fihashen1  
hash1elsn  none  would be easy to prove if 𝐴 ∈ 𝑉 is changed to 𝐴 ∈ Fin  
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  none  The set.mm proof uses isocnv3 .  
fz1iso  zfz1iso  The set.mm proof of fz1iso depends on OrdIso. Furthermore, trichotomy rather than weak linearity would seem to be needed.  
ishashinf  none  May be possible with the antecedent changed from ¬ 𝐴 ∈ Fin to ω ≼ 𝐴 but the set.mm proof does not work as is.  
phphashd , phphashrd  none  would appear to need hashclb or some other way of showing that the subset is finite  
seqcoll  seq3coll  The functions 𝐹 and 𝐻 need to be defined on ℤ_{≥}‘𝑀 not just a subset thereof.  
seqcoll2  none  Presumably can be done with modifications similar to seq3coll.  
dfword and all theorems relating to words over a set  none  presumably mostly provable  
seqshft  seq3shft  
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.  
reccn2  reccn2ap  
isershft  iser3shft  
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.  
iseralt  none  The set.mm proof relies on caurcvg2 which does not specify a rate of convergence.  
dfsum  dfsumdc  The iset.mm definition/theorem adds a decidability condition and an if expression (which is to deal with differences in using seq for finite sums). It does function similarity to the set.mm definition of Σ.  
sumex  fsumcl, isumcl  
sumeq2w  sumeq2  Presumably could be proved, and perhaps also would rely only on extensionality (and logical axioms). But unused in set.mm.  
sumeq2ii  sumeq2  
sum2id  none  The set.mm proof does not work asis. Lightly used in set.mm.  
sumfc  sumfct  
fsumcvg  fsum3cvg  
sumrb  sumrbdc  
summo  summodc  
zsum  zsumdc  
fsum  fsum3  
sumz  isumz  
sumss  isumss  
sumss2  isumss2  
fsumcvg2  fsum3cvg2  
fsumsers  fsumsersdc  
fsumcvg3  fsum3cvg3  
fsumser  fsum3ser  
fsummsnunz  none  Could be proved if we added a 𝑍 ∈ V condition, but unused in set.mm.  
isumdivc  isumdivapc  Changes not equal to apart  
sumsplit  sumsplitdc  Adds decidability conditions  
fsumcom2  fisumcom2  Although it is possible that (𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ Fin can be proved from the other hypotheses, the set.mm proof of that uses ssfi .  
fsum0diag  fisum0diag  Adds a 𝑁 ∈ ℤ hypothesis  
fsumrev2  fisumrev2  Adds 𝑀 ∈ ℤ and 𝑁 ∈ ℤ hypotheses  
fsum0diag2  fisum0diag2  Adds a 𝑁 ∈ ℤ hypothesis  
fsumdivc  fsumdivapc  Changes not equal to apart  
fsumless  fsumlessfi  Whether this can be proved without the 𝐶 ∈ Fin condition is unknown but such a proof would be fairly different from the set.mm proof.  
seqabs  fsumabs  Finite sums are more naturally expressed with Σ rather than seq especially in iset.mm. Use fsum3ser as needed.  
cvgcmp  cvgcmp2n  The set.mm proof of cvgcmp relies on caurcvg2 which does not specify a rate of convergence.  
cvgcmpce  none  The proof, and perhaps the statement of the theorem, would need some changes related to the rate of convergence.  
abscvgcvg  none  The set.mm proof relies on cvgcmpce  
climfsum  none  Likely provable, but lightly used in set.mm.  
qshash  none  The set.mm proof will not work asis.  
ackbijnn  none  iset.mm does not have ackbij1  
incexclem , incexc , incexc2  none  A metamath 100 theorem but otherwise unused in set.mm.  
isumless  isumlessdc  Adds a decidability condition on the index set for the sum  
isumsup2 , isumsup  none  Having an upper bound on the partial sums would not suffice; a stronger convergence condition would be needed.  
isumltss  none  Should be provable with the addition of a decidability condition such as the one found in isumss2 and fsum3cvg3.  
climcnds  none  The set.mm proof will not work without modifications.  
divcnvshft  none  The set.mm proof uses ovex to show that 𝐴 / (𝑘 + 𝐵) is a set, even when 𝑘 + 𝐵 might be zero. This could be solved by adding another usage of dfdiv or proving (1 / 0) = ∅ but relying on the value of dividing by zero is not something we usually let ourselves do. Another solution would be to add a 0 < (𝑀 + 𝐵) hypothesis.  
supcvg  none  The set.mm proof uses countable choice and also various supremum theorems proved via excluded middle.  
infcvgaux1i , infcvgaux2i  none  See supcvg entry  
harmonic  none  Should be feasible once we get isumless and climcnds (or similar theorems). A Metamath 100 theorem but otherwise unused in set.mm.  
geoserg  geosergap  Not equal is changed to apart  
geoser  geoserap  Not equal is changed to apart  
pwm1geoser  pwm1geoserap1  Adds a condition that the base is apart from one. The set.mm proof relies on case elimination on whether the base is one or not equal to one.  
geomulcvg  none  The set.mm proof relies on cvgcmpce and expmulnbnd and would appear to also require 𝐴 to be apart from zero.  
cvgrat  cvgratgt0  Adds a 0 < 𝐴 condition which presumably is omitted from the set.mm theorem only for convenience (the theorem isn't interesting unless it holds).  
mertens  mertensabs  Because we don't (yet at least) have abscvgcvg or anything else relating the convergence of a sequence's absolute values to the convergence of the sequence itself, we add the condition that both the sequence 𝐹 and the sequence of its absolute values converge (that is, seq0( + , 𝐹) ∈ dom ⇝ is an additional hypothesis beyond what set.mm has).  
clim2div  clim2divap  
prodfmul  prod3fmul  The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁).  
prodfn0  prodfap0  
prodfrec  prodfrecap  
prodfdiv  prodfdivap  in addition to changing not equal to apart, various hypotheses need to hold for (ℤ_{≥}‘𝑀) not merely (𝑀...𝑁)  
ntrivcvg  ntrivcvgap  
ntrivcvgn0  ntrivcvgap0  
ntrivcvgfvn0  none  To be useful, presumably not equal needs to be changed to apart. This means the set.mm proof does not work and we need another approach (for example, something a bit like seq3p1 or seq3split but for convergence expressed with ⇝ rather than for a finite subsequence).  
ntrivcvgtail  none  the set.mm proof depends on ntrivcvgfvn0 . Would need not equal changed to apart.  
ntrivcvgmullem , ntrivcvgmul  none  the set.mm proof depends on ntrivcvgtail . Would need not equal changed to apart.  
dfprod  dfproddc  Changes not equal to apart, adds a decidability condition for indexing by a set of integers, and passes a more fully defined sequence to seq in the finite case. Should function similarly to the set.mm definition of ∏.  
prodex  none  presumably will need to be replaced by fprodcl and iprodcl analogous to sumex  
prodeq2ii  prodeq2  the set.mm proof uses excluded middle  
prod2id  none  the set.mm proof uses prodeq2ii  
prodrblem  prodrbdclem  
fprodcvg  fproddccvg  
prodrblem2  prodrbdclem2  
prodrb  prodrbdc  
prodmolem3  prodmodclem3  
prodmolem2a  prodmodclem2a  
prodmolem2  prodmodclem2  
prodmo  prodmodc  
zprod  zproddc  
iprod  iprodap  
zprodn0  zprodap0  
iprodn0  iprodap0  
fprod  fprodseq  
eftval  eftvalcn  Adds an easily satisfied condition.  
fprodefsum  none  Presumably feasible once finite products are better developed.  
tanval  tanvalap  
tancl , tancld  tanclap, tanclapd  
tanval2  tanval2ap  
tanval3  tanval3ap  
retancl , retancld  retanclap, retanclapd  
tanneg  tannegap  
sinhval , coshval , resinhcl , rpcoshcl , recoshcl , retanhcl , tanhlt1 , tanhbnd  none yet  should be provable  
tanadd  tanaddap  
sinltx  sin01bnd, sinbnd  Although we can prove the 𝐴 ≤ 1 case (see sin01bnd) or the 1 < 𝐴 case (from sinbnd), set.mm uses real number trichotomy to combine those cases.  
ruc  none  A proof would need either excluded middle or countable choice, per [BauerHanson]  
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 sequence passed to seq, at least as handled in theorems such as seqf, 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  The 𝐹:𝑆⟶𝑆 hypothesis is added (related theorems already have that hypothesis).  
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  
unben  none  not possible as stated, as shown by exmidunben  
isstruct2  isstruct2im, isstruct2r  The difference is the addition of the 𝐹 ∈ 𝑉 condition for the reverse direction.  
isstruct  isstructim, isstructr  The difference is the addition of the 𝐹 ∈ 𝑉 condition for the reverse direction.  
slotfn  slotslfn  
strfvnd  strnfvnd  
strfvn  strnfvn  
strfvss  strfvssn  
setsval  setsvala  
setsidvald  strsetsid  
fsets  none  Apparently would need decidable equality on 𝐴 or some other condition.  
setsdm  none  The set.mm proof relies on undif1  
setsstruct2  none  The set.mm proof relies on setsdm  
setsexstruct2 , setsstruct  none  The set.mm proofs rely on setsstruct2  
setsres  setsresg  
setsabs  setsabsd  
strfvd  strslfvd  
strfv2d  strslfv2d  
strfv2  strslfv2  
strfv  strslfv  
strfv3  strslfv3  
strssd  strslssd  
strss  strslss  
str0  strsl0  
strfvi  none  The set.mm proof uses excluded middle to combine the proper class and set cases.  
setsid  setsslid  
setsnid  setsslnid  
sbcie2s  none  Apparently would require conditions that 𝐴 and 𝐵 are sets.  
sbcie3s  none  Apparently would require conditions that 𝐴, 𝐵, and 𝐶 are sets.  
elbasfv , elbasov , strov2rcl  none  The set.mm proofs rely on excluded middle.  
basprssdmsets  none  The set.mm proof relies on setsdm  
ressval  ressid2, ressval2  For the 𝐵 ⊆ 𝐴 and ¬ 𝐵 ⊆ 𝐴 cases, respectively.  
ressbas  none  Apparently needs to have conditions added, for example that 𝑊 is a set plus one of 𝐵 ⊆ 𝐴 or ¬ 𝐵 ⊆ 𝐴.  
ressbas2 , ressbasss  none  The set.mm proof relies on ressbas .  
resslem , ress0  none  The set.mm proof relies on excluded middle.  
ressinbas  none  Apparently needs to have conditions added, for example that 𝑊 is a set plus one of 𝐵 ⊆ 𝐴 or ¬ 𝐵 ⊆ 𝐴.  
ressval3d  none  The set.mm proof relies on setsidvald and sspss .  
ressress  none  The set.mm proof relies on ressinbas and excluded middle.  
ressabs  none  The set.mm proof relies on ressress but at first glance this would appear to be feasible given the 𝐵 ⊆ 𝐴 condition.  
strle1  strle1g  
strle2  strle2g  
strle3  strle3g  
1strstr  1strstrg  
2strstr  2strstrg  
2strbas  2strbasg  
2strop  2stropg  
2strstr1  2strstr1g  
2strbas1  2strbas1g  
2strop1  2strop1g  
grpstr  grpstrg  
grpbase  grpbaseg  
grpplusg  grpplusgg  
ressplusg  none  The set.mm proof relies on resslem  
grpbasex , grpplusgx  grpbaseg, grpplusgg  Marked as discouraged even in set.mm.  
rngstr  rngstrg  
rngbase  rngbaseg  
rngplusg  rngplusgg  
rngmulr  rngmulrg  
ressmulr , ressstarv  none  The set.mm proof relies on resslem  
srngstr  srngstrd  
srngbase  srngbased  
srngplusg  srngplusgd  
srngmulr  srngmulrd  
srnginvl  srnginvld  
lmodstr  lmodstrd  
lmodbase  lmodbased  
lmodplusg  lmodplusgd  
lmodsca  lmodscad  
lmodvsca  lmodvscad  
ipsstr  ipsstrd  
ipsbase  ipsbased  
ipsaddg  ipsaddgd  
ipsmulr  ipsmulrd  
ipssca  ipsscad  
ipsvsca  ipsvscad  
ipsip  ipsipd  
resssca , ressvsca , ressip  none  The set.mm proof relies on resslem  
phlstr , phlbase , phlplusg , phlsca , phlvsca , phlip  none  Intuitionizing these will be straightforward once we get around to it, in a manner similar to lmodstrd. The proofs will use theorems like strle1g, strleund, and opelstrsl.  
topgrpstr  topgrpstrd  
topgrpbas  topgrpbasd  
topgrpplusg  topgrpplusgd  
topgrptset  topgrptsetd  
resstset  none  The set.mm proof relies on resslem  
otpsstr , otpsbas , otpstset , otpsle  none  Unused in set.mm. If we want to develop this more we may need to figure out whether to define order in terms of < or ≤ as the relationship between those may be different without excluded middle.  
0rest  none  Might need a 𝐴 ∈ V condition added, and this theorem seems to be mostly be used in conjunction with excluded middle.  
topnval  topnvalg  
topnid  topnidg  
topnpropd  topnpropgd  
prdsbasex  none  Would need some conditions on whether 𝑅 is a function, on set existence, or the like. However, it is unused in set.mm.  
imasvalstr , prdsvalstr , prdsvallem , prdsval , prdssca , prdsbas , prdsplusg , prdsmulr , prdsvsca , prdsip , prdsle , prdsless , prdsds , prdsdsfn , prdstset , prdshom , prdsco , prdsbas2 , prdsbasmpt , prdsbasfn , prdsbasprj , prdsplusgval , prdsplusgfval , prdsmulrval , prdsmulrfval , prdsleval , prdsdsval , prdsvscaval , prdsvscafval , prdsbas3 , prdsbasmpt2 , prdsbascl , prdsdsval2 , prdsdsval3 , pwsval , pwsbas , pwselbasb , pwselbas , pwsplusgval , pwsmulrval , pwsle , pwsleval , pwsvscafval , pwsvscaval , pwssca , pwsdiagel , pwssnf1o  none  At a minimum, these theorems would need new set existence conditions and other routine intuitionizing. At worst, they would need a bigger revamp for things like how order works.  
dfordt , dfxrs , and all theorems involving ordTop or RR*s  none  The set.mm definitions would not seem to fit with constructive definitions of these concepts (for example, the if in dfxrs would apparently needed to be expressed in terms of a suitable maximum and perhaps other changes are needed too)  
dfqtop , dfimas , dfqus and all theorems defined in terms of quotient topology, image structure, and quotient ring.  none  presumably could be added in some form  
dfxps and all theorems mentioning the binary product on a structure (syntax Xs.)  none  The set.mm definition depends on dfimas ( "s ) and dfprds ( Xs_ ). By its nature the definition of the binary product considers every structure slot (including most notably order which presumably will need to be handled differently in iset.mm).  
dfmre , dfmrc and all theorems using the Moore or mrCls syntax  none  The closest we have currently is dfcls but even that doesn't function as it does in set.mm (because complements are different without excluded middle).  
dfcnfld and all theorems using CCfld  none  Could presumably be defined in some form, but we'd have to look at the literature definitions of a constructive field and see how we'd need to define this. Plus questions about whether to define order in terms of < or ≤.  
istop2g  istopfin  
iinopn  none  The set.mm proof relies on abrexfi  
riinopn  none  The set.mm proof relies on iinopn (the other issues in the set.mm proof could apparently be handled by fin0or).  
rintopn  none  The set.mm proof relies on riinopn  
toponsspwpw  toponsspwpwg  
toprntopon  none  Presumably could be proved but the set.mm proof does not work as it is.  
topsn  none  The set.mm proof relies on pwsn  
tpsprop2d  none  The set.mm proof does not work asis. Unused in set.mm  
basdif0  none  The set.mm proof relies on undif1  
0top  none  The set.mm proof relies on sssn  
en2top  none  The set.mm proof relies on strict dominance  
2basgen  2basgeng  
tgdif0  none  The set.mm proof relies on excluded middle  
indistopon  none  The set.mm proof relies on sspr  
indistop , indisuni  none  The set.mm proof relies on indistopon  
fctop  none  The set.mm proof relies on theorems we don't have including con1d , ssfi , unfi , rexnal , and difindi .  
fctop2  none  The set.mm proof relies on fctop  
cctop  none  The set.mm proof relies on theorems we don't have including con1d , rexnal , and difindi .  
ppttop , pptbas  none  The set.mm proof relies on theorems we don't have including orrd and ianor  
indistpsx , indistps , indistps2 , indistpsALT , indistps2ALT  none  The set.mm proofs rely on indiscrete topology theorems we don't have  
isopn2  none  The set.mm proof relies on dfss4  
opncld  none  The set.mm proof relies on isopn2  
iincld  none  The set.mm proof relies on opncld  
intcld  none  The set.mm proof relies on iincld  
incld  none  The set.mm proof relies on intcld  
riincld  none  The set.mm proof relies on iincld , incld , and case elimination  
clscld  none  The set.mm proof relies on intcld  
clsf  none  The set.mm proof relies on clscld  
clsval2  none  The set.mm proof relies on dfss4 and opncld  
ntrval2  none  The set.mm proof relies on dfss4 and clsval2  
ntrdif , clsdif  none  
cmclsopn  none  The set.mm proof relies on dfss4 and clsval2  
cmntrcld  none  The set.mm proof relies on opncld  
iscld3 , iscld4  none  
clsidm  none  The set.mm proof relies on clscld  
0ntr  none  The set.mm proof relies on ssdif0  
elcls , elcls2  none  
clsndisj  none  The set.mm proof relies on elcls  
elcls3  none  The set.mm proof relies on elcls  
opncldf1 , opncldf2 , opncldf3  none  The set.mm proofs rely on dfss4 and opncld  
isclo  none  One direction of the biconditional may be provable by taking the set.mm proof and replacing undif with undifss  
isclo2  none  The set.mm proof relies on isclo  
indiscld  none  Something along these lines may be possible once we define the indiscrete topology  
neips  neipsm  
neindisj  none  The set.mm proof relies on clsndisj  
opnnei  none  Apparently the set.mm proof could easily be adapted for the case in which 𝑆 is inhabited  
neindisj2  none  The set.mm proof relies on elcls  
neipeltop , neiptopuni , neiptoptop , neiptopnei , neiptopreu  none  The set.mm proofs rely on several theorems we do not have.  
dflp and all theorems using the limPt syntax  none  
dfperf and all theorems using the Perf syntax  none  
restbas  restbasg  
restsn2  none  The set.mm proof relies on topsn  
restcld  none  The set.mm proof relies on opncld  
restcldi  none  The set.mm proof relies on restcld  
restcldr  none  The set.mm proof relies on restcld  
restfpw  none  The set.mm proof relies on ssfi  
neitr  none  The set.mm proof relies on inundif  
restcls  none  The set.mm proof relies on clscld  
restntr  none  The set.mm proof relies on excluded middle  
resstopn  none  The set.mm proof relies on resstset  
resstps  none  The set.mm proof relies on resstopn  
lmrel  lmreltop  
iscnp2  iscnp  
cnptop1 , cnptop2  none  
cnprcl  cnprcl2k  
cnpf , cnpcl  cnpf2  
cnprcl2  cnprcl2k  
cnpimaex  icnpimaex  
cnpco  cnptopco  
iscncl  none  The set.mm proof relies on opncld  
cncls2i  none  The set.mm proof relies on clscld  
cnclsi  none  The set.mm proof relies on cncls2i  
cncls2  none  The set.mm proof relies on cncls2i and iscncl  
cncls  none  The set.mm proof relies on cncls2 and cnclsi  
cncnp2  cncnp2m  
cnpresti  cnptopresti  
cnprest  cnptoprest  
cnprest2  cnptoprest2  
cnindis  none  The set.mm proof relies on indiscrete topology theorems that we don't have.  
paste  none  The set.mm proof relies on restcldr  
lmcls , lmcld  none  The set.mm proof relies on elcls  
lmcnp  lmtopcnp  
dfcmp and all compactness (syntax Comp) theorems  none  How compactness fares without excluded middle is a complicated topic. See for example [HoTT], section 11.5.  
dfhaus and all Hausdorff (syntax Haus) theorems  none  Perhaps there would need to be an apartness relation to replace the use of negated equality.  
dfconn and all connected toplogy (syntax Conn) theorems  none  would apparently need a lot of changes to work  
df1stc and all firstcountable theorems  none  Worth considering the definition of countable seen in theorems such as ctm and finct, as well as whatever else might come up.  
df2ndc and all secondcountable theorems  none  Worth considering the definition of countable seen in theorems such as ctm and finct, as well as whatever else might come up.  
dflly and all theorems using the Locally syntax  none  
dfxko and all theorems using the compactopen topology syntax (^ko)  none  not clear what is possible here  
ptval  none  This would need more extensive development of theorems related to the Xt_ syntax (not just dfpt itself).  
ptpjpre1  none  Perhaps would be provable in the case where 𝐴 has decidable equality.  
elpt , elptr , elptr2 , ptbasid , ptuni2 , ptbasin , ptbasin2 , ptbas , ptpjpre2 , ptbasfi , pttop , ptopn , ptopn2  none  Although some parts of these product topology theorems may be intuitionizable, it isn't clear doing so would produce a set of theorems which function as desired.  
txcld  none  The set.mm proof relies on difxp  
txcls  none  The set.mm proof relies on txcld  
txcnpi  none  Should be provable (via icnpimaex and cnpf2) but may need an additional 𝐿 ∈ Top hypothesis.  
ptcld  none  The set.mm proof depends on pttop , boxcutc , ptopn2 , and riincld  
dfac14  none  The left hand side implies excluded middle by acexmid; we could see whether the proof that the right hand side implies choice is also valid without excluded middle.  
txindis  none  The set.mm proof relies on excluded middle, indistop , and indisuni .  
dfhmph and all theorems using that syntax  none  presumably would need some modifications to the parts which use set difference  
hmeofval  hmeofvalg  
hmeocls  none  the set.mm proof uses cncls2i  
hmeoqtop  none  relies on qTop syntax  
pt1hmeo  none  the set.mm proof uses ptcn  
ptuncnv , ptunhmeo  none  the set.mm proofs use ptuni  
xmetrtri2  none  Presumably this or something similar could be defined once we define RR*s ( dfxrs ) or something along those lines.  
xmetgt0 , metgt0  xmeteq0, meteq0  Presumably would require defining apartness on 𝑋 or something along those lines.  
xbln0  xblm  
blin  blininf  
setsmsbas  setsmsbasg  
setsmsds  setsmsdsg  
setsmstset  setsmstsetg  
setsmstopn , setsxms , setsms , tmsval , tmslem , tmsbas , tmsds , tmstopn , tmsxms , tmsms  none  Presumably could prove these or similar theorems, analogous to setsmsbasg  
blcld  none  The set.mm proof relies on xrltnle  
blcls  none  The set.mm proof relies on blcld  
blsscls  none  The set.mm proof relies on blcls  
stdbdmetval  bdmetval  
stdbdxmet  bdxmet  
stdbdmet  bdmet  
stdbdbl  bdbl  
stdbdmopn  bdmopn  
ressxms , ressms  none  Awaits revision of dfress as described at Clean up multifunction restriction operator for extensible structures in iset.mm  
prdsxms , prdsms  none  This would need more extensive development of theorems related to the Xs_ syntax (not just dfprds itself).  
pwsxms , pwsms  none  This would need more extensive development of theorems related to the ^s syntax (not just dfpws itself).  
tmsxps  xmetxp  tmsxps relies on structure products and related theorems  
tmsxpsmopn  xmettx  tmsxpsmopn relies on structure products and related theorems  
dscmet , dscopn  none  The set.mm definition for the discrete metric, and the proofs, would seem to rely on equality being decidable.  
qtopbaslem  qtopbasss  
iooretop  iooretopg  
icccld , icopnfcld , iocmnfcld , qdensere  none  depend on various closed set theorems  
cnfldtopn  none  if we use (MetOpen‘(abs ∘ − )) as our notation for the topology of the complex numbers, this theorem is not needed  
cnfldtopon  cntoptopon  
cnfldtop  cntoptop  
unicntop  unicntopcntop  
cnopn  cnopncntop  
qdensere2  none  the set.mm proof depends on qdensere  
blcvx  none  presumably provable for either the 𝑇 = 0 case or the 𝑇 ∈ (0(,]1) case; set.mm uses excluded middle to combine those two cases  
tgioo2  tgioo2cntop  
rerest  rerestcntop  
tgioo3  none  Until we have defined RRfld (presumably closely related to the issues described at the dfcnfld entry here), we can use (topGen‘ran (,)) as a notation for the topology of the real numbers (as seen at tgioo2cntop).  
zcld  none  the set.mm proof uses the floor function in ways that we are unlikely to be able to intuitionize  
iccntr  none  the set.mm proof uses real number trichotomy in many steps  
opnreen  none  the set.mm proof is not usable asis but it would be interesting to see if some portions can be adapted  
rectbntr0  none  the set.mm proof relies on various theorems we do not have  
xmetdcn2  none  the set.mm theorem is defined in terms of the RR*s syntax  
xmetdcn  none  the set.mm theorem is defined in terms of the ordTop syntax and uses xmetdcn2 in the proof  
metdcn2  none  the set.mm proof relies on xmetdcn  
metdcn  none  the set.mm proof relies on metdcn2  
msdcn  none  the set.mm proof relies on metdcn2  
cnmpt1ds  none  the set.mm proof relies on msdcn  
cnmpt2ds  none  the set.mm proof relies on msdcn  
abscn  abscn2, abscncf  presumably provable (expressing the topology of the complex numbers as (MetOpen‘(abs ∘ − )) if iset.mm doesn't have CCfld yet).  
metdsval  none  the set.mm proof uses infex  
metdsf  none  the set.mm proof uses infxrcl  
addcnlem  addcncntoplem  expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))  
addcn  addcncntop  expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))  
subcn  subcncntop  expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))  
mulcn  mulcncntop  expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))  
divcn  divcnap  
fsumcn  fsumcncntop  
fsum2cn  none  the set.mm proof uses fsumcn  
expcn  none  the set.mm proof uses mulcn  
divccn  none  Not equal would need to be changed to apart. Also, the set.mm proof uses mulcn  
sqcn  none  the set.mm proof uses expcn  
divccncf  divccncfap  
cncfcn  cncfcncntop  
cncfcn1  cncfcn1cntop  
cncfmpt2f  cncfmpt2fcntop  
cncfmpt2ss  none  would apparently only need a change to the notation for the topology on the complex numbers  
cdivcncf  cdivcncfap  
cnmpopc  none  this kind of piecewise definition would apparently rely on real number trichotomy or something similar  
cnrehmeo  cnrehmeocntop  
ivth  ivthinc  
ivth2  ivthdec  
ivthle2  ivthdec  the set.mm proof uses leloe  
dflimc  dflimced  dflimced is adapted from ellimc3 in set.mm  
dfdv  dfdvap  The definition is adjusted for the notation of the topology on the complex numbers, and for apartness versus negated equality.  
dfdvn and all theorems mentioning iterated derivative (Dn)  none  should be easily intuitionizable  
dfcpn and all theorems mentioning times continuously differentiable functions (C^n)  none  should be easily intuitionizable  
reldv  reldvg  
limcvallem , limcfval , ellimc  none  rely on decidability of real number equality  
ellimc3  ellimc3apf, ellimc3ap  
limcdif  limcdifap  changes not equal to apart and adds 𝐴 ⊆ ℂ hypothesis  
ellimc2  none  Presumably provable with not equal changed to apart. If iset.mm doesn't have CCfld yet, use (MetOpen‘(abs ∘ − )) for the topology of the complex numbers (see cnfldtopn in set.mm).  
limcmo  limcimo  
limcmpt  limcmpted  
limcmpt2  none  
limcres  none  Although this would appear to be provable, it might benefit from some additional theorems which help us manipulate ↾_{t} and metric spaces. If iset.mm doesn't have CCfld yet, use (MetOpen‘(abs ∘ − )) for the topology of the complex numbers (see cnfldtopn in set.mm). Proof sketch: because interiors are open, we can form a ball around 𝐵 which is contained in ((int‘𝐽)‘(𝐶 ∪ {𝐵})) which gives us the delta we need to apply ellimc3ap for (𝐹 lim_{ℂ} 𝐵) (given that we can apply ellimc3ap for ((𝐹 ↾ 𝐶) lim_{ℂ} 𝐵) when working within 𝐶).  
cnplimc  cnplimccntop  
limccnp  limccnpcntop  
limccnp2  limccnp2cntop  
limcco  limccoap  limccoap is only usable in the case where 𝑥 # 𝑋 implies R(x) # 𝐶 so it is less general than limcco  
limciun  none  The set.mm proof relies on fofi , rintopn and ellimc2 .  
limcun  none  The set.mm proof relies on limciun .  
dvlem  dvlemap  not equal is changed to apart  
dvfval  dvfvalap  changes not equal to apart and changes the notation for the topology on the complex numbers  
eldv  eldvap  changes not equal to apart and changes the notation for the topology on the complex numbers  
dvbssntr  dvbssntrcntop  changes the notation for the topology on the complex numbers  
dvbsss  dvbsssg  
dvfg  dvfgg  
dvf  dvfpm  
dvfcn  dvfcnpm  
dvres  none  The set.mm proof relies on restntr and limcres . It may be worth seeing if it is easier to prove the 𝑆 ∈ {ℝ, ℂ} case.  
dvres2  none  The set.mm proof relies on restntr  
dvres3  none  The set.mm proof relies on dvres2  
dvres3a  none  The set.mm proof relies on dvres2  
dvidlem  dvidlemap  
dvcnp  none  would appear to rely on decidable equality of real numbers  
dvcnp2  dvcnp2cntop  
dvaddbr  dvaddxxbr  dvaddbr allows 𝑋 and 𝑌 to be different and uses excluded middle when handling that possibility.  
dvmulbr  dvmulxxbr  
dvadd  dvaddxx  
dvmul  dvmulxx  
dvaddf  dviaddf  
dvmulf  dvimulf  
dvcmul  none  unused in set.mm and the set.mm proof depends on dvres2  
dvcmulf  none  the set.mm proof depends on dvres , dvres3 , and caofid2  
dvcobr  dvcoapbr  dvcoapbr adds a 𝑢 # 𝐶 → (𝐺‘𝑢) # (𝐺‘𝐶) condition  
dvco  none  the set.mm proof depends on dvcobr  
dvcof  none  the set.mm proof depends on dvcobr and dvco  
dvrec  dvrecap  
dvmptres3  none  the set.mm proof depends on dvres3a  
dvmptid  dvmptidcn  the version for real numbers would presumably be provable as well  
dvmptc  dvmptccn  the version for real numbers would presumably be provable as well  
dvmptcl  dvmptclx  adds a 𝑋 ⊆ 𝑆 hypothesis  
dvmptadd  dvmptaddx  adds a 𝑋 ⊆ 𝑆 hypothesis  
dvmptmul  dvmptmulx  adds a 𝑋 ⊆ 𝑆 hypothesis  
dvmptres2  none  the set.mm proof uses dvres  
dvmptres  none  the set.mm proof uses dvmptres2  
dvmptcmul  dvmptcmulcn  dvmptcmulcn is the case where both 𝑋 and 𝑆 are ℂ itself rather than subsets. The set.mm proof of dvmptcmul uses dvmptres2 .  
dvmptdivc  none  the set.mm proof uses dvmptcmul  
dvmptneg  dvmptnegcn  dvmptnegcn is for ℂ rather than a subset thereof  
dvmptsub  dvmptsubcn  dvmptsubcn is for ℂ rather than a subset thereof  
dvmptcj  dvmptcjx  adds a 𝑋 ⊆ 𝑆 hypothesis  
dvmptre  none  Presumably needs a 𝑋 ⊆ ℝ condition added. Also, the set.mm proof relies on dvmptcmul (with 𝑆 set to ℝ).  
dvmptim  none  Presumably needs a 𝑋 ⊆ ℝ condition added. Also, the set.mm proof relies on dvmptcmul (with 𝑆 set to ℝ).  
dvmptntr  none  the set.mm proof uses dvres  
dvmptco  none  the set.mm proof uses dvcof  
dvrecg  none  the set.mm proof uses dvmptco  
dvmptdiv  none  the set.mm proof uses dvrecg  
dvmptfsum  none  the set.mm proof uses dvmptc and dvmptres  
dvcnvlem , dvcnv  none  Not equal would need to change to apart and notation for the topology on the complex numbers would change. More seriously, the set.mm proof uses limcco . Changing to limccoap may be possible given a condition along the lines of ∀𝑥 ∈ 𝑋∀𝑦 ∈ 𝑋(𝑥 # 𝑦 ↔ (𝐹‘𝑥) # (𝐹‘𝑦).  
dvexp3  none  the set.mm proof uses dvmptres and dvmptco  
dvle  none  the set.mm proof uses iccntr , dvmptntr , dvmptsub , and dvge0  
dvcnvre  none  the set.mm proof depends on compactness ( icccmp and cncfcnvcn ), restntr , evthicc2 , dvres , iccntr , and dvne0  
efcvx  none  the set.mm proof uses dvres , dvres3 , iccntr , and dvcvx  
reefgim  none  
pilem2  pilem3  our proof of pilem3 is different enough from set.mm that it doesn't need to go via pilem2  
tanabsge  none  the set.mm proof uses real number trichotomy  
sinq12ge0  none  the set.mm proof uses leloe  
cosq14ge0  none  the set.mm proof uses sinq12ge0  
pige3ALT  pige3  the set.mm proof uses various theorems we do not have  
sineq0  none  the set.mm proof uses various theorems not in iset.mm  
coseq1  none  the set.mm proof uses sineq0  
efeq1  none  the set.mm proof uses sineq0  
cosne0  none  the set.mm proof uses sineq0  
cosord  cosordlem, cos11  presumably provable but the set.mm proof uses real number trichotomy  
sinord  none  the set.mm proof depends on cosord  
recosf1o  ioocosf1o  the set.mm proof of recosf1o relies on ivthle2  
resinf1o  none  the set.mm proof relies on recosf1o  
tanord1  none  the set.mm proof relies on ltord1  
tanord  none  the set.mm proof relies on tanord1 , real number trichotomy, and ltord1  
tanregt0  none  the set.mm proof relies on cosne0 , rpcoshcl , rptanhcl , and tanhbnd  
efgh  none  depends on SubGrp and CCfld  
efif1o  none  depends on complex square root  
efifo  none  depends on efif1o  
eff1o , efabl , efsubm , circgrp , circsubm  none  
dflog  dfrelog  
dfcxp  dfrpcxp  we only define the power function for a positive real base for reasons described in the dfrelog comment  
logrn , ellogrn , dflog2  none  see dfrelog comment for discussion of complex logarithms  
relogrn  none  Should be provable given reeff1o but perhaps it is better to avoid the theorems involving ran log from set.mm because they would mean something different with dfrelog than with the set.mm definition.  
logrncn , eff1o2 , logf1o  none  see dfrelog comment for discussion of complex logarithms  
logrncl  none  see dfrelog comment for discussion of complex logarithms  
logcl  relogcl  
logimcl  none  see dfrelog comment for discussion of complex logarithms  
logcld  relogcld  
logimcld , logimclad , abslogimle , logrnaddcl  none  see dfrelog comment for discussion of complex logarithms  
eflog  reeflog  
logeq0im1  none  see dfrelog comment for discussion of complex logarithms  
logccne0  logrpap0  
logne0  logrpap0  would be provable but logrpap0 changes not equal to apart and will generally be more helpful)  
logef  relogef  
logeftb  relogeftb  
logneg , logm1 , lognegb  none  See dfrelog comment for discussion of complex logarithms (including logarithms on negative reals, since iset.mm only defines the logarithm on ℝ^{+}).  
explog  reexplog  
relog  none  see dfrelog comment for discussion of complex logarithms  
reloggim  none  may be possible if more group theorems and notation are available  
logfac  none  Should be provable. Because of the way seqhomo is used in the set.mm proof, it may be necessary to specialcase 𝑁 = 1 and start the main proof with two, or prove an analogue of seq3homo which allows using ℝ^{+} on one side of the equation and ℝ on the other.  
eflogeq  none  see dfrelog comment for discussion of complex logarithms  
logcj , efiarg , cosargd , cosarg0d , argregt0 , argrege0 , argimgt0 , argimlt0 , logimul , logneg2 , logmul2 , logdiv2 , abslogle , tanarg  none  see dfrelog comment for discussion of complex logarithms  
logdivlt  none  the set.mm proof uses real number trichotomy  
logdivle  none  the set.mm proof uses logdivlt  
dvrelog  none  the set.mm proof uses dvres3 and dvcnvre  
relogcn  none  the set.mm proof uses dvrelog  
ellogdm , logdmn0 , logdmnrp , logdmss , logcnlem2 , logcnlem3 , logcnlem4 , logcnlem5 , logcn , dvloglem , logdmopn , logf1o2 , dvlog , dvlog2lem , dvlog2  none  see dfrelog comment for discussion of complex logarithms  
advlog  none  the set.mm proof uses dvmptid , dvmptres , dvrelog , dvmptc , and dvmptsub  
advlogexp  none  the set.mm proof uses various derivative theorems not present in iset.mm  
efopn  none  the set.mm proof makes use of the complex logarithm  
logtayl , logtaylsum , logtayl2  none  see dfrelog comment for discussion of complex logarithms  
logccv  none  the set.mm proof uses dvrelog , dvmptneg , dvmptres2 , dvcvx , and soisoi  
cxpval , cxpef , cxpefd  rpcxpef  as described at dfrpcxp we only support positive real bases  
0cxp , 0cxpd  none  as described at dfrpcxp we only support positive real bases  
cxpexpz , cxpexp , cxpexpzd  cxpexpnn, cxpexprp  as described at dfrpcxp we only support positive real bases  
cxp0 , cxp0d  rpcxp0, rpcxp0d  as described at dfrpcxp we only support positive real bases  
cxp1 , cxp1d  rpcxp1, rpcxp1d  as described at dfrpcxp we only support positive real bases  
cxpcl , cxpcld  rpcncxpcl, rpcncxpcld  as described at dfrpcxp we only support positive real bases  
recxpcl , recxpcld  rpcxpcl  as described at dfrpcxp we only support positive real bases  
cxpne0 , cxpne0d  cxpap0  the base must be a positive real and the result changes not equal to apart  
cxpeq0  none  since we do not support a mantissa of zero, does not apply  
cxpadd , cxpaddd  rpcxpadd  
cxpp1 , cxpp1d  rpcxpp1  
cxpneg , cxpnegd  rpcxpneg  
cxpsub , cxpsubd  rpcxpsub  
cxpge0 , cxpge0d  rpcxpcl  we only support positive real bases  
mulcxp , mulcxpd  rpmulcxp  
divcxp , divcxpd  rpdivcxp  
cxpmul2 , cxpmul2d  cxpmul plus cxpexprp  
cxproot  rpcxproot  
cxpmul2z , cxpmul2zd  cxpmul plus cxpexprp  
abscxp2  abscxp  
cxplea , cxplead  none  the set.mm proof uses leloe  
cxple2 , cxple2d  rpcxple2  
cxplt2 , cxplt2d  rpcxplt2  
cxple2a , cxple2ad  none  the set.mm proof uses leloe  
cxpsqrt  rpcxpsqrt  
cxpsqrtth  rpcxpsqrtth  
dvcxp1  none  the set.mm proof uses dvrelog , dvmptco , and dvmptres3  
dvcxp2  none  the set.mm proof uses dvmptco  
dvsqrt  none  the set.mm proof uses dvcxp1  
dvcncxp1  none  this is for complex bases, see dvcxp1 entry concerning a positive real base  
dvcnsqrt  none  see dfrsqrt comment for discussion of complex square roots  
cxpcn  none  as described at dfrpcxp we only support positive real bases  
cxpcn2  none  presumably provable; the obvious proof would be via relogcn  
cxpcn3  none  as described at dfrpcxp we only support positive real bases  
resqrtcn  none  the set.mm proof is in terms of the complex exponential, but this theorem should be provable one way or another  
sqrtcn  none  see dfrsqrt comment for discussion of complex square roots  
cxpaddle  none  the set.mm proof relies on leloe and other theorems we do not have  
abscxpbnd  rpabscxpbnd  
root1id , root1eq1 , root1cj , cxpeq  none  as described at dfrpcxp we only support positive real bases  
loglesqrt  none  presumably provable, but the set.mm proof relies on dvmptc , dvmptres , dvrelog , dvmptco , dvle , and relogcn  
logrec  none  see dfrelog comment for discussion of complex logarithms  
logbval  rplogbval  
logbcl  rplogbcl  
logbid1  rplogbid1  
logb1  rplogb1  
elogb  rpelogb  
logbchbase  rplogbchbase  
relogbcl  rplogbcl  
relogbreexp  rplogbreexp  
relogbzexp  rplogbzexp  
relogbmul  rprelogbmul  
relogbmulexp  rprelogbmulexp  
relogbdiv  rprelogbdiv  
relogbexp  relogbexpap  
relogbcxp  rplogbcxp  
cxplogb  rpcxplogb  
relogbcxpb  relogbcxpbap  
logbmpt , logbf , logbfval , relogbf , logblog  none  we could add a version of these if iset.mm gets the curry syntax  
irrdiff  apdiff 
This
page was last updated on 15Aug2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 