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 6 first (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 axbnd (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 axbnd 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  axbnd  ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀x∀z(x = y → ∀z x = y))) 
Left Membership Equality  ax13  ⊢ (x = y → (x ∈ z → y ∈ z)) 
Right Membership Equality  ax14  ⊢ (x = y → (z ∈ x → z ∈ y)) 
Distinctness  ax17  ⊢ (φ → ∀xφ), where x does not occur in φ 
Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets." A set can be an element of another set, and this relationship is indicated by the symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. These axioms were developed in response to Russell's Paradox, a discovery that revolutionized the foundations of mathematics and logic.
In the IZF axioms that follow, all set variables are assumed to be distinct. If you click on their links you will see the explicit distinct variable conditions.
Axiom of Extensionality  axext  ⊢ (∀z(z ∈ x ↔ z ∈ y) → x = y) 
Axiom of Collection  axcoll  ⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ) 
Axiom of Separation  axsep  ⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ)) 
Axiom of Power Sets  axpow  ⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y) 
Axiom of Pairing  axpr  ⊢ ∃z∀w((w = x ∨ w = y) → w ∈ z) 
Axiom of Union  axun  ⊢ ∃y∀z(∃w(z ∈ w ∧ w ∈ x) → z ∈ y) 
Axiom of Set Induction  axsetind  ⊢ (∀𝑎(∀y ∈ 𝑎 [y / 𝑎]φ → φ) → ∀𝑎φ) 
Axiom of Infinity  axiinf  ⊢ ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x)) 
We develop set theory based on the Intuitionistic ZermeloFraenkel (IZF) system, mostly following the IZF axioms as laid out in [Crosilla]. Constructive ZermeloFraenkel (CZF), also described in Crosilla, is not as easy to formalize in metamath because the Axiom of Restricted Separation would require us to develop the ability to classify formulas as bounded formulas, similar to the machinery we have built up for asserting on whether variables are free in formulas.
Listed here are some examples of starting points for your journey through the maze. Some are stated just as they would be in a nonconstructive context; others are here to highlight areas which look different constructively. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory. The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic CrossReference useful.
Propositional calculus Predicate calculus Set theory 
For the student or master of classical mathematics, constructive mathematics can be baffling. One can get over some of the intial hurdles of understanding how constructive mathematics works and why it might be interesting by reading [Bauer] but that work does little to explain in concrete terms how to write proofs in intuitionistic logic. Fortunately, metamath helps with one of the biggest hurdles: noticing when one is even using the law of the excluded middle or the axiom of choice. But suppose you have a classical proof from the Metamath Proof Explorer and it fails to verify when you copy it over to the Intuitionistic Logic Explorer. What then? Here are some rules of thumb in converting classical proofs to intuitionistic ones.
This is a list of theorems from the Metamath Proof Explorer (which assumes the law of the excluded middle throughout) which we do not have in the Intuitionistic Logic Explorer (generally because they are not provable without the law of the excluded middle, although some could be proved but aren't for a variety of reasons), together with the closest replacements.
set.mm  iset.mm  notes  

ax3 , con4d , con34b , necon4bd  con3  The form of contraposition which removes negation does not hold in intutionistic logic.  
pm2.18  pm2.01  See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.  
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  
dfor , pm4.64 , pm2.54 , orri , orrd  pm2.53, ori, ord  
pm4.63  pm3.2im  
iman  imanim  
annim  annimim  
oran  oranim  
ianor  pm3.14  
ecase3d  none  This is a form of case elimination.  
dedlem0b  dedlemb  
3ianor  3ianorr  
dfex  exalim  
alex  alexim  
exnal  exnalim  
alexn  alexnim  
exanali  exanaliim  
19.35  19.351  
19.30  none  
19.36  19.361  
19.37  19.371  
19.32  19.32r  
19.31  19.31r  
exdistrf  exdistrfor  
exmo  exmonim  
mo2  mo2r, mo3  
rexnal  rexnalim  
dfral2  ralexim  
dfrex2  rexalim  
rexanali  none  
nrexralim  none  
nfrald  nfraldxy, nfraldya  
nfrexd  nfrexdxy, nfrexdya  
nfral  nfralxy, nfralya  
nfra2  nfra1, nfralya  
nfrex  nfrexxy, nfrexya  
r19.30  none  
ralcom2  ralcom  
sspss  sspssr  
n0f  n0rf  
n0  n0r  
neq0  neq0r  
reximdva0  reximdva0m  
r19.45zv  r19.45mv  
dfif2  dfif  
ifsb  none  
dfif4  none  Unused in set.mm  
dfif5  none  Unused in set.mm  
ifnot  none  
ifan  none  
ifor  none  
ifeq1da, ifeq2da  none  
ifclda  none  
ifeqda  none  
elimif , ifbothda , ifboth , ifid , eqif , ifval , elif , ifel , ifcl , ifcld , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD  none  
dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel , ifex , ifexg  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
trintss  trintssm  
trint0  trint0m  
moabex  euabex  In general, most of the set.mm theorems still hold, but a decent number of the ones get caught up on "there are two cases: the set exists or it does not"  
snex  snexg, snex  The iset.mm version of snex has an additional hypothesis  
opex  opexg, opex  The iset.mm version of opex has additional hypotheses  
dfso  dfiso  Although we define 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  
pitric  For the specific order  
nqtric  For the specific order  
sotrieq  sotritrieq  For a trichotomous order  
sotrieq2  see sotrieq and then apply ioran  
issoi  issod, ispod  Many of the set.mm usages of issoi don't carry over, so there is less need for this convenience theorem.  
isso2i  issod  Presumably this could be proved if we need it.  
dffr and all theorems using Fr  none  Because iset.mm assumes axsetind without reluctance, all sets are wellfounded. We could adopt a treatment more like set.mm if people want to investigate set theories which are constructive but which do not assume axsetind.  
dfwe (and all theorems using We)  none  Ordering is moderately different in constructive logic, so if there is anything along these lines worth doing it will be different from set.mm.  
tz7.7  none  
ordelssne  none  
ordelpss  none  
ordsseleq  onelss, eqimss  Taken together, onelss and eqimss represent the reverse direction of the biconditional from ordsseleq  
ordtri3or  nntri3or  Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid.  
ordtri2  nntri2  ordtri2 for all ordinals presumably implies excluded middle although we don't have a specific proof analogous to ordtriexmid.  
ordtri3 , ordtri4 , ordtri2or2 , ordtri2or3 , dford2  none  Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid. We don't have similar proofs for every variation of of trichotomy but most of them are presumably powerful enough to imply excluded middle.  
ordtri1 , ontri1 , onssneli , onssnel2i  ssnel, nntri1  ssnel is a trichotomylike theorem which does hold, although it is an implication whereas ordtri1 is a biconditional. nntri1 is biconditional, but just for natural numbers.  
ordtr2 , ontr2  none  See also ordelpss in set.mm  
ordtr3  none  This is weak linearity of ordinals, which presumably implies excluded middle by ordsoexmid.  
ordtri2or  none  Implies excluded middle as shown at ordtri2orexmid.  
ord0eln0 , on0eln0  ne0i, nn0eln0  
nsuceq0  nsuceq0g  
ordsssuc  trsucss  
ordequn  none  If you know which ordinal is larger, you can achieve a similar result via theorems such as oneluni or ssequn1.  
ordun  onun2  
dmxpid  dmxpm  
relimasn  imasng  
opswap  opswapg  
cnvso  cnvsom  
iotaex  euiotaex  
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  
1stexg, 2ndexg  for the functions and  
ndmfv  ndmfvg  The case is fvprc.  
elfvdm  relelfvdm  
funiunfv  fniunfv, funiunfvdm  
funiunfvf  funiunfvdmf  
eluniima  eluniimadm  
riotaex  riotacl  
nfriotad  nfriotadxy  
csbriota , csbriotagOLD  csbriotag  
riotaxfrd  none  Although it may be intuitionizable, it is lightly used in set.mm.  
ovex  fnovex  Sometimes or fvexg or relrnfvex may work.  
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 , ndmovcl , ndmovrcl , ndmovcom , ndmovass , ndmovdistr , ndmovord , and ndmovordi  none  Although these theorems are moderately widely used in set.mm, in many cases they are being used for case elimination and the set.mm proofs are not intuitionistic. We might bring back some of them later (which may have conditions that the sets exist, but aren't in the domain), but maybe we'll find a way to avoid them.  
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  
ordeleqon  none  
ssonprc  none  not provable (we conjecture), but interesting enough to intuitionize anyway. is provable, and is provable. (Why isn't dfpss stated so that the set difference is inhabited? If so, you could prove .)  
onint  none  Conjectured to not be provable without excluded middle. If you apply onint to a pair you can derive totality of the order.  
onint0  none  Thought to be "trivially not intuitionistic", and it is not clear if there is an alternate way to state it that is true. If the empty set is in A then of course ^ A = (/), but the converse seems difficult. I don't know so much about the structure of the ordinals without linearity,  
onssmin, onminesb, onminsb  none  Conjectured to not be provable without excluded middle, for the same reason as onint.  
oninton  none yet  This one (with nonempty changed to inhabited) I think can still be salvaged though. From the fact that it is inhabited you get that it exists, and is a subset of an ordinal x. It is an intersection of transitive sets so it is transitive, and of course all its members are members of x so they are transitive too. And E. Fr A falls to subsets.  
onintrab, onintrab2  none yet  The set.mm proof uses oninton.  
oneqmin  none  Falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.  
onminex  none yet  falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.  
onmindif2  none  Conjectured to not be provable without excluded middle.  
onmindif2  none  Conjectured to not be provable without excluded middle.  
ordpwsuc  ordpwsucss  See the ordpwsucss comment for discussion of the succcessorlike properites of . 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 = 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 ). 

ordzsl, onzsl, dflim3, nlimon  none  
dflim4  dfilim  We conjecture that dflim4 is not equivalent to dfilim.  
limsuc  none yet  Conjectured to be provable.  
limsssuc  none yet  Conjectured to be provable.  
tfinds  tfis3  
1stval  1stvalg  
2ndval  2ndvalg  
1stnpr  none  May be intuitionizable, but very lightly used in set.mm.  
2ndnpr  none  May be intuitionizable, but very lightly used in set.mm.  
brtpos  brtposg  
ottpos  ottposg  
ovtpos  ovtposg  
pwuninel  pwuninel2  The set.mm proof of pwuninel uses case elimination.  
iunonOLD  iunon  
smofvon2  smofvon2dm  
tfr1  tfri1  
tfr2  tfri2  
tfr3  tfri3  
tfr2b , recsfnon , recsval  none  These transfinite recursion theorems are lightly used in set.mm.  
dfrdg  dfirdg  This definition combines the successor and limit cases (rather than specifying them as separate cases in a way which relies on excluded middle). In the words of [Crosilla], p. "Settheoretic principles incompatible with intuitionistic logic", "we can still define many of the familiar settheoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit."  
rdgfnon  rdgifnon  
ordge1n0  ordge1n0im, ordgt0ge1  
ondif1  dif1o  In set.mm, ondif1 is used for Cantor Normal Form  
ondif2 , dif20el  none  The set.mm proof is not intuitionistic  
brwitnlem  none  The set.mm proof is not intuitionistic  
om0r  om0, nnm0r  
om00  nnm00  
om00el  none  
suc11reg  suc11g  
frfnom  frecfnom  frecfnom adopts the frec notation and adds conditions on the characteristic function and initial value.  
fr0g  frec0g  frec0g adopts the frec notation and adds a condition on the characteristic function.  
frsuc  frecsuc  frecsuc adopts the frec notation and adds conditions on the characteristic function and initial value.  
om0x  om0  
oaord1  none yet  
oaword  oawordi  The other direction presumably could be proven but isn't yet.  
omwordi  nnmword  The set.mm proof of omwordi relies on case elimination.  
omword1  nnmword  
nnawordex  nnaordex  nnawordex is only used a few places in set.mm  
swoso  none  Unused in set.mm.  
ecdmn0  ecdmn0m  
erdisj, qsdisj, qsdisj2, uniinqs  none  These could presumably be restated to be provable, but they are lightly used in set.mm  
xpider  xpiderm  
iiner  iinerm  
riiner  riinerm  
brecop2  none  This is a form of reverse closure and uses excluded middle in its proof.  
erov , erov2  none  Unused in set.mm.  
eceqoveq  none  Unused in set.mm.  
2pwuninel  2pwuninelg  
axreg , axreg2 , zfregcl  axsetind  axreg implies excluded middle as seen at regexmid  
addcompi  addcompig  
addasspi  addasspig  
mulcompi  mulcompig  
mulasspi  mulasspig  
distrpi  distrpig  
addcanpi  addcanpig  
mulcanpi  mulcanpig  
addnidpi  addnidpig  
ltapi  ltapig  
ltmpi  ltmpig  
nlt1pi  nlt1pig  
indpi  finds  Although indpi presumably could be proved, it is lightly used in set.mm  
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 is a function, but so far there hasn't been a need to do so.  
addcomnq  addcomnqg  
mulcomnq  mulcomnqg  
mulassnq  mulassnqg  
recmulnq  recmulnqg  
ltanq  ltanqg  
ltmnq  ltmnqg  
ltexnq  ltexnqq  
archnq  archnqq  
dfnp  dfinp  
df1p  dfi1p  
dfplp  dfiplp  
dfltp  dfiltp  
elnp , elnpi  elinp  
prn0  prml, prmu  
prpssnq  prssnql, prssnqu  
elprnq  elprnql, elprnqu  
prcdnq  prcdnql, prcunqu  
prub  prubl  
prnmax  prnmaxl  
npomex  none  
prnmadd  prnmaddl  
genpv  genipv  
genpcd  genpcdl  
genpnmax  genprndl  
ltrnq  ltrnqg, ltrnqi  
genpcl  addclpr, mulclpr  
genpass  genpassg  
addclprlem1  addnqprllem, addnqprulem  
addclprlem2  addnqprl, addnqpru  
plpv  plpvlu  
mpv  mpvlu  
mulclprlem  mulnqprl, mulnqpru  
addcompr  addcomprg  
addasspr  addassprg  
mulcompr  mulcomprg  
mulasspr  mulassprg  
distrlem1pr  distrlem1prl, distrlem1pru  
distrlem4pr  distrlem4prl, distrlem4pru  
distrlem5pr  distrlem5prl, distrlem5pru  
distrpr  distrprg  
ltprord  ltprordil  There hasn't yet been a need to investigate versions which are biconditional or which involve proper subsets.  
psslinpr  ltsopr  
prlem934  prarloc2  
ltaddpr2  ltaddpr  
ltexprlem1 , ltexprlem2 , ltexprlem3 , ltexprlem4  none  See the lemmas for ltexpri generally.  
ltexprlem5  ltexprlempr  
ltexprlem6  ltexprlemfl, ltexprlemfu  
ltexprlem7  ltexprlemrl, ltexprlemru  
ltapr  ltaprg  
addcanpr  addcanprg  
prlem936  prmuloc2  
reclem2pr  recexprlempr  
reclem3pr  recexprlem1ssl, recexprlem1ssu  
reclem4pr  recexprlemss1l, recexprlemss1u, recexprlemex  
supexpr , suplem1pr , suplem2pr  none  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.  
mulcmpblnrlem  mulcmpblnrlemg  
ltsrpr  ltsrprg  
dmaddsr , dmmulsr  none  Although these presumably could be proved in a way similar to dmaddpq and dmmulpq (in fact dmaddpqlem would seem to be easily generalizable to anything of the form ), we haven't yet had a need to do so.  
addcomsr  addcomsrg  
addasssr  addasssrg  
mulcomsr  mulcomsrg  
mulasssr  mulasssrg  
distrsr  distrsrg  
ltasr  ltasrg  
sqgt0sr  mulgt0sr  The case would also intuitionize (looks like this part of set.mm's sqgt0sr proof would intuitionize well), but for the theorem as a whole, "not equal to zero" would need to be changed to "apart from zero".  
recexsr  recexsrlem  This would follow from sqgt0sr (as in the set.mm proof of recexsr), but as noted there "not equal to zero" would need to be changed to "apart from zero".  
mappsrpr , ltpsrpr , map2psrpr  none  Although variants of these theorems could be intuitionized, in set.mm they are only used for supremum theorems, so we can consider this in more detail when we tackle what kind of supremum theorems to prove.  
supsrlem , supsr  none  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle.  
axaddf , axaddf , axmulf , axmulf  none  Because these are described as deprecated in set.mm, we haven't figured out what would be involved in proving them for iset.mm.  
ax1ne0 , ax1ne0  ax0lt1, ax0lt1  
axrrecex , axrrecex  axprecex, axprecex  
axprelttri , axprelttri  axpreltirr, axpreltwlin, axpreltirr, axpreltwlin  
axpresup , axpresup , axsup  none yet  The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. If we want a set of axioms for real numbers which allows us to avoid constructiondependent theorems beyond this point, we'll need a modified Least Upper Bound property, a statement concerning Dedekind cuts or something similar, or some other axiom(s).  
elimne0  none  Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.  
xrltnle  xrlenlt  
ssxr  dfxr  Lightly used in set.mm  
ltnle , ltnlei , ltnled  lenlt  
lttri2 , lttri3 , lttri4 , letri3  none  Real number trichotomy is not provable.  
leloe , eqlelt , leloei , leloed , eqleltd  none  
leltne , leltned  none  
lelttr , lelttri , lelttrd  none yet  This should be provable, as it is part of Definition 11.2.7(vi) of [HoTT], p. (varies). But the set.mm proof does not work asis.  
ltletr , ltletri , ltletrd  none yet  This should be provable, as it is part of Definition 11.2.7(vi) of [HoTT], p. (varies). But the set.mm proof does not work asis.  
ltneOLD  ltne  
letric , letrii , letrid  none  A form of real number trichotomy  
ltlen , ltleni , ltlend  none  
ltadd2 , ltadd2i , ltadd2d , ltadd2dd  none yet  This will be provable based on additive inverse once we have addcom and a few other prerequisites. We'll probably end up moving it down to the "Ordering on reals (cont.)" section.  
ne0gt0  none  We presumably could prove this if we changed "not equal to zero" to "apart from zero".  
lecasei , lelttric , ltlecasei  none  These are real number trichotomy  
lttri2i  none  This can be read as "two real numbers are nonequal if and only if they are apart" which relies on excluded middle  
lttri3i  none  The direction (which can also be read as "if two real numbers are not apart, then they are equal) is proved via trichotomy in set.mm  
letri3i  none  Equivalent to lttri3i by lenlt  
le2tri3i  none  This is an elaborated version of letri3i  
ne0gt0d , lttrid , lttri2d , lttri3d , lttri4d , letri3d  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 
This
page was last updated on 15Aug2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 