| 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 | ` |- ph ` & ` |- ph -> ps ` ⇒ ` |- ps ` |
| Left 'and' elimination | ax-ia1 | ` |- ( ( ph /\ ps ) -> ph ) ` |
| Right 'and' elimination | ax-ia2 | ⊢ ((φ ∧ ψ) → ψ) |
| 'And' introduction | ax-ia3 | ⊢ (φ → (ψ → (φ ∧ ψ))) |
| Definition of 'or' | ax-io | ⊢ (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ))) |
| 'Not' introduction | ax-in1 | ⊢ ((φ → ¬ φ) → ¬ φ) |
| 'Not' elimination | ax-in2 | ⊢ (¬ φ → (φ → ψ)) |
Unlike in classical propositional logic, 'and' and 'or' are not readily defined in terms of implication and 'not'. In particular, φ ∨ ψ is not equivalent to ¬ φ → ψ, nor is φ → ψ equivalent to ¬ φ ∨ ψ, nor is φ ∧ ψ equivalent to ¬ (φ → ¬ ψ).
The ax-in1 axiom is a form of proof by contradiction which does hold intuitionistically. That is, if φ implies a contradiction (such as its own negation), then one can conclude ¬ φ. By contrast, assuming ¬ φ and then deriving a contradiction only serves to prove ¬ ¬ φ, which in intuitionistic logic is not the same as φ.
The biconditional can be defined as the conjunction of two implications, as in dfbi2 and df-bi.
Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (for-all) and ∃ (there-exists). Unlike in classical logic, ∃ cannot be defined in terms of ∀. As in classical logic, we also add = for equality (which is key to how we handle substitution in metamath) and ∈ (which for current purposes can just be thought of as an arbitrary predicate, but which will later come to mean set membership).
Our axioms are based on the classical set.mm predicate logic axioms, but adapted for intuitionistic logic, chiefly by adding additional axioms for ∃ and also changing some aspects of how we handle negations.
| 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]. The one exception to the statement that we use IZF is that a few sections develop set theory using Constructive Zermelo-Fraenkel (CZF), also described in Crosilla. These sections start at ~ wbd (including the section header right before it) and the biggest complication is the machinery to classify formulas as bounded formulas, for purposes of the Axiom of Restricted Separation ~ ax-bdsep .
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 , necon4d , necon4bd | ~ con3 | The form of contraposition which removes negation does not hold in intutionistic logic. | |
| pm2.18 | ~ pm2.01 | See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these. | |
| pm2.18d , pm2.18i | ~ pm2.01d | See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these. | |
| notnotrd , notnotri , notnotr , notnotb | ~ notnot | Double negation introduction holds but not double negation elimination. | |
| mt3d | ~ mtod | ||
| nsyl2 | ~ nsyl | ||
| mt4d | ~ mt2d | ||
| nsyl4 | ~ con1dc | ||
| pm2.61 , pm2.61d , pm2.61d1 , pm2.61d2 , pm2.61i , pm2.61ii , pm2.61nii , pm2.61iii , pm2.61ian , pm2.61dan , pm2.61ddan , pm2.61dda , pm2.61ine , pm2.61ne , pm2.61dne , pm2.61dane , pm2.61da2ne , pm2.61da3ne , pm2.61iine | none | If the proposition being eliminated is decidable (for example due to ~ nndceq , ~ zdceq , ~ zdcle , ~ zdclt , ~ eluzdc , or ~ fzdcel ), then case elimination will work using theorems such as ~ exmiddc and ~ mpjaodan | |
| dfbi1 , dfbi3 | ~ df-bi , ~ dfbi2 | ||
| 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 , ~ dfordc | ||
| imor , imori | ~ imorr , ~ imorri , ~ imordc | ||
| pm4.63 | ~ pm3.2im | ||
| iman | ~ imanim , ~ imanst | ||
| annim | ~ annimim | ||
| oran , pm4.57 | ~ oranim , ~ orandc | ||
| ianor | ~ pm3.14 , ~ ianordc | ||
| pm4.14 | ~ pm4.14dc , ~ pm3.37 | ||
| pm4.52 | ~ pm4.52im | ||
| pm4.53 | ~ pm4.53r | ||
| pm5.17 | ~ xorbin | The combination of ~ df-xor and ~ xorbin is the forward direction of pm5.17 | |
| biluk | ~ bilukdc | ||
| biadan | ~ biadani | The set.mm proof of biadan depends on biluk | |
| ecase | none | This is a form of case elimination. | |
| ecase3d | none | This is a form of case elimination. | |
| dedlem0b | ~ dedlemb | ||
| pm4.42 | ~ pm4.42r | ||
| 3ianor | ~ 3ianorr | ||
| df-nan and other theorems using NAND (Sheffer stroke) notation | none | A quick glance at the internet shows this mostly being used in the presence of excluded middle; in any case it is not currently present in iset.mm | |
| df-xor | ~ df-xor | Although the definition of exclusive or is called df-xor in both set.mm and iset.mm (at least currently), the definitions are not equivalent (in the absence of excluded middle). | |
| xnor | none | The set.mm proof uses theorems not in iset.mm. | |
| xorass | none | The set.mm proof uses theorems not in iset.mm. | |
| xor2 | ~ xoranor , ~ xor2dc | ||
| xornan | ~ xor2dc | ||
| xornan2 | none | See discussion under df-nan | |
| xorneg2 , xorneg1 , xorneg | none | The set.mm proofs use theorems not in iset.mm. | |
| xorexmid | none | A form of excluded middle | |
| df-ex | ~ exalim | ||
| alex | ~ alexim | ||
| exnal | ~ exnalim | ||
| alexn | ~ alexnim | ||
| exanali | ~ exanaliim | ||
| 19.35 , 19.35ri | ~ 19.35-1 | ||
| 19.30 | none | ||
| 19.39 | ~ i19.39 | ||
| 19.24 | ~ i19.24 | ||
| 19.36 , 19.36v | ~ 19.36-1 | ||
| 19.37 , 19.37v | ~ 19.37-1 | ||
| 19.32 | ~ 19.32r | ||
| 19.31 | ~ 19.31r | ||
| exdistrf | ~ exdistrfor | ||
| df-mo | ~ df-mo | The definitions are different although they currently share the same name. | |
| exmo | ~ exmonim | ||
| mof | ~ mo2r , ~ mo3 | ||
| df-eu , dfeu | ~ eu5 | Although this is a definition in set.mm and a theorem in iset.mm it is otherwise the same (with a different name). | |
| eu6 | ~ df-eu | Although this is a definition in iset.mm and a theorem in set.mm it is otherwise the same (with a different name). | |
| nfabd2 | ~ nfabd | ||
| nne | ~ nner , ~ nnedc | ||
| exmidne | ~ dcne | ||
| necon1ad | ~ necon1addc | ||
| necon1bd | ~ necon1bddc | ||
| necon4ad | ~ necon4addc | ||
| necon4bd | ~ necon4bddc | ||
| necon1d | ~ necon1ddc | ||
| necon4d | ~ necon4ddc | ||
| necon1ai | ~ necon1aidc | ||
| necon1bi | ~ necon1bidc | ||
| necon4ai | ~ necon4aidc | ||
| necon1i | ~ necon1idc | ||
| necon4i | ~ necon4idc | ||
| necon4abid | ~ necon4abiddc | ||
| necon4bbid | ~ necon4bbiddc | ||
| necon4bid | ~ necon4biddc , ~ apcon4bid | ||
| necon1abii | ~ necon1abiidc | ||
| necon1bbii | ~ necon1bbiidc | ||
| necon1abid | ~ necon1abiddc | ||
| necon1bbid | ~ necon1bbiddc | ||
| necon2abid | ~ necon2abiddc | ||
| necon2bbid | ~ necon2bbiddc | ||
| necon2abii | ~ necon2abiidc | ||
| necon2bbii | ~ necon2bbiidc | ||
| nebi | ~ nebidc | ||
| pm2.61ne, pm2.61ine, pm2.61dne, pm2.61dane, pm2.61da2ne, pm2.61da3ne | ~ pm2.61dc | ||
| neor | ~ pm2.53 , ~ ori , ~ ord | ||
| neorian | ~ pm3.14 | ||
| nnel | none | The reverse direction could be proved; the forward direction is double negation elimination. | |
| nfrald | ~ nfraldxy , ~ nfraldya | ||
| rexnal | ~ rexnalim | ||
| rexanali | none | ||
| nrexralim | none | ||
| dfral2 | ~ ralexim | ||
| dfrex2 | ~ rexalim , ~ dfrex2dc | ||
| nfrexd | ~ nfrexdxy , ~ nfrexdya | ||
| nfral | ~ nfralxy , ~ nfralya | ||
| nfra2 | ~ nfra1 , ~ nfralya | ||
| nfrex | ~ nfrexxy , ~ nfrexya | ||
| r19.30 | none | ||
| r19.35 | ~ r19.35-1 | ||
| ralcom2 | ~ ralcom | ||
| 2reuswap | ~ 2reuswapdc | ||
| rmo2 | ~ rmo2i | ||
| df-pss and all proper subclass theorems | none | In set.mm, "A is a proper subclass of B" is defined to be ` ( A C_ B /\ A =/= B ) ` and this definition is almost always used in conjunction with excluded middle. A more natural definition might be ` ( A C_ B /\ E. x x e. ( B \ A ) )` , if we need proper subclass at all. | |
| nss | ~ nssr | ||
| ddif | ~ ddifnel , ~ ddifss | ||
| df-symdif , dfsymdif2 | ~ symdifxor | The symmetric difference notation and a number of the theorems could be brought over from set.mm. | |
| dfss4 | ~ ssddif , ~ dfss4st | ||
| dfun3 | ~ unssin | ||
| dfin3 | ~ inssun | ||
| dfin4 | ~ inssddif | ||
| unineq | none | ||
| difindi | ~ difindiss | ||
| difdif2 | ~ difdif2ss | ||
| indm | ~ indmss | ||
| undif3 | ~ undif3ss | ||
| n0f | ~ n0rf | ||
| n0 | ~ n0r , ~ notm0 , ~ fin0 , ~ fin0or | ||
| neq0 | ~ neq0r | ||
| reximdva0 | ~ reximdva0m | ||
| ssdif0 | ~ ssdif0im | ||
| inssdif0 | ~ inssdif0im | ||
| abn0 | ~ abn0r , ~ abn0m | ||
| rabn0 | ~ rabn0m , ~ rabn0r | ||
| csb0 | ~ csbconstg , ~ csbprc | The set.mm proof uses excluded middle to combine the ` A e. _V ` and ` -. A e. _V ` cases. | |
| sbcel12 | ~ sbcel12g | ||
| sbcne12 | ~ sbcne12g | ||
| undif1 | ~ undif1ss | ||
| undif2 | ~ undif2ss | ||
| inundif | ~ inundifss | ||
| undif | ~ undifss | subset rather than equality, for any sets | |
| ~ undiffi | where both container and subset are finite | ||
| ~ undifdc | where the container has decidable equality and the subset is finite | ||
| ~ undifdcss | when membership in the subset is decidable | ||
| for any sets | implies excluded middle as shown at ~ undifexmid | ||
| forward direction only, for any sets | still implies excluded middle as shown at ~ exmidundifim | ||
| ssundif | ~ ssundifim | ||
| uneqdifeq | ~ uneqdifeqim | ||
| r19.2z | ~ r19.2m | ||
| r19.3rz | ~ r19.3rm | ||
| r19.28z | ~ r19.28m | ||
| r19.9rzv | ~ r19.9rmv | ||
| r19.37zv | ~ r19.3rmv | ||
| r19.45zv | ~ r19.45mv | ||
| r19.44zv | ~ r19.44mv | ||
| r19.27z | ~ r19.27m | ||
| r19.36zv | ~ r19.36av | ||
| dfif2 | ~ df-if | ||
| ifsb | ~ ifsbdc | ||
| dfif4 | none | Unused in set.mm | |
| dfif5 | none | Unused in set.mm | |
| ifeq1da | ~ ifeq1dadc | ||
| ifnot | none | ||
| ifor | none | ||
| ifeq2da | none | ||
| ifclda | ~ ifcldadc | ||
| ifeqda | none | ||
| elimif , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD | none | ||
| ifbothda | ~ ifbothdadc | ||
| ifboth | ~ ifbothdc | ||
| ifid | ~ ifiddc | ||
| eqif | ~ eqifdc | ||
| ifcl , ifcld | ~ ifcldcd , ~ ifcldadc | ||
| ifan | ~ ifandc | ||
| dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel | none | Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form. | |
| ifex , ifexg | ~ ifcldcd , ~ ifcldadc | ||
| ifpr | none | Should be provable if the condition is decidable. | |
| difsnid | ~ difsnss | One direction, for any set | |
| ~ nndifsnid | for a natural number | ||
| ~ dcdifsnid | for a set with decidable equality | ||
| ~ fidifsnid | for a finite set | ||
| pwpw0 | ~ pwpw0ss | ||
| sssn | ~ sssnr | One direction, for any classes. | |
| ~ sssnm | When the subset is inhabited. | ||
| for all sets | Equivalent to excluded middle by ~ exmidsssn . | ||
| ssunsn2 , ssunsn | none | ||
| eqsn | ~ eqsnm | ||
| ssunpr | none | ||
| sspr | ~ ssprr | ||
| sstp | ~ sstpr | ||
| prnebg | none | ||
| pwsn | ~ pwsnss | Also see ~ exmidpw | |
| pwpr | ~ pwprss | ||
| pwtp | ~ pwtpss | ||
| pwpwpw0 | ~ pwpwpw0ss | ||
| iundif2 | ~ iundif2ss | ||
| iindif2 | ~ iindif2m | ||
| iinin2 | ~ iinin2m | ||
| iinin1 | ~ iinin1m | ||
| iinvdif | ~ iindif2m | Unused in set.mm | |
| riinn0 | ~ riinm | ||
| riinrab | ~ iinrabm | ||
| iinuni | ~ iinuniss | ||
| iununi | ~ iununir | ||
| rintn0 | ~ rintm | ||
| disjor | ~ disjnim | ||
| disjors | ~ disjnims | ||
| disji | none | ||
| disjprg , disjxiun , disjxun | none | ||
| disjss3 | none | Might need to be restated or have decidability conditions added | |
| trintss | ~ trintssm | ||
| ax-rep | ~ ax-coll | There are a lot of ways to state replacement and most/all of them hold, for example ~ zfrep6 or ~ funimaexg . | |
| csbexg , csbex | ~ csbexga , ~ csbexa | set.mm uses case elimination to remove the ` A e. _V ` condition. | |
| intex | ~ inteximm , ~ intexr | inteximm is the forward direction (but for inhabited rather than non-empty classes) and intexr is the reverse direction. | |
| intexab | ~ intexabim | ||
| intexrab | ~ intexrabim | ||
| iinexg | ~ iinexgm | Changes not empty to inhabited | |
| intabs | none | Lightly used in set.mm, and the set.mm proof is not intuitionistic | |
| reuxfr2d , reuxfr2 , reuxfrd , reuxfr | none | The set.mm proof of reuxfr2d relies on 2reuswap | |
| moabex | ~ euabex | In general, most of the set.mm ` E! ` theorems still hold, but a decent number of the ` E* ` ones get caught up on "there are two cases: the set exists or it does not" | |
| snex | ~ snexg , ~ snex | The iset.mm version of ~ snex has an additional hypothesis. We conjecture that the set.mm snex ( ` { A } e. _V ` with no condition on whether ` A ` is a set) is not provable. The axioms of set theory allow us to construct rank levels from others, but not to construct something from nothing (except the 0 rank and stuff you can bootstrap from there). A class provides no "data" about where it lives, because it is spread out over the whole universe - you only get the ability to ask yes-no(-maybe) questions about set membership in the class. An assertion that a class exists is a piece of data that gives you a bound on the rank of this set, which can be used to build other existing things like unions and powersets of this class and so on. Anything with unbounded rank cannot be proven to exist. So snex, which starts from an arbitrary class and produces evidence that { A } exists, cannot be provable, because the bound here can't depend on A and cannot be upper bounded by anything independent of A either - there are singletons at every rank. However, we can refute a singleton being a proper class - see ~ notnotsnex . |
|
| nssss | ~ nssssr | ||
| rmorabex | ~ euabex | See discussion under moabex | |
| nnullss | ~ mss | ||
| opex | ~ opexg , ~ opex | The iset.mm version of ~ opex has additional hypotheses | |
| otex | ~ otexg | ||
| opnz | ~ opm , ~ opnzi | ||
| df-so | ~ df-iso | Although we define ` Or ` to describe a weakly linear order (such as real numbers), there are some orders which are also trichotomous, for example ~ nntri3or , ~ pitri3or , and ~ nqtri3or . | |
| sotric | ~ sotricim | One direction, for any weak linear order. | |
| ~ sotritric | For a trichotomous order. | ||
| ~ nntri2 | For the specific order ` _E Or _om ` | ||
| ~ pitric | For the specific order ` | ||
| ~ 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 | ~ df-frind | ||
| fri , dffr2 , frc | none | That any subset of the base set has an element which is minimal accordng to a well-founded relation presumably implies excluded middle (or is otherwise unprovable). | |
| frss | ~ freq2 | Because the definition of ` Fr ` is different than set.mm, the proof would need to be different. | |
| frirr | ~ frirrg | We do not yet have a lot of theorems for the case where ` A ` is a proper class. | |
| fr2nr | none | Shouldn't be hard to prove if we need it (using a proof similar to ~frirrg and ~ en2lp ). | |
| frminex | none | Presumably unprovable. | |
| efrn2lp | none | Should be easy but lightly used in set.mm | |
| dfepfr , epfrc | none | Presumably unprovable. | |
| df-we | ~ df-wetr | ||
| wess | none | See frss entry. Holds for ` _E ` (see for example ~ wessep ). | |
| weso | ~ wepo | ||
| wecmpep | none | ` We ` does not imply trichotomy in iset.mm | |
| wefrc , wereu , wereu2 | none | Presumably not provable | |
| dmxp | ~ dmxpm | ||
| relimasn | ~ imasng | ||
| xpnz | ~ xpm | ||
| xpeq0 | ~ xpeq0r , ~ sqxpeq0 | ||
| difxp | none | The set.mm proof relies on ianor | |
| rnxp | ~ rnxpm | ||
| ssxpb | ~ ssxpbm | ||
| xp11 | ~ xp11m | ||
| xpcan | ~ xpcanm | ||
| xpcan2 | ~ xpcan2m | ||
| xpima2 | ~ xpima2m | ||
| sossfld , sofld , soex | none | the set.mm proofs rely on trichotomy | |
| csbrn | ~ csbrng | ||
| dmsnn0 | ~ dmsnm | ||
| rnsnn0 | ~ rnsnm | ||
| relsn2 | ~ relsn2m | ||
| dmsnopss | ~ dmsnopg | The domain is empty in the ` -. B e. _V ` case which follows readily from ~ opprc2 and ~ dmsn0 . But we presumably cannot combine the ` B e. _V ` and ` -. B e. _V ` cases (set.mm uses excluded middle to do so). | |
| dmsnsnsn | ~ dmsnsnsng | ||
| opswap | ~ opswapg | ||
| unixp | ~ unixpm | ||
| cnvso | ~ cnvsom | ||
| unixp0 | ~ unixp0im | ||
| unixpid | none | We could prove the theorem for the case where A is inhabited | |
| cnviin | ~ cnviinm | ||
| xpco | ~ xpcom | ||
| xpcoid | ~ xpcom | ||
| tz7.7 | none | ||
| ordelssne | none | ||
| ordelpss | none | ||
| ordsseleq , onsseleq | ~ onelss , ~ eqimss , ~ nnsseleq | Taken together, ~ onelss and ~ eqimss represent the reverse direction of the biconditional from ordsseleq . For natural numbers the biconditional is provable. | |
| ordtri3or | ~ nntri3or | Ordinal trichotomy implies the law of the excluded middle as shown in ~ ordtriexmid . | |
| ordtri2 | ~ nntri2 | ordtri2 for all ordinals presumably implies excluded middle although we don't have a specific proof analogous to ~ ordtriexmid . | |
| ordtri3 , ordtri4 , ordtri2or3 , dford2 | none | Ordinal trichotomy implies the law of the excluded middle as shown in ~ ordtriexmid . We don't have similar proofs for every variation of of trichotomy but most of them are presumably powerful enough to imply excluded middle. | |
| ordtri1 , ontri1 , onssneli , onssnel2i | ~ ssnel , ~ nntri1 | ~ ssnel is a 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 | ~ nntr2 | ontr2 implies excluded middle as shown at ~ ontr2exmid | |
| ordtr3 | none | This is weak linearity of ordinals, which presumably implies excluded middle by ~ ordsoexmid . | |
| ord0eln0 , on0eln0 | ~ ne0i , ~ nn0eln0 | ||
| nsuceq0 | ~ nsuceq0g | ||
| ordsssuc | ~ trsucss , ~ nnsssuc | ||
| ordequn | none | If you know which ordinal is larger, you can achieve a similar result via theorems such as ~ oneluni or ~ ssequn1 . | |
| ordun | ~ onun2 | ||
| ordtri2or | none | Implies excluded middle as shown at ~ ordtri2orexmid . | |
| ordtri2or2 | ~ nntri2or2 | ordtri2or2 implies excluded middle as shown at ~ ordtri2or2exmid . | |
| onsseli | none | See entry for ordsseleq | |
| unizlim | none | The reverse direction is basically ~ uni0 plus ~ limuni | |
| on0eqel | ~ 0elnn | The full on0eqel is conjectured to imply excluded middle by an argument similar to ~ ordtriexmid | |
| snsn0non | none | Presumably would be provable (by first proving ` -. (/) e. { { (/) } } ` as in the set.mm proof, and then using that to show that ` { { (/) } } ` is not a transitive set). | |
| onxpdisj | none | Unused in set.mm | |
| onnev | none | Presumably provable (see snsn0non entry) | |
| iotaex | ~iotacl , ~ euiotaex | ||
| dffun3 | ~ dffun5r | ||
| dffun5 | ~ dffun5r | ||
| resasplit | ~ resasplitss | ||
| fresaun | none | The set.mm proof relies on resasplit | |
| fresaunres2 , fresaunres1 | none | The set.mm proof relies on resasplit | |
| fint | ~ fintm | ||
| foconst | none | Although it presumably holds if non-empty is changed to inhabited, it would need a new proof and it is unused in set.mm. | |
| f1oprswap | none | The ` A =/= B ` case is handled (basically) by ~ f1oprg . If there is a proof of the original f1oprswap which does not rely on case elimination, it would look very different from the set.mm proof. | |
| dffv3 | ~ dffv3g | ||
| fvex | ~ funfvex | when evaluating a function within its domain | |
| ~ fvexg , ~ fvex | when the function is a set and is evaluated at a set | ||
| ~ relrnfvex | when evaluating a relation whose range is a set | ||
| ~ mptfvex | when the function is defined via maps-to, yields a set for all inputs, and is evaluated at a set | ||
| ~ 1stexg , ~ 2ndexg | for the functions ` 1st ` and ` 2nd ` | ||
| ~ slotex | for a slot of an extensible structure | ||
| fvexi , fvexd | see fvex | ||
| fvif | ~ fvifdc | ||
| fvrn0 | none | The set.mm proof uses case elimination on whether ` ( F `` X ) ` is the empty set. | |
| fvssunirn | ~ fvssunirng , ~ relfvssunirn | ||
| ndmfv | ~ ndmfvg | The ` -. A e. _V ` case is ~ fvprc . | |
| elfvdm | ~ relelfvdm | ||
| elfvex , elfvexd | ~ relelfvdm , ~ mptrcl | ||
| dffn5 | ~ dffn5im | ||
| fvmpti | ~ fvmptg | The set.mm proof relies on case elimination on ` C e. _V ` | |
| fvmpt2i | ~ fvmpt2 | The set.mm proof relies on case elimination on ` C e. _V ` | |
| fvmptss | ~ fvmptssdm | ||
| fvmptex | none | The set.mm proof relies on case elimination | |
| fvmptnf | none | The set.mm proof relies on case elimination | |
| fvmptn | none | The set.mm proof relies on case elimination | |
| fvmptss2 | ~ fvmpt | What fvmptss2 adds is the cases where this is a proper class, or we are out of the domain. | |
| fvopab4ndm | none | ||
| fndmdifeq0 | none | Although it seems like this might be intuitionizable, it is lightly used in set.mm. | |
| f0cli | ~ ffvelrn | ||
| dff3 | ~ dff3im | ||
| dff4 | ~ dff4im | ||
| fvunsn | ~ fvunsng | ||
| fnsnsplit | ~ fnsnsplitss | Subset rather than equality, for a function on any set. | |
| ~ fnsnsplitdc | For a function on a set with decidable equality. | ||
| fsnunf2 | none | Apparently would need decidable equality on ` S ` or some other condition. | |
| funresdfunsn | ~ funresdfunsnss | Subset rather than equality, for a function on any set. | |
| ~ funresdfunsndc | For a function on a set with decidable equality. | ||
| funiunfv | ~ fniunfv , ~ funiunfvdm | ||
| funiunfvf | ~ funiunfvdmf | ||
| eluniima | ~ eluniimadm | ||
| dff14a , dff14b | none | The set.mm proof depends, in an apparently essential way, on excluded middle. | |
| fveqf1o | none | The set.mm proof relies on f1oprswap , which we don't have | |
| soisores | ~ isoresbr | ||
| soisoi | none | The set.mm proof relies on trichotomy | |
| isocnv3 | none | It seems possible that one direction of the biconditional could be proved. | |
| isomin | none | ||
| riotaex | ~ riotacl , ~ riotaexg | ||
| nfriotad | ~ nfriotadxy | ||
| csbriota , csbriotagOLD | ~ csbriotag | ||
| riotaxfrd | none | Although it may be intuitionizable, it is lightly used in set.mm. The set.mm proof relies on reuxfrd . | |
| ovex | ~ fnovex | when the operation is a function evaluated within its domain. | |
| ~ ovexg | when the operation is a set and is evaluated at a set | ||
| ~ relrnfvex | when the operation is a relation whose range is a set | ||
| ~ mpt2fvex | When the operation is defined via maps-to, yields a set on any inputs, and is being evaluated at two sets. | ||
| ~ addcl , ~ expcl , etc | If there is a closure theorem for a particular operation, that is often the way to intuitionize ovex (check for your particular operation, as these are just a few examples). | ||
| ovrcl | ~ elmpocl , ~ relelfvdm | ||
| 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 | ~ elmpocl , ~ relelfvdm | ||
| caov4 | ~ caov4d | Note that ~ caov4d has a closure hypothesis. | |
| caov411 | ~ caov411d | Note that ~ caov411d has a closure hypothesis. | |
| caov42 | ~ caov42d | Note that ~ caov42d has a closure hypothesis. | |
| caovdir | ~ caovdird | ~ caovdird adds some constraints about where the operations are evaluated. | |
| caovdilem | ~ caovdilemd | ||
| caovlem2 | ~ caovlem2d | ||
| caovmo | ~ caovimo | ||
| mpondm0 | none | could be proved, but usually is used in conjunction with excluded middle | |
| elovmporab | none | could be proved, but unused in set.mm | |
| elovmporab1 | none | could be proved | |
| 2mpo0 | none | Possibly provable, but an inhabited set version would be more likely to be helpful (if anything is). | |
| relmptopab | none | Presumably would need a condition that ` B e. dom F ` | |
| ofval | ~ fnofval | ||
| offn , offveq , caofid0l , caofid0r , caofid1 , caofid2 | none | Assuming we really need to add conditions that the operations are functions being evaluated within their domains, there would be a fair bit of intuitionizing. | |
| ordeleqon | none | ||
| ssonprc | none | not provable (we conjecture), but interesting enough to intuitionize anyway. ` U. A = On -> A e/ V ` is provable, and ` ( B e. On /\ U. A C_ B ) -> A e. V ` is provable. (One thing we presumably could prove is ` ( U. A C_ On /\ E. x x e. ( On \ U. A ) ) -> A e. V ` which might be easier to understand if we define (or think of) proper subset as meaning that the set difference is inhabited.) | |
| onint | ~ onintss | onint implies excluded middle as shown in ~ onintexmid . | |
| onint0 | none | Thought to be "trivially not intuitionistic", and it is not clear if there is an alternate way to state it that is true. If the empty set is in A then of course |^| A = (/), but the converse seems difficult. I don't know so much about the structure of the ordinals without linearity, | |
| onssmin, onminesb, onminsb | none | Conjectured to not be provable without excluded middle, for the same reason as onint. | |
| oninton | ~ onintonm | ||
| onintrab | none | The set.mm proof relies on the converse of ~ inteximm . | |
| onintrab2 | ~ onintrab2im | The converse would appear to need the converse of ~ inteximm . | |
| oneqmin | none | Falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum. | |
| onminex | none | ||
| onmindif2 | none | Conjectured to not be provable without excluded middle. | |
| onmindif2 | none | Conjectured to not be provable without excluded middle. | |
| ordpwsuc | ~ ordpwsucss | See the ~ ordpwsucss comment for discussion of the succcessor-like properites of ` ( ~P A i^i On ) ` . Full ordpwsuc implies excluded middle as seen at ~ ordpwsucexmid . | |
| ordsucelsuc | ~ onsucelsucr , ~ nnsucelsuc | The converse of ~ onsucelsucr implies excluded middle, as shown at ~ onsucelsucexmid . | |
| ordsucsssuc | ~ onsucsssucr , ~ nnsucsssuc | The converse of ~ onsucsssucr implies excluded middle, as shown at ~ onsucsssucexmid . | |
| ordsucuniel | ~ sucunielr , ~ nnsucuniel | Full ordsucuniel implies excluded middle, as shown at ~ ordsucunielexmid . | |
| ordsucun | none yet | Conjectured to be provable in the reverse direction, but not the forward direction (implies some order totality). | |
| ordunpr | none | Presumably not provable without excluded middle. | |
| ordunel | none | Conjectured to not be provable (ordunel implies ordsucun). | |
| onsucuni, ordsucuni | none | Conjectured to not be provable without excluded middle. | |
| orduniorsuc | none | Presumably not provable. | |
| ordunisuc | ~ onunisuci , ~ unisuc , ~ unisucg | ||
| orduniss2 | ~ onuniss2 | ||
| 0elsuc | none | This theorem may appear to be innocuous but it implies excluded middle as shown at ~ 0elsucexmid . | |
| onuniorsuci | none | Conjectured to not be provable without excluded middle. | |
| onuninsuci, orduninsuc | none | Conjectured to be provable in the forward direction but not the reverse one. | |
| ordunisuc2 | ~ ordunisuc2r | The forward direction is conjectured to imply excluded middle. Here is a sketch of the proposed proof. Let om' be the set of all finite iterations of suc' A = ` ( ~P A i^i On ) ` on ` (/) `. (We can formalize this proof but not until we have om and at least finite induction.) Then om' = U. om' because if x e. om' then x = suc'^n (/) for some n, and then x C_ suc'^n (/) implies x e. suc'^(n+1) (/) e. om' so x e. U. om'.
Now supposing the theorem, we know that A. x e. om' suc x e. om', so in particular 2o e. om', that is, 2o = suc'^n (/) for some n. (Note that 1o = suc' (/) - see ~ pw0 .) For n = 0 and n = 1 this is clearly false, and for n = m+3 we have 1o e. suc' suc' (/) , so 2o C_ suc' suc' (/), so 2o e. suc' suc' suc' (/) C_ suc' suc' suc' suc'^m (/) = 2o, contradicting ordirr. Thus 2o = suc' suc' (/) = suc' 1o. Applying this to X = ` { x e. { (/) } | ph } ` we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ~ ordtriexmidlem2 for ` X = (/) ` and ~ rabsnt as seen in the ~ onsucsssucexmid proof for ` X = 1o ` ). |
|
| ordzsl, onzsl, dflim3, nlimon | none | ||
| dflim4 | ~ df-ilim | We conjecture that dflim4 is not equivalent to ~ df-ilim . | |
| limsuc | none | This would be trivial if dflim4 were the definition of a limit ordinal. With ~ dflim2 as the definition, limsuc might need ordunisuc2 (which we believe is not provable, see its entry in this list). | |
| limsssuc | none | Conjectured to be provable (is this also based on dflim4 being the definition of limit ordinal or is it unrelated?). | |
| tfinds , tfindsg | ~ tfis3 | We are unable to separate limit and successor ordinals using case elimination. | |
| findsg | ~ uzind4 | findsg presumably could be proved, but there hasn't been a need for it. | |
| xpexr | none | ||
| 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. | |
| ovmptss | none | The set.mm proof relies on fvmptss | |
| relmpt2opab | none | The set.mm proof relies on ovmptss | |
| 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 | ||
| omopth2 | none | The set.mm proof relies on ordinal trichotomy. | |
| omeulem1 , omeu | none | The set.mm proof relies on ordinal trichotomy, omopth2 , oaord , and other theorems we don't have. | |
| suc11reg | ~ suc11g | ||
| frfnom | ~ frecfnom | frecfnom adopts the ` frec ` notation and adds conditions on the characteristic function and initial value. | |
| fr0g | ~ frec0g | frec0g adopts the ` frec ` notation and adds a condition on the characteristic function. | |
| frsuc | ~ frecsuc | frecsuc adopts the ` frec ` notation and adds conditions on the characteristic function and initial value. | |
| om0x | ~ om0 | ||
| oa0r | none | The set.mm proof distinguishes between limit and successor cases using case elimination. | |
| oaordi | ~ nnaordi | The set.mm proof of oaordi relies on being able to distinguish between limit ordinals and successor ordinals via case elimination. | |
| oaord | ~ nnaord | The set.mm proof of oaord relies on ordinal trichotomy. | |
| oawordri | none | Implies excluded middle as shown at ~ oawordriexmid | |
| oaword | ~ oawordi | The other direction presumably could be proven but isn't yet. | |
| oaord1 | none yet | ||
| oaword2 | none | The set.mm proof relies on oawordri and oa0r | |
| oawordeu | none | The set.mm proof relies on a number of things we don't have | |
| oawordex | ~ nnawordex | The set.mm proof relies on oawordeu | |
| omwordi | ~ nnmword | The set.mm proof of omwordi relies on case elimination. | |
| omword1 | ~ nnmword | ||
| oawordex | ~ nnawordex | ||
| swoso | none | Unused in set.mm. | |
| ecdmn0 | ~ ecdmn0m | ||
| erdisj, qsdisj, qsdisj2, uniinqs | none | These could presumably be restated to be provable, but they are lightly used in set.mm | |
| iiner | ~ iinerm | ||
| riiner | ~ riinerm | ||
| brecop2 | none | This is a form of reverse closure and uses excluded middle in its proof. | |
| erov , erov2 | none | Unused in set.mm. | |
| eceqoveq | none | Unused in set.mm. | |
| ralxpmap | none | Lightly used in set.mm. The set.mm proof relies on fnsnsplit and undif . | |
| nfixp | ~ nfixpxy , ~ nfixp1 | set.mm (indirectly) uses excluded middle to combine the cases where ` x ` and ` y ` are distinct and where they are not. | |
| ixpexg | ~ ixpexgg | ||
| ixpiin | ~ ixpiinm | ||
| ixpint | ~ ixpintm | ||
| ixpn0 | ~ ixpm | ||
| undifixp | none | The set.mm proof relies on undif | |
| resixpfo | none | The set.mm proof relies on membership in ` B ` being decidable and would need to have nonempty changed to inhabited, but might be adaptable with those conditions added. However, this theorem is currently only used in the proof of Tychonoff's Theorem, which we do not expect to be able to prove. | |
| boxriin | none | Would seem to need a condition that ` I ` has decidable equality. | |
| boxcutc | none | Would seem to need a condition that ` A ` has decidable equality. | |
| 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 | ||
| snfi | ~ snfig | ||
| difsnen | ~ fidifsnen | ||
| undom | none | The set.mm proof uses undif2 and we just have ~ undif2ss | |
| xpdom3 | ~ xpdom3m | ||
| domunsncan | none | The set.mm proof relies on difsnen | |
| omxpenlem , omxpen , omf1o | none | The set.mm proof relies on omwordi , oaord , om0r , and other theorems we do not have | |
| pw2f1o , pw2eng , pw2en | none | Presumably would require some kind of decidability hypothesis. Discussions of this sort tend to get into how many truth values there are and sets like ` { s | s C_ 1o } ` (relatively undeveloped so far except for a few results like ~ exmid01 and ~ uni0b ). | |
| enfixsn | none | The set.mm proof relies on difsnen | |
| sbth and its lemmas, sbthb , sbthcl | ~ fisbth | The Schroeder-Bernstein Theorem is equivalent to excluded middle by ~ exmidsbth | |
| fodomr | none | Equivalent to excluded middle per ~ exmidfodomr | |
| mapdom1 | ~ mapdom1g | ||
| 2pwuninel | ~ 2pwuninelg | ||
| mapunen | none | The set.mm proof relies on fresaunres1 and fresaunres2 . | |
| map2xp | none | The set.mm proof relies on mapunen | |
| mapdom2 , mapdom3 | none | The set.mm proof relies on case elimination and undif . At a minimum, it would appear that nonempty would need to be changed to inhabited. | |
| pwen | none | The set.mm proof relies on pw2eng | |
| limenpsi | none | The set.mm proof relies on sbth | |
| limensuci , limensuc | none | The set.mm proof relies on undif | |
| infensuc | none | The set.mm proof relies on limensuc | |
| php | ~ phpm | ||
| snnen2o | ~ snnen2og , ~ snnen2oprc | ||
| onomeneq , onfin , onfin2 | none | The set.mm proofs rely on excluded middle | |
| nnsdomo , sucdom2 , sucdom , 0sdom1dom , sdom1 | none | iset.mm doesn't yet have strict dominance | |
| 1sdom2 | ~ 1nen2 | Although the presence of ~ 1nen2 might make it look like a natural definition for strict dominance would be ` A ~<_ B /\ -. A ~~ B ` , that definition may be more suitable for finite sets than all sets, so at least for now we only define ` ~~ ` and express certain theorems (such as this one) in terms of equinumerosity which in set.mm are expressed in terms of strict dominance. | |
| modom , modom2 | none | The set.mm proofs rely on excluded middle | |
| 1sdom , unxpdom , unxpdom2 , sucxpdom | none | iset.mm doesn't yet have strict dominance | |
| pssinf | none | The set.mm proof relies on sdomnen | |
| isinf | ~ isinfinf | ||
| fineqv | none | The set.mm proof relies on theorems we don't have, and even for the theorems we do have, we'd need to carefully look at what axioms they rely on. | |
| pssnn | none | The set.mm proof uses excluded middle. | |
| ssnnfi | none | The proof in ~ ssfiexmid would apply to this as well as to ssfi , since ` { (/) } e. _om ` | |
| ssfi | ~ ssfirab | when the subset is defined by a decidable property | |
| ~ ssfidc | when membership in the subset is decidable | ||
| for the general case | Implies excluded middle as shown at ~ ssfiexmid | ||
| domfi | none | Implies excluded middle as shown at ~ domfiexmid | |
| xpfir | none | Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi | |
| infi | none | Implies excluded middle as shown at ~ infiexmid . It is conjectured that we could prove the special case ` ( A e. Fin /\ B e. Fin /\ ( A u. B ) e. Fin ) -> ( A i^i B ) e. Fin ` | |
| rabfi | none | Presumably the proof of ~ ssfiexmid could be adapted to show this implies excluded middle | |
| finresfin | none | The set.mm proof is in terms of ssfi | |
| f1finf1o | none | The set.mm proof is not intuitionistic | |
| nfielex | none | The set.mm proof relies on neq0 | |
| diffi | ~ diffisn , ~ diffifi | diffi is not provable, as shown at ~ diffitest | |
| enp1ilem , enp1i , en2 , en3 , en4 | none | The set.mm proof relies on excluded middle and undif1 | |
| findcard3 | none | The set.mm proof is in terms of strict dominance. | |
| frfi | none | Not known whether this can be proved (either with the current ~ df-frind or any other possible concept analogous to ` Fr ` ). | |
| fimax2g | ~ fimax2gtri | ||
| fimaxg | none | The set.mm proof of fimaxg relies on fimax2g which relies on frfi and fri | |
| fisupg | none | The set.mm proof relies on excluded middle and presumably this theorem would need to be modified to be provable. | |
| unbnn | none | the impossibility proof at ~ exmidunben should apply here as well | |
| unbnn2 | none | the impossibility proof at ~ exmidunben should apply here as well | |
| unfi | ~ unsnfi | For the union of a set and a singleton whose element is not a member of that set | |
| ~ unfidisj | For the union of two disjoint sets | ||
| ~ unfiin | When the intersection is known to be finite | ||
| for any two finite sets | Implies excluded middle as shown at ~ unfiexmid . | ||
| difinf | ~ difinfinf | ||
| prfi | ~ prfidisj | for two unequal sets | |
| in general | The set.mm proof depends on unfi and it would appear that mapping ` { A , B } ` to a natural number would decide whether ` A ` and ` B ` are equal and thus imply any set has decidable equality. | ||
| tpfi | ~ tpfidisj | ||
| fiint | ~ fiintim | ||
| fodomfi | none | Might be provable, for example via ~ ac6sfi or induction directly. The set.mm proof does use undom in addition to induction. | |
| fofinf1o | none | The set.mm proof uses excluded middle in several places. | |
| dmfi | ~ fundmfi | ||
| resfnfinfin | ~ resfnfinfinss | ||
| residfi | none | Presumably provable, but lightly used in set.mm | |
| cnvfi | ~ relcnvfi | ||
| rnfi | ~ funrnfi | ||
| fofi | ~ f1ofi | Presumably precluded by an argument similar to ~ domfiexmid (the set.mm proof relies on domfi). | |
| iunfi | ~ iunfidisj | for a disjoint collection | |
| in general | Presumably not possible for the same reasons as in ~ unfiexmid | ||
| unifi | none | Presumably the issues are similar to iunfi | |
| pwfi | none | The set.mm proof uses domfi and other theorems we don't have | |
| abrexfi | none | At first glance it would appear that the mapping would need to be one to one or some other condition. | |
| fisuppfi | ~ preimaf1ofi | The set.mm proof of fisuppfi uses ssfi | |
| df-fi and all theorems using the fi (class of finite intersections) notation | none | Although some of these theorems could be intuitionized if there is a need, others rely on excluded middle in apparently essential ways. | |
| dfsup2 | none | The set.mm proof uses excluded middle in several places and the theorem is lightly used in set.mm. | |
| supmo | ~ supmoti | The conditions on the order are different. | |
| supexd , supex | none | The set.mm proof uses rmorabex | |
| supeu | ~ supeuti | ||
| supval2 | ~ supval2ti | ||
| eqsup | ~ eqsupti | ||
| eqsupd | ~ eqsuptid | ||
| supcl | ~ supclti | ||
| supub | ~ supubti | ||
| suplub | ~ suplubti | ||
| suplub2 | ~ suplub2ti | ||
| supnub | none | Presumably provable, although the set.mm proof relies on excluded middle and it is not used until later in set.mm. | |
| sup0riota , sup0 , infempty | none | Suitably modified verions may be provable, but they are unused in set.mm. | |
| supmax | ~ supmaxti | ||
| fisup2g , fisupcl | none | Other variations may be possible, but the set.mm proof will not work as-is or with small modifications. | |
| supgtoreq | none | The set.mm proof uses fisup2g and also trichotomy. | |
| suppr | none | The formulation using ` if ` would seem to require a trichotomous order. For real numbers, supremum on a pair does yield the maximum of two numbers: see ~ maxcl , ~ maxle1 , ~ maxle2 , ~ maxleast , and ~ maxleb . | |
| supiso | ~ supisoti | ||
| infexd , infex | none | See supexd | |
| eqinf , eqinfd | ~ eqinfti , ~ eqinftid | ||
| infval | ~ infvalti | ||
| infcllem | ~ cnvinfex | infcllem has an unnecessary hypothesis; other than that these are the same | |
| infcl | infclti | ||
| inflb | ~ inflbti | ||
| infglb | ~ infglbti | ||
| infglbb | none | Presumably provable with additional conditions (see suplub2) | |
| infnlb | ~ infnlbti | ||
| infmin | ~ infminti | ||
| infmo | ~ infmoti | ||
| infeu | ~ infeuti | ||
| fimin2g , fiming | none | The set.mm proof relies on frfi and fri | |
| fiinfg , fiinf2g | none | The set.mm proof relies on fiming | |
| fiinfcl | none | See fisupcl | |
| infltoreq | none | The set.mm proof depends on supgtoreq and fiinfcl | |
| infpr | none | See suppr | |
| infsn | ~ infsnti | ||
| infiso | ~ infisoti | ||
| ax-reg , axreg2 , zfregcl | ~ ax-setind | ax-reg implies excluded middle as seen at ~ regexmid | |
| unbnn3 | none | the impossibility proof at ~ exmidunben should apply here as well | |
| df-rank and all theorems related to the rank function | none | One possible definition is Definition 9.3.4 of [AczelRathjen], p. 91 | |
| df-aleph and all theorems involving aleph | none | ||
| df-cf and all theorems involving cofinality | none | ||
| df-acn and all theorems using this definition | none | ||
| cardf2 , cardon , isnum2 | ~ cardcl , ~ isnumi | It would also be easy to prove ` Fun card ` if there is a need. | |
| ennum | none | The set.mm proof relies on isnum2 | |
| tskwe | none | Relies on df-sdom | |
| xpnum | none | The set.mm proof relies on isnum2 | |
| cardval3 | ~ cardval3ex | ||
| cardid2 | none | The set.mm proof relies on onint | |
| isnum3 | none | ||
| oncardid | none | The set.mm proof relies on cardid2 | |
| cardidm | none | Presumably this would need a condition on ` A ` but even with that, the set.mm proof relies on cardid2 | |
| oncard | none | The set.mm proof relies on theorems we don't have, and this theorem is unused in set.mm. | |
| ficardom | none | Both the set.mm proof, and perhaps some possible alternative proofs, rely on onomeneq and perhaps other theorems we don't have currently. | |
| ficardid | none | The set.mm proof relies on cardid2 | |
| cardnn | none | The set.mm proof relies on a variety of theorems we don't have currently. | |
| cardnueq0 | none | The set.mm proof relies on cardid2 | |
| cardne | none | The set.mm proof relies on ordinal trichotomy (and if that can be solved there might be some more minor problems which require revisions to the theorem) | |
| carden2a | none | The set.mm proof relies on excluded middle. | |
| carden2b | ~ carden2bex | ||
| card1 , cardsn | none | Rely on a variety of theorems we don't currently have. Lightly used in set.mm. | |
| carddomi2 | none | The set.mm proof relies on excluded middle. | |
| sdomsdomcardi | none | Relies on a variety of theorems we don't currently have. | |
| prdom2 | none | The set.mm proof would only work in the case where ` A = B ` is decidable. If we can prove fodomfi , that would appear to imply prsomd2 fairly quickly. | |
| dif1card | none | The set.mm proof relies on cardennn | |
| leweon | none | We lack the well ordering related theorems this relies on, and it isn't clear they are provable. | |
| r0weon | none | We lack the well ordering related theorems this relies on, and it isn't clear they are provable. | |
| infxpen | none | The set.mm proof relies on well ordering related theorems that we don't have (and may not be able to have), and it isn't clear that infxpen is provable. | |
| infxpidm2 | none | Depends on cardinality theorems we don't have. | |
| infxpenc | none | Relies on notations and theorems we don't have. | |
| infxpenc2 | none | Relies on theorems we don't have. | |
| dfac8a | none | The set.mm proof does not work as-is and numerability may not be able to work the same way. | |
| dfac8b | none | We are lacking much of what this proof relies on and we may not be able to make numerability and well-ordering work as in set.mm. | |
| dfac8c | none | The set.mm proof does not work as-is and well-ordering may not be able to work the same way. | |
| ac10ct | none | The set.mm proof does not work as-is and well-ordering may not be able to work the same way. | |
| ween | none | The set.mm proof does not work as-is and well-ordering and numerability may not be able to work the same way. | |
| ac5num , ondomen , numdom , ssnum , onssnum , indcardi | none | Numerability (or cardinality in general) is not well developed and to a certain extent cannot be. | |
| df-cda | ~ df-dju | df-cda and df-dju are essentially the same. Current thinking is that we want to remove df-cda and the +c syntax from set.mm in favor of df-dju and use ` |_| ` in much the same way that cardinal multiplication uses the df-xp ( ` X. ` ) syntax rather than having a notation specific to cardinals. | |
| cdafn | ~ djuex | Since ` |_| ` is defined on proper classes, the similarity here is somewhat approximate. | |
| cdaval | ~ df-dju | ||
| cdadju | none | not needed as iset.mm does not have df-cda | |
| uncdadom , undjudom | none | The set.mm proof relies on undom | |
| cdaun | ~ endjudisj | ||
| cdaen | ~ djuen | ||
| cdaenun | ~ djuenun | ||
| cda1en | ~ dju1en | ||
| cda1dif | none | ||
| dju1dif | none | presumably provable | |
| cda0en | ~ dju0en | ||
| xp2cda | ~ xp2dju | ||
| cdacomen | ~ djucomen | ||
| cdaassen | ~ djuassen | ||
| cdadom3 | ~ djudoml | ||
| fodom , fodomnum | none | Presumably not provable as stated | |
| fodomb | none | That the reverse direction is equivalent to excluded middle is ~ exmidfodomr . The forward direction is presumably also not provable. | |
| entri3 | ~ fientri3 | Because full entri3 is equivalent to the axiom of choice, it implies excluded middle. | |
| infinf | ~ infnfi | Defining "A is infinite" as ` _om ~<_ A ` follows definition 8.1.4 of [AczelRathjen], p. 71. It can presumably not be shown to be equivalent to ` -. A e. Fin ` in the absence of excluded middle (see ~ inffiexmid which isn't exactly about ` -. A e. Fin <-> _om ~<_ A` but which is close). | |
| df-wina , df-ina , df-tsk , df-gru , ax-groth and all theorems related to inaccessibles and large cardinals | none | For an introduction to inaccessibles and large set properties see Chapter 18 of [AczelRathjen], p. 165 (including why "large set properties" is more apt terminology than "large cardinal properties" in the absence of excluded middle). | |
| df-wun and all weak universe theorems | none | ||
| addcompi | ~ addcompig | ||
| addasspi | ~ addasspig | ||
| mulcompi | ~ mulcompig | ||
| mulasspi | ~ mulasspig | ||
| distrpi | ~ distrpig | ||
| addcanpi | ~ addcanpig | ||
| mulcanpi | ~ mulcanpig | ||
| addnidpi | ~ addnidpig | ||
| ltapi | ~ ltapig | ||
| ltmpi | ~ ltmpig | ||
| nlt1pi | ~ nlt1pig | ||
| 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 | ||
| nqpr | ~ nqprlu | ||
| mulclprlem | ~ mulnqprl , ~ mulnqpru | ||
| addcompr | ~ addcomprg | ||
| addasspr | ~ addassprg | ||
| mulcompr | ~ mulcomprg | ||
| mulasspr | ~ mulassprg | ||
| distrlem1pr | ~ distrlem1prl , ~ distrlem1pru | ||
| distrlem4pr | ~ distrlem4prl , ~ distrlem4pru | ||
| distrlem5pr | ~ distrlem5prl , ~ distrlem5pru | ||
| distrpr | ~ distrprg | ||
| ltprord | ~ ltprordil | There hasn't yet been a need to investigate versions which are biconditional or which involve proper subsets. | |
| psslinpr | ~ ltsopr | ||
| prlem934 | ~ prarloc2 | ||
| ltaddpr2 | ~ ltaddpr | ||
| ltexprlem1 , ltexprlem2 , ltexprlem3 , ltexprlem4 | none | See the lemmas for ~ ltexpri generally. | |
| ltexprlem5 | ~ ltexprlempr | ||
| ltexprlem6 | ~ ltexprlemfl , ~ ltexprlemfu | ||
| ltexprlem7 | ~ ltexprlemrl , ~ ltexprlemru | ||
| ltapr | ~ ltaprg | ||
| addcanpr | ~ addcanprg | ||
| prlem936 | ~ prmuloc2 | ||
| reclem2pr | ~ recexprlempr | ||
| reclem3pr | ~ recexprlem1ssl , ~ recexprlem1ssu | ||
| reclem4pr | ~ recexprlemss1l , ~ recexprlemss1u , ~ recexprlemex | ||
| supexpr , suplem1pr , suplem2pr | ~ caucvgprpr | The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences. | |
| mulcmpblnrlem | ~ mulcmpblnrlemg | ||
| ltsrpr | ~ ltsrprg | ||
| dmaddsr , dmmulsr | none | Although these presumably could be proved in a way similar to ~ dmaddpq and ~dmmulpq (in fact ~ dmaddpqlem would seem to be easily generalizable to anything of the form ` ( ( S X. T ) /. R ) ` ), we haven't yet had a need to do so. | |
| addcomsr | ~ addcomsrg | ||
| addasssr | ~ addasssrg | ||
| mulcomsr | ~ mulcomsrg | ||
| mulasssr | ~ mulasssrg | ||
| distrsr | ~ distrsrg | ||
| ltasr | ~ ltasrg | ||
| sqgt0sr | ~ mulgt0sr , ~ apsqgt0 | ||
| recexsr | ~ recexsrlem | This would follow from sqgt0sr (as in the set.mm proof of recexsr), but "not equal to zero" would need to be changed to "apart from zero". | |
| mappsrpr , ltpsrpr , map2psrpr | ~ prsrpos , ~ prsrlt , ~ srpospr | ||
| supsrlem , supsr | ~ caucvgsr | The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences. | |
| 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 | ~ axcaucvg , ~ ax-caucvg , ~ caucvgre | The Least Upper Bound property for sets of real numbers does not hold, in general, without excluded middle. We express completeness using sequences. | |
| 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 , lttri2i , lttri2d | ~ qlttri2 | Real number trichotomy is not provable. | |
| lttri4 | ~ ztri3or , ~ qtri3or | Real number trichotomy is not provable. | |
| leloe , eqlelt , leloei , leloed , eqleltd | none | ||
| leltne , leltned | ~ leltap , ~ leltapd | ||
| ltneOLD | ~ ltne , ~ ltap | ||
| letric , letrii , letrid | ~ zletric , ~ qletric | ||
| ltlen , ltleni , ltlend | ~ ltleap , ~ zltlen , ~ qltlen | ||
| ne0gt0 , ne0gt0d | ~ ap0gt0 , ~ ap0gt0d | ||
| lecasei , ltlecasei | none | These are real number trichotomy | |
| lelttric | ~ zlelttric , ~ qlelttric | ||
| lttrid , lttri4d | none | These are real number trichotomy | |
| leneltd | ~ leltapd | ||
| dedekind , dedekindle | 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. | |
| ltord1 , leord1 , ltord2 , leord2 | none | The set.mm proof relies on real number trichotomy. | |
| wloglei , wlogle | none | These depend on real number trichotomy and are not used until later in set.mm. | |
| recex | ~ recexap | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcand, mulcan2d | ~ mulcanapd , ~ mulcanap2d | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcanad , mulcan2ad | ~ mulcanapad , ~ mulcanap2ad | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcan , mulcan2 , mulcani | ~ mulcanap , ~ mulcanap2 , ~ mulcanapi | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mul0or , mul0ori , mul0ord | ~ mul0eqap | Remark 2.19 of [Geuvers] says that ` ( A x. B ) = 0 -> ( A = 0 \/ B = 0 ) ` does not hold in general and has a counterexample. | |
| mulne0b , mulne0bd , mulne0bad , mulne0bbd | ~ mulap0b , ~ mulap0bd , ~ mulap0bad , ~ mulap0bbd | ||
| mulne0 , mulne0i , mulne0d | ~ mulap0 , ~ mulap0i , ~ mulap0d | ||
| receu | ~ receuap | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulnzcnopr | none | ||
| msq0i , msq0d | ~ sqeq0 , ~ sqeq0i | These slight restatements of sqeq0 are unused in set.mm. | |
| mulcan1g , mulcan2g | various cancellation theorems | Presumably this is unavailable for the same reason that mul0or is unavailable. | |
| 1div0 | none | This could be proved, but the set.mm proof does not work 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 | ||
| divmulass | ~ divmulassap | ||
| divmulasscom | ~ divmulasscomap | ||
| divdir , divcan3 , divcan4 | ~ divdirap , ~ divcanap3 , ~ divcanap4 | ||
| div11 , divid , div0 | ~ div11ap , ~ dividap , ~ div0ap | ||
| diveq1 , divneg | ~ diveqap1 , ~ divnegap | ||
| muldivdir | ~ muldivdirap | ||
| divsubdir | ~ divsubdirap | ||
| recrec , rec11 , rec11r | ~ recrecap , ~ rec11ap , ~ rec11rap | ||
| divmuldiv , divdivdiv , divcan5 | ~ divmuldivap , ~ divdivdivap , ~ divcanap5 | ||
| divmul13 , divmul24 , divmuleq | ~ divmul13ap , ~ divmul24ap , ~ divmuleqap | ||
| recdiv , divcan6 , divdiv32 , divcan7 | ~ recdivap , ~ divcanap6 , ~ divdiv32ap , ~ divcanap7 | ||
| dmdcan , divdiv1 , divdiv2 , recdiv2 | ~ dmdcanap , ~ divdivap1 , ~ divdivap2 , ~ recdivap2 | ||
| ddcan , divadddiv , divsubdiv | ~ ddcanap , ~ divadddivap , ~ divsubdivap | ||
| ddcan , divadddiv , divsubdiv | ~ ddcanap , ~ divadddivap , ~ divsubdivap | ||
| conjmul , rereccl, redivcl | ~ conjmulap , ~ rerecclap , ~ redivclap | ||
| div2neg , divneg2 | ~ div2negap , ~ divneg2ap | ||
| recclzi , recne0zi , recidzi | ~ recclapzi , ~ recap0apzi , ~ recidapzi | ||
| reccli , recidi , recreci | ~ recclapi , ~ recidapi , ~ recrecapi | ||
| dividi , div0i | ~ dividapi , ~ div0api | ||
| divclzi , divcan1zi , divcan2zi | ~ divclapzi , ~ divcanap1zi , ~ divcanap2zi | ||
| divreczi , divcan3zi , divcan4zi | ~ divrecapzi , ~ divcanap3zi , ~ divcanap4zi | ||
| rec11i , rec11ii | ~ rec11api , ~ rec11apii | ||
| divcli , divcan2i , divcan1i , divreci , divcan3i , divcan4i | ~ divclapi , ~ divcanap2i , ~ divcanap1i , ~ divrecapi , ~ divcanap3i , ~ divcanap4i | ||
| div0i | ~ divap0i | ||
| divasszi , divmulzi , divdirzi , divdiv23zi | ~ divassapzi , ~ divmulapzi , ~ divdirapzi , ~ divdiv23apzi | ||
| divmuli , divdiv32i | ~ divmulapi , ~ divdiv32api | ||
| divassi , divdiri , div23i , div11i | ~ divassapi , ~ divdirapi , ~ div23api , ~ div11api | ||
| divmuldivi, divmul13i, divadddivi, divdivdivi | ~ divmuldivapi , ~ divmul13api , ~ divadddivapi , ~ divdivdivapi | ||
| rerecclzi , rereccli , redivclzi , redivcli | ~ rerecclapzi , ~ rerecclapi , ~ redivclapzi , ~ redivclapi | ||
| reccld , rec0d , recidd , recid2d , recrecd , dividd , div0d | ~ recclapd , ~ recap0d , ~ recidapd , ~ recidap2d , ~ recrecapd , ~ dividapd , ~ div0apd | ||
| divcld , divcan1d , divcan2d , divrecd , divrec2d , divcan3d , divcan4d | ~ divclapd , ~ divcanap1d , ~ divcanap2d , ~ divrecapd , ~ divrecap2d , ~ divcanap3d , ~ divcanap4d | ||
| diveq0d , diveq1d , diveq1ad , diveq0ad , divne1d , div0bd , divnegd , divneg2d , div2negd | ~ diveqap0d , ~ diveqap1d , ~ diveqap1ad , ~ diveqap0ad , ~ divap1d , ~ divap0bd , ~ divnegapd , ~ divneg2apd , ~ div2negapd | ||
| divne0d , recdivd , recdiv2d , divcan6d , ddcand , rec11d | ~ divap0d , ~ recdivapd , ~ recdivap2d , ~ divcanap6d , ~ ddcanapd , ~ rec11apd | ||
| divmuld , div32d , div13d , divdiv32d , divcan5d , divcan5rd , divcan7d , dmdcand , dmdcan2d , divdiv1d , divdiv2d | ~ divmulapd , ~ div32apd , ~ div13apd , ~ divdiv32apd , ~ divcanap5d , ~ divcanap5rd , ~ divcanap7d , ~ dmdcanapd , ~ dmdcanap2d , ~ divdivap1d , ~ divdivap2d | ||
| divmul2d, divmul3d, divassd, div12d, div23d, divdird, divsubdird, div11d | ~ divmulap2d , ~ divmulap3d , ~ divassapd , ~ div12apd , ~ div23apd , ~ divdirapd , ~ divsubdirapd , ~ div11apd | ||
| divmuldivd | ~ divmuldivapd | ||
| rereccld , redivcld | ~ rerecclapd , ~ redivclapd | ||
| diveq1bd | ~ diveqap1bd | ||
| div2sub , div2subd | ~ div2subap , ~ div2subapd | ||
| mvllmuld | ~ mvllmulapd | ||
| elimgt0 , elimge0 | none | Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form. | |
| mulge0b , mulsuble0b | none | Presumably unprovable for reasons analogous to mul0or. | |
| mulle0b | ~ mulle0r | The converse of mulle0r is presumably unprovable for reasons analogous to mul0or. | |
| ledivp1i , ltdivp1i | none | Presumably could be proved, but unused in set.mm. | |
| fimaxre | ~ fimaxq , ~ fimaxre2 | When applied to a pair fimaxre could show which of two unequal real numbers is larger, so perhaps not provable for that reason. (see ~ fin0 for inhabited versus nonempty). | |
| fimaxre3 | none | The set.mm proof relies on abrexfi . | |
| fiminre | none | See fimaxre | |
| sup2 , sup3 , sup3ii | none | We won't be able to have the least upper bound property for all inhabited bounded sets, as shown at ~ sup3exmid . | |
| infm3 | none | See sup3 | |
| suprcl , suprcld , suprclii | ~ supclti | ||
| suprub , suprubd , suprubii | ~ suprubex | ||
| suprlub , suprlubii | ~ suprlubex | ||
| suprnub , suprnubii | ~ suprnubex | ||
| suprleub , suprleubii | ~ suprleubex | ||
| supaddc , supadd | none | Presumably provable with suitable conditions for the existence of the supremums | |
| supmul1 , supmul | none | Presumably provable with suitable conditions for the existence of the supremums | |
| riotaneg | none | The theorem is unused in set.mm and the set.mm proof relies on reuxfrd | |
| infrecl | ~ infclti | ||
| infrenegsup | ~ infrenegsupex | ||
| infregelb | none yet | Presumably could be handled in a way analogous to ~ suprleubex | |
| infrelb | none yet | Presumably could be handled in a way analogous to ~ suprubex | |
| supfirege | ~ suprubex | The question here is whether results like ~ maxle1 can be generalized (presumably by induction) from pairs to finite sets. | |
| crne0 | ~ crap0 | ||
| ofsubeq0 , ofnegsub , ofsubge0 | none | Depend on ofval and/or offn . | |
| df-nn | ~ dfnn2 | ||
| dfnn3 | ~ dfnn2 | Presumably could be proved, as it is a slight variation of dfnn2 | |
| avgle | ~ qavgle | ||
| nnunb | none | Presumably provable from ~ arch but unused in set.mm. | |
| frnnn0supp , frnnn0fsupp | ~ nn0supp | iset.mm does not yet have either the notation, or in some cases the theorems, related to the support of a function or a fintely supported function. | |
| suprzcl | ~ suprzclex | ||
| zriotaneg | none | Lightly used in set.mm | |
| suprfinzcl | none | ||
| decex | ~ deccl | ||
| halfthird | none | Presumably will be easy to intuitionize | |
| 5recm6rec | none | Presumably will be easy to intuitionize | |
| uzwo , uzwo2 , nnwo , nnwof , nnwos | none | Presumably would imply excluded middle, unless there is something which makes this different from ~ nnregexmid . | |
| negn0 | ~ negm | ||
| uzinfi, nninf, nn0inf | none | Presumably provable | |
| infssuzle | ~ infssuzledc | ||
| infssuzcl | ~ infssuzcldc | ||
| supminf | ~ supminfex | ||
| zsupss , suprzcl2 | ~ zsupcl , ~ suprzclex | ||
| suprzub | none | Presumably could prove something like this with different conditions for the existence of the supremum (see ~ infssuzledc for something along these lines). | |
| uzsupss | ~ zsupcl | ||
| uzwo3 , zmin | none | Proved in terms of supremum theorems and presumably not possible without excluded middle. | |
| zbtwnre | none | Proved in terms of supremum theorems and presumably not possible without excluded middle. | |
| rebtwnz | ~ qbtwnz | ||
| rpneg | ~ rpnegap | ||
| xrlttri , xrlttri2 | none | A generalization of real trichotomy. | |
| xrleloe , xrleltne , dfle2 | none | Consequences of real trichotomy. | |
| xrltlen | none | We presumably could prove an analogue to ~ ltleap but we have not yet defined apartness for extended reals (` =//= ` is for complex numbers). | |
| dflt2 | none | ||
| xrletri | none | ||
| xrmax1 | ~ xrmax1sup | ||
| xrmax2 | ~ xrmax2sup | ||
| xrmin1 , xrmin2 | ~ xrmin1inf , ~ xrmin2inf | ||
| xrmaxeq | ~ xrmaxleim | ||
| xrmineq | ~ xrmineqinf | ||
| xrmaxlt | ~ xrmaxltsup | ||
| xrltmin | ~ xrltmininf | ||
| xrmaxle | ~ xrmaxlesup | ||
| xrlemin | ~ xrlemininf | ||
| max0sub , ifle | none | ||
| max1 | ~ maxle1 | ||
| max2 | ~ maxle2 | ||
| 2resupmax | ~ 2zsupmax | for integers | |
| in general | The set.mm proof uses real trichotomy in an apparently essential way. We express maximum in iset.mm using ` sup ( { A , B } , RR , < ) ` rather than ` if ( A <_ B , B , A ) ` . The former has the expected maximum properties such as ~ maxcl , ~ maxle1 , ~ maxle2 , ~ maxleast , and ~ maxleb . | ||
| ssfzunsnext | none | Presumably provable using ~ 2zsupmax and similar theorems. | |
| min1 | ~ min1inf | ||
| min2 | ~ min2inf | ||
| maxle | ~ maxleastb | ||
| lemin | ~ lemininf | ||
| maxlt | ~ maxltsup | ||
| ltmin | ~ ltmininf | ||
| lemaxle | ~ maxle2 | ||
| qsqueeze | none yet | Presumably provable from ~ qbtwnre and ~ squeeze0 , but unused in set.mm. | |
| qextltlem , qextlt , qextle | none | The set.mm proof is not intuitionistic. | |
| xralrple , alrple | none yet | Now that we have ~ qbtwnxr , it looks like the set.mm proof would work with minor changes. | |
| xnegex | ~ xnegcl | ||
| xmulval | none | The set.mm definition would appear to only function if comparing a real number with zero is decidable (which we will not be able to show in general) | |
| xnn0xaddcl | none | presumably provable | |
| xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xmulcld | none | Although a few of these contain hypotheses that arguments are apart from zero (and thus could be proved with the current definition of ` *e ` ), in general extended real multiplication will not work as in set.mm using that definition. | |
| xrsupss | none | the set.mm proof relies on sup3 which implies excluded middle by ~ sup3exmid | |
| supxrcl | none | the set.mm proof relies on xrsupss | |
| infxrcl | none | presumably not provable for all the usual ~ sup3exmid reasons | |
| ixxub , ixxlb | none | ||
| iccen | none | ||
| supicc , supiccub , supicclub , supicclub2 | none | ||
| ixxun , ixxin | none | ||
| ioon0 | ~ ioom | Non-empty is changed to inhabited | |
| iooid | ~ iooidg | ||
| ndmioo | none | See discussion at ndmov but set.mm uses excluded middle, both in proving this and in using it. | |
| lbioo , ubioo | ~ lbioog , ~ ubioog | ||
| iooin | ~ iooinsup | ||
| icc0 | ~ icc0r | ||
| ioorebas | ~ ioorebasg | ||
| ge0xmulcl | none | Relies on xmulcl ; see discussion in this list for that theorems. | |
| icoun , snunioo , snunico , snunioc , prunioo | none | ||
| ioojoin | none | ||
| difreicc | none | ||
| iccsplit | none | This depends, apparently in an essential way, on real number trichotomy. | |
| xov1plusxeqvd | none | This presumably could be proved if not equal is changed to apart, but is lightly used in set.mm. | |
| fzn0 | ~ fzm | ||
| fz0 | none | Although it would be possible to prove a version of this with the additional conditions that ` M e. _V ` and ` N e. _V ` , the theorem is lightly used in set.mm. | |
| fzon0 | ~ fzom | ||
| fzo0n0 | ~ fzo0m | ||
| ssfzoulel | none | Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm. | |
| fzonfzoufzol | none | Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm. | |
| elfznelfzo , elfznelfzob , injresinjlem , injresinj | none | Some or all of this presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm. | |
| flcl , reflcl , flcld | ~ flqcl , ~ flqcld | ||
| fllelt | ~ flqlelt | ||
| flle | ~ flqle | ||
| flltp1 , fllep1 | ~ flqltp1 | ||
| fraclt1 , fracle1 | ~ qfraclt1 | ||
| fracge0 | ~ qfracge0 | ||
| flge | ~ flqge | ||
| fllt | ~ flqlt | ||
| flflp1 | none | The set.mm proof relies on case elimination. | |
| flidm | ~ flqidm | ||
| flidz | ~ flqidz | ||
| flltnz | ~ flqltnz | ||
| flwordi | ~ flqwordi | ||
| flword2 | ~ flqword2 | ||
| flval2 , flval3 | none | Unused in set.mm | |
| flbi | ~ flqbi | ||
| flbi2 | ~ flqbi2 | ||
| ico01fl0 | none | Presumably could be proved for rationals, but lightly used in set.mm. | |
| flge0nn0 | ~ flqge0nn0 | ||
| flge1nn | ~ flqge1nn | ||
| refldivcl | ~ flqcl | ||
| fladdz | ~ flqaddz | ||
| flzadd | ~ flqzadd | ||
| flmulnn0 | ~ flqmulnn0 | ||
| fldivle | ~ flqle | ||
| ltdifltdiv | none | Unused in set.mm. | |
| fldiv4lem1div2uz2 , fldiv4lem1div2 | none | Presumably provable, but lightly used in set.mm. | |
| ceilval | ~ ceilqval | The set.mm ceilval, with a real argument and no additional conditions, is probably provable if there is a need. | |
| dfceil2 , ceilval2 | none | Unused in set.mm. | |
| ceicl | ~ ceiqcl | ||
| ceilcl | ~ ceilqcl | ||
| ceilge | ~ ceilqge | ||
| ceige | ~ ceiqge | ||
| ceim1l | ~ ceiqm1l | ||
| ceilm1lt | ~ ceilqm1lt | ||
| ceile | ~ ceiqle | ||
| ceille | ~ ceilqle | ||
| ceilidz | ~ ceilqidz | ||
| flleceil | ~ flqleceil | ||
| fleqceilz | ~ flqeqceilz | ||
| quoremz , quoremnn0 , quoremnn0ALT | none | Unused in set.mm. | |
| intfrac2 | ~ intqfrac2 | ||
| fldiv | ~ flqdiv | ||
| fldiv2 | none | Presumably would be provable if real is changed to rational. | |
| fznnfl | none | Presumably would be provable if real is changed to rational. | |
| uzsup , ioopnfsup , icopnfsup , rpsup , resup , xrsup | none | As with most theorems involving supremums, these would likely need significant changes | |
| modval | ~ modqval | As with theorems such as ~ flqcl , we prove most of the modulo related theorems for rationals, although other conditions on real arguments other than whether they are rational would be possible in the future. | |
| modvalr | ~ modqvalr | ||
| modcl , modcld | ~ modqcl , ~ modqcld | ||
| flpmodeq | ~ flqpmodeq | ||
| mod0 | ~ modq0 | ||
| mulmod0 | ~ mulqmod0 | ||
| negmod0 | ~ negqmod0 | ||
| modge0 | ~ modqge0 | ||
| modlt | ~ modqlt | ||
| modelico | ~ modqelico | ||
| moddiffl | ~ modqdiffl | ||
| moddifz | ~ modqdifz | ||
| modfrac | ~ modqfrac | ||
| flmod | ~ flqmod | ||
| intfrac | ~ intqfrac | ||
| modmulnn | ~ modqmulnn | ||
| modvalp1 | ~ modqvalp1 | ||
| modid | ~ modqid | ||
| modid0 | ~ modqid0 | ||
| modid2 | ~ modqid2 | ||
| 0mod | ~ q0mod | ||
| 1mod | ~ q1mod | ||
| modabs | ~ modqabs | ||
| modabs2 | ~ modqabs2 | ||
| modcyc | ~ modqcyc | ||
| modcyc2 | ~ modqcyc2 | ||
| modadd1 | ~ modqadd1 | ||
| modaddabs | ~ modqaddabs | ||
| modaddmod | ~ modqaddmod | ||
| muladdmodid | ~ mulqaddmodid | ||
| modmuladd | ~ modqmuladd | ||
| modmuladdim | ~ modqmuladdim | ||
| modmuladdnn0 | ~ modqmuladdnn0 | ||
| negmod | ~ qnegmod | ||
| modadd2mod | ~ modqadd2mod | ||
| modm1p1mod0 | ~ modqm1p1mod0 | ||
| modltm1p1mod | ~ modqltm1p1mod | ||
| modmul1 | ~ modqmul1 | ||
| modmul12d | ~ modqmul12d | ||
| modnegd | ~ modqnegd | ||
| modadd12d | ~ modqadd12d | ||
| modsub12d | ~ modqsub12d | ||
| modsubmod | ~ modqsubmod | ||
| modsubmodmod | ~ modqsubmodmod | ||
| 2txmodxeq0 | ~ q2txmodxeq0 | ||
| 2submod | ~ q2submod | ||
| modmulmod | ~ modqmulmod | ||
| modmulmodr | ~ modqmulmodr | ||
| modaddmulmod | ~ modqaddmulmod | ||
| moddi | ~ modqdi | ||
| modsubdir | ~ modqsubdir | ||
| modeqmodmin | ~ modqeqmodmin | ||
| modirr | none | A version of this (presumably modified) may be possible, but it is unused in set.mm | |
| om2uz0i | ~ frec2uz0d | ||
| om2uzsuci | ~ frec2uzsucd | ||
| om2uzuzi | ~ frec2uzuzd | ||
| om2uzlti | ~ frec2uzltd | ||
| om2uzlt2i | ~ frec2uzlt2d | ||
| om2uzrani | ~ frec2uzrand | ||
| om2uzf1oi | ~ frec2uzf1od | ||
| om2uzisoi | ~ frec2uzisod | ||
| om2uzoi , ltweuz , ltwenn , ltwefz | none | Based on theorems like ~ nnregexmid it is not clear what, if anything, along these lines is possible. | |
| om2uzrdg | ~ frec2uzrdg | ||
| uzrdglem | ~ frecuzrdglem | ||
| uzrdgfni | ~ frecuzrdgtcl | ||
| uzrdg0i | ~ frecuzrdg0 | ||
| uzrdgsuci | ~ frecuzrdgsuc | ||
| uzinf | none | See ominf | |
| uzrdgxfr | none | Presumably could be proved if restated in terms of ` frec ` (a la ~ frec2uz0d ). However, it is lightly used in set.mm. | |
| fzennn | ~ frecfzennn | ||
| fzen2 | ~ frecfzen2 | ||
| cardfz | none | Cardinality does not work the same way without excluded middle and iset.mm has few cardinality related theorems. | |
| hashgf1o | ~ frechashgf1o | ||
| fzfi | ~ fzfig | ||
| fzfid | ~ fzfigd | ||
| fzofi | ~ fzofig | ||
| fsequb | none | Seems like it might be provable, but unused in set.mm | |
| fsequb2 | none | The set.mm proof does not work as-is | |
| fseqsupcl | none | The set.mm proof relies on fisupcl and it is not clear whether this supremum theorem or anything similar can be proved. | |
| fseqsupubi | none | The set.mm proof relies on fsequb2 and suprub and it is not clear whether this supremum theorem or anything similar can be proved. | |
| uzindi | none | This could presumably be proved, perhaps from ~ uzsinds , but is lightly used in set.mm | |
| axdc4uz | none | Although some versions of constructive mathematics accept dependent choice, we have not yet developed it in iset.mm | |
| ssnn0fi , rabssnn0fi | none | Conjectured to imply excluded middle along the lines of ~ nnregexmid or ~ ssfiexmid | |
| df-seq | ~ df-seqfrec | ||
| seqval | ~ seq3val | ||
| seqfn | ~ seqf | ||
| seq1 , seq1i | ~ seq3-1 | ||
| seqp1 , seqp1i | ~ seq3p1 | ||
| seqm1 | ~ seq3m1 | ||
| seqcl2 | ~ seqf2 | ~ seqf2 requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| seqcl | ~ seqf , ~ seq3clss | ~ seqf requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . This requirement is relaxed somewhat in ~ seq3clss . | |
| seqfveq2 | ~ seq3fveq2 | ||
| seqfeq2 | ~ seq3feq2 | ||
| seqfveq | ~ seq3fveq | ||
| seqfeq | ~ seq3feq | ||
| seqshft2 | ~ seq3shft2 | ||
| seqres | none | Should be intuitionizable as with the other ` seq ` theorems, but unused in set.mm | |
| sermono | ~ ser3mono | ser3mono requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in sermono . | |
| seqsplit | ~ seq3split | seq3split requires that ` F ` be defined on ` ( ZZ>= `` K ) ` not merely ` ( K ... N ) ` as in seqsplit . This is not a problem when used on infinite sequences; finite sums may find it easier to use ~ fsumsplit instead. | |
| seq1p | ~ seq3-1p | Requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqcaopr3 | ~ seq3caopr3 | The functions ` F ` , ` G ` , and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| seqcaopr2 | ~ seq3caopr2 | The functions ` F ` , ` G ` , and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| seqcaopr | ~ seq3caopr | The functions ` F ` , ` G ` , and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| seqf1o | ~ seq3f1o | The functions ` G ` and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . Also, a single set ` S ` takes the place of ` C ` and ` S ` because that is sufficient flexibility at least for now. | |
| seradd | ~ ser3add | The functions ` F ` , ` G ` , and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| sersub | ~ ser3sub | The functions ` F ` , ` G ` , and ` H ` need to be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` . | |
| seqid3 | ~ seq3id3 | ||
| seqid | ~ seq3id | ||
| seqid2 | ~ seq3id2 | ||
| seqhomo | ~ seq3homo | ||
| seqz | ~ seq3z | The sequence has to be defined on ` ( ZZ>= `` M ) ` not just ` ( M ... N ) ` | |
| seqfeq4 | ~ seqfeq3 | The sequence has to be defined on ` ( ZZ>= `` M ) ` not just ` ( M ... N ) ` | |
| seqdistr | ~ seq3distr | ||
| serge0 | ~ ser3ge0 | The sequence has to be defined on ` ( ZZ>= `` M ) ` not just ` ( M ... N ) ` | |
| serle | ~ ser3le | Changes several hypotheses from ` ( M ... N ) ` to ` ( ZZ>= `` M ) ` | |
| ser1const | ~ fsumconst | Finite summation in iset.mm is easier to express using ` sum_ ` rather than ` seq ` directly. | |
| seqof , seqof2 | none | It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet. | |
| expval | ~ exp3val | The set.mm theorem does not exclude the case of dividing by zero. | |
| expneg | ~ expnegap0 | The set.mm theorem does not exclude the case of dividing by zero. | |
| expneg2 | ~ expineg2 | ||
| expn1 | ~ expn1ap0 | ||
| expcl2lem | ~ expcl2lemap | ||
| reexpclz | ~ reexpclzap | ||
| expclzlem | ~ expclzaplem | ||
| expclz | ~ expclzap | ||
| expne0 | ~ expap0 | ||
| expne0i | ~ expap0i | ||
| expnegz | ~ expnegzap | ||
| mulexpz | ~ mulexpzap | ||
| exprec | ~ exprecap | ||
| expaddzlem , expaddz | ~ expaddzaplem , ~ expaddzap | ||
| expmulz | ~ expmulzap | ||
| expsub | ~ expsubap | ||
| expp1z | ~ expp1zap | ||
| expm1 | ~ expm1ap | ||
| expdiv | ~ expdivap | ||
| ltexp2 , leexp2 , leexp2 , ltexp2d , leexp2d | none | Presumably provable, but the set.mm proof uses ltord1 | |
| ltexp2r , ltexp2rd | none | Presumably provable, but the set.mm proof uses ltexp2 | |
| sqdiv | ~ sqdivap | ||
| sqgt0 | ~ sqgt0ap | ||
| sqrecii , sqrecd | ~ exprecap | ||
| sqdivi | ~ sqdivapi | ||
| sqgt0i | ~ sqgt0api | ||
| sqlecan | ~ lemul1 | Unused in set.mm | |
| sqeqori | none | The reverse direction is ~ oveq1 together with ~ sqneg . The forward direction is presumably not provable, see mul0or for more discussion. | |
| 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 | ||
| expne0d | ~ expap0d | ||
| expnegd | ~ expnegapd | ||
| exprecd | ~ exprecapd | ||
| expp1zd | ~ expp1zapd | ||
| expm1d | ~ expm1apd | ||
| expsubd | ~ expsubapd | ||
| sqdivd | ~ sqdivapd | ||
| expdivd | ~ expdivapd | ||
| reexpclzd | ~ reexpclzapd | ||
| sqgt0d | ~ sqgt0apd | ||
| mulsubdivbinom2 | none | Presumably provable if not equal is changed to apart. | |
| muldivbinom2 | none | Presumably provable if not equal is changed to apart. | |
| nn0le2msqi | ~ nn0le2msqd | Although nn0le2msqi could be proved, having a version in deduction form will be more useful. | |
| nn0opthlem1 | ~ nn0opthlem1d | Although nn0opthlem1 could be proved, having a version in deduction form will be more useful. | |
| nn0opthlem2 | ~ nn0opthlem2d | Although nn0opthlem2 could be proved, having a version in deduction form will be more useful. | |
| nn0opthi | ~ nn0opthd | Although nn0opthi could be proved, having a version in deduction form will be more useful. | |
| nn0opth2i | ~ nn0opth2d | Although nn0opth2i could be proved, having a version in deduction form will be more useful. | |
| facmapnn | ~ faccl | Presumably provable now that iset.mm has ~ df-map . But ~ faccl would be sufficient for the uses in set.mm. | |
| faclbnd4 , faclbnd5 , and lemmas | none | Presumably provable; unused in set.mm. | |
| df-hash | ~ df-ihash | ||
| hashkf , hashgval , hashginv | none | Due to the differences between df-hash in set.mm and ~ df-ihash here, there's no particular need for these as stated | |
| hashinf | ~ hashinfom | The condition that ` A ` is infinite is changed from ` -. A e. Fin ` to ` _om ~<_ A ` . | |
| hashbnd | none | The set.mm proof is not intuitionistic. | |
| hashfxnn0 , hashf , hashxnn0 , hashresfn , dmhashres , hashnn0pnf | none | Although ~ df-ihash is defined for finite sets and infinite sets, it is not clear we would be able to show this definition (or another definition) is defined for all sets. | |
| hashnnn0genn0 | none | Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize. | |
| hashnemnf | none | Presumably provable but the set.mm proof relies on hashnn0pnf | |
| hashv01gt1 | ~ hashfiv01gt1 | It is not clear there would be any way to combine the finite and infinite cases. | |
| hasheni | ~ hashen , ~ hashinfom | It is not clear there would be any way to combine the finite and infinite cases. | |
| hasheqf1oi | ~ fihasheqf1oi | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashf1rn | ~ fihashf1rn | It is not clear there would be any way to combine the finite and infinite cases. | |
| hasheqf1od | ~ fihasheqf1od | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashcard | none | Cardinality is not well developed in iset.mm | |
| hashxrcl | none | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashclb | none | Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize. | |
| nfile | ~ filtinf | It is not clear there would be any way to combine the case where ` A ` is finite and the case where it is infinite. | |
| hashvnfin | none | This is a form of reverse closure, presumably not provable. | |
| hashnfinnn0 | ~ hashinfom | ||
| isfinite4 | ~ isfinite4im | ||
| hasheq0 | ~ fihasheq0 | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashneq0 , hashgt0n0 | ~ fihashneq0 | ||
| hashen1 | ~ fihashen1 | ||
| hashrabrsn | none | Presumably would need conditions around the existence of ` A ` and decidability of ` ph ` but unused in set.mm. | |
| hashrabsn01 | none | Presumably would need conditions around the existence of ` A ` and decidability of ` ph ` but unused in set.mm. | |
| hashrabsn1 | none | The set.mm proof uses excluded middle and this theorem is unused in set.mm. | |
| hashfn | ~ fihashfn | There is an added condition that the domain be finite. | |
| hashgadd | ~ omgadd | ||
| hashgval2 | none | Presumably provable, when restated as ` ( # |`` _om ) = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) ` , but lightly used in set.mm. | |
| hashdom | ~ fihashdom | There is an added condition that ` B ` is finite. | |
| hashdomi | ~ fihashdom | It is presumably not possible to extend ~ fihashdom beyond the finite set case. | |
| hashun2 | none | The set.mm proof relies on undif2 (we just have ~ undif2ss ) and diffi (we just have ~ diffifi ) | |
| hashun3 | none | The set.mm proof relies on various theorems we do not have | |
| hashinfxadd | none | ||
| hashunx | none | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashge0 | ~ hashcl | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashgt0 , hashge1 | ~ hashnncl | It is not clear there would be any way to combine the finite and infinite cases. | |
| hashnn0n0nn | ~ hashnncl | To the extent this is reverse closure, we probably can't prove it. For inhabited versus non-empty, see ~ fin0 | |
| elprchashprn2 | ~ hashsng | Given either ` N e. _V ` or ` -. N e. _V ` this could be proved (as ` ( # `` { M , N } ) ` reduces to ~ hashsng or ~ hash0 respectively), but is not clear we can combine the cases (even ~ 1domsn may not be enough). | |
| hashprb | ~ hashprg | ||
| hashprdifel | none | This would appear to be a form of reverse closure. | |
| hashle00 | ~ fihasheq0 | ||
| hashgt0elex , hashgt0elexb | ~ fihashneq0 | See ~ fin0 for inhabited versus non-empty. It isn't clear it would be possible to also include the infinite case as hashgt0elex does. | |
| hashss | ~ fihashss | ||
| prsshashgt1 | ~ fiprsshashgt1 | ||
| hashin | none | Presumably additional conditions would be needed (see infi entry). | |
| hashssdif | ~ fihashssdif | ||
| hashdif | none | Modified versions presumably would be provable, but this is unused in set.mm. | |
| hashsn01 | none | Presumably not provable | |
| hashsnle1 | none | At first glance this would appear to be the same as ~ 1domsn but to apply ~ fihashdom would require that the singleton be finite, which might imply that we cannot improve on ~ hashsng . | |
| hashsnlei | none | Presumably not provable | |
| hash1snb , euhash1 , hash1n0 , hashgt12el , hashgt12el2 | none | Conjectured to be provable in the finite set case | |
| hashunlei | none | Not provable per ~ unfiexmid (see also entry for hashun2) | |
| hashsslei | ~ fihashss | Would be provable if we transfered ` B e. Fin ` from the conclusion to the hypothesis but as written falls afoul of ~ ssfiexmid . | |
| hashmap | none | Probably provable but the set.mm proof relies on a number of theorems which we don't have. | |
| hashpw | none | Unlike pw2en this is only for finite sets, so it presumably is provable. The set.mm proof may be usable. | |
| hashfun | none | Presumably provable but the set.mm proof relies on excluded middle and undif. | |
| hashres , hashreshashfun | none | Presumably would need to add ` B e. Fin ` or similar conditions. | |
| hashimarn , hashimarni | none | Presumably would need an additional condition such as ` F e. Fin ` but unused in set.mm. | |
| fnfz0hashnn0 | none | Presumably would need an additional condition such as ` N e. NN0 ` but unused in set.mm. | |
| fnfzo0hashnn0 | none | Presumably would need an additional condition such as ` N e. NN0 ` but unused in set.mm. | |
| hashbc | none | The set.mm proof uses pwfi and ssfi . | |
| hashf1 | none | The set.mm proof uses ssfi , excluded middle, abn0 , diffi and perhaps other theorems we don't have. | |
| hashfac | none | The set.mm proof uses hashf1 . | |
| leiso | none | The set.mm proof uses isocnv3 . | |
| fz1iso | ~ zfz1iso | The set.mm proof of fz1iso depends on OrdIso. Furthermore, trichotomy rather than weak linearity would seem to be needed. | |
| ishashinf | none | May be possible with the antecedent changed from ` -. A e. Fin ` to ` _om ~<_ A ` but the set.mm proof does not work as is. | |
| seqcoll | ~ seq3coll | The functions ` F ` and ` H ` need to be defined on ` ZZ>= `` M ` not just a subset thereof. | |
| seqcoll2 | none | Presumably can be done with modifications similar to ~ seq3coll . | |
| seqshft | ~ seq3shft | ||
| df-sgn and theorems related to the sgn function | none | To choose a value near zero requires knowing the argument with unlimited precision. It would be possible to define for rational numbers, or real numbers apart from zero. | |
| mulre | ~ mulreap | ||
| rediv | ~ redivap | ||
| imdiv | ~ imdivap | ||
| cjdiv | ~ cjdivap | ||
| sqeqd | none | The set.mm proof is not intuitionistic, and this theorem is unused in set.mm. | |
| cjdivi | ~ cjdivapi | ||
| cjdivd | ~ cjdivapd | ||
| redivd | ~ redivapd | ||
| imdivd | ~ imdivapd | ||
| df-sqrt | ~ df-rsqrt | See discussion of complex square roots in the comment of ~ df-rsqrt . Here's one possibility if we do want to define square roots on (some) complex numbers: It should be possible to define the complex square root function on all complex numbers satisfying ` ( Im `` x ) =//= 0 \/ 0 <_ ( Re `` x ) ` , using a similar construction to the one used in set.mm. You need the real square root as a basis for the construction, but then there is a trick using the complex number x + |x| (see sqreu) that yields the complex square root whenever it is apart from zero (you need to divide by it at one point IIRC), which is exactly on the negative real line. You can either live with this constraint, which gives you the complex square root except on the negative real line (which puts a hole at zero), or you can extend it by continuity to zero as well by joining it with the real square root. The disjunctive domain of the resulting function might not be so useful though. | |
| sqrtval | ~ sqrtrval | See discussion of complex square roots in the comment of ~ df-rsqrt | |
| 01sqrex and its lemmas | ~ resqrex | Both set.mm and iset.mm prove resqrex although via different mechanisms so there is no need for 01sqrex. | |
| cnpart | none | See discussion of complex square roots in the comment of ~ df-rsqrt | |
| sqrmo | ~ rsqrmo | See discussion of complex square roots in the comment of ~ df-rsqrt | |
| resqreu | ~ rersqreu | Although the set.mm theorem is primarily about real square roots, the iset.mm equivalent removes some complex number related parts. | |
| sqrtneg , sqrtnegd | none | Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of ~ df-rsqrt | |
| 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 | |
| absrpcl , absrpcld | ~ absrpclap , ~ absrpclapd | ||
| absdiv , absdivzi , absdivd | ~ absdivap , ~ absdivapzi , ~ absdivapd | ||
| absor , absori , absord | ~ qabsor | It also would be possible to prove this for real numbers apart from zero, if we wanted | |
| absmod0 | none | See df-mod ; we may want to supply this for rationals or integers | |
| absexpz | ~ absexpzap | ||
| max0add | ~ max0addsup | ||
| absz | none | Although this is presumably provable, the set.mm proof is not intuitionistic and it is lightly used in set.mm | |
| recval | ~ recvalap | ||
| absgt0 , absgt0i | ~ absgt0ap , absgt0api | ||
| absmax | ~ maxabs | ||
| abs1m | none | Because this theorem provides ` ( * `` A ) / ( abs `` A ) ` as the answer if ` A =/= 0 ` and ` i ` as the answer if ` A = 0 ` , and uses excluded middle to combine those cases, it is presumably not provable as stated. We could prove the theorem with the additional condition that ` A =//= 0 ` , but it is unused in set.mm. | |
| abslem2 | none | Although this could presumably be proved if not equal were changed to apart, it is lightly used in set.mm. | |
| rddif , absrdbnd | none | If there is a need, we could prove these for rationals or real numbers apart from any rational. Alternately, we could prove a result with a slightly larger bound for any real number. | |
| rexuzre | none | Unless the real number ` j ` is known to be apart from an integer, it isn't clear there would be any way to prove this (see the steps in the set.mm proof which rely on the floor of a real number). It is unused in set.mm for whatever that is worth. | |
| caubnd | none | If we can prove fimaxre3 it would appear that the set.mm proof would work with small changes (in the case of the maximum of two real numbers, using ~ maxle1 , ~ maxle2 , and ~ maxcl ). | |
| sqreulem , sqreu , sqrtcl , sqrtcld , sqrtthlem , sqrtf , sqrtth , sqsqrtd , msqsqrtd , sqr00d , sqrtrege0 , sqrtrege0d , eqsqrtor , eqsqrtd , eqsqrt2d | ~ rersqreu , ~ resqrtcl , ~ resqrtcld , ~ resqrtth | As described at ~ df-rsqrt , square roots of complex numbers are in set.mm defined with the help of excluded middle. | |
| df-limsup and all superior limit theorems | none | This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc. | |
| df-rlim and theorems related to limits of partial functions on the reals | none | This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to convergence. | |
| df-o1 and theorems related to eventually bounded functions | none | This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc. | |
| df-lo1 and theorems related to eventually upper bounded functions | none | This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc. | |
| reccn2 | ~ reccn2ap | ||
| isershft | ~ iser3shft | ||
| isercoll and its lemmas, isercoll2 | none yet | The set.mm proof would need modification | |
| climsup | none | To show convergence would presumably require a hypothesis related to the rate of convergence. | |
| climbdd | none | Presumably could be proved but the current proof of caubnd would need at least some minor adjustments. | |
| caurcvg2 | ~ climrecvg1n | ||
| caucvg | ~ climcvg1n | ||
| caucvgb | ~ climcaucn , ~ climcvg1n | Without excluded middle, there are additional complications related to the rate of convergence. | |
| iseralt | none | The set.mm proof relies on caurcvg2 which does not specify a rate of convergence. | |
| df-sum | ~ df-sumdc | The iset.mm definition/theorem adds a decidability condition and an ` if ` expression (which is to deal with differences in using ` seq ` for finite sums). It does function similarity to the set.mm definiton of ` sum_ ` . | |
| sumex | ~ fsumcl , ~ isumcl | ||
| sumeq2w | ~ sumeq2 | Presumably could be proved, and perhaps also would rely only on extensionality (and logical axioms). But unused in set.mm. | |
| sumeq2ii | ~ sumeq2d | ||
| sum2id | none | The set.mm proof does not work as-is. Lightly used in set.mm. | |
| sumfc | ~ sumfct | ||
| fsumcvg | ~ fsum3cvg | ||
| sumrb | ~ sumrbdc | ||
| summo | ~ summodc | ||
| zsum | ~ zsumdc | ||
| fsum | ~ fsum3 | ||
| sumz | ~ isumz | ||
| sumss | ~ isumss | ||
| sumss2 | ~ isumss2 | ||
| fsumcvg2 | ~ fsum3cvg2 | ||
| fsumsers | ~ fsumsersdc | ||
| fsumcvg3 | ~ fsum3cvg3 | ||
| fsumser | ~ fsum3ser | ||
| fsummsnunz | none | Could be proved if we added a ` Z e. _V ` condition, but unused in set.mm. | |
| isumdivc | ~ isumdivapc | Changes not equal to apart | |
| sumsplit | ~ sumsplitdc | Adds decidability conditions | |
| fsumcom2 | ~ fisumcom2 | Although it is possible that ` ( ph /\ k e. C ) -> D e. Fin ` can be proved from the other hypotheses, the set.mm proof of that uses ssfi . | |
| fsum0diag | ~ fisum0diag | Adds a ` N e. ZZ ` hypothesis | |
| fsumrev2 | ~ fisumrev2 | Adds ` M e. ZZ ` and ` N e. ZZ ` hypotheses | |
| fsum0diag2 | ~ fisum0diag2 | Adds a ` N e. ZZ ` hypothesis | |
| fsumdivc | ~ fsumdivapc | Changes not equal to apart | |
| fsumless | ~ fsumlessfi | Whether this can be proved without the ` C e. Fin ` condition is unknown but such a proof would be fairly different from the set.mm proof. | |
| seqabs | ~ fsumabs | Finite sums are more naturally expressed with ` sum_ ` rather than ` seq ` especially in iset.mm. Use ~ fsum3ser as needed. | |
| cvgcmp | none | Apparently would need an additional condition on the rate of convergence. The set.mm proof relies on caurcvg2 which does not specify a rate of convergence. | |
| cvgcmpce | none | The proof, and perhaps the statement of the theorem, would need some changes related to the rate of convergence. | |
| abscvgcvg | none | The set.mm proof relies on cvgcmpce | |
| climfsum | none | Likely provable, but lightly used in set.mm. | |
| qshash | none | The set.mm proof will not work as-is. | |
| ackbijnn | none | iset.mm does not have ackbij1 | |
| incexclem , incexc , incexc2 | none | A metamath 100 theorem but otherwise unused in set.mm. | |
| isumless | ~ isumlessdc | Adds a decidability condition on the index set for the sum | |
| isumsup2 , isumsup | none | Having an upper bound on the partial sums would not suffice; a stronger convergence condition would be needed. | |
| isumltss | none | Should be provable with the addition of a decidability condition such as the one found in ~ isumss2 and ~ fsum3cvg3 . | |
| climcnds | none | The set.mm proof will not work without modifications. | |
| divcnvshft | none | The set.mm proof uses ovex to show that ` A / ( k + B ) ` is a set, even when ` k + B ` might be zero. This could be solved by adding another usage of ~ df-div or proving ` ( 1 / 0 ) = (/) ` but relying on the value of dividing by zero is not something we usually let ourselves do. Another solution would be to add a ` 0 < ( M + B ) ` hypothesis. | |
| supcvg | none | The set.mm proof uses countable choice and also various supremum theorems proved via excluded middle. | |
| infcvgaux1i , infcvgaux2i | none | See supcvg entry | |
| harmonic | none | Should be feasible once we get isumless and climcnds (or similar theorems). A Metamath 100 theorem but otherwise unused in set.mm. | |
| geoserg | ~ geosergap | Not equal is changed to apart | |
| geoser | ~ geoserap | Not equal is changed to apart | |
| pwm1geoser | ~ pwm1geoserap1 | Adds a condition that the base is apart from one. The set.mm proof relies on case elimination on whether the base is one or not equal to one. | |
| geomulcvg | none | The set.mm proof relies on cvgcmpce and expmulnbnd and would appear to also require ` A ` to be apart from zero. | |
| cvgrat | ~ cvgratgt0 | Adds a ` 0 < A ` condition which presumably is omitted from the set.mm theorem only for convenience (the theorem isn't interesting unless it holds). | |
| mertens | ~ mertensabs | Because we don't (yet at least) have abscvgcvg or anything else relating the convergence of a sequence's absolute values to the convergence of the sequence itself, we add the condition that both the sequence ` F ` and the sequence of its absolute values converge (that is, ` seq 0 ( + , F ) e. dom ~~> ` is an additional hypothesis beyond what set.mm has). | |
| df-prod and theorems using it | none | To define this, we will need to tackle all the issues analogous to ~ df-sumdc plus some more around, for example, not equal to zero versus apart from zero | |
| eftval | ~ eftvalcn | Adds an easily satisfied condition. | |
| fprodefsum | none | Presumably feasible once finite products are better developed. | |
| eflt | ~ efltim | The set.mm proof of the converse relies on ltord1 | |
| efle | ~ efler | The set.mm proof of the converse relies on eflt | |
| tanval | ~ tanvalap | ||
| tancl , tancld | ~ tanclap , ~ tanclapd | ||
| tanval2 | ~ tanval2ap | ||
| tanval3 | ~ tanval3ap | ||
| retancl , retancld | ~ retanclap , ~ retanclapd | ||
| tanneg | ~ tannegap | ||
| sinhval , coshval , resinhcl , rpcoshcl , recoshcl , retanhcl , tanhlt1 , tanhbnd | none yet | should be provable | |
| tanadd | ~ tanaddap | ||
| sinltx | ~ sin01bnd , ~ sinbnd | Although we can prove the ` A <_ 1 ` case (see ~ sin01bnd ) or the ` 1 < A ` case (from ~ sinbnd ), set.mm uses real number trichotomy to combine those cases. | |
| ruc | none | Apparently not provable without countable choice, assuming the following result holds up: Andrej Bauer (12-May-2022), "The countable reals", Topos Institute Colloquium | |
| dvdsaddre2b | none | Something along these lines (perhaps with real changed to rational) may be possible | |
| fsumdvds , 3dvds | none | May be possible when summation is well enough developed | |
| sumeven , sumodd , evensumodd , oddsumodd , pwp1fsum , oddpwp1fsum | none | Presumably possible when summation is well enough developed | |
| divalglem0 and other ~ divalg lemmas | ~ divalglemnn and other lemmas | Since the end result ~ divalg is the same, we don't list all the differences in lemmas here. | |
| gcdcllem1 , gcdcllem2 , gcdcllem3 | ~ gcdn0cl , ~ gcddvds , ~ dvdslegcd | These are lemmas which are part of the proof of theorems that iset.mm proves a somewhat different way | |
| seq1st | none | The sequence passed to ` seq ` , at least as handled in theorems such as ~ seqf , must be defined on all integers greater than or equal to ` M ` , not just at ` M ` itself. It may be possible to patch this up, but seq1st is unused in set.mm. | |
| algr0 | ~ ialgr0 | The ` F : S --> S ` hypothesis is added (related theorems already have that hypothesis). | |
| df-lcmf and theorems using it | none | Although this could be defined, most of the theorems would need decidability conditions analogous to ~ zsupcl | |
| absproddvds , absprodnn | none | Needs product to be developed, but once that is done seems like it might be possible. | |
| fissn0dvds , fissn0dvdsn0 | none | Possibly could be proved using ~ findcard2 or the like. | |
| coprmprod , coprmproddvds | none | Can investigate once product is better developed. | |
| isprm5 | none | Presumably provable, but the set.mm proof relies on excluded middle in multiple places. | |
| isprm7 | none | The set.mm proof relies on isprm5 | |
| maxprmfct | none | Presumably provable with suitable adjustments to the condition for the existence of the supremum | |
| ncoprmlnprm | none | Presumably provable but the set.mm proof uses excluded middle | |
| zsqrtelqelz | ~ nn0sqrtelqelz | We don't yet have much on the square root of a negative number | |
| df-odz and all theorems concerning the order function on the class of integers mod N | none | Presumably could be defined, but would require changes to how we show the infimum exists. Lightly used in set.mm. | |
| eulerth | none | The lemma eulerthlem2 relies on seqf1o | |
| fermltl | none | Relies on eulerth | |
| prmdiv | none | Relies on eulerth | |
| prmdiveq | none | Relies on prmdiv | |
| prmdivdiv | none | Relies on prmdiveq | |
| phisum | none | May be provable once summation is better developed | |
| unben | none | not possible as stated, as shown by ~ exmidunben | |
| isstruct2 | ~ isstruct2im , ~ isstruct2r | The difference is the addition of the ` F e. V ` condition for the reverse direction. | |
| isstruct | ~ isstructim , ~ isstructr | The difference is the addition of the ` F e. V ` condition for the reverse direction. | |
| slotfn | ~ slotslfn | ||
| strfvnd | ~ strnfvnd | ||
| strfvn | ~ strnfvn | ||
| strfvss | ~ strfvssn | ||
| setsval | ~ setsvala | ||
| setsidvald | ~ strsetsid | ||
| fsets | none | Apparently would need decidable equality on ` A ` or some other condition. | |
| setsdm | none | The set.mm proof relies on undif1 | |
| setsstruct2 | none | The set.mm proof relies on setsdm | |
| setsexstruct2 , setsstruct | none | The set.mm proofs rely on setsstruct2 | |
| setsres | ~ setsresg | ||
| setsabs | ~ setsabsd | ||
| strfvd | ~ strslfvd | ||
| strfv2d | ~ strslfv2d | ||
| strfv2 | ~ strslfv2 | ||
| strfv | ~ strslfv | ||
| strfv3 | ~ strslfv3 | ||
| strssd | ~ strslssd | ||
| strss | ~ strslss | ||
| str0 | ~ strsl0 | ||
| strfvi | none | The set.mm proof uses excluded middle to combine the proper class and set cases. | |
| setsid | ~ setsslid | ||
| setsnid | ~ setsslnid | ||
| sbcie2s | none | Apparently would require conditions that ` A ` and ` B ` are sets. | |
| sbcie3s | none | Apparently would require conditions that ` A ` , ` B ` , and ` C ` are sets. | |
| elbasfv , elbasov , strov2rcl | none | The set.mm proofs rely on excluded middle. | |
| basprssdmsets | none | The set.mm proof relies on setsdm | |
| ressval | ~ ressid2 , ~ ressval2 | For the ` B C_ A ` and ` -. B C_ A ` cases, respectively. | |
| ressbas | none | Apparently needs to have conditions added, for example that ` W ` is a set plus one of ` B C_ A ` or ` -. B C_ A ` . | |
| ressbas2 , ressbasss | none | The set.mm proof relies on ressbas . | |
| resslem , ress0 | none | The set.mm proof relies on excluded middle. | |
| ressinbas | none | Apparently needs to have conditions added, for example that ` W ` is a set plus one of ` B C_ A ` or ` -. B C_ A ` . | |
| ressval3d | none | The set.mm proof relies on setsidvald and sspss . | |
| ressress | none | The set.mm proof relies on ressinbas and excluded middle. | |
| ressabs | none | The set.mm proof relies on ressress but at first glance this would appear to be feasible given the ` B C_ A ` condition. | |
| strle1 | ~ strle1g | ||
| strle2 | ~ strle2g | ||
| strle3 | ~ strle3g | ||
| 1strstr | ~ 1strstrg | ||
| 2strstr | ~ 2strstrg | ||
| 2strbas | ~ 2strbasg | ||
| 2strop | ~ 2stropg | ||
| 2strstr1 | ~ 2strstr1g | ||
| 2strbas1 | ~ 2strbas1g | ||
| 2strop1 | ~ 2strop1g | ||
| grpstr | ~ grpstrg | ||
| grpbase | ~ grpbaseg | ||
| grpplusg | ~ grpplusgg | ||
| ressplusg | none | The set.mm proof relies on resslem | |
| grpbasex , grpplusgx | ~ grpbaseg , ~ grpplusgg | Marked as discouraged even in set.mm. | |
| rngstr | ~ rngstrg | ||
| rngbase | ~ rngbaseg | ||
| rngplusg | ~ rngplusgg | ||
| rngmulr | ~ rngmulrg | ||
| ressmulr , ressstarv | none | The set.mm proof relies on resslem | |
| srngstr | ~ srngstrd | ||
| srngbase | ~ srngbased | ||
| srngplusg | ~ srngplusgd | ||
| srngmulr | ~ srngmulrd | ||
| srnginvl | ~ srnginvld | ||
| lmodstr | ~ lmodstrd | ||
| lmodbase | ~ lmodbased | ||
| lmodplusg | ~ lmodplusgd | ||
| lmodsca | ~ lmodscad | ||
| lmodvsca | ~ lmodvscad | ||
| ipsstr | ~ ipsstrd | ||
| ipsbase | ~ ipsbased | ||
| ipsaddg | ~ ipsaddgd | ||
| ipsmulr | ~ ipsmulrd | ||
| ipssca | ~ ipsscad | ||
| ipsvsca | ~ ipsvscad | ||
| ipsip | ~ ipsipd | ||
| resssca , ressvsca , ressip | none | The set.mm proof relies on resslem | |
| phlstr , phlbase , phlplusg , phlsca , phlvsca , phlip | none | Intuitionizing these will be straightforward once we get around to it, in a manner similar to ~ lmodstrd . The proofs will use theorems like ~ strle1g , ~ strleund , and ~ opelstrsl . | |
| topgrpstr | ~ topgrpstrd | ||
| topgrpbas | ~ topgrpbasd | ||
| topgrpplusg | ~ topgrpplusgd | ||
| topgrptset | ~ topgrptsetd | ||
| resstset | none | The set.mm proof relies on resslem | |
| otpsstr , otpsbas , otpstset , otpsle | none | Unused in set.mm. If we want to develop this more we may need to figure out whether to define order in terms of ` < ` or ` <_ ` as the relationship between those may be different without excluded middle. | |
| 0rest | none | Might need a ` A e. _V ` condition added, and this theorem seems to be mostly be used in conjunction with excluded middle. | |
| topnval | ~ topnvalg | ||
| topnid | ~ topnidg | ||
| topnpropd | ~ topnpropgd | ||
| prdsbasex | none | Would need some conditions on whether ` R ` is a function, on set existence, or the like. However, it is unused in set.mm. | |
| imasvalstr , prdsvalstr , prdsvallem , prdsval , prdssca , prdsbas , prdsplusg , prdsmulr , prdsvsca , prdsip , prdsle , prdsless , prdsds , prdsdsfn , prdstset , prdshom , prdsco , prdsbas2 , prdsbasmpt , prdsbasfn , prdsbasprj , prdsplusgval , prdsplusgfval , prdsmulrval , prdsmulrfval , prdsleval , prdsdsval , prdsvscaval , prdsvscafval , prdsbas3 , prdsbasmpt2 , prdsbascl , prdsdsval2 , prdsdsval3 , pwsval , pwsbas , pwselbasb , pwselbas , pwsplusgval , pwsmulrval , pwsle , pwsleval , pwsvscafval , pwsvscaval , pwssca , pwsdiagel , pwssnf1o | none | At a minimum, these theorems would need new set existence conditions and other routine intuitionizing. At worst, they would need a bigger revamp for things like how order works. | |
| df-ordt , df-xrs , and all theorems involving ordTop or RR*s | none | The set.mm definitions would not seem to fit with constructive definitions of these concepts (for example, the ` if ` in df-xrs would apparently needed to be expressed in terms of a suitable maximum and perhaps other changes are needed too) | |
| df-qtop , df-imas , df-qus and all theorems defined in terms of quotient topology, image structure, and quotient ring. | none | presumably could be added in some form | |
| df-xps and all theorems mentioning the binary product on a structure (syntax Xs.) | none | The set.mm definition depends on df-cda ( +c ), df-imas ( "s ), and df-prds ( Xs_ ) | |
| df-mre , df-mrc and all theorems using the Moore or mrCls syntax | none | The closest we have currently is ~ df-cls but even that doesn't function as it does in set.mm (because complements are different without excluded middle). | |
| df-cnfld and all theorems using CCfld | none | Could presumably be defined in some form, but we'd have to look at the literature definitions of a constructive field and see how we'd need to define this. Plus questions about whether to define order in terms of ` < ` or ` <_ ` . | |
| istop2g | ~ istopfin | ||
| iinopn | none | The set.mm proof relies on abrexfi | |
| riinopn | none | The set.mm proof relies on iinopn (the other issues in the set.mm proof could apparently be handled by ~ fin0or ). | |
| rintopn | none | The set.mm proof relies on riinopn | |
| toponsspwpw | ~ toponsspwpwg | ||
| toprntopon | none | Presumably could be proved but the set.mm proof does not work as it is. | |
| topsn | none | The set.mm proof relies on pwsn | |
| tpsprop2d | none | The set.mm proof does not work as-is. Unused in set.mm | |
| basdif0 | none | The set.mm proof relies on undif1 | |
| 0top | none | The set.mm proof relies on sssn | |
| en2top | none | The set.mm proof relies on strict dominance | |
| 2basgen | ~ 2basgeng | ||
| tgdif0 | none | The set.mm proof relies on excluded middle | |
| indistopon | none | The set.mm proof relies on sspr | |
| indistop , indisuni | none | The set.mm proof relies on indistopon | |
| fctop | none | The set.mm proof relies on theorems we don't have including con1d , ssfi , unfi , rexnal , and difindi . | |
| fctop2 | none | The set.mm proof relies on fctop | |
| cctop | none | The set.mm proof relies on theorems we don't have including con1d , rexnal , and difindi . | |
| ppttop , pptbas | none | The set.mm proof relies on theorems we don't have including orrd and ianor | |
| indistpsx , indistps , indistps2 , indistpsALT , indistps2ALT | none | The set.mm proofs rely on indiscrete topology theorems we don't have | |
| isopn2 | none | The set.mm proof relies on dfss4 | |
| opncld | none | The set.mm proof relies on isopn2 | |
| iincld | none | The set.mm proof relies on opncld | |
| intcld | none | The set.mm proof relies on iincld | |
| incld | none | The set.mm proof relies on intcld | |
| riincld | none | The set.mm proof relies on iincld , incld , and case elimination | |
| clscld | none | The set.mm proof relies on intcld | |
| clsf | none | The set.mm proof relies on clscld | |
| clsval2 | none | The set.mm proof relies on dfss4 and opncld | |
| ntrval2 | none | The set.mm proof relies on dfss4 and clsval2 | |
| ntrdif , clsdif | none | ||
| cmclsopn | none | The set.mm proof relies on dfss4 and clsval2 | |
| cmntrcld | none | The set.mm proof relies on opncld | |
| iscld3 , iscld4 | none | ||
| clsidm | none | The set.mm proof relies on clscld | |
| 0ntr | none | The set.mm proof relies on ssdif0 | |
| elcls , elcls2 | none | ||
| clsndisj | none | The set.mm proof relies on elcls | |
| elcls3 | none | The set.mm proof relies on elcls | |
| opncldf1 , opncldf2 , opncldf3 | none | The set.mm proofs rely on dfss4 and opncld | |
| isclo | none | One direction of the biconditional may be provable by taking the set.mm proof and replacing undif with ~ undifss | |
| isclo2 | none | The set.mm proof relies on isclo | |
| indiscld | none | Something along these lines may be possible once we define the indiscrete topology | |
| neips | ~ neipsm | ||
| neindisj | none | The set.mm proof relies on clsndisj | |
| opnnei | none | Apparently the set.mm proof could easily be adapted for the case in which ` S ` is inhabited | |
| neindisj2 | none | The set.mm proof relies on elcls | |
| neipeltop , neiptopuni , neiptoptop , neiptopnei , neiptopreu | none | The set.mm proofs rely on several theorems we do not have. | |
| df-lp and all theorems using the limPt syntax | none | ||
| df-perf and all theorems using the Perf syntax | none | ||
| restbas | ~ restbasg | ||
| restsn2 | none | The set.mm proof relies on topsn | |
| restcld | none | The set.mm proof relies on opncld | |
| restcldi | none | The set.mm proof relies on restcld | |
| restcldr | none | The set.mm proof relies on restcld | |
| restfpw | none | The set.mm proof relies on ssfi | |
| neitr | none | The set.mm proof relies on inundif | |
| restcls | none | The set.mm proof relies on clscld | |
| restntr | none | The set.mm proof relies on excluded middle | |
| resstopn | none | The set.mm proof relies on resstset | |
| resstps | none | The set.mm proof relies on resstopn | |
| lmrel | ~ lmreltop | ||
| iscnp2 | ~ iscnp | ||
| cnptop1 , cnptop2 | none | ||
| cnprcl | ~ cnprcl2k | ||
| cnpf , cnpcl | ~ cnpf2 | ||
| cnprcl2 | ~ cnprcl2k | ||
| cnpimaex | ~ icnpimaex | ||
| cnpco | ~ cnptopco | ||
| iscncl | none | The set.mm proof relies on opncld | |
| cncls2i | none | The set.mm proof relies on clscld | |
| cnclsi | none | The set.mm proof relies on cncls2i | |
| cncls2 | none | The set.mm proof relies on cncls2i and iscncl | |
| cncls | none | The set.mm proof relies on cncls2 and cnclsi | |
| cncnp2 | ~ cncnp2m | ||
| cnpresti | ~ cnptopresti | ||
| cnprest | ~ cnptoprest | ||
| cnprest2 | ~ cnptoprest2 | ||
| cnindis | none | The set.mm proof relies on indiscrete topology theorems that we don't have. | |
| paste | none | The set.mm proof relies on restcldr | |
| lmcls , lmcld | none | The set.mm proof relies on elcls | |
| lmcnp | ~ lmtopcnp | ||
| df-cmp and all compactness (syntax Comp) theorems | none | How compactness fares without excluded middle is a complicated topic. See for example [HoTT], section 11.5. | |
| df-haus and all Hausdorff (syntax Haus) theorems | none | Perhaps there would need to be an apartness relation to replace the use of negated equality. | |
| df-conn and all connected toplogy (syntax Conn) theorems | none | would apparently need a lot of changes to work | |
| df-1stc and all first-countable theorems | none | Worth considering the definition of countable seen in theorems such as ~ ctm and ~ finct , as well as whatever else might come up. | |
| df-2ndc and all second-countable theorems | none | Worth considering the definition of countable seen in theorems such as ~ ctm and ~ finct , as well as whatever else might come up. | |
| df-lly and all theorems using the Locally syntax | none | ||
| df-xko and all theorems using the compact-open topology syntax (^ko) | none | not clear what is possible here | |
| ptval | none | This would need more extensive development of theorems related to the Xt_ syntax (not just ~ df-pt itself). | |
| ptpjpre1 | none | Perhaps would be provable in the case where ` A ` has decidable equality. | |
| elpt , elptr , elptr2 , ptbasid , ptuni2 , ptbasin , ptbasin2 , ptbas , ptpjpre2 , ptbasfi , pttop , ptopn , ptopn2 | none | Although some parts of these product topology theorems may be intuitionizable, it isn't clear doing so would produce a set of theorems which function as desired. | |
| txcld | none | The set.mm proof relies on difxp | |
| txcls | none | The set.mm proof relies on txcld | |
| txcnpi | none | Should be provable (via ~ icnpimaex and ~ cnpf2 ) but may need an additional ` L e. Top ` hypothesis. | |
| ptcld | none | The set.mm proof depends on pttop , boxcutc , ptopn2 , and riincld | |
| dfac14 | none | The left hand side implies excluded middle by ~ acexmid ; we could see whether the proof that the right hand side implies choice is also valid without excluded middle. | |
| txindis | none | The set.mm proof relies on excluded middle, indistop , and indisuni . | |
| df-hmeo and all theorems using the Homeo syntax | none | apparently intuitionizable | |
| xmetrtri2 | none | Presumably this or something similar could be defined once we define RR*s ( df-xrs ) or something along those lines. | |
| xmetgt0 , metgt0 | ~ xmeteq0 , ~ meteq0 | Presumably would require defining apartness on ` X ` or something along those lines. | |
| xbln0 | ~ xblm | ||
| blin | ~ blininf | ||
| setsmsbas | ~ setsmsbasg | ||
| setsmsds | ~ setsmsdsg | ||
| setsmstset | ~ setsmstsetg | ||
| setsmstopn , setsxms , setsms , tmsval , tmslem , tmsbas , tmsds , tmstopn , tmsxms , tmsms | none | Presumably could prove these or similar theorems, analogous to ~ setsmsbasg | |
| blcld | none | The set.mm proof relies on xrltnle | |
| blcls | none | The set.mm proof relies on blcld | |
| blsscls | none | The set.mm proof relies on blcls | |
| stdbdmetval | ~ bdmetval | ||
| stdbdxmet | ~ bdxmet | ||
| stdbdmet | ~ bdmet | ||
| stdbdbl | ~ bdbl | ||
| stdbdmopn | ~ bdmopn | ||
| ressxms , ressms | none | Awaits revision of ~ df-ress as described at Clean up multifunction restriction operator for extensible structures in iset.mm | |
| prdsxms , prdsms | none | This would need more extensive development of theorems related to the Xs_ syntax (not just ~ df-prds itself). | |
| pwsxms , pwsms | none | This would need more extensive development of theorems related to the ^s syntax (not just ~ df-pws itself). | |
| txmetcnp | none | The set.mm proof depends on df-xps and related theorems | |
| txmetcn | none | The set.mm proof depends on txmetcnp | |
| dscmet , dscopn | none | The set.mm definition for the discrete metric, and the proofs, would seem to rely on equality being decidable. | |
| qtopbaslem | ~ qtopbasss | ||
| iooretop | ~ iooretopg | ||
| icccld , icopnfcld , iocmnfcld , qdensere | none | depend on various closed set theorems | |
| cnfldtopn | none | if we use ` ( MetOpen `` ( abs o. - ) ) ` as our notation for the topology of the complex numbers, this theorem is not needed | |
| cnfldtopon | ~ cntoptopon | ||
| cnfldtop | ~ cntoptop | ||
| qdensere2 | none | the set.mm proof depends on qdensere | |
| blcvx | none | presumably provable for either the ` T = 0 ` case or the ` T e. ( 0 (,] 1 ) ` case; set.mm uses excluded middle to combine those two cases | |
| tgioo2 | ~ tgioo2cntop | ||
| rerest | ~ rerestcntop | ||
| tgioo3 | none | Until we have defined RRfld (presumably closely related to the issues described at the df-cnfld entry here), we can use ` ( topGen `` ran (,) ) ` as a notation for the topology of the real numbers (as seen at ~ tgioo2cntop ). | |
| zcld | none | the set.mm proof uses the floor function in ways that we are unlikely to be able to intuitionize | |
| iccntr | none | the set.mm proof uses real number trichotomy in many steps | |
| opnreen | none | the set.mm proof is not usable as-is but it would be interesting to see if some portions can be adapted | |
| rectbntr0 | none | the set.mm proof relies on various theorems we do not have | |
| xmetdcn2 | none | the set.mm theorem is defined in terms of the RR*s syntax and uses txmetcn in the proof | |
| xmetdcn | none | the set.mm theorem is defined in terms of the ordTop syntax and uses xmetdcn2 in the proof | |
| metdcn2 | none | the set.mm proof relies on xmetdcn | |
| metdcn | none | the set.mm proof relies on metdcn2 | |
| msdcn | none | the set.mm proof relies on metdcn2 | |
| cnmpt1ds | none | the set.mm proof relies on msdcn | |
| cnmpt2ds | none | the set.mm proof relies on msdcn | |
| metdsval | none | the set.mm proof uses infex | |
| metdsf | none | the set.mm proof uses infxrcl | |
| addcnlem , addcn , subcn , mulcn | none | the set.mm proof uses txmetcn | |
| divcn | none | the set.mm proof uses mulcn | |