| 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]. Constructive Zermelo-Fraenkel (CZF), also described in Crosilla, is not as easy to formalize in metamath because the Axiom of Restricted Separation would require us to develop the ability to classify formulas as bounded formulas, similar to the machinery we have built up for asserting on whether variables are free in formulas.
Listed here are some examples of starting points for your journey through the maze. Some are stated just as they would be in a non-constructive context; others are here to highlight areas which look different constructively. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory.
The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic Cross-Reference useful.
| Propositional calculus Predicate calculus Set theory Real and complex numbers |
For the student or master of classical mathematics, constructive mathematics can be baffling. One can get over some of the intial hurdles of understanding how constructive mathematics works and why it might be interesting by reading [Bauer] but that work does little to explain in concrete terms how to write proofs in intuitionistic logic. Fortunately, metamath helps with one of the biggest hurdles: noticing when one is even using the law of the excluded middle or the axiom of choice. But suppose you have a classical proof from the Metamath Proof Explorer and it fails to verify when you copy it over to the Intuitionistic Logic Explorer. What then? Here are some rules of thumb in converting classical proofs to intuitionistic ones.
This is a list of theorems from the Metamath Proof Explorer (which assumes the law of the excluded middle throughout) which we do not have in the Intuitionistic Logic Explorer (generally because they are not provable without the law of the excluded middle, although some could be proved but aren't for a variety of reasons), together with the closest replacements.
| set.mm | iset.mm | notes | |
|---|---|---|---|
| ax-3 , con4d , con34b , necon4bd | ~ con3 | The form of contraposition which removes negation does not hold in intutionistic logic. | |
| pm2.18 | ~ pm2.01 | See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these. | |
| pm2.18d , pm2.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 | ||
| 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 | ||
| 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 | ||
| imor , imori | ~ imorr , ~ imorri , ~ imordc | ||
| pm4.63 | ~ pm3.2im | ||
| iman | ~ imanim | ||
| annim | ~ annimim | ||
| oran | ~ oranim | ||
| ianor | ~ pm3.14 | ||
| biluk | ~ bilukdc | ||
| ecase3d | none | This is a form of case elimination. | |
| dedlem0b | ~ dedlemb | ||
| 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 | ||
| exmo | ~ exmonim | ||
| mo2 | ~ mo2r , ~ mo3 | ||
| nne | ~ nner , ~ nnedc | ||
| exmidne | ~ dcne | ||
| neor | ~ pm2.53 , ~ ori , ~ ord | ||
| neorian | ~ pm3.14 | ||
| nnel | none | The reverse direction could be proved; the forward direction is double negation elimination. | |
| nfrald | ~ nfraldxy , ~ nfraldya | ||
| rexnal | ~ rexnalim | ||
| rexanali | none | ||
| nrexralim | none | ||
| dfral2 | ~ ralexim | ||
| dfrex2 | ~ rexalim | ||
| nfrexd | ~ nfrexdxy , ~ nfrexdya | ||
| nfral | ~ nfralxy , ~ nfralya | ||
| nfra2 | ~ nfra1 , ~ nfralya | ||
| nfrex | ~ nfrexxy , ~ nfrexya | ||
| r19.30 | none | ||
| r19.35 | ~ r19.35-1 | ||
| ralcom2 | ~ ralcom | ||
| nss | ~ nssr | ||
| sspss | ~ sspssr | ||
| n0f | ~ n0rf | ||
| n0 | ~ n0r , ~ fin0 , ~ fin0or | ||
| neq0 | ~ neq0r | ||
| reximdva0 | ~ reximdva0m | ||
| rabn0 | ~ rabn0m , ~ rabn0r | ||
| ssdif0 | ~ ssdif0im | ||
| inssdif0 | ~ inssdif0im | ||
| undif1 | ~ undif1ss | ||
| undif2 | ~ undif2ss | ||
| inundif | ~ inundifss | ||
| undif | ~ undifss | ||
| ssundif | ~ ssundifim | ||
| uneqdifeq | ~ uneqdifeqim | ||
| r19.2z | ~ r19.2m | ||
| r19.45zv | ~ r19.45mv | ||
| dfif2 | ~ df-if | ||
| ifsb | none | ||
| dfif4 | none | Unused in set.mm | |
| dfif5 | none | Unused in set.mm | |
| ifnot | none | ||
| ifan | none | ||
| ifor | none | ||
| ifeq1da, ifeq2da | none | ||
| ifclda | none | ||
| ifeqda | none | ||
| elimif , ifbothda , ifid , eqif , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD | none | ||
| ifboth | ~ ifbothdc | ||
| ifcl , ifcld | ~ ifcldcd | ||
| dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel , ifex , ifexg | none | Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form. | |
| difsnid | ~ difsnss | One direction, for any set | |
| ~ nndifsnid | for a natural number | ||
| ~ fidifsnid | for a finite set | ||
| iundif2 | ~ iundif2ss | ||
| iindif2 | ~ iindif2m | ||
| iinin2 | ~ iinin2m | ||
| iinin1 | ~ iinin1m | ||
| iinvdif | ~ iindif2m | Unused in set.mm | |
| riinn0 | ~ riinm | ||
| riinrab | ~ iinrabm | ||
| iinuni | ~ iinuniss | ||
| iununi | ~ iununir | ||
| rintn0 | ~ rintm | ||
| trintss | ~ trintssm | ||
| trint0 | ~ trint0m | ||
| 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 | |
| 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 | |
| nssss | ~ nssssr | ||
| opex | ~ opexg , ~ opex | The iset.mm version of ~ opex has additional hypotheses | |
| df-so | ~ df-iso | Although we define ` Or ` to describe a weakly linear order (such as real numbers), there are some orders which are also trichotomous, for example ~ nntri3or , ~ pitri3or , and ~ nqtri3or . | |
| sotric | ~ sotricim | One direction, for any weak linear order. | |
| ~ sotritric | For a trichotomous order. | ||
| ~ nntri2 | For the specific order ` _E Or _om ` | ||
| ~ pitric | For the specific order ` | ||
| ~ 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 | |
| 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. | |
| ordtri2or2 | ~ nntri2or2 | ordtri2or2 implies excluded middle as shown at ~ ordtri2or2exmid . | |
| ordtri1 , ontri1 , onssneli , onssnel2i | ~ ssnel , ~ nntri1 | ~ ssnel is a trichotomy-like theorem which does hold, although it is an implication whereas ordtri1 is a biconditional. ~ nntri1 is biconditional, but just for natural numbers. | |
| ordtr2 , ontr2 | none | Implies excluded middle as shown at ~ ontr2exmid | |
| ordtr3 | none | This is weak linearity of ordinals, which presumably implies excluded middle by ~ ordsoexmid . | |
| ordtri2or | none | Implies excluded middle as shown at ~ ordtri2orexmid . | |
| ord0eln0 , on0eln0 | ~ ne0i , ~ nn0eln0 | ||
| nsuceq0 | ~ nsuceq0g | ||
| ordsssuc | ~ trsucss | ||
| ordequn | none | If you know which ordinal is larger, you can achieve a similar result via theorems such as ~ oneluni or ~ ssequn1 . | |
| ordun | ~ onun2 | ||
| dmxpid | ~ dmxpm | ||
| relimasn | ~ imasng | ||
| opswap | ~ opswapg | ||
| cnvso | ~ cnvsom | ||
| iotaex | ~iotacl , ~ euiotaex | ||
| dffun3 | ~ dffun5r | ||
| dffun5 | ~ dffun5r | ||
| 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 ` | ||
| ndmfv | ~ ndmfvg | The ` -. A e. _V ` case is ~ fvprc . | |
| elfvdm | ~ relelfvdm | ||
| elfvex | ~ relelfvdm | ||
| f0cli | ~ ffvelrn | ||
| dff3 | ~ dff3im | ||
| dff4 | ~ dff4im | ||
| fvunsn | ~ fvunsng | ||
| funiunfv | ~ fniunfv , ~ funiunfvdm | ||
| funiunfvf | ~ funiunfvdmf | ||
| eluniima | ~ eluniimadm | ||
| riotaex | ~ riotacl , ~ riotaexg | ||
| nfriotad | ~ nfriotadxy | ||
| csbriota , csbriotagOLD | ~ csbriotag | ||
| riotaxfrd | none | Although it may be intuitionizable, it is lightly used in set.mm. | |
| ovex | ~ fnovex | when the operation is a function evaluated within its domain. | |
| ~ 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. | ||
| fnov | ~ fnovim | ||
| ov3 | ~ ovi3 | Although set.mm's ov3 could be proved, it is only used a few places in set.mm, and in iset.mm those places need the modified form found in ~ ovi3 . | |
| oprssdm | none | ||
| ndmovg , ndmov | ~ ndmfvg | These theorems are generally used in set.mm for case elimination which is why we just have the general ~ ndmfvg rather than an operation-specific version. | |
| ndmovcl , ndmovcom , ndmovass , ndmovdistr , ndmovord , and ndmovordi | none | These theorems are generally used in set.mm for case elimination and the most straightforward way to avoid them is to add conditions that we are evaluating functions within their domains. | |
| ndmovrcl | ~ elmpt2cl , ~ relelfvdm | ||
| caov4 | ~ caov4d | Note that ~ caov4d has a closure hypothesis. | |
| caov411 | ~ caov411d | Note that ~ caov411d has a closure hypothesis. | |
| caov42 | ~ caov42d | Note that ~ caov42d has a closure hypothesis. | |
| caovdir | ~ caovdird | ~ caovdird adds some constraints about where the operations are evaluated. | |
| caovdilem | ~ caovdilemd | ||
| caovlem2 | ~ caovlem2d | ||
| caovmo | ~ caovimo | ||
| ofval | ~ fnofval | ||
| offn , offveq , caofid0l , caofid0r , caofid1 , caofid2 | none | Assuming we really need to add conditions that the operations are functions being evaluated within their domains, there would be a fair bit of intuitionizing. | |
| ordeleqon | none | ||
| ssonprc | none | not provable (we conjecture), but interesting enough to intuitionize anyway. ` U. A = On -> A e/ V ` is provable, and ` ( B e. On /\ U. A C_ B ) -> A e. V ` is provable. (Why isn't ~ df-pss stated so that the set difference is inhabited? If so, you could prove ` U. A C. On -> A e. V `.) | |
| onint | ~ 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 | 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 yet | Conjectured to be provable. | |
| limsssuc | none yet | Conjectured to be provable. | |
| tfinds | ~ tfis3 | ||
| findsg | ~ uzind4 | findsg presumably could be proved, but there hasn't been a need for it. | |
| xpexr2 | ~ xpexr2m | ||
| 1stval | ~ 1stvalg | ||
| 2ndval | ~ 2ndvalg | ||
| 1stnpr | none | May be intuitionizable, but very lightly used in set.mm. | |
| 2ndnpr | none | May be intuitionizable, but very lightly used in set.mm. | |
| brtpos | ~ brtposg | ||
| ottpos | ~ ottposg | ||
| ovtpos | ~ ovtposg | ||
| pwuninel | ~ pwuninel2 | The set.mm proof of pwuninel uses case elimination. | |
| iunonOLD | ~ iunon | ||
| smofvon2 | ~ smofvon2dm | ||
| tfr1 | ~ tfri1 | ||
| tfr2 | ~ tfri2 | ||
| tfr3 | ~ tfri3 | ||
| tfr2b , recsfnon , recsval | none | These transfinite recursion theorems are lightly used in set.mm. | |
| df-rdg | ~ df-irdg | This definition combines the successor and limit cases (rather than specifying them as separate cases in a way which relies on excluded middle). In the words of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic", "we can still define many of the familiar set-theoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit." | |
| rdgfnon | ~ rdgifnon | ||
| ordge1n0 | ~ ordge1n0im , ~ ordgt0ge1 | ||
| ondif1 | ~ dif1o | In set.mm, ondif1 is used for Cantor Normal Form | |
| ondif2 , dif20el | none | The set.mm proof is not intuitionistic | |
| brwitnlem | none | The set.mm proof is not intuitionistic | |
| om0r | ~ om0 , ~ nnm0r | ||
| om00 | ~ nnm00 | ||
| om00el | none | ||
| suc11reg | ~ suc11g | ||
| frfnom | ~ frecfnom | frecfnom adopts the ` frec ` notation and adds conditions on the characteristic function and initial value. | |
| fr0g | ~ frec0g | frec0g adopts the ` frec ` notation and adds a condition on the characteristic function. | |
| frsuc | ~ frecsuc | frecsuc adopts the ` frec ` notation and adds conditions on the characteristic function and initial value. | |
| om0x | ~ om0 | ||
| oaord1 | none yet | ||
| oaword | ~ oawordi | The other direction presumably could be proven but isn't yet. | |
| omwordi | ~ nnmword | The set.mm proof of omwordi relies on case elimination. | |
| omword1 | ~ nnmword | ||
| nnawordex | ~ nnaordex | nnawordex is only used a few places in set.mm | |
| swoso | none | Unused in set.mm. | |
| ecdmn0 | ~ ecdmn0m | ||
| erdisj, qsdisj, qsdisj2, uniinqs | none | These could presumably be restated to be provable, but they are lightly used in set.mm | |
| xpider | ~ xpiderm | ||
| iiner | ~ iinerm | ||
| riiner | ~ riinerm | ||
| brecop2 | none | This is a form of reverse closure and uses excluded middle in its proof. | |
| erov , erov2 | none | Unused in set.mm. | |
| eceqoveq | none | Unused in set.mm. | |
| df-sdom , relsdom , brsdom , dfdom2 , sdomdom , sdomnen , brdom2 , bren2 , domdifsn | none | Many aspects of strict dominance as developed in set.mm rely on excluded middle and a different definition would be needed if we wanted strict dominance to have the expected properties. | |
| en1b | ~ en1bg | ||
| mapsnen , map1 , pw2f1olem , pw2f1o , pw2eng , pw2en | none | We have not added set exponentiation to iset.mm yet. | |
| snfi | ~ snfig | ||
| difsnen | ~ 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 | |
| enfixsn | none | The set.mm proof relies on difsnen | |
| sbth and its lemmas, sbthb , sbthcl | ~ fisbth | The Schroeder-Bernstein Theorem implies excluded middle | |
| 2pwuninel | ~ 2pwuninelg | ||
| php | ~ phpm | ||
| snnen2o | ~ snnen2og , ~ snnen2oprc | ||
| onomeneq , onfin , onfin2 | none | The set.mm proofs rely on excluded middle | |
| nnsdomo , sucdom2 , sucdom , 0sdom1dom , 1sdom2 , sdom1 | none | iset.mm doesn't yet have strict dominance | |
| modom , modom2 | none | The set.mm proofs rely on excluded middle | |
| 1sdom , unxpdom , unxpdom2 , sucxpdom | none | iset.mm doesn't yet have strict dominance | |
| pssinf | none | The set.mm proof relies on sdomnen | |
| fisseneq | none | The set.mm proof relies on excluded middle | |
| ominf | none | Although this theorem presumably could be proved, it would probably need a very different proof than the set.mm one | |
| isinf | none | The set.mm proof uses the converse of ~ ssdif0im | |
| fineqv | none | The set.mm proof relies on theorems we don't have, and even for the theorems we do have, we'd need to carefully look at what axioms they rely on. | |
| pssnn | none | The set.mm proof uses excluded middle. | |
| ssnnfi | none | The proof in ~ ssfiexmid would apply to this as well as to ssfi , since ` { (/) } e. _om ` | |
| ssfi | none | Implies excluded middle as shown at ~ ssfiexmid | |
| domfi | none | The set.mm proof is in terms of ssfi | |
| xpfir | none | Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi | |
| infi | none | Presumably the proof of ~ ssfiexmid could be adapted to show this implies excluded middle | |
| rabfi | none | Presumably the proof of ~ ssfiexmid could be adapted to show this implies excluded middle | |
| finresfin | none | The set.mm proof is in terms of ssfi | |
| f1finf1o | none | The set.mm proof is not intuitionistic | |
| nfielex | none | The set.mm proof relies on neq0 | |
| en1eqsn , en1eqsnbi | none | The set.mm proof relies on fisseneq | |
| diffi | ~ 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. | |
| unfi | none | Not provable according to Remark 8.1.17 of [AczelRathjen]. | |
| ax-reg , axreg2 , zfregcl | ~ ax-setind | ax-reg implies excluded middle as seen at ~ regexmid | |
| df-rank and all theorems realted 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. | |
| entri3 | ~ fientri3 | Because full entri3 is equivalent to the axiom of choice, it implies excluded middle. | |
| 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). | |
| 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 , 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 | ||
| lttri2i | none | This can be read as "two real numbers are non-equal if and only if they are apart" which relies on excluded middle | |
| lttrid , lttri2d , 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. | |
| ltordlem , ltord1 , leord1 , eqord1 , ltord2 , leord2 , eqord2 | none | These depend on real number trichotomy and are not used until later in set.mm. | |
| wloglei , wlogle | none | These depend on real number trichotomy and are not used until later in set.mm. | |
| recex | ~ recexap | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcand, mulcan2d | ~ mulcanapd , ~ mulcanap2d | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcanad , mulcan2ad | ~ mulcanapad , ~ mulcanap2ad | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulcan , mulcan2 , mulcani | ~ mulcanap , ~ mulcanap2 , ~ mulcanapi | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mul0or , mul0ori , mul0ord | none | Remark 2.19 of [Geuvers] says that this does not hold in general and has a counterexample. | |
| mulne0b , mulne0bd , mulne0bad , mulne0bbd | ~ mulap0b , ~ mulap0bd , ~ mulap0bad , ~ mulap0bbd | ||
| mulne0 , mulne0i , mulne0d | ~ mulap0 , ~ mulap0i , ~ mulap0d | ||
| receu | ~ receuap | In theorems involving reciprocals or division, not equal to zero changes to apart from zero. | |
| mulnzcnopr | none | ||
| msq0i , msq0d | ~ 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 | ||
| divdir , divcan3 , divcan4 | ~ divdirap , ~ divcanap3 , ~ divcanap4 | ||
| div11 , divid , div0 | ~ div11ap , ~ dividap , ~ div0ap | ||
| diveq1 , divneg , divsubdir | ~ diveqap1 , ~ divnegap , ~ divsubdirap | ||
| recrec , rec11 , rec11r | ~ recrecap , ~ rec11ap , ~ rec11rap | ||
| divmuldiv , divdivdiv , divcan5 | ~ divmuldivap , ~ divdivdivap , ~ divcanap5 | ||
| divmul13 , divmul24 , divmuleq | ~ divmul13ap , ~ divmul24ap , ~ divmuleqap | ||
| recdiv , divcan6 , divdiv32 , divcan7 | ~ recdivap , ~ divcanap6 , ~ divdiv32ap , ~ divcanap7 | ||
| dmdcan , divdiv1 , divdiv2 , recdiv2 | ~ dmdcanap , ~ divdivap1 , ~ divdivap2 , ~ recdivap2 | ||
| ddcan , divadddiv , divsubdiv | ~ ddcanap , ~ divadddivap , ~ divsubdivap | ||
| ddcan , divadddiv , divsubdiv | ~ ddcanap , ~ divadddivap , ~ divsubdivap | ||
| conjmul , rereccl, redivcl | ~ conjmulap , ~ rerecclap , ~ redivclap | ||
| div2neg , divneg2 | ~ div2negap , ~ divneg2ap | ||
| recclzi , recne0zi , recidzi | ~ recclapzi , ~ recap0apzi , ~ recidapzi | ||
| reccli , recidi , recreci | ~ recclapi , ~ recidapi , ~ recrecapi | ||
| dividi , div0i | ~ dividapi , ~ div0api | ||
| divclzi , divcan1zi , divcan2zi | ~ divclapzi , ~ divcanap1zi , ~ divcanap2zi | ||
| divreczi , divcan3zi , divcan4zi | ~ divrecapzi , ~ divcanap3zi , ~ divcanap4zi | ||
| rec11i , rec11ii | ~ rec11api , ~ rec11apii | ||
| divcli , divcan2i , divcan1i , divreci , divcan3i , divcan4i | ~ divclapi , ~ divcanap2i , ~ divcanap1i , ~ divrecapi , ~ divcanap3i , ~ divcanap4i | ||
| div0i | ~ divap0i | ||
| divasszi , divmulzi , divdirzi , divdiv23zi | ~ divassapzi , ~ divmulapzi , ~ divdirapzi , ~ divdiv23apzi | ||
| divmuli , divdiv32i | ~ divmulapi , ~ divdiv32api | ||
| divassi , divdiri , div23i , div11i | ~ divassapi , ~ divdirapi , ~ div23api , ~ div11api | ||
| divmuldivi, divmul13i, divadddivi, divdivdivi | ~ divmuldivapi , ~ divmul13api , ~ divadddivapi , ~ divdivdivapi | ||
| rerecclzi , rereccli , redivclzi , redivcli | ~ rerecclapzi , ~ rerecclapi , ~ redivclapzi , ~ redivclapi | ||
| reccld , rec0d , recidd , recid2d , recrecd , dividd , div0d | ~ recclapd , ~ recap0d , ~ recidapd , ~ recidap2d , ~ recrecapd , ~ dividapd , ~ div0apd | ||
| divcld , divcan1d , divcan2d , divrecd , divrec2d , divcan3d , divcan4d | ~ divclapd , ~ divcanap1d , ~ divcanap2d , ~ divrecapd , ~ divrecap2d , ~ divcanap3d , ~ divcanap4d | ||
| diveq0d , diveq1d , diveq1ad , diveq0ad , divne1d , div0bd , divnegd , divneg2d , div2negd | ~ diveqap0d , ~ diveqap1d , ~ diveqap1ad , ~ diveqap0ad , ~ divap1d , ~ divap0bd , ~ divnegapd , ~ divneg2apd , ~ div2negapd | ||
| divne0d , recdivd , recdiv2d , divcan6d , ddcand , rec11d | ~ divap0d , ~ recdivapd , ~ recdivap2d , ~ divcanap6d , ~ ddcanapd , ~ rec11apd | ||
| divmuld , div32d , div13d , divdiv32d , divcan5d , divcan5rd , divcan7d , dmdcand , dmdcan2d , divdiv1d , divdiv2d | ~ divmulapd , ~ div32apd , ~ div13apd , ~ divdiv32apd , ~ divcanap5d , ~ divcanap5rd , ~ divcanap7d , ~ dmdcanapd , ~ dmdcanap2d , ~ divdivap1d , ~ divdivap2d | ||
| divmul2d, divmul3d, divassd, div12d, div23d, divdird, divsubdird, div11d | ~ divmulap2d , ~ divmulap3d , ~ divassapd , ~ div12apd , ~ div23apd , ~ divdirapd , ~ divsubdirapd , ~ div11apd | ||
| divmuldivd | ~ divmuldivapd | ||
| rereccld , redivcld | ~ rerecclapd , ~ redivclapd | ||
| mvllmuld | ~ mvllmulapd | ||
| elimgt0 , elimge0 | none | Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form. | |
| mulge0b , mulle0b , mulsuble0b | none | Presumably unprovable for reasons analogous to mul0or. | |
| ledivp1i , ltdivp1i | none | Presumably could be proved, but unused in set.mm. | |
| crne0 | ~ crap0 | ||
| ofsubeq0 , ofnegsub , ofsubge0 | none | Depend on ofval and/or offn . | |
| df-nn | ~ dfnn2 | ||
| dfnn3 | ~ dfnn2 | Presumably could be proved, as it is a slight variation of dfnn2 | |
| avgle | none | ||
| nnunb | none | Presumably provable from ~ arch but unused in set.mm. | |
| frnnn0supp , frnnn0fsupp | ~ nn0supp | iset.mm does not yet have either the notation, or in some cases the theorems, related to the support of a function or a fintely supported function. | |
| suprzcl | none | ||
| zriotaneg | none | Lightly used in set.mm | |
| suprfinzcl | none | ||
| decex | ~ deccl | ||
| uzwo , uzwo2 , nnwo , nnwof , nnwos | none | Presumably would imply excluded middle, unless there is something which makes this different from ~ nnregexmid . | |
| uzinfmi , nninfm , nn0infm , infmssuzle , infmssuzcl | none | We do not yet have a supremum notation, or most supremum theorems, in iset.mm | |
| negn0 | ~ negm | ||
| supminf | none | We do not yet have a supremum notation, or most supremum theorems, in iset.mm | |
| zsupss , suprzcl2 , suprzub , uzsupss | none | We do not yet have a supremum notation, or most supremum theorems, in iset.mm | |
| 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 , xrmax2 , xrmin1 , xrmin2 , xrmaxeq , xrmineq , xrmaxlt , xrltmin , xrmaxle , xrlemin , max1 , max2 , min1 , min2 , maxle , lemin , maxlt , ltmin , max0sub , ifle | none | ||
| qbtwnre , qbtwnxr | none yet | These should be provable, but the set.mm proof relies on zbtwnre (which in turn is proved using the least upper bound property). The most straightforward solution is to use a construction-dependent proof in terms of ~ df-iltp (the only complicated part of which is connecting ` Q. ` and ` QQ ` ). This is the solution adopted by Theorem 11.2.6 of [HoTT]. | |
| qsqueeze | none yet | Once we have qbtwnre , we should be able to prove this as a consequence of ~ squeeze0 . | |
| qextltlem , qextlt , qextle | none | The set.mm proof is not intuitionistic. | |
| xralrple , alrple | none yet | If we had qbtwnxr , it looks like the set.mm proof would work with minor changes. | |
| xnegex | ~ xnegcl | ||
| xaddval , xaddf , xmulval , xaddpnf1 , xaddpnf2 , xaddmnf1 , xaddmnf2 , pnfaddmnf , mnfaddpnf , rexadd , rexsub , xaddnemnf , xaddnepnf , xnegid , xaddcl , xaddcom , xaddid1 , xaddid2 , xnegdi , xaddass , xaddass2 , xpncan , xnpcan , xleadd1a , xleadd2a , xleadd1 , xltadd1 , xltadd2 , xaddge0 , xle2add , xlt2add , xsubge0 , xposdif , xlesubadd , xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xaddcld , xmulcld , xadd4d | none | There appears to be no fundamental obstacle to proving these, because disjunctions can arise from ~ elxr rather than excluded middle. However, ` -e ` , ` +e ` , and ` *e ` are lightly used in set.mm, and the set.mm proofs would require significant changes. | |
| ixxub , ixxlb | none | ||
| iccen | none | ||
| supicc , supiccub , supicclub , supicclub2 | none | ||
| ixxun , ixxin | none | ||
| ioo0 | none | Once we have qbtwnxr , it may be possible to rearrange the logic from set.mm so that this proof works (via ~ rabeq0 , ~ ralnex , and ~ xrlenlt perhaps). | |
| ioon0 | none | Presumably non-empty would need to be changed to inhabited, see also discussion at ioo0 | |
| iooid | ~ iooidg | ||
| ndmioo | none | See discussion at ndmov but set.mm uses excluded middle, both in proving this and in using it. | |
| lbioo , ubioo | ~ lbioog , ~ ubioog | ||
| iooin | none | ||
| ico0 , ioc0 | none | Possibly similar to ioo0 ; see discussion there. | |
| icc0 | ~ icc0r | ||
| ioorebas | ~ ioorebasg | ||
| ge0xaddcl , ge0xmulcl | none | Rely on xaddcl and xmulcl ; see discussion in this list for those theorems. | |
| icoun , snunioo , snunico , snunioc , prunioo | none | ||
| ioojoin | none | ||
| difreicc | none | ||
| iccsplit | none | This depends, apparently in an essential way, on real number trichotomy. | |
| xov1plusxeqvd | none | This presumably could be proved if not equal is changed to apart, but is lightly used in set.mm. | |
| fzn0 | ~ fzm | ||
| fz0 | none | Although it would be possible to prove a version of this with the additional conditions that ` 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 | none | Presumably would be provable if real is changed to rational. | |
| intfracq | none | Presumably provable. | |
| fldiv , 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 | |
| df-mod and other modulus theoerms. | none | As with df-fl it may be feasible to define this for rational numbers rather than reals. | |
| om2uz0i | ~ frec2uz0d | ||
| om2uzsuci | ~ frec2uzsucd | ||
| om2uzuzi | ~ frec2uzuzd | ||
| om2uzlti | ~ frec2uzltd | ||
| om2uzlt2i | ~ frec2uzlt2d | ||
| om2uzrani | ~ frec2uzrand | ||
| om2uzf1oi | ~ frec2uzf1od | ||
| om2uzisoi | ~ frec2uzisod | ||
| om2uzoi , ltweuz , ltwenn , ltwefz | none | We do not have a syntax for well ordering and based on theorems like ~ nnregexmid , there is probably little room for this concept. | |
| om2uzrdg | ~ frec2uzrdg | ||
| uzrdglem | ~ frecuzrdglem | ||
| uzrdgfni | ~ frecuzrdgfn | ||
| uzrdg0i | ~ frecuzrdg0 | ||
| uzrdgsuci | ~ frecuzrdgsuc | ||
| uzinf | none | See ominf | |
| uzrdgxfr | none | Presumably could be proved if restated in terms of ` frec ` (a la ~ frec2uz0d ). However, it is lightly used in set.mm. | |
| fzennn | ~ frecfzennn | ||
| fzen2 | ~ frecfzen2 | ||
| cardfz | none | Cardinality does not work the same way without excluded middle and iset.mm has few cardinality related theorems. | |
| hashgf1o | ~ frechashgf1o | ||
| fzfi | ~ fzfig | ||
| fzfid | ~ fzfigd | ||
| fzofi | ~ fzofig | ||
| fsequb | none | Seems like it might be provable, but unused in set.mm | |
| fsequb2 | none | The set.mm proof does not work as-is | |
| fseqsupcl , fseqsupubi | none | iset.mm does not have the "sup" syntax and lacks most supremum theorems from set.mm. | |
| uzindi | none | This could presumably be proved, perhaps from ~ uzind4 , but is lightly used in set.mm | |
| axdc4uz | none | Although some versions of constructive mathematics accept dependent choice, we have not yet developed it in iset.mm | |
| ssnn0fi , rabssnn0fi | none | Conjectured to imply excluded middle along the lines of ~ nnregexmid or ~ ssfiexmid | |
| df-seq | ~ df-iseq | ||
| seqex | ~ iseqex | The only difference is the differing syntax of ` seq ` . | |
| seqeq1 , seqeq2 , seqeq3 , seqeq1d , seqeq2d , seqeq3d , seqeq123d | ~ iseqeq1 , ~ iseqeq2 , ~ iseqeq3 | ||
| nfseq | ~ nfiseq | ||
| seqval | ~ iseqval | ||
| seqfn | ~ iseqfn | ||
| seq1 , seq1i | ~ iseq1 | ||
| seqp1 , seqp1i | ~ iseqp1 | ||
| seqm1 | ~ iseqm1 | ||
| seqcl2 | none yet | Presumably could prove this (with adjustments analogous to ~ iseqp1 ). The third argument to ` seq ` in iset.mm would correspond to ` C ` rather than ` D ` (some of the other ` seq ` related theorems do not allow ` C ` and ` D ` to be different, but seqcl2 does). | |
| seqf2 | none yet | Presumably could prove this, analogously to seqcl2. | |
| seqcl | ~ iseqcl | iseqcl requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seqcl . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqf | ~ iseqf | ||
| seqfveq2 | ~ iseqfveq2 | ||
| seqfeq2 | ~ iseqfeq2 | ||
| seqfveq | ~ iseqfveq | ||
| seqfeq | ~ iseqfeq | ||
| seqshft2 | ~ iseqshft2 | ||
| seqres | none | Should be intuitionizable as with the other ` seq ` theorems, but unused in set.mm | |
| serf | ~ iserf | ||
| serfre | ~ iserfre | ||
| sermono | ~ isermono | isermono requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in sermono . Given that the intention is to use this for infinite series, there may be no need to look into whether this requirement can be relaxed. | |
| seqsplit | ~ iseqsplit | iseqsplit 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, but perhaps this requirement could be relaxed if there is a need. | |
| seq1p | ~ iseq1p | iseq1p requires that ` F ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seq1p . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqcaopr3 | ~ iseqcaopr3 | iseqcaopr3 requires that ` F ` , ` G ` , and ` H ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seqcaopr3 . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqcaopr2 | ~ iseqcaopr2 | iseqcaopr2 requires that ` F ` , ` G ` , and ` H ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seqcaopr2 . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqcaopr | ~ iseqcaopr | iseqcaopr requires that ` F ` , ` G ` , and ` H ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seqcaopr . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqf1o | none | May be adaptable with sufficient attention to issues such as whether the operation ` .+ ` is closed with respect to ` C ` as well as ` S ` , and perhaps other issues. | |
| seradd | ~ iseradd | iseradd requires that ` F ` , ` G ` , and ` H ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in seradd . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| sersub | ~ isersub | isersub requires that ` F ` , ` G ` , and ` H ` be defined on ` ( ZZ>= `` M ) ` not merely ` ( M ... N ) ` as in sersub . This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need. | |
| seqid3 | ~ iseqid3 , ~ iseqid3s | ~ iseqid3 and ~ iseqid3s differ with respect to which entries in ` F ` need to be zero. Further refinements to the hypotheses including where ` F ` needs to be defined and the like might be possible (with a greater amount of work), but perhaps these are sufficient. | |
| seqid | ~ iseqid | ||
| seqid2 | none yet | It should be possible to come up with a (presumably modified) versiona of this, but we have not done so yet. | |
| seqhomo | ~ iseqhomo | ||
| seqz , seqfeq4 , seqfeq3 | none yet | It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet. | |
| seqdistr | ~ iseqdistr | ||
| ser0 | ~ iser0 | The only difference is the syntax of ` seq ` . | |
| ser0f | ~ iser0f | The only difference is the syntax of ` seq ` . | |
| serge0 | ~ serige0 | This theorem uses ` CC ` as the final argument to ` seq ` which probably will be more convenient even if all the values are elements of a subset of ` CC ` . | |
| serle | ~ serile | This theorem uses ` CC ` as the final argument to ` seq ` which probably will be more convenient even if all the values are elements of a subset of ` CC ` . | |
| ser1const , seqof , seqof2 | none yet | It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet. | |
| df-exp | ~ df-iexp | The difference is that ` seq ` in iset.mm takes three arguments compared with two in set.mm. | |
| expval | ~ expival | ||
| expnnval | ~ expinnval | ||
| expneg | ~ expnegap0 | The set.mm theorem does not exclude the case of dividing by zero. | |
| expneg2 | ~ expineg2 | ||
| expn1 | ~ expn1ap0 | ||
| expcl2lem | ~ expcl2lemap | ||
| reexpclz | ~ reexpclzap | ||
| expclzlem | ~ expclzaplem | ||
| expclz | ~ expclzap | ||
| expne0 | ~ expap0 | ||
| expne0i | ~ expap0i | ||
| expnegz | ~ expnegzap | ||
| mulexpz | ~ mulexpzap | ||
| exprec | ~ exprecap | ||
| expaddzlem , expaddz | ~ expaddzaplem , ~ expaddzap | ||
| expmulz | ~ expmulzap | ||
| expsub | ~ expsubap | ||
| expp1z | ~ expp1zap | ||
| expm1 | ~ expm1ap | ||
| expdiv | ~ expdivap | ||
| expcan , expcand | none | Presumably provable, but the set.mm proof uses eqord1 and the theorem is lightly used in set.mm | |
| ltexp2 , leexp2 , leexp2 , ltexp2d , leexp2d | none | Presumably provable, but the set.mm proof uses ltord1 | |
| ltexp2r , ltexp2rd | none | Presumably provable, but the set.mm proof uses ltexp2 | |
| sqdiv | ~ sqdivap | ||
| sqgt0 | ~ sqgt0ap | ||
| iexpcyc | none yet | See discussion under df-mod ; modulus for integers would suffice so issues with modulus for reals would not be an impediment. | |
| sqrecii , sqrecd | ~ exprecap | ||
| sqdivi | ~ sqdivapi | ||
| sqgt0i | ~ sqgt0api | ||
| sqlecan | ~ lemul1 | Unused in set.mm | |
| sqeqori | none | The reverse direction is ~ oveq1 together with ~ sqneg . The forward direction is presumably not provable, see mul0or for more discussion. | |
| subsq0i , sqeqor | none | Variations of sqeqori . | |
| sq01 | none | Lightly used in set.mm. Presumably not provable as stated, for reasons analogous to mul0or . | |
| crreczi | none | Presumably could be proved if not-equal is changed to apart, but unused in set.mm. | |
| expmulnbnd | none | Should be possible to prove this or something similar, but the set.mm proof relies on case elimination based on whether ` 0 <_ A ` or not. | |
| digit2 , digit1 | none | Depends on modulus and floor, and unused in set.mm. | |
| modexp | none | Depends on modulus. Presumably it, or something similar, can be made to work as it is mostly about integers rather than reals. | |
| discr1 , discr | none | The set.mm proof uses real number trichotomy. | |
| sqrecd | ~ sqrecapd | ||
| expclzd | ~ expclzapd | ||
| exp0d | ~ expap0d | ||
| expnegd | ~ expnegapd | ||
| exprecd | ~ exprecapd | ||
| expp1zd | ~ expp1zapd | ||
| expm1d | ~ expm1apd | ||
| expsubd | ~ expsubapd | ||
| sqdivd | ~ sqdivapd | ||
| expdivd | ~ expdivapd | ||
| reexpclzd | ~ reexpclzapd | ||
| sqgt0d | ~ sqgt0apd | ||
| seqshft | none currently | need to figure out how to adjust this for the differences between set.mm and iset.mm concerning ` seq `. | |
| 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 | none | We could prove this for rationals, or 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 | none | This would hold if we defined the maximum of two real numbers and recast this theoerem in terms of that (rather than using ` if ` in a way which relies on real number trichotomy). | |
| absz | none | Although this is presumably provable, the set.mm proof is not intuitionistic and it is lightly used in set.mm | |
| recval | ~ recvalap | ||
| absgt0 , absgt0i | ~ absgt0ap , absgt0api | ||
| absmax | none | The right hand side of this theorem (which is in terms of absolute value) could serve as a definition of maximum, but the left hand side (in terms of ` if ` ) is not well behaved in the absence of trichotomy. | |
| 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 | As described under df-fl , floor is problematic without excluded middle. | |
| rexanre | none yet | May be feasible once we've added maximum for real numbers | |
| rexfiuz | none | Relies on findcard2 | |
| rexuzre | none | Presumably could be intuitionized although it would be easier after we add maximum for real numbers. It is unused in set.mm for whatever that is worth. | |
| rexico | none | May be feasible once we've added maximum for real numbers | |
| caubnd | none | The caubnd proof uses theorems related to finite sets and maximums which are not present in iset.mm, so this will need developing those areas and/or a different approach than set.mm. | |
| 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. | |
| serclim0 | ~ iserclim0 | The only difference is the syntax of ` seq ` . | |
| reccn2 | none yet | Will need to be revamped to deal with negated equality versus apartness and perhaps other issues. | |
| clim2ser | ~ clim2iser | The only difference is the syntax of ` seq ` . | |
| clim2ser2 | ~ clim2iser2 | The only difference is the syntax of ` seq ` . | |
| iserex | ~ iiserex | The only difference is the syntax of ` seq ` . | |
| isermulc2 | ~ iisermulc2 | The only difference is the syntax of ` seq ` . | |
| iserle | ~ iserile | The only difference is the syntax of ` seq ` . | |
| iserge0 | ~ iserige0 | The only difference is the syntax of ` seq ` . | |
| climserle | ~ climserile | The only difference is the syntax of ` seq ` . | |
| isershft | none yet | Relies on seqshft | |
| isercoll and its lemmas, isercoll2 | none yet | The set.mm proof would need modification | |
| climsup | none | To even show convergence would presumably require a hypothesis related to the rate of convergence. Not to mention the lack of much in the way of supremum notation or theorems in iset.mm. | |
| 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. | |
| serf0 | ~ serif0 | The only difference is the syntax of ` seq ` . | |
| iseralt | none | The set.mm proof relies on caurcvg2 which does not specify a rate of convergence. | |
| sumex | none | This will need to replaced by suitable closure theorems. | |
| sumeq2w | sumeq2 | Presumably could be proved, and perhaps also would rely only on extensionality (and logical axioms). But unused in set.mm. | |
| seq1st | none | The second argument to ` seq ` , at least as handled in theorems such as ~ iseqfn , 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 | Several hypotheses are tweaked or added to reflect differences in how ` seq ` works | |
| algrf | ~ ialgrf | Several hypotheses are tweaked or added to reflect differences in how ` seq ` works | |
| algrp1 | ~ ialgrp1 | Several hypotheses are tweaked or added to reflect differences in how ` seq ` works | |
| alginv | ~ ialginv | Two hypotheses are tweaked or added to reflect differences in how ` seq ` works | |
| algcvg | ~ ialgcvg | ` seq ` as defined in ~ df-iseq has a third argument | |
| algcvga | ~ ialgcvga | Two hypotheses are tweaked or added to reflect differences in how ` seq ` works | |
| algfx | ~ ialgfx | Two hypotheses are tweaked or added to reflect differences in how ` seq ` works |
| This
page was last updated on 15-Aug-2015. Your comments are welcome: Norman Megill Copyright terms: Public domain |
W3C HTML validation [external] |


Friday Facts #309 discusses several controversial opinions different members of the dev team have on certain game mechanics. I hastily made some polls and people have, rightly so, pointed out that the phrasing of some of the questions is really confusing. I took the tiles of each section verbatim to make sure that it was clear which proposal you're voting for but didn't realise that having things phrased negatively would muddy the waters. So I suggest you take these results with a heaping of salt.
Since the API for the polls site doesn't support CORS I need to use a reverse proxy (CORS Anywhere). A side effect of this is that the site can bump into the ratelimit so you may be viewing older data.


An editor can also insert text, as this is his prerogative and duty when the writer dropped the, ah, word.


WITNESS LIST
Defense & Veterans' Affairs Committee
May 14, 2014 - 10:00 AM
Interim Charge 4 - Veteran Courts
On:
Allen, Sheila (Nueces County Veterans Treatment Court)
Barill, Angie Juarez (El Paso Veteran Court Program)
Burnett, Christopher (Criminal Justice Division, Office of the Governor)
Cantu, Eliseo (Texas Veterans Commission)
Christian, Wayne (Bexar County Veterans Treatment Court)
Collins, Dominique (Dallas Veteran's Court)
Denton, Mike (Travis County Veteran Court)
Ellis, Ryan (Veterans Treatment Court of Galveston County)
Freeman, Vonda (Dallas County Veterans Court)
Glass, Jackson (Travis County Veterans Court)
Hale, Oscar (Self)
Henry, Mark (Galveston County)
Horne, Marianne (North Texas Addiction Counseling and Education Inc)
Klas, Brian (Williamson County Veterans Court)
Maier, Robert (Williamson County Veterans Court)
Molina, Jason (Nueces County CSCD)
Morrison, Steve (Williamson County Community Supervision and Corrections Department)
Overstreet, Charles (Tarrant County Veterans Court)
Palladino, Thomas (Texas Veterans Commission)
Palomo, Beckie (Self)
Parker, Randall (Bexar County Veterans Treatment Court)
Pierce, Kathy (Williamson County Veterans Court)
Prather, Jude (Hays County and City of San Marcos)
Randolph, Ryan (Tarrant County Veterans Court)
Reed, Leon (Tarrant County Veterans)
Sanchez, David (Cameron County Veterans Court)
Skurka, Mark (Nueces County District Attorney)
Williams, Guy (Nueces County Veteran's Court)
Wright, Tim (Williamson County Veterans Court)
Young, Courtney (Tarrant County Veterans' Court)
Interim Charge 6 - Veterans' Mental Health Policies
On:
Beck, Michael (Military Veteran Peer Network)
Hanna, Sean (Military Veteran Peer Network)
Little, Morgan (Self; Texas Coalition of Veterans Organizations)
Palladino, Thomas (Texas Veterans Commission)
Shore, Sam (Dept. of State Health Services)
Vallarta, Cruz (Self)
1


A metric measure of mass
1000 grams are equal to a kilogram (1000g = 1kg), 1000 kilograms are equal to a tonne (100kg = 1 tonne), 1 gram is are equal to 1000 milligrams (1g = 1000mg)


Heart Disease Prediction System
© All rights reserved by Self-Determination@2005 | Devoloped by Sayantan Das | 2019


Configure Users
Configure Groups
Configure Roles
Add new Users, change user names and passwords, and edit notification information.
Assign and unassign Users to Groups.
Configure Roles that define On Call schedules for users.


A template marker is a special marker symbol created in an Excel template that will be bound to data.
Essential XlsIO allows you to create and bind markers with data from various sources, such as a data table, variables, and arrays. This will allow the user to control the format of the data when it is bound to a template document.
Each marker starts with a prefix, by default it is the "%" character; it is followed by the variable name and properties. There can be several arguments after the variable that are delimited by a character; by default, it is the ";" character.
Click "Create Document" button to view an Excel spreadsheet generated by Essential XlsIO. Please note that Microsoft Excel Viewer or Microsoft Excel is required to view the resultant document.
Data Table CLR Objects


Grids / Multiple Selection
A demonstration of different selection types available in TreeGrid directive for AngularJS. By clicking on check box on the right, you can change the built-in property:
- selectionMode - determines how many rows can be selected at the same time and also changes the selection process
There are four acceptable values:
- 'none' - selection is disabled
- 'one' - Only one row can be selected
- 'multi-simple' - Multiple rows can be selected using mouse clicks or keyboard keys
- 'multi-extended' - Multiple rows can be selected using mouse clicks or keyboard keys, including the SHIFT key
In multi-selection mode, rows can become selected using the CTRL key or Arrow keys. Furthermore by pressing the CTRL+SPACE keys, you can select/deselect rows. The 'multi-extended' mode allows selection of multiple rows in wide range. While SHIFT key is pressed, all rows from first to last clicked row will become selected.


Just hanging around with this project, eventually I'll add more and more fetures.
Take a look at the src/pages/
directory to add or change tabs,
update any existing page or create new pages.
REST services provided by https://jsonplaceholder.typicode.com/


Tan uses two quotes:
"Self-awareness is a neutral mode that maintains self-reflectiveness even in the midst of turbulent emotions."
-Daniel Goleman
"Mindfulness means paying attention in a particular way: on purpose, in the present moment, and non-judgmentally."
-Jon Kabat-Zinn
Basically both concepts exist for the same purpose - being mindful and self aware is to pay attention to yourself and your emotions so as not to let them become or consume you.
Because I already keep a journal I decided to try the body scan technique. Initially I found it difficult to concentrate because the ambience at my place/krd isn't exactly relaxed. However I took my time to really focus and found it to be very soothing. I'm currently quite emotionally exhausted and it was amazing to be able to let everything go for a moment and actually feel it leave my body.
Honeslty I found that part of the chapter so important and definitely something I needed to read. I think it's so easy to forget that our emotions aren't our core selves-that they come and go and we experience them only momentarily. Though I also think it's important to remember that people suffer from chronic depression and anxiety as well as many other forms of mental illness it can take a lot more than being mindful and self aware for them to overcome and deal with it.


view in a browser:
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link3?t_params=I_AERIEBTSTERMS%3DN%26I_AERIELOCMOBILE%3D0%26I_AERIESUM1%3DN%26I_GMAILMOBILE%3D0%26AAP_FLAG%3DN%26CUSTOMER_NBR%3D1235023277209%26EMAIL%3Dhubleeph606%2540tumblr.com&AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Free Shipping & Returns On All Bras
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link11?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Aerie®
Semi-Annual Sale
In Stores & Aerie.com
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link12b?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
make a pretty splash with
30% Off All Swim
Prices As Marked
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link12d?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Shop Swimsuits
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link12f?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Bras $14.99 & Up
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link10a?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Shop Bras
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link10c?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Undies 5 For $16.50*
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link13a?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Shop Undies
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link13c?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Find Sizes 30A - 40DD At Aerie.com
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link16d?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Forward
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link6?RAF_TRACK=&AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Become A Fan On Facebook
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link23?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Follow Us On Twitter
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link7?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Pinterest
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link25?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
shopkick
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link1?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Instagram
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link5?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Come Hang Out…Find A Store
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link20?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Mobile Alerts
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link24?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Download The Aerie App
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link18?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Earn Up To 40% Off
Sign Up For AEREWARDS
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link19?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
***********************************************************
Beginning January 14, 2013 at 6:00 am EST through
June 30, 2013 at 11:59 pm PDT receive automatic free shipping on all
orders with the purchase of one (1) or more Aerie bras. Offer is valid
on orders shipping to U.S. & Canadian addresses only. Offer not valid on
international orders. This offer is good for U.S. standard shipping
within 3 to 7 business days pending credit approval and authorization.
Orders to Canadian addresses will be shipped via Canada post within 6 to
10 business days to urban areas and 15 to 22 business days to rural
areas. Shopping bag must contain at least one (1) Aerie bra to qualify
for free shipping. This free shipping offer can be combined with other
discount offers. No discount code is required at the aerie.com shopping
bag. Not applicable toward previously purchased merchandise. All
deliveries are pending credit approval, merchandise availability,
delivery and weather conditions. Free shipping promotion and associated
terms & conditions subject to change at Aerie’s sole discretion.
Beginning January 14, 2013 at 6:00 am EST through June 30, 2013 at 11:59
pm PDT, and shipping to U.S. & Canadian addresses, receive free returns
on all Aerie bras. If you need to return an Aerie bra(s), simply attach
the free return label included with your order. It’s that easy. Offer
excludes other Aerie merchandise, AE and AEO Factory. Free return
promotion and associated terms & conditions subject to change at AE’s
sole discretion.
Beginning June 19, 2013 at 6:00 am EDT through June 25, 2013 in stores
and online, get 30% off Aerie swim merchandise. This 30% off discount is
automatically applied. Discount applies to Aerie swim merchandise costs
only, not tax and shipping & handling costs. This discount is not
redeemable for cash, nor applicable toward previously purchased
merchandise. Excludes Aerie Clearance, AE merchandise, AE swim and
merchandise from these brands: Adidas, Bass, BC, Bed Stu, Birkenstock,
Chronicle, Clarks, Creative Rec, DV, Eastland, GOLA, Havaianas, Keds, Me
Too, MIA, Minnetonka, New Balance, New Balance/PF Flyers, Old Soles,
Palladium, Pro Keds, Reebok, Saucony, Seychelles, Sperry, Steve Madden,
Sweet Shoes, Tailgate, Timberland, Tretorn, Volley and college and pro
merchandise. Discount promotion and associated terms and conditions
subject to change at AE’s sole discretion.
*Select Styles. Must Buy 5 For Discount.
© 2013 AEO MANAGEMENT CO. ALL RIGHTS RESERVED.
***********************************************************
Update Your Email Address:
<EMAIL_ADDRESS>Sign Up For Email:
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link17?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Privacy Policy:
http://e.ae.com/a/tBRwcfYB7u3j4B8zYi2NuZn6S4q/link15?AAP_FLAG=N&CUSTOMER_NBR=1235023277209
Add<EMAIL_ADDRESS>to your address book.
Our mailing address: 77 Hot Metal Street, Pittsburgh, PA 15203


Rooftop Run 64 km
Bogong => Hotham AUS
Website: aura.asn.au/BogongToHotham.html
Race Winners
(27 runnings, 26 runnings as an ultramarathon)
07
Jan
2007
08
Jan
2006
09
Jan
2005
04 Jan
2004
05 Jan
2003
06 Jan
2002
07 Jan
2001
09 Jan
2000
10
Jan
1999
1998
1997
07 Jan
1996
08 Jan
1995
1994
03 Jan
1993
05 Jan
1992
06 Jan
1991
07 Jan
1990
08
Jan
1989
Notes: 1984 was the inaugural year. The 1991 race was cancelled due to 12
hours of rain just before the race. The 2012 race was stopped at 35 km due
to severe weather.
11 Jan
2015
---
cancelled due to
forecast flooding
---
cancelled due to forecast flooding
12 Jan
2014
6:44:42
Stuart Gibson-2
8:09:47
Beth Cardelli-4
06 Jan 2013
---
cancelled
due to threat of bush fires
---
cancelled
due to threat of bush fires
08
Jan
2012
4:02:28
Damon Goerke-2
5:00:10
Beth Cardelli-3
09
Jan
2011
6:59:21
Stuart Gibson (AUS)
8:14:27
Beth
Cardelli-2
10 Jan
2010
7:20:32
John Winsbury (NZL)
9:00:15
Beth Cardelli (AUS)
11 Jan
2009
7:35:
Damon Goerke (AUS)
9:28:
Nadine Kahler-2
06 Jan
2008
7:39:
Tony Fattorini (AUS)
9:22:
Nadine Kahler (AUS)
---
cancelled
due to bush fires
---
cancelled
due to bush fires
7:01:
Magnus Michelsson (AUS)
11:26:
Tasmin Barnes (AUS)
7:51:
David Criniti (AUS)
9:30:
Vanessa Haverd (AUS)
---
run short
due to bush fires
---
run short due to bush fires
7:54:26
Jonathan Worswick-3
7:46:15
Peter
Mitchell-2
---
n/a
7:30:37
Nigel
Aylott-2
---
n/a
7:51:07
Jonathan Worswick-2
9:02:20
Victoria Tanner (AUS)
7:06:39
Nigel Aylott (AUS)
---
n/a
---
Andrew Kromar-2
---
n/a
8:02:26
Peter Mitchell (AUS)
---
n/a
6:41:02
Andrew Kromar (AUS)
---
n/a
8:03:00
Jonathan Worswick (AUS)
8:29:38
Dawn Tiller-2
7:22:34
James Evans (AUS)
7:44:50
Bruce Inglis (AUS)
9:35:06
Dawn Tiller (AUS)
7:16:10
Neil
Hooper-4
---
cancelled
---
cancelled
7:11:10
Neil
Hooper-3
10:20:08
Sue Dreverman (AUS)
9:10:10
Jonathan Broxap (AUS)
27
Dec
1987
7:57:
Peter LeBusque (AUS)
1986
---
n/a
28
Dec
1985
6:58:52
Neil
Hooper-2
Dec
1984
7:14:
Neil Hooper (AUS)
Most Wins
(1984/date)
Men
3
Jonathan Worswick (AUS)
1995,2000,2003
Women 4
Beth Cardelli (AUS)
2010-13
Prize Money
(ADR qualified runners)
No information on prize money has been received for this race.
Race Time Bias
(sec/km)
The race time bias is not calculated for
distances beyond the marathon.
Competitive Level
(1990-date)
Insufficient data to calculate the competitive level.
Last Updated on
21 Jan 2016
Contributors: Juraj Gasparovic (50), Klaas Loonstra (25)


1. Pick a network name, such as and access the admin interface
An easy way to display web content on remotely devices!
3. In the admin interface, set the URL the remote device should display.
X-Frame-Options
must not be set to
sameorigin
.


My favorite places
San Francisco
Here are some interesting facts about SF!
- The Chinese fortune cookie was invented by a Japanese resident of San Francisco.
- Irish coffee? It was perfected and popularized in the City by the Bay.
- San Francisco was part of Mexico until the Mexican-American War in 1848.
Phoenix
Here are some interesting facts about Phoenix!!!
- a unique bird, resembling an eagle but with rich red and gold plumage
- lived for five or six centuries in the Arabian desert
- after this time burning itself on a funeral pyre ignited by the sun and fanned by its own wings, and rising from the ashes with renewed youth to live through another cycle.
Seattle
Here are some interesting facts about Seattle !!!!!!!!
- The land that is now the city of Seattle has been inhabited for at least 4,000 years.
- George Vancouver was the first European to visit Seattle in May 1792 during his 4-year-long expedition to chart the Pacific Northwest.
- The Boeing Company, founded in the Seattle area by William Boeing, was originally a boat company. Mr. Boeing was fascinated with flying and airplanes.
If you are curious about some of my favorite things take a LOOK!


Model
└─Model
public class Model
extends Model
| Fields inherited from CrossORM\Core\Model | |
|---|---|
| _dynamic_methods, _method_hooks, _validate_on, config, db_id, dynamic_methods, fields, id_field, orm, table_name |
| Methods inherited from CrossORM\Core\Model | |
|---|---|
| __call, __construct, __get, __isset, __set, _class_name_to_table_name, _get_table_name, _validate_fields, factory, find_many, find_one, prepare_fields |
Model class, wraps around the ORM


CM Punk's brutal and honest advice to Seth Rollins on WWE Backstage
by Nishant JayaramCM Punk debuted on WWE Backstage this week and it was one hell of a show, packed with a lot of interesting tidbits and analysis by Punk and the rest of the crew.
Punk was asked by Renee Young about former Universal Champion Seth Rollins, who has tweeted on more than one occasion about Punk, challenging him to a match.
Also Read: CM Punk reveals what brought him back to professional wrestling
The new member of WWE Backstage had some important and honest advice to Rollins. He said,
"I want my journalistic integrity to be intact, so this isn't the show where you come on and shoot your little angles.
Rollins replied to Punk's comments on him, calling him a "coward".
Also Read: CM Punk reveals how he'll criticize the current wrestling landscape
Punk delivered on his first show on WWE Backstage and fans will be wanting to hear more from the former WWE Champion.
We want to know what you think of the matches that you see on TV! Go to our WWE page here and rate and comment what you thought of them!


Warehouse Keeper Holvas:
You did it! Well done!
Let me examine this. Hmmm... as I expected, I am already familiar with most of this content.
It covers your race's physical appearance and combat prowess.
Interesting, but not particularly unique...
Wait a moment...
What is it?


Welcome to get_home_ip_remotely’s documentation!¶
Introduction¶
Get the dynamic public IP from router at home remotely.
Deployment¶
Install the required lib:
$ pip3 install -r requirements.txt
At home:
Make sure your router IP is public, if not, ask for your ISP to get it.
Log in your router with browser, and research which page can get the IP, what is authorization filed in cookies, and what is regular expression of getting ip in the page source.
Example:
# Config of getting public IP from router ROUTER_IP_URL = 'http://<IP_ADDRESS>/userRpm/StatusRpm.htm' AUTHORIZATION_HEADERS = { 'Authorization': 'Basic YWRtaW46SklNNDgxNDg2MGppbQ=='} IP_REGEX = r'wanPara\s+=\s+new\s+Array\(.*?"(\d+\.\d+\.\d+\.\d+)",'
Modify file ‘config.py’ for getting the IP, email, and encryption.
Add a cron job(Linux) or Windows job for sending the IP(need modify the following path).
cron job(Linux):
0 8-20 * * * /usr/bin/python3 /the/path/to/project/get_home_ip_remotely/get_ip_then_send_via_email.py
Add Windows job:
$ schtasks /create /tn send_ip /sc HOURLY /tr "D:\Python36\python.exe D:\path_to_project\get_home_ip_remotely\get_ip_then_send_via_email.py" /ST 09:00 /ET 18:00
At remote:
Modify file ‘config.py’ for email, and decryption(may not if using the same config file).
Add domains which will be filled into hosts with the public IP in the file ‘domain.txt’, one domain per line, and can comment a domain with hash ‘#’.
Add a cron job(Linux) or Windows job for pulling and updating the IP(need modify the following path).
cron job(Linux, need root right to update /etc/hosts):
01 8-20 * * * /usr/bin/python3 /the/path/to/project/get_home_ip_remotely/pull_update_ip.py
Add Windows job:
$ schtasks /create /tn update_ip /sc HOURLY /tr "D:\Python36\python.exe D:\path_to_project\get_home_ip_remotely\pull_update_ip.py" /ST 09:01 /ET 18:01 /ru system
How to run unittest¶
First, modify the config file ‘config.py’.
Run all tests:
$ cd /project/root/dir $ python3 -m unittest discover tests -v
- Or
$ cd /project/root/dir $ python3 -m unittest -v
Run some module’s tests or some test:
$ cd /project/root/dir $ python3 -m unittest -v tests.test_get_ip_then_send_via_email $ python3 -m unittest -v tests.test_pull_update_ip $ python3 -m unittest -v tests.test_pull_update_ip.TestDecryptText $ python3 -m unittest -v tests.test_pull_update_ip.TestUpdateHosts
License¶
Apache License 2.0