Home - Intuitionistic Logic Explorer

Created by Mario Carneiro

Intuitionistic Logic Proof Explorer

Intuitionistic Logic (Wikipedia [accessed 19-Jul-2015], Stanford Encyclopedia of Philosophy [accessed 19-Jul-2015]) 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 Overview of intuitionistic logic Overview of this work The axioms Some theorems How to intuitionize classical proofs Metamath Proof Explorer cross reference Bibliography

Related pages Table of Contents and Theorem List Most Recent Proofs (this mirror) (latest) Bibliographic Cross-Reference Definition List ASCII Equivalents for Text-Only Browsers Metamath database iset.mm (ASCII file) External links GitHub repository [accessed 06-Jan-2018]

Overview of intuitionistic logic

(Placeholder for future use)

Overview of this work

(By Gérard Lang, 7-May-2018)

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 6 first (ax-ia1, ax-ia2, ax-ia3, ax-io, ax-in1 and ax-in2), when added to ax-1, ax-2 and ax-mp, allow for the development of intuitionistic propositional logic. We omit the classical axiom ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) (which is ax-3 in set.mm). Each of our new axioms is a theorem of classical propositional logic, but ax-3 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 (ax-ial, ax-i5r, ax-ie1 and ax-ie2) together with the set.mm axioms ax-4, ax-5, ax-7 and ax-gen do not mention equality or distinct variables.

The ax-i9 axiom is just a slight variation of the classical ax-9. The classical axiom ax-12 is strengthened into first ax-i12 and then ax-bnd (two results which would be fairly readily equivalent to ax-12 classically but which do not follow from ax-12, at least not in an obvious way, in intuitionistic logic). The substitution of ax-i9, ax-i12, and ax-bnd for ax-9 and ax-12 and the inclusion of ax-8, ax-10, ax-11, ax-13, ax-14 and ax-17 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 ax-3, 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.

The axioms

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.

Axioms of intuitionistic propositional calculus

Axiom Simp	ax-1	⊢ (φ → (ψ → φ))
Axiom Frege	ax-2	⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
Rule of Modus Ponens	ax-mp	|- ph   &   |- ph -> ps   ⇒   |- ps
Left 'and' elimination	ax-ia1	|- ((ph /\ ps) -> ph)
Right 'and' elimination	ax-ia2	⊢ ((φ ∧ ψ) → ψ)
'And' introduction	ax-ia3	⊢ (φ → (ψ → (φ ∧ ψ)))
Definition of 'or'	ax-io	⊢ (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ)))
'Not' introduction	ax-in1	⊢ ((φ → ¬ φ) → ¬ φ)
'Not' elimination	ax-in2	⊢ (¬ φ → (φ → ψ))

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 ax-in1 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 df-bi.

Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (for-all) and ∃ (there-exists). 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.

Axioms of intuitionistic predicate logic

Axiom of Specialization	ax-4	⊢ (∀xφ → φ)
Axiom of Quantified Implication	ax-5	⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))
The converse of ax-5o	ax-i5r	⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ψ))
Axiom of Quantifier Commutation	ax-7	⊢ (∀x∀yφ → ∀y∀xφ)
Rule of Generalization	ax-gen	⊢ φ   =>    ⊢ ∀xφ
x is bound in ∀xφ	ax-ial	⊢ (∀xφ → ∀x∀xφ)
x is bound in ∃xφ	ax-ie1	⊢ (∃xφ → ∀x∃xφ)
Define existential quantification	ax-ie2	⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))
Axiom of Equality	ax-8	⊢ (x = y → (x = z → y = z))
Axiom of Existence	ax-i9	⊢ ∃x x = y
Axiom of Quantifier Substitution	ax-10	⊢ (∀x x = y → ∀y y = x)
Axiom of Variable Substitution	ax-11	⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
Axiom of Quantifier Introduction	ax-i12	⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
Axiom of Bundling	ax-bnd	⊢ (∀z z = x ∨ (∀z z = y ∨ ∀x∀z(x = y → ∀z x = y)))
Left Membership Equality	ax-13	⊢ (x = y → (x ∈ z → y ∈ z))
Right Membership Equality	ax-14	⊢ (x = y → (z ∈ x → z ∈ y))
Distinctness	ax-17	⊢ (φ → ∀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 e. 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.

Intuitionistic Zermelo-Fraenkel Set Theory (IZF)

Axiom of Extensionality	ax-ext	⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y)
Axiom of Collection	ax-coll	⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)
Axiom of Separation	ax-sep	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ))
Axiom of Power Sets	ax-pow	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
Axiom of Pairing	ax-pr	⊢ ∃z∀w((w = x ∨ w = y) → w ∈ z)
Axiom of Union	ax-un	⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y)
Axiom of Set Induction	ax-setind	⊢ (∀𝑎(∀y ∈ 𝑎 [y / 𝑎]φ → φ) → ∀𝑎φ)
Axiom of Infinity	ax-iinf	⊢ ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x))

We develop set theory based on the Intuitionistic Zermelo-Fraenkel (IZF) system, mostly following the IZF axioms as laid out in [Crosilla]. Constructive Zermelo-Fraenkel (CZF), also described in Crosilla, is not as easy to formalize in metamath because the Axiom of Restricted Separation would require us to develop the ability to classify formulas as bounded formulas, similar to the machinery we have built up for asserting on whether variables are free in formulas.

A Theorem Sampler   

From a psychological point of view, learning constructive mathematics is agonizing, for it requires one to first unlearn certain deeply ingrained intuitions and habits acquired during classical mathematical training.
—Andrej Bauer

Listed here are some examples of starting points for your journey through the maze. Some are stated just as they would be in a non-constructive 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 Cross-Reference useful.

Propositional calculus

Law of identity

Praeclarum theorema

Contraposition introduction

Double negation introduction

Triple negation

Definition of exclusive or

Negation and the false constant

Predicate calculus

Existential and universal quantifier swap

Existentially quantified implication

x = x

Definition of proper substitution

Double existential uniqueness

Set theory

Commutative law for union

A basic relationship between class and wff variables

Two ways of saying "is a set"

The ZF axiom of foundation implies excluded middle

Russell's paradox

Ordinal trichotomy implies excluded middle

Mathematical (finite) induction

Peano's postulates for arithmetic: 1 2 3 4 5

Two natural numbers are either equal or not equal (a special case of the law of the excluded middle which we can prove).

A natural number is either zero or a successor

The axiom of choice implies excluded middle

Burali-Forti paradox

Transfinite induction

Closure law for ordinal addition

Real and complex numbers

Properties of apartness: 1 2 3 4

How to intuitionize classical proofs   

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.

