Metamath Home Intuitionistic Logic Explorer Home Page First >
Last >
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent

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 φ   &   φψ   ⇒   ψ
    Left 'and' eliminationax-ia1 ((φ ψ) → φ)
    Right 'and' eliminationax-ia2 ((φ ψ) → ψ)
    'And' introductionax-ia3 (φ → (ψ → (φ ψ)))
    Definition of 'or'ax-io (((φ χ) → ψ) ↔ ((φψ) (χψ)))
    'Not' introductionax-in1 ((φ → ¬ φ) → ¬ φ)
    'Not' eliminationax-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 (xyφyxφ)
    Rule of Generalization ax-gen φ   =>    xφ
    x is bound in xφ ax-ial (xφxxφ)
    x is bound in xφ ax-ie1 (xφxxφ)
    Define existential quantification ax-ie2 (x(ψxψ) → (x(φψ) ↔ (xφψ)))
    Axiom of Equality ax-8 (x = y → (x = zy = z))
    Axiom of Existence ax-i9 x x = y
    Axiom of Quantifier Substitution ax-10 (x x = yy 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 = yz x = y)))
    Axiom of Bundling ax-bnd (z z = x (z z = y xz(x = yz x = y)))
    Left Membership Equality ax-13 (x = y → (x zy z))
    Right Membership Equality ax-14 (x = y → (z xz 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 xz y) → x = y)
    Axiom of Collection ax-coll (x 𝑎 yφ𝑏x 𝑎 y 𝑏 φ)
    Axiom of Separation ax-sep yx(x y ↔ (x z φ))
    Axiom of Power Sets ax-pow yz(w(w zw x) → z y)
    Axiom of Pairing ax-pr zw((w = x w = y) → w z)
    Axiom of Union ax-un yz(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.


    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 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 ∃! 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
    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 𝜔
    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 Because iset.mm assumes ax-setind without reluctance, all sets are well-founded. We could adopt a treatment more like set.mm if people want to investigate set theories which are constructive but which do not assume 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 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. A = On → A𝑉 is provable, and (B On AB) → A 𝑉 is provable. (Why isn't df-pss stated so that the set difference is inhabited? If so, you could prove A ⊊ On → A 𝑉.)
    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 (𝒫 A ∩ 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 = (𝒫 A ∩ On) on . (We can formalize this proof but not until we have om and at least finite induction.) Then om' = U. om' because if x e. om' then x = suc'^n (/) for some n, and then x C_ suc'^n (/) implies x e. suc'^(n+1) (/) e. om' so x e. U. om'.

    Now supposing the theorem, we know that A. x e. om' suc x e. om', so in particular 2o e. om', that is, 2o = suc'^n (/) for some n. (Note that 1o = suc' (/) - see pw0.) For n = 0 and n = 1 this is clearly false, and for n = m+3 we have 1o e. suc' suc' (/) , so 2o C_ suc' suc' (/), so 2o e. suc' suc' suc' (/) C_ suc' suc' suc' suc'^m (/) = 2o, contradicting ordirr.

    Thus 2o = suc' suc' (/) = suc' 1o. Applying this to X = {x {∅} ∣ φ} we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ordtriexmidlem2 for 𝑋 = ∅ and rabsnt as seen in the onsucsssucexmid proof for 𝑋 = 1𝑜).

    ordzsl, onzsl, dflim3, nlimon none
    dflim4 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 {∅} 𝜔
    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 ((𝑆 × 𝑇) / 𝑅)), 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 · 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 ). This is the solution adopted by Theorem 11.2.6 of [HoTT].
    qsqueeze none yet Once we have qbtwnre , we should be able to prove this as a consequence of squeeze0.
    qextltlem , qextlt , qextle none The set.mm proof is not intuitionistic.
    xralrple , alrple none yet If we had qbtwnxr , it looks like the set.mm proof would work with minor changes.
    xnegex xnegcl
    xaddval , xaddf , xmulval , xaddpnf1 , xaddpnf2 , xaddmnf1 , xaddmnf2 , pnfaddmnf , mnfaddpnf , rexadd , rexsub , xaddnemnf , xaddnepnf , xnegid , xaddcl , xaddcom , xaddid1 , xaddid2 , xnegdi , xaddass , xaddass2 , xpncan , xnpcan , xleadd1a , xleadd2a , xleadd1 , xltadd1 , xltadd2 , xaddge0 , xle2add , xlt2add , xsubge0 , xposdif , xlesubadd , xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xaddcld , xmulcld , xadd4d none There appears to be no fundamental obstacle to proving these, because disjunctions can arise from elxr rather than excluded middle. However, -𝑒, +𝑒, and ·e are lightly used in set.mm, and the set.mm proofs would require significant changes.
    ixxub , ixxlb none
    iccen none
    supicc , supiccub , supicclub , supicclub2 none
    ixxun , ixxin none
    ioo0 none Once we have qbtwnxr , it may be possible to rearrange the logic from set.mm so that this proof works (via rabeq0, ralnex, and xrlenlt perhaps).
    ioon0 none Presumably 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 𝑀 V and 𝑁 V, the theorem is lightly used in set.mm.
    fzon0 fzom
    fzo0n0 fzo0m
    ssfzoulel none Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    fzonfzoufzol none Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    elfznelfzo , elfznelfzob , injresinjlem , injresinj none Some or all of this presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    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

    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].

      This page was last updated on 15-Aug-2015.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C HTML validation [external]