![]() |
Intuitionistic Logic Explorer Home Page | First > Last > |
Mirrors > Home > ILE Home > Th. List > Recent |
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 | Related pages External links |
(Placeholder for future use)
(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 first six (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-bndl (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-bndl 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.
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 | ax-1 | ⊢ (φ → (ψ → φ)) |
Axiom Frege | ax-2 | ⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) |
Rule of Modus Ponens | ax-mp | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Left 'and' elimination | ax-ia1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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.
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-bndl | ⊢ (∀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
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 | 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.
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 Predicate calculus Set theory Real and complex numbers |
For the student or master of classical mathematics, constructive mathematics can be baffling. One can get over some of the intial hurdles of understanding how constructive mathematics works and why it might be interesting by reading [Bauer] but that work does little to explain in concrete terms how to write proofs in intuitionistic logic. Fortunately, metamath helps with one of the biggest hurdles: noticing when one is even using the law of the excluded middle or the axiom of choice. But suppose you have a classical proof from the Metamath Proof Explorer and it fails to verify when you copy it over to the Intuitionistic Logic Explorer. What then? Here are some rules of thumb in converting classical proofs to intuitionistic ones.
This is a list of theorems from the Metamath Proof Explorer (which assumes the law of the excluded middle throughout) which we do not have in the Intuitionistic Logic Explorer (generally because they are not provable without the law of the excluded middle, although some could be proved but aren't for a variety of reasons), together with the closest replacements.
set.mm | iset.mm | notes | |
---|---|---|---|
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 ![]() ![]() ![]() |
|
intabs | none | Lightly used in set.mm, and the set.mm proof is not intuitionistic | |
moabex | euabex | In general, most of the set.mm ![]() ![]() |
|
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 ![]() | |
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. | |
df-fr and all theorems using Fr | none | Right now iset.mm does not have a well-founded predicate
( Presumably if we were to add This definition has some problems when A is a proper class. As such,
ax-setind has to be stated as a schema instead:
There are two ways to say no infinite descending sequence, using
R Fr A R Fr2 A R Fr3 A 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 |
|
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 ![]() ![]() |
||
ndmfv | ndmfvg | The ![]() ![]() ![]() ![]() |
|
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. ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 =
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 = |
|
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 ![]() |
|
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
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 ![]() ![]() |
|
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, ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 | The difference is that ![]() |
|
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 ![]() ![]() ![]() |
|
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
|
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
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
|
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 |
This
page was last updated on 15-Aug-2015. Your comments are welcome: Norman Megill ![]() Copyright terms: Public domain |
W3C HTML validation [external] |