• If you see case elimination ( pm2.61 or its variants) you'll probably end up with two theorems for the two cases. In particular, if the cases were A e. _V and -. A e. _V you probably just care about the A e. _V case.
• Non-empty almost always needs to be changed to inhabited (those terms are defined at n0rf).
• If the original proof relied on propositional/predicate logic which isn't a theorem of intuitionistic logic, maybe there is a way of expressing the logic more directly. This is perhaps the hardest one to put in cookbook form: you might need to try some things and see if anything works.
• If the original proof relied on df-ex so that it could prove a theorem for A. and then get E. for free (or vice versa), instead go look at the original proof and try to come up the analogues to each step for the other quantifier (for example, cbvrexcsf, sbcrext, rexxpf). Similarly, if you have a theorem for <_ and are trying to prove the corresponding theorem for < you'll probably need to use analogous steps rather than negation (examples: leaddsub, ltsub1, ltsub2).
• If you are dealing with a definition, try to find the best constructive definition from the literature ([HoTT] book, Stanford Encyclopedia of Philosophy, [Bauer], etc). Once you pick a definition, that'll affect the proofs which rely on that definition.
• If there is case elimination on whether variables are distinct, most of the time you just need the variant with distinct variables. Sometimes you can then remove the constraint with a temporary variable (e.g. the various sbco2* variants, nfralya, r19.3rm).
• Sometimes one direction of a biconditional holds, or subset holds instead of equality. You might be able to keep the easy direction and worry about the other one later.
• If there is case elimination sometimes only one of the two cases is possible. For example, in mosubopt the rest of the formula being proved constrains which case matters.
• If you need an additional condition (for example, because the original proof used case elimination) and you are proving a biconditional, consider whether both sides of the biconditional imply the condition. If so, you'll be able to prove the biconditional with that condition as an antecedent, and then use pm5.21nii or one of its variants to remove the antecedent (example: elxp4).
• If your proof relies on dveeq2 try dveeq2or and likewise for the other things downstream of ax-i12 or ax-bnd.
• If you have a disjunction, be reluctant to turn it into an implication using ord and the like. Instead, show that each disjunct implies what you are trying to prove and use jaoi to join those two implications into something which can hook up to the disjunction.
• Disjunctive syllogism holds in intuitionistic logic and we state it a few ways (for example orel1 and ecased) but we don't have a wide variety of convenience theorems. Unless we add those, you'll use ord or something similar followed by mpd or something similar. This may add a few steps but they are straightforward ones.
• If your proof is doing tricky things perhaps in the interest of shortness, try just expanding the definitions and applying logic in a straightforward way. See if this gets you a working (although perhaps longer) proof.
• If your proof relies on a biconditional in set.mm which isn't in iset.mm, see if one direction is in iset.mm and see which direction your proof is using. For example 19.35-1 or exnalim.
• If you are doing things with inhabited classes (beyond just applying existing inhabited class theorems), you may be able to dig up some predicate logic you haven't used in a while (e.g. raaan).
• Consider the possibility of giving up. Some things just won't have intuitionistic proofs. The more it looks like excluded middle or other non-intuitionistic statements, the more likely you are dealing with one of these. But it can be hard to have good intuition about this. In some cases it may be possible to ask "can I use this statement to prove ph \/ -. ph for an arbitrary proposition" (see ordtriexmid for example ), but this is not always an easy technique to apply.
• Switching between 2th and 2false might help (e.g. dfnul2, dfnul3, rab0).
• In many cases statements which are equivalent in classical logic become several non-equivalent statements (e.g. exclusive or, ordinals, non-empty versus inhabited, apartness versus negated equality). This is usually a good place to look for a literature reference, but don't be afraid to change the statement being proved to "what you really meant is X" as appropriate.
• If a statement has multiple equivalences in set.mm (e.g. mo2 and mo3 , or dffun2 and dffun3 ) and only some of them in iset.mm, sometimes a pretty similar proof will work (that is, which one to use in the original proof may have been a fairly arbitrary choice).
• A number of theorems related to functions (especially ovex and fvex ) in set.mm perform case elimination based on whether we are evaluating the function within its domain or outside it. The most straightforward solution is to use fnovex or funfvex which only work within the domain. Using these may involve rearranging logic, for example by changing rexlimivw to rexlimdva (example: ovelrn or indeed most uses of fnovex and funfvex). If a function value is inhabited, we know we are evaluating it within its domain by relelfvdm.
• With excluded middle, (/) e. A and A =/= (/) are equivalent (where A is an ordinal). In such theorems, (/) e. A is generally the more interesting condition constructively.
• Reverse closure in set.mm uses excluded middle (for example ovrcl or ndmfvrcl ). The most general way to handle this is to add more conditions that we are evaluating operations within their domains (for example set.mm's addasspi versus iset.mm's addasspig in which conditions such as A e. N. are added, or set.mm's ltbtwnnq versus iset.mm's ltbtwnnqq, in which E.x is changed to E.x e. Q.). If the result of applying a function is inhabited, then we know we applied it within its domain - that is relelfvdm or elmpt2cl may be useful.
• With excluded middle not equal ( =/=) and apart (#) are equivalent. When working with real and complex numbers, apartness is almost always what you want. See df-ap for more on apartness.
• Exclusive or (ph \/_ ps) is equivalent to ph <-> -. ps given excluded middle but we just have one direction (xorbin). Consider intuitionizing ph <-> -. ps as ph \/_ ps (example: rpnegap).
• If you get stuck, ask! (for example in a GitHub issue or on the mailing list). We have a number of contributors who have experience in constructive mathematics in general, or iset.mm in particular, and one of the best things about doing/learning mathematics in metamath is the collaborative nature of how we develop it.

Metamath Proof Explorer cross reference   

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
ax-3 , con4d , con34b , necon4bd	con3	The form of contraposition which removes negation does not hold in intutionistic logic.
pm2.18	pm2.01	See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.
pm2.18d	pm2.01d	See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.
notnotrd , notnotri , notnot2 , notnot	notnot1	Double negation introduction holds but not double negation elimination.
mt3d	mtod
nyl2	nsyl
pm2.61 , pm2.61d , pm2.61d1 , pm2.61d2 , pm2.61i , pm2.61ii , pm2.61nii , pm2.61iii , pm2.61ian , pm2.61dan , pm2.61ddan , pm2.61dda , pm2.61ine , pm2.61ne , pm2.61dne , pm2.61dane , pm2.61da2ne , pm2.61da3ne , pm2.61iine	none
impcon4bid, con4bid, notbi, con1bii, con4bii, con2bii	con3, condc
xor3 , nbbn	xorbin, xornbi, xor3dc, nbbndc
biass	biassdc
df-or , pm4.64 , pm2.54 , orri , orrd	pm2.53, ori, ord
pm4.63	pm3.2im
iman	imanim
annim	annimim
oran	oranim
ianor	pm3.14
biluk	bilukdc
ecase3d	none	This is a form of case elimination.
dedlem0b	dedlemb
3ianor	3ianorr
df-ex	exalim
alex	alexim
exnal	exnalim
alexn	alexnim
exanali	exanaliim
19.35	19.35-1
19.30	none
19.36	19.36-1
19.37	19.37-1
19.32	19.32r
19.31	19.31r
exdistrf	exdistrfor
exmo	exmonim
mo2	mo2r, mo3
nne	nner, nnedc
exmidne	dcne
neor	pm2.53, ori, ord
neorian	pm3.14
nnel	none	The reverse direction could be proved; the forward direction is double negation elimination.
nfrald	nfraldxy, nfraldya
rexnal	rexnalim
rexanali	none
nrexralim	none
dfral2	ralexim
dfrex2	rexalim
nfrexd	nfrexdxy, nfrexdya
nfral	nfralxy, nfralya
nfra2	nfra1, nfralya
nfrex	nfrexxy, nfrexya
r19.30	none
r19.35	r19.35-1
ralcom2	ralcom
sspss	sspssr
n0f	n0rf
n0	n0r
neq0	neq0r
reximdva0	reximdva0m
rabn0	rabn0m, rabn0r
ssdif0	ssdif0im
inssdif0	inssdif0im
undif2	undif2ss
uneqdifeq	uneqdifeqim
r19.45zv	r19.45mv
dfif2	df-if
ifsb	none
dfif4	none	Unused in set.mm
dfif5	none	Unused in set.mm
ifnot	none
ifan	none
ifor	none
ifeq1da, ifeq2da	none
ifclda	none
ifeqda	none
elimif , ifbothda , ifboth , ifid , eqif , ifval , elif , ifel , ifcl , ifcld , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD	none
dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel , ifex , ifexg	none	Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
iundif2	iundif2ss
trintss	trintssm
trint0	trint0m
csbexg , csbex	csbexga, csbexa	set.mm uses case elimination to remove the A e. _V condition.
intabs	none	Lightly used in set.mm, and the set.mm proof is not intuitionistic
moabex	euabex	In general, most of the set.mm E! theorems still hold, but a decent number of the E* ones get caught up on "there are two cases: the set exists or it does not"
snex	snexg, snex	The iset.mm version of snex has an additional hypothesis
opex	opexg, opex	The iset.mm version of opex has additional hypotheses
df-so	df-iso	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 om
	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.
df-fr and all theorems using Fr	none	Right now iset.mm does not have a well-founded predicate (Fr in set.mm). This means that various theorems (involving ordinals, especially) require the Axiom of Set Induction ax-setind (the IZF equivalent to the Axiom of Foundation/Regularity in ZF), where the set.mm proofs of those theorems do not. Presumably if we were to add Fr we'd define it as being inductive, that is, a property that satisfies the epsilon (or R) induction principle is always true. For example: R Fr A <-> A. s(A.x(A.y(y Rx -> y e. s) -> x e. s) -> A C_ s) This definition has some problems when A is a proper class. As such, ax-setind has to be stated as a schema instead: A.x(A.y(y e. x -> y e. S) -> x e. S) -> S = _V There are two ways to say no infinite descending sequence, using E.-. or -. A., which are not intuitionistically equivalent. Furthermore there are some trivial commutations that are not intuitionistically valid. So I think that makes the following definition possibilities: R Fr A <-> A. s(A.x(A.y(y Rx -> y e. s) -> x e. s) -> A C_ s) R Fr2 A <-> A. s( s C_ A -> (A.x e. sE.y e. sy Rx -> s = (/))) R Fr3 A <-> A. s( s C_ A -> (E.xx e. s -> E.x e. sA.y e. s-. y Rx)) The set.mm definition is roughly Fr3 (but it uses nonempty in place of inhabited). We can probably just focus on the first definition, but ideally we'd prove it in set.mm (to show that given excluded middle it is equivalent to the definition of Fr in set.mm). If we adopted well-foundedness along these lines, we'd be able to add well-foundedness to the definition of an ordinal and prove many of the ordinal theorems without ax-setind. The proof of ordirr would be similar to the current proof of elirr except that ax-setind would be replaced by _E Fr A and _V throughout the elirr proof would be replaced by A. Likewise for en2lp. These theorems (for ordinals) would then not rely on ax-setind.
df-we (and all theorems using We)	none	Ordering is moderately different in constructive logic, so if there is anything along these lines worth doing it will be different from set.mm.
tz7.7	none
ordelssne	none
ordelpss	none
ordsseleq	onelss, eqimss	Taken together, onelss and eqimss represent the reverse direction of the biconditional from ordsseleq
ordtri3or	nntri3or	Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid.
ordtri2	nntri2	ordtri2 for all ordinals presumably implies excluded middle although we don't have a specific proof analogous to ordtriexmid.
ordtri3 , ordtri4 , ordtri2or2 , ordtri2or3 , dford2	none	Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid. We don't have similar proofs for every variation of of trichotomy but most of them are presumably powerful enough to imply excluded middle.
ordtri1 , ontri1 , onssneli , onssnel2i	ssnel, nntri1	ssnel is a trichotomy-like theorem which does hold, although it is an implication whereas ordtri1 is a biconditional. nntri1 is biconditional, but just for natural numbers.
ordtr2 , ontr2	none	See also ordelpss in set.mm
ordtr3	none	This is weak linearity of ordinals, which presumably implies excluded middle by ordsoexmid.
ordtri2or	none	Implies excluded middle as shown at ordtri2orexmid.
ord0eln0 , on0eln0	ne0i, nn0eln0
nsuceq0	nsuceq0g
ordsssuc	trsucss
ordequn	none	If you know which ordinal is larger, you can achieve a similar result via theorems such as oneluni or ssequn1.
ordun	onun2
dmxpid	dmxpm
relimasn	imasng
opswap	opswapg
cnvso	cnvsom
iotaex	iotacl, euiotaex
dffun3	dffun5r
dffun5	dffun5r
fvex	funfvex	when evaluating a function within its domain
	fvexg, fvex	when the function is a set and is evaluated at a set
	relrnfvex	when evaluating a relation whose range is a set
	mptfvex	when the function is defined via maps-to, yields a set for all inputs, and is evaluated at a set
	1stexg, 2ndexg	for the functions 1st and 2nd
ndmfv	ndmfvg	The -. A e. _V case is fvprc.
elfvdm	relelfvdm
elfvex	relelfvdm
f0cli	ffvelrn
funiunfv	fniunfv, funiunfvdm
funiunfvf	funiunfvdmf
eluniima	eluniimadm
riotaex	riotacl, riotaexg
nfriotad	nfriotadxy
csbriota , csbriotagOLD	csbriotag
riotaxfrd	none	Although it may be intuitionizable, it is lightly used in set.mm.
ovex	fnovex	when the operation is a function evaluated within its domain.
	fvexg, fvex	when the operation is a set and is evaluated at a set
	relrnfvex	when the operation is a relation whose range is a set
	mpt2fvex	When the operation is defined via maps-to, yields a set on any inputs, and is being evaluated at two sets.
fnov	fnovim
ov3	ovi3	Although set.mm's ov3 could be proved, it is only used a few places in set.mm, and in iset.mm those places need the modified form found in ovi3.
oprssdm	none
ndmovg , ndmov	ndmfvg	These theorems are generally used in set.mm for case elimination which is why we just have the general ndmfvg rather than an operation-specific version.
ndmovcl , ndmovcom , ndmovass , ndmovdistr , ndmovord , and ndmovordi	none	These theorems are generally used in set.mm for case elimination and the most straightforward way to avoid them is to add conditions that we are evaluating functions within their domains.
ndmovrcl	elmpt2cl, relelfvdm
caov4	caov4d	Note that caov4d has a closure hypothesis.
caov411	caov411d	Note that caov411d has a closure hypothesis.
caov42	caov42d	Note that caov42d has a closure hypothesis.
caovdir	caovdird	caovdird adds some constraints about where the operations are evaluated.
caovdilem	caovdilemd
caovlem2	caovlem2d
caovmo	caovimo
ofval	fnofval
offn , offveq , caofid0l , caofid0r , caofid1 , caofid2	none	Assuming we really need to add conditions that the operations are functions being evaluated within their domains, there would be a fair bit of intuitionizing.
ordeleqon	none
ssonprc	none	not provable (we conjecture), but interesting enough to intuitionize anyway. U.A = On -> A e/ V is provable, and (B e. On /\ U.A C_ B) -> A e. V is provable. (Why isn't df-pss stated so that the set difference is inhabited? If so, you could prove U.A C. On -> A e. V.)
onint	none	Conjectured to not be provable without excluded middle. If you apply onint to a pair you can derive totality of the order.
onint0	none	Thought to be "trivially not intuitionistic", and it is not clear if there is an alternate way to state it that is true. If the empty set is in A then of course |^| A = (/), but the converse seems difficult. I don't know so much about the structure of the ordinals without linearity,
onssmin, onminesb, onminsb	none	Conjectured to not be provable without excluded middle, for the same reason as onint.
oninton	none yet	This one (with non-empty changed to inhabited) I think can still be salvaged though. From the fact that it is inhabited you get that it exists, and is a subset of an ordinal x. It is an intersection of transitive sets so it is transitive, and of course all its members are members of x so they are transitive too. And E. Fr A falls to subsets.
onintrab, onintrab2	none yet	The set.mm proof uses oninton.
oneqmin	none	Falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.
onminex	none yet	falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.
onmindif2	none	Conjectured to not be provable without excluded middle.
onmindif2	none	Conjectured to not be provable without excluded middle.
ordpwsuc	ordpwsucss	See the ordpwsucss comment for discussion of the succcessor-like properites of ( ~PA i^i On). Full ordpwsuc implies excluded middle as seen at ordpwsucexmid.
ordsucelsuc	onsucelsucr, nnsucelsuc	The converse of onsucelsucr implies excluded middle, as shown at onsucelsucexmid.
ordsucsssuc	onsucsssucr, nnsucsssuc	The converse of onsucsssucr implies excluded middle, as shown at onsucsssucexmid.
ordsucuniel	sucunielr	Full ordsucuniel implies excluded middle, as shown at ordsucunielexmid.
ordsucun	none yet	Conjectured to be provable in the reverse direction, but not the forward direction (implies some order totality).
ordunpr	none	Presumably not provable without excluded middle.
ordunel	none	Conjectured to not be provable (ordunel implies ordsucun).
onsucuni, ordsucuni	none	Conjectured to not be provable without excluded middle.
orduniorsuc	none	Presumably not provable.
ordunisuc	onunisuci, unisuc, unisucg
orduniss2	onuniss2
onsucuni2	none yet	Conjectured to be provable.
0elsuc	none yet	Conjectured to be provable.
onuniorsuci	none	Conjectured to not be provable without excluded middle.
onuninsuci, ordununsuc	none	Conjectured to be provable in the forward direction but not the reverse one.
onsucssi	none yet	Conjectured to be provable.
nlimsucg	none yet	Conjectured to be provable.
ordunisuc2	ordunisuc2r	The forward direction is conjectured to imply excluded middle. Here is a sketch of the proposed proof. Let om' be the set of all finite iterations of suc' A = ( ~PA i^i On) on (/). (We can formalize this proof but not until we have om and at least finite induction.) Then om' = U. om' because if x e. om' then x = suc'^n (/) for some n, and then x C_ suc'^n (/) implies x e. suc'^(n+1) (/) e. om' so x e. U. om'. Now supposing the theorem, we know that A. x e. om' suc x e. om', so in particular 2o e. om', that is, 2o = suc'^n (/) for some n. (Note that 1o = suc' (/) - see pw0.) For n = 0 and n = 1 this is clearly false, and for n = m+3 we have 1o e. suc' suc' (/) , so 2o C_ suc' suc' (/), so 2o e. suc' suc' suc' (/) C_ suc' suc' suc' suc'^m (/) = 2o, contradicting ordirr. Thus 2o = suc' suc' (/) = suc' 1o. Applying this to X = {x e. { (/) } | ph } we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ordtriexmidlem2 for X = (/) and rabsnt as seen in the onsucsssucexmid proof for X = 1o).
ordzsl, onzsl, dflim3, nlimon	none
dflim4	df-ilim	We conjecture that dflim4 is not equivalent to df-ilim.
limsuc	none yet	Conjectured to be provable.
limsssuc	none yet	Conjectured to be provable.
tfinds	tfis3
findsg	uzind4	findsg presumably could be proved, but there hasn't been a need for it.
xpexr2	xpexr2m
1stval	1stvalg
2ndval	2ndvalg
1stnpr	none	May be intuitionizable, but very lightly used in set.mm.
2ndnpr	none	May be intuitionizable, but very lightly used in set.mm.
brtpos	brtposg
ottpos	ottposg
ovtpos	ovtposg
pwuninel	pwuninel2	The set.mm proof of pwuninel uses case elimination.
iunonOLD	iunon
smofvon2	smofvon2dm
tfr1	tfri1
tfr2	tfri2
tfr3	tfri3
tfr2b , recsfnon , recsval	none	These transfinite recursion theorems are lightly used in set.mm.
df-rdg	df-irdg	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. "Set-theoretic principles incompatible with intuitionistic logic", "we can still define many of the familiar set-theoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit."
rdgfnon	rdgifnon
ordge1n0	ordge1n0im, ordgt0ge1
ondif1	dif1o	In set.mm, ondif1 is used for Cantor Normal Form
ondif2 , dif20el	none	The set.mm proof is not intuitionistic
brwitnlem	none	The set.mm proof is not intuitionistic
om0r	om0, nnm0r
om00	nnm00
om00el	none
suc11reg	suc11g
frfnom	frecfnom	frecfnom adopts the frec notation and adds conditions on the characteristic function and initial value.
fr0g	frec0g	frec0g adopts the frec notation and adds a condition on the characteristic function.
frsuc	frecsuc	frecsuc adopts the frec notation and adds conditions on the characteristic function and initial value.
om0x	om0
oaord1	none yet
oaword	oawordi	The other direction presumably could be proven but isn't yet.
omwordi	nnmword	The set.mm proof of omwordi relies on case elimination.
omword1	nnmword
nnawordex	nnaordex	nnawordex is only used a few places in set.mm
swoso	none	Unused in set.mm.
ecdmn0	ecdmn0m
erdisj, qsdisj, qsdisj2, uniinqs	none	These could presumably be restated to be provable, but they are lightly used in set.mm
xpider	xpiderm
iiner	iinerm
riiner	riinerm
brecop2	none	This is a form of reverse closure and uses excluded middle in its proof.
erov , erov2	none	Unused in set.mm.
eceqoveq	none	Unused in set.mm.
df-sdom , relsdom , brsdom , dfdom2 , sdomdom , sdomnen , brdom2 , bren2 , domdifsn	none	Many aspects of strict dominance as developed in set.mm rely on excluded middle and a different definition would be needed if we wanted strict dominance to have the expected properties.
en1b	en1bg
mapsnen , map1 , pw2f1olem , pw2f1o , pw2eng , pw2en	none	We have not added set exponentiation to iset.mm yet.
snfi	snfig
difsnen	none	The set.mm proof uses excluded middle.
undom	none	The set.mm proof uses undif2 and we just have undif2ss
xpdom3	xpdom3m
domunsncan	none	The set.mm proof relies on difsnen
omxpenlem , omxpen , omf1o	none	The set.mm proof relies on omwordi
enfixsn	none	The set.mm proof relies on difsnen
sbth and its lemmas, sbthb , sbthcl	none	The Schroeder-Bernstein Theorem implies excluded middle
2pwuninel	2pwuninelg
onomeneq , onfin , onfin2	none	The set.mm proofs rely on excluded middle
nndomo	none	Should be provable but the set.mm proof wouldn't work
nnsdomo , sucdom2 , sucdom , 0sdom1dom , 1sdom2 , sdom1	none	iset.mm doesn't yet have strict dominance
modom , modom2	none	The set.mm proofs rely on excluded middle
1sdom , unxpdom , unxpdom2 , sucxpdom	none	iset.mm doesn't yet have strict dominance
pssinf	none	The set.mm proof relies on sdomnen
fisseneq	none	The set.mm proof relies on excluded middle
ominf	none	Although this theorem presumably could be proved, it would probably need a very different proof than the set.mm one
isinf	none	The set.mm proof uses the converse of ssdif0im
fineqv	none	The set.mm proof relies on theorems we don't have, and even for the theorems we do have, we'd need to carefully look at what axioms they rely on.
pssnn	none	The set.mm proof uses excluded middle.
ssnnfi	none	The proof in ssfiexmid would apply to this as well as to ssfi , since { (/) } e. om
ssfi	ssfiexmid
domfi	none	The set.mm proof is in terms of ssfi
xpfir	none	Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi
infi	none	Presumably the proof of ssfiexmid could be adapted to show this implies excluded middle
rabfi	none	Presumably the proof of ssfiexmid could be adapted to show this implies excluded middle
finresfin	none	The set.mm proof is in terms of ssfi
f1finf1o	none	The set.mm proof is not intuitionistic
nfielex	none	The set.mm proof relies on neq0
en1eqsn , en1eqsnbi	none	The set.mm proof relies on fisseneq
diffi	none	The set.mm proof is in terms of ssfi
dif1en	none	The set.mm proof relies on diffi
ax-reg , axreg2 , zfregcl	ax-setind	ax-reg implies excluded middle as seen at regexmid
addcompi	addcompig
addasspi	addasspig
mulcompi	mulcompig
mulasspi	mulasspig
distrpi	distrpig
addcanpi	addcanpig
mulcanpi	mulcanpig
addnidpi	addnidpig
ltapi	ltapig
ltmpi	ltmpig
nlt1pi	nlt1pig
df-nq	df-nqqs
df-nq	df-nqqs
df-erq	none	Not needed given df-nqqs
df-plq	df-plqqs
df-mq	df-mqqs
df-1nq	df-1nqqs
df-ltnq	df-ltnqqs
elpqn	none	Not needed given df-nqqs
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
df-np	df-inp
df-1p	df-i1p
df-plp	df-iplp
df-ltp	df-iltp
elnp , elnpi	elinp
prn0	prml, prmu
prpssnq	prssnql, prssnqu
elprnq	elprnql, elprnqu
prcdnq	prcdnql, prcunqu
prub	prubl
prnmax	prnmaxl
npomex	none
prnmadd	prnmaddl
genpv	genipv
genpcd	genpcdl
genpnmax	genprndl
ltrnq	ltrnqg, ltrnqi
genpcl	addclpr, mulclpr
genpass	genpassg
addclprlem1	addnqprllem, addnqprulem
addclprlem2	addnqprl, addnqpru
plpv	plpvlu
mpv	mpvlu
mulclprlem	mulnqprl, mulnqpru
addcompr	addcomprg
addasspr	addassprg
mulcompr	mulcomprg
mulasspr	mulassprg
distrlem1pr	distrlem1prl, distrlem1pru
distrlem4pr	distrlem4prl, distrlem4pru
distrlem5pr	distrlem5prl, distrlem5pru
distrpr	distrprg
ltprord	ltprordil	There hasn't yet been a need to investigate versions which are biconditional or which involve proper subsets.
psslinpr	ltsopr
prlem934	prarloc2
ltaddpr2	ltaddpr
ltexprlem1 , ltexprlem2 , ltexprlem3 , ltexprlem4	none	See the lemmas for ltexpri generally.
ltexprlem5	ltexprlempr
ltexprlem6	ltexprlemfl, ltexprlemfu
ltexprlem7	ltexprlemrl, ltexprlemru
ltapr	ltaprg
addcanpr	addcanprg
prlem936	prmuloc2
reclem2pr	recexprlempr
reclem3pr	recexprlem1ssl, recexprlem1ssu
reclem4pr	recexprlemss1l, recexprlemss1u, recexprlemex
supexpr , suplem1pr , suplem2pr	none	The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.
mulcmpblnrlem	mulcmpblnrlemg
ltsrpr	ltsrprg
dmaddsr , dmmulsr	none	Although these presumably could be proved in a way similar to dmaddpq and dmmulpq (in fact dmaddpqlem would seem to be easily generalizable to anything of the form (( S X. T) /. R)), we haven't yet had a need to do so.
addcomsr	addcomsrg
addasssr	addasssrg
mulcomsr	mulcomsrg
mulasssr	mulasssrg
distrsr	distrsrg
ltasr	ltasrg
sqgt0sr	mulgt0sr, apsqgt0
recexsr	recexsrlem	This would follow from sqgt0sr (as in the set.mm proof of recexsr), but "not equal to zero" would need to be changed to "apart from zero".
mappsrpr , ltpsrpr , map2psrpr	none	Although variants of these theorems could be intuitionized, in set.mm they are only used for supremum theorems, so we can consider this in more detail when we tackle what kind of supremum theorems to prove.
supsrlem , supsr	none	The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.
axaddf , ax-addf , axmulf , ax-mulf	none	Because these are described as deprecated in set.mm, we haven't figured out what would be involved in proving them for iset.mm.
ax1ne0 , ax-1ne0	ax0lt1, ax-0lt1, 1ap0, 1ne0
axrrecex , ax-rrecex	axprecex, ax-precex
axpre-lttri , ax-pre-lttri	axpre-ltirr, axpre-ltwlin, ax-pre-ltirr, ax-pre-ltwlin
axpre-sup , ax-pre-sup , axsup	none yet	The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. If we want a set of axioms for real numbers which allows us to avoid construction-dependent theorems beyond this point, we'll need a modified Least Upper Bound property, a statement concerning Dedekind cuts or something similar, or some other axiom(s).
elimne0	none	Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
xrltnle	xrlenlt
ssxr	df-xr	Lightly used in set.mm
ltnle , ltnlei , ltnled	lenlt, zltnle
lttri2 , lttri4	ztri3or	Real number trichotomy is not provable.
leloe , eqlelt , leloei , leloed , eqleltd	none
leltne , leltned	none
ltneOLD	ltne
letric , letrii , letrid	zletric
ltlen , ltleni , ltlend	ltleap, zltlen
ne0gt0	none	We presumably could prove this if we changed "not equal to zero" to "apart from zero".
lecasei , ltlecasei	none	These are real number trichotomy
lelttric	zlelttric
lttri2i	none	This can be read as "two real numbers are non-equal if and only if they are apart" which relies on excluded middle
ne0gt0d , lttrid , lttri2d , lttri4d	none	These are real number trichotomy
dedekind , dedekindle	none
mul02lem1	none	The one use in set.mm is not needed in iset.mm.
negex	negcl
msqgt0 , msqgt0i , msqgt0d	apsqgt0	"Not equal to zero" is changed to "apart from zero"
relin01	none	Relies on real number trichotomy.
ltordlem , ltord1 , leord1 , eqord1 , ltord2 , leord2 , eqord2	none	These depend on real number trichotomy and are not used until later in set.mm.
wloglei , wlogle	none	These depend on real number trichotomy and are not used until later in set.mm.
recex	recexap	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
mulcand, mulcan2d	mulcanapd, mulcanap2d	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
mulcanad , mulcan2ad	mulcanapad, mulcanap2ad	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
mulcan , mulcan2 , mulcani	mulcanap, mulcanap2, mulcanapi	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
mul0or , mul0ori , mul0ord	none	Remark 2.19 of [Geuvers] says that this does not hold in general and has a counterexample.
mulne0b , mulne0bd , mulne0bad , mulne0bbd	mulap0b, mulap0bd, mulap0bad, mulap0bbd
mulne0 , mulne0i , mulne0d	mulap0, mulap0i, mulap0d
receu	receuap	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
mulnzcnopr	none
msq0i , msq0d	none	This probably could be proved in terms of tightness of apartness and A # 0 /\ B # 0 -> (A x. B) # 0, but is unused in set.mm.
mulcan1g , mulcan2g	various cancellation theorems	Presumably this is unavailable for the same reason that mul0or is unavailable.
1div0	none	This could be proved, but the set.mm proof does not work as-is.
divval	divvalap	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
divmul , divmul2 , divmul3	divmulap, divmulap2, divmulap3	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
divcl , reccl	divclap, recclap	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
divcan1 , divcan2	divcanap1, divcanap2	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
diveq0	diveqap0	In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
divne0b , divne0	divap0b, divap0
recne0	recap0
recid , recid2	recidap, recidap2
divrec	divrecap
divrec2	divrecap2
divass	divassap
div23 , div32 , div13 , div12	div23ap, div32ap, div13ap, div12ap
divdir , divcan3 , divcan4	divdirap, divcanap3, divcanap4
div11 , divid , div0	div11ap, dividap, div0ap
diveq1 , divneg , divsubdir	diveqap1, divnegap, divsubdirap
recrec , rec11 , rec11r	recrecap, rec11ap, rec11rap
divmuldiv , divdivdiv , divcan5	divmuldivap, divdivdivap, divcanap5
divmul13 , divmul24 , divmuleq	divmul13ap, divmul24ap, divmuleqap
recdiv , divcan6 , divdiv32 , divcan7	recdivap, divcanap6, divdiv32ap, divcanap7
dmdcan , divdiv1 , divdiv2 , recdiv2	dmdcanap, divdivap1, divdivap2, recdivap2
ddcan , divadddiv , divsubdiv	ddcanap, divadddivap, divsubdivap
ddcan , divadddiv , divsubdiv	ddcanap, divadddivap, divsubdivap
conjmul , rereccl, redivcl	conjmulap, rerecclap, redivclap
div2neg , divneg2	div2negap, divneg2ap
recclzi , recne0zi , recidzi	recclapzi, recap0apzi, recidapzi
reccli , recidi , recreci	recclapi, recidapi, recrecapi
dividi , div0i	dividapi, div0api
divclzi , divcan1zi , divcan2zi	divclapzi, divcanap1zi, divcanap2zi
divreczi , divcan3zi , divcan4zi	divrecapzi, divcanap3zi, divcanap4zi
rec11i , rec11ii	rec11api, rec11apii
divcli , divcan2i , divcan1i , divreci , divcan3i , divcan4i	divclapi, divcanap2i, divcanap1i, divrecapi, divcanap3i, divcanap4i
div0i	divap0i
divasszi , divmulzi , divdirzi , divdiv23zi	divassapzi, divmulapzi, divdirapzi, divdiv23apzi
divmuli , divdiv32i	divmulapi, divdiv32api
divassi , divdiri , div23i , div11i	divassapi, divdirapi, div23api, div11api
divmuldivi, divmul13i, divadddivi, divdivdivi	divmuldivapi, divmul13api, divadddivapi, divdivdivapi
rerecclzi , rereccli , redivclzi , redivcli	rerecclapzi, rerecclapi, redivclapzi, redivclapi
reccld , rec0d , recidd , recid2d , recrecd , dividd , div0d	recclapd, recap0d, recidapd, recidap2d, recrecapd, dividapd, div0apd
divcld , divcan1d , divcan2d , divrecd , divrec2d , divcan3d , divcan4d	divclapd, divcanap1d, divcanap2d, divrecapd, divrecap2d, divcanap3d, divcanap4d
diveq0d , diveq1d , diveq1ad , diveq0ad , divne1d , div0bd , divnegd , divneg2d , div2negd	diveqap0d, diveqap1d, diveqap1ad, diveqap0ad, divap1d, divap0bd, divnegapd, divneg2apd, div2negapd
divne0d , recdivd , recdiv2d , divcan6d , ddcand , rec11d	divap0d, recdivapd, recdivap2d, divcanap6d, ddcanapd, rec11apd
divmuld , div32d , div13d , divdiv32d , divcan5d , divcan5rd , divcan7d , dmdcand , dmdcan2d , divdiv1d , divdiv2d	divmulapd, div32apd, div13apd, divdiv32apd, divcanap5d, divcanap5rd, divcanap7d, dmdcanapd, dmdcanap2d, divdivap1d, divdivap2d
divmul2d, divmul3d, divassd, div12d, div23d, divdird, divsubdird, div11d	divmulap2d, divmulap3d, divassapd, div12apd, div23apd, divdirapd, divsubdirapd, div11apd
rereccld , redivcld	rerecclapd, redivclapd
mvllmuld	mvllmulapd
elimgt0 , elimge0	none	Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
mulge0b , mulle0b , mulsuble0b	none	Presumably unprovable for reasons analogous to mul0or.
ledivp1i , ltdivp1i	none	Presumably could be proved, but unused in set.mm.
crne0	crap0
ofsubeq0 , ofnegsub , ofsubge0	none	Depend on ofval and/or offn .
df-nn	dfnn2
dfnn3	dfnn2	Presumably could be proved, as it is a slight variation of dfnn2
avgle	none
nnunb	none	Presumably provable from arch but unused in set.mm.
frnnn0supp , frnnn0fsupp	nn0supp	iset.mm does not yet have either the notation, or in some cases the theorems, related to the support of a function or a fintely supported function.
suprzcl	none
zriotaneg	none	Lightly used in set.mm
suprfinzcl	none
decex	deccl
uzwo , uzwo2 , nnwo , nnwof , nnwos	none	Presumably would imply excluded middle, unless there is something which makes this different from nnregexmid.
uzinfmi , nninfm , nn0infm , infmssuzle , infmssuzcl	none	We do not yet have a supremum notation, or most supremum theorems, in iset.mm
negn0	negm
supminf	none	We do not yet have a supremum notation, or most supremum theorems, in iset.mm
zsupss , suprzcl2 , suprzub , uzsupss	none	We do not yet have a supremum notation, or most supremum theorems, in iset.mm
rpneg	rpnegap
xrlttri , xrlttri2	none	A generalization of real trichotomy.
xrleloe , xrleltne , dfle2	none	Consequences of real trichotomy.
xrltlen	none	We presumably could prove an analogue to ltleap but we have not yet defined apartness for extended reals (# is for complex numbers).
dflt2	none
xrletri	none
xrmax1 , xrmax2 , xrmin1 , xrmin2 , xrmaxeq , xrmineq , xrmaxlt , xrltmin , xrmaxle , xrlemin , max1 , max2 , min1 , min2 , maxle , lemin , maxlt , ltmin , max0sub , ifle	none
qbtwnre , qbtwnxr	none yet	These should be provable, but the set.mm proof relies on zbtwnre (which in turn is proved using the least upper bound property). The most straightforward solution is to use a construction-dependent proof in terms of df-iltp (the only complicated part of which is connecting Q. and QQ). This is the solution adopted by Theorem 11.2.6 of [HoTT].
qsqueeze	none yet	Once we have qbtwnre , we should be able to prove this as a consequence of squeeze0.
qextltlem , qextlt , qextle	none	The set.mm proof is not intuitionistic.
xralrple , alrple	none yet	If we had qbtwnxr , it looks like the set.mm proof would work with minor changes.
xnegex	xnegcl
xaddval , xaddf , xmulval , xaddpnf1 , xaddpnf2 , xaddmnf1 , xaddmnf2 , pnfaddmnf , mnfaddpnf , rexadd , rexsub , xaddnemnf , xaddnepnf , xnegid , xaddcl , xaddcom , xaddid1 , xaddid2 , xnegdi , xaddass , xaddass2 , xpncan , xnpcan , xleadd1a , xleadd2a , xleadd1 , xltadd1 , xltadd2 , xaddge0 , xle2add , xlt2add , xsubge0 , xposdif , xlesubadd , xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xaddcld , xmulcld , xadd4d	none	There appears to be no fundamental obstacle to proving these, because disjunctions can arise from elxr rather than excluded middle. However, -e, +e, and xe are lightly used in set.mm, and the set.mm proofs would require significant changes.
ixxub , ixxlb	none
iccen	none
supicc , supiccub , supicclub , supicclub2	none
ixxun , ixxin	none
ioo0	none	Once we have qbtwnxr , it may be possible to rearrange the logic from set.mm so that this proof works (via rabeq0, ralnex, and xrlenlt perhaps).
ioon0	none	Presumably non-empty would need to be changed to inhabited, see also discussion at ioo0
iooid	iooidg
ndmioo	none	See discussion at ndmov but set.mm uses excluded middle, both in proving this and in using it.
lbioo , ubioo	lbioog, ubioog
iooin	none
ico0 , ioc0	none	Possibly similar to ioo0 ; see discussion there.
icc0	icc0r
ioorebas	ioorebasg
ge0xaddcl , ge0xmulcl	none	Rely on xaddcl and xmulcl ; see discussion in this list for those theorems.
icoun , snunioo , snunico , snunioc , prunioo	none
ioojoin	none
difreicc	none
iccsplit	none	This depends, apparently in an essential way, on real number trichotomy.
xov1plusxeqvd	none	This presumably could be proved if not equal is changed to apart, but is lightly used in set.mm.
fzn0	fzm
fz0	none	Although it would be possible to prove a version of this with the additional conditions that M e. _V and N e. _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.
df-fl , df-ceil , and other floor and ceiling theoerms.	none	Most of the theorems in this section are conjectured to imply excluded middle. Imagine a real number which is around 2.99995 or 3.00001 . In order to determine whether its floor is 2 or 3, it would be necessary to compute the number to arbitrary precision. For similarity to the Metamath Proof Explorer, it may be desirable to define floor and ceiling, but only provide most of the theorems where the argument is a rational number.
df-mod and other modulus theoerms.	none	As with df-fl it may be feasible to define this for rational numbers rather than reals.
om2uz0i	frec2uz0d
om2uzsuci	frec2uzsucd
om2uzuzi	frec2uzuzd
om2uzlti	frec2uzltd
om2uzlt2i	frec2uzlt2d
om2uzrani	frec2uzrand
om2uzf1oi	frec2uzf1od
om2uzisoi	frec2uzisod
om2uzoi , ltweuz , ltwenn , ltwefz	none	We do not have a syntax for well ordering and based on theorems like nnregexmid, there is probably little room for this concept.
om2uzrdg	frec2uzrdg
uzrdglem	frecuzrdglem
uzrdgfni	frecuzrdgfn
uzrdg0i	frecuzrdg0
uzrdgsuci	frecuzrdgsuc
uzinf	none	See ominf
uzrdgxfr	none	Presumably could be proved if restated in terms of frec (a la frec2uz0d). However, it is lightly used in set.mm.
fzennn	frecfzennn
fzen2	frecfzen2
cardfz	none	Cardinality does not work the same way without excluded middle and iset.mm has few cardinality related theorems.
hashgf1o	frechashgf1o
fzfi	fzfig
fzfid	fzfigd
fzofi	fzofig
fsequb	none	Seems like it might be provable, but unused in set.mm
fsequb2	none	The set.mm proof does not work as-is
fseqsupcl , fseqsupubi	none	iset.mm does not have the "sup" syntax and lacks most supremum theorems from set.mm.
uzindi	none	This could presumably be proved, perhaps from uzind4, but is lightly used in set.mm
axdc4uz	none	Although some versions of constructive mathematics accept dependent choice, we have not yet developed it in iset.mm
ssnn0fi , rabssnn0fi	none	Conjectured to imply excluded middle along the lines of nnregexmid or ssfiexmid
df-seq	df-iseq
seqex	iseqcl
seqeq1 , seqeq2 , seqeq3 , seqeq1d , seqeq2d , seqeq3d , seqeq123d	iseqeq1, iseqeq2, iseqeq3
nfseq	nfiseq
seqval	iseqval
seqfn	iseqfn
seq1 , seq1i	iseq1
seqp1 , seqp1i	iseqp1
seqcl	iseqcl
seqfveq2	iseqfveq2
seqfeq2	iseqfeq2
seqfveq	iseqfveq
df-exp	df-iexp
expval	expival
expnnval	expinnval
expneg	expnegap0	The set.mm theorem does not exclude the case of dividing by zero.
expneg2	expineg2
expn1	expn1ap0
expcl2lem	expcl2lemap
reexpclz	reexpclzap
expclzlem	expclzaplem
expclz	expclzap
expne0	expap0
expne0i	expap0i
expnegz	expnegzap
mulexpz	mulexpzap
exprec	exprecap
expaddzlem , expaddz	expaddzaplem, expaddzap
expmulz	expmulzap
expsub	expsubap
expp1z	expp1zap
expm1	expm1ap
expdiv	expdivap
expcan , expcand	none	Presumably provable, but the set.mm proof uses eqord1 and the theorem is lightly used in set.mm
ltexp2 , leexp2 , leexp2 , ltexp2d , leexp2d	none	Presumably provable, but the set.mm proof uses ltord1
ltexp2r , ltexp2rd	none	Presumably provable, but the set.mm proof uses ltexp2
sqdiv	sqdivap
sqgt0	sqgt0ap
iexpcyc	none yet	See discussion under df-mod ; modulus for integers would suffice so issues with modulus for reals would not be an impediment.
sqrecii , sqrecd	exprecap
sqdivi	sqdivapi
sqgt0i	sqgt0api
sqlecan	lemul1	Unused in set.mm
sqeqori	none	The reverse direction is oveq1 together with sqneg. The forward direction is presumably not provable, see mul0or for more discussion.
subsq0i , sqeqor	none	Variations of sqeqori .
sq01	none	Lightly used in set.mm. Presumably not provable as stated, for reasons analogous to mul0or .
crreczi	none	Presumably could be proved if not-equal is changed to apart, but unused in set.mm.
expmulnbnd	none	Should be possible to prove this or something similar, but the set.mm proof relies on case elimination based on whether 0 <_ A or not.
digit2 , digit1	none	Depends on modulus and floor, and unused in set.mm.
modexp	none	Depends on modulus. Presumably it, or something similar, can be made to work as it is mostly about integers rather than reals.
discr1 , discr	none	The set.mm proof uses real number trichotomy.
sqrecd	sqrecapd
expclzd	expclzapd
exp0d	expap0d
expnegd	expnegapd
exprecd	exprecapd
expp1zd	expp1zapd
expm1d	expm1apd
expsubd	expsubapd
sqdivd	sqdivapd
expdivd	expdivapd
reexpclzd	reexpclzapd
sqgt0d	sqgt0apd
mulre	mulreap
rediv	redivap
imdiv	imdivap
cjdiv	cjdivap
sqeqd	none	The set.mm proof is not intuitionistic, and this theorem is unused in set.mm.
cjdivi	cjdivapi
cjdivd	cjdivapd
redivd	redivapd
imdivd	imdivapd
df-sqrt	df-rsqrt	See discussion of complex square roots in the comment of df-rsqrt
sqrtval	sqrtrval	See discussion of complex square roots in the comment of df-rsqrt
01sqrex and its lemmas	none	We have not yet defined real number completeness enough to prove the existence of these square roots, but we expect we'll eventually be able to prove this theorem from cauappcvgpr or similar theorems.
cnpart	none	See discussion of complex square roots in the comment of df-rsqrt
resqrex	none yet	This will be provable once completeness is better developed
sqrmo	none	See discussion of complex square roots in the comment of df-rsqrt
resqreu	none yet	Once completeness is better developed, it should be possible to adjust this to reflect sqrtrval
resqrtcl	none yet	Once completeness is better developed, this will be provable via resqrex
resqrtth , remsqsqrt	none yet	These will be provable once completeness is better developed
sqrtge0 , sqrtgt0	none yet	These will be provable once completeness is better developed
sqrtmul , sqrtle , sqrtlt , sqrt11 , sqrt00	none yet	These should be provable once completeness is better developed
rpsqrtcl	none yet	This is a variation of sqrtgt0
sqrtdiv	none yet	Should be provable once completeness is better developed
sqrtneg	none	Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of df-rsqrt
sqrtsq2	none yet	Should be provable once completeness is better developed
sqrt2gt1lt2	none yet	Should be provable once completeness is better developed
sqrtm1	none	Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of df-rsqrt
abscl	none yet	Should be easy once we get resqrtcl
absvalsq , absvalsq2 , sqabsadd , sqabssub	none yet	Should be easy once we prove resqrtth
absge0	none yet	Should be easy once we prove sqrtge0
absrpcl	none yet	Should be provable once we have proved completeness and more of the square root theorems. Not equal presumably will need to be changed to apart.
abs00 , abs00ad	none yet	Should be provable once we have proved completeness and more of the square root theorems. We will presumably also be able to prove (( abs ` A) # 0 <-> A # 0 which is stronger and is something we'd likely want.
absreimsq , absreim	none yet	Should be provable once we have proved absvalsq2
absmul	none yet	Should be provable once we have proved sqrtmul
absdiv	none yet	Should be provable once we have proved completeness and more of the square root theorems. Not equal will need to be changed to apart.
leabs	none	The set.mm proof relies on real number trichotomy. Here is a sketch of a proof which might work once absge0 is proved. Suppose ( abs ` A) < A. By sowlin, ( abs ` A) < 0 \/ 0 < A. But absge0 tells us that ( abs ` A) < 0 is not possible, and 0 < A implies ( abs ` A) = A via absid. This is a contradiction so -. ( abs ` A) < A, which by lenlt implies A <_ ( abs ` A).
absor	none	We could prove this for rationals if we wanted
absresq	none yet	This will follow once we have proved absvalsq
absmod0	none	See df-mod ; we may want to supply this for rationals or integers
absexp	none yet	Should be provable once we have proved absmul
absexpz	none yet	Should be provable, with not equal changed to apart, once we have proved absexp
abssq , sqabs	none yet	Should be provable once we have absexp or other completeness related results
absrele , absimle	none yet	Should be provable once we have proved sqrtle
max0add	none	Relies on real number trichotomy
absz	none	Although this is presumably provable, the set.mm proof is not intuitionistic and it is lightly used in set.mm

Bibliography   

1. [Apostol] Apostol, Tom M., Calculus, vol. 1, 2nd ed., John Wiley & Sons Inc. (1967) [QA300.A645 1967].
2. [Bauer] Bauer, Andrej, "Five stages of accepting constructive mathematics," Bulletin (New Series) of the American Mathematical Society, 54:481-498 (2017), DOI: 10.1090/bull/1556 .
3. [BauerTaylor] Andrej Bauer and Paul Taylor, "The Dedekind Reals in Abstract Stone Duality", Mathematical structures in computer science, 19(4):757–838, 2009, http://www.paultaylor.eu/ASD/dedras.pdf
4. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
5. [Bobzien] Bobzien, Susanne, "Stoic Logic", The Cambridge Companion to Stoic Philosophy, Brad Inwood (ed.), Cambridge University Press (2003-2006), https://philpapers.org/rec/BOBSL.
6. [BourbakiEns] Bourbaki, Nicolas, Théorie des ensembles, Springer-Verlag, Berlin Heidelberg (2007); available in English (for purchase) at http://www.springer.com/us/book/9783540225256 (retrieved 15-Aug-2016). Page references in iset.mm are for the French edition.
7. [BourbakiTop1] Bourbaki, Nicolas, Topologie générale, Chapitres 1 à 4, Springer-Verlag, Berlin Heidelberg (2007); available in English (for purchase) at http://www.springer.com/us/book/9783540642411 (retrieved 15-Aug-2016). Page references in set.mm are for the French edition.
8. [ChoquetDD] Choquet-Bruhat, Yvonne and Cecile DeWitt-Morette, with Margaret Dillard-Bleick, Analysis, Manifolds and Physics, Elsevier Science B.V., Amsterdam (1982) [QC20.7.A5C48 1981].
9. [Crosilla] Crosilla, Laura, "Set Theory: Constructive and Intuitionistic ZF", The Stanford Encyclopedia of Philosophy (Summer 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/sum2015/entries/set-theory-constructive/.
10. [Moschovakis] Moschovakis, Joan, "Intuitionistic Logic", The Stanford Encyclopedia of Philosophy (Spring 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/spr2015/entries/logic-intuitionistic/.
11. [Eisenberg] Eisenberg, Murray, Axiomatic Theory of Sets and Classes, Holt, Rinehart and Winston, Inc., New York (1971) [QA248.E36].
12. [Enderton] Enderton, Herbert B., Elements of Set Theory, Academic Press, Inc., San Diego, California (1977) [QA248.E5].
13. [Gleason] Gleason, Andrew M., Fundamentals of Abstract Analysis, Jones and Bartlett Publishers, Boston (1991) [QA300.G554].
14. [Geuvers] Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg, "Skeleton for the Proof development leading to the Fundamental Theorem of Algebra", October 2, 2000, http://www.cs.ru.nl/~herman/PUBS/FTA.mathproof.ps.gz (accessed 19 Feb 2020).
15. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
16. [Heyting] Heyting, A., Intuitionism: An introduction, North-Holland publishing company, Amsterdam, second edition (1966).
17. [Hitchcock] Hitchcock, David, The peculiarities of Stoic propositional logic, McMaster University; available at http://www.humanities.mcmaster.ca/~hitchckd/peculiarities.pdf (retrieved 3 Jul 2016).
18. [HoTT] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, first edition.
19. [Jech] Jech, Thomas, Set Theory, Academic Press, San Diego (1978) [QA248.J42].
20. [KalishMontague] Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic with identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:81-101 (1965) [QA.A673].
21. [Kreyszig] Kreysig, Erwin, Introductory Functional Analysis with Applications, John Wiley & Sons, New York (1989) [QA320.K74].
22. [Kunen] Kunen, Kenneth, Set Theory: An Introduction to Independence Proofs, Elsevier Science B.V., Amsterdam (1980) [QA248.K75].
23. [KuratowskiMostowski] Kuratowski, K. and A. Mostowski, Set Theory: with an Introduction to Descriptive Set Theory, 2nd ed., North-Holland, Amsterdam (1976) [QA248.K7683 1976].
24. [Levy] Levy, Azriel, Basic Set Theory, Dover Publications, Mineola, N.Y. (2002) [QA248.L398 2002].
25. [Lopez-Astorga] Lopez-Astorga, Miguel, "The First Rule of Stoic Logic and its Relationship with the Indemonstrables", Revista de Filosofía Tópicos (2016); available at http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf (retrieved 3 Jul 2016).
26. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
27. [Megill] Megill, N., "A Finitely Axiomatized Formalization of Predicate Calculus with Equality," Notre Dame Journal of Formal Logic, 36:435-453 (1995) [QA.N914]; available at http://projecteuclid.org/euclid.ndjfl/1040149359 (accessed 11 Nov 2014); the PDF preprint has the same content (with corrections) but pages are numbered 1-22, and the database references use the numbers printed on the page itself, not the PDF page numbers.
28. [Mendelson] Mendelson, Elliott, Introduction to Mathematical Logic, 2nd ed., D. Van Nostrand (1979) [QA9.M537].
29. [Monk1] Monk, J. Donald, Introduction to Set Theory, McGraw-Hill, Inc. (1969) [QA248.M745].
30. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
31. [Quine] Quine, Willard van Orman, Set Theory and Its Logic, Harvard University Press, Cambridge, Massachusetts, revised edition (1969) [QA248.Q7 1969].
32. [Sanford] Sanford, David H., If P, then Q: Conditionals and the Foundations of Reasoning, 2nd ed., Routledge Taylor & Francis Group (2003); ISBN 0-415-28369-8; available at https://books.google.com/books?id=h_AUynB6PA8C&pg=PA39#v=onepage&q&f=false (retrieved 3 Jul 2016).
33. [Schechter] Schechter, Eric, Handbook of Analysis and Its Foundations, Academic Press, San Diego (1997) [QA300.S339].
34. [Stoll] Stoll, Robert R., Set Theory and Logic, Dover Publications, Inc. (1979) [QA248.S7985 1979].
35. [Suppes] Suppes, Patrick, Axiomatic Set Theory, Dover Publications, Inc. (1972) [QA248.S959].
36. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
37. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].
38. [WhiteheadRussell] Whitehead, Alfred North, and Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, Cambridge, 1962 [QA9.W592 1962].