HomeHome Intuitionistic Logic Explorer
Theorem List (p. 19 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1801-1900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdveeq1 1801* Quantifier introduction when one pair of variables is distinct.
 
Theoremdveeq1ALT 1802* Version of dveeq1 1801 using ax-16 1644 instead of ax-17 1402.
 
Theoremdveel1 1803* Quantifier introduction when one pair of variables is distinct.
 
Theoremdveel2 1804* Quantifier introduction when one pair of variables is distinct.
 
Theoremsbal2 1805* Move quantifier in and out of substitution.
 
Theoremax15 1806 Axiom ax-15 1807 is redundant if we assume ax-17 1402. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.

Note that is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 1804 and ax-17 1402. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements.

This theorem should not be referenced in any proof. Instead, use ax-15 1807 below so that theorems needing ax-15 1807 can be more easily identified.

 
Axiomax-15 1807 Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1402; see theorem ax15 1806. Alternately, ax-17 1402 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1402. We retain ax-15 1807 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1402, which might be easier to study for some theoretical purposes.
 
Theoremax17el 1808* Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-17 1402 considered as a metatheorem.)
 
Theoremdveel2ALT 1809* Version of dveel2 1804 using ax-16 1644 instead of ax-17 1402.
 
Theoremax11eq 1810 Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Atomic formula for equality predicate.
 
Theoremax11el 1811 Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Atomic formula for membership predicate.
 
Theoremax11f 1812 Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. We can start with any formula in which is not free.
   =>   
 
Theoremax11indn 1813 Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Negation case.
   =>   
 
Theoremax11indi 1814 Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Implication case.
   &       =>   
 
Theoremax11indalem 1815 Lemma for ax11inda2 1817 and ax11inda 1818.
   =>   
 
Theoremax11inda2ALT 1816* A proof of ax11inda2 1817 that is slightly more direct.
   =>   
 
Theoremax11inda2 1817* Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Quantification case. When and are distinct, this theorem avoids the dummy variables needed by the more general ax11inda 1818.
   =>   
 
Theoremax11inda 1818* Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Quantification case. (When and are distinct, ax11inda2 1817 may be used instead to avoid the dummy variable in the proof.)
   =>   
 
Theorema12stdy1 1819 Part of a study related to ax-12 1393. The consequent introduces a new variable . There are no distinct variable restrictions.
 
Theorema12stdy2 1820 Part of a study related to ax-12 1393. The consequent is quantified with a different variable. There are no distinct variable restrictions.
 
Theorema12stdy3 1821 Part of a study related to ax-12 1393. The consequent introduces two new variables. There are no distinct variable restrictions.
 
Theorema12stdy4 1822 Part of a study related to ax-12 1393. The second antecedent of ax-12 1393 is replaced. There are no distinct variable restrictions.
 
Theorema12lem1 1823 Proof of first hypothesis of a12study 1825.
 
Theorema12lem2 1824 Proof of second hypothesis of a12study 1825.
 
Theorema12study 1825 Rederivation of axiom ax-12 1393 from two shorter formulas, without using ax-12 1393. See a12lem1 1823 and a12lem2 1824 for the proofs of the hypotheses (using ax-12 1393). This is the only known breakdown of ax-12 1393 into shorter formulas. See a12studyALT 1826 for an alternate proof. Note that the proof depends on ax-11o 1654, whose proof ax11o 1653 depends on ax-12 1393, meaning that we would have to replace ax-11 1389 with ax-11o 1654 in an axiomatization that uses the hypotheses in place of ax-12 1393. Whether this can be avoided is an open problem.
   &       =>   
 
Theorema12studyALT 1826 Alternate proof of a12study 1825, also without using ax-12 1393.
   &       =>   
 
Theorema12study2 1827* Reprove ax-12 1393 using dvelimfALT2 1648, showing that ax-12 1393 can be replaced by dveeq2 1646 (whose needed instances are the hypotheses here) if we allow distinct variables in axioms other than ax-17 1402. (Contributed by Andrew Salmon, 21-Jul-2011.)
   &       =>   
 
Theorema12study3 1828 Rederivation of axiom ax-12 1393 from two other formulas, without using ax-12 1393. See equvini 1602 and equveli 1603 for the proofs of the hypotheses (using ax-12 1393). Although the second hypothesis (when expanded to primitives) is longer than ax-12 1393, an open problem is whether it can be derived without ax-12 1393 or from a simpler axiom.

Note also that the proof depends on ax-11o 1654, whose proof ax11o 1653 depends on ax-12 1393, meaning that we would have to replace ax-11 1389 with ax-11o 1654 in an axiomatization that uses the hypotheses in place of ax-12 1393. Whether this can be avoided is an open problem.

   &       =>   
 
1.5.6  Existential uniqueness
 
Syntaxweu 1829 Extend wff definition to include existential uniqueness ("there exists a unique such that ").
 
Syntaxwmo 1830 Extend wff definition to include uniqueness ("there exists at most one such that ").
 
Theoremeujust 1831* A soundness justification theorem for df-eu 1833, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. See eujustALT 1832 for a proof that provides an example of how it can be achieved through the use of dvelim 1799. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
TheoremeujustALT 1832* A soundness justification theorem for df-eu 1833, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 1799.
 
Definitiondf-eu 1833* Define existential uniqueness, i.e. "there exists exactly one such that ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1844, eu2 1848, eu3 1849, and eu5 1862 (which in some cases we show with a hypothesis in place of a distinct variable condition on and ). Double uniqueness is tricky: does not mean "exactly one and one " (see 2eu4 1907).
 
Definitiondf-mo 1834 Define "there exists at most one such that ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 1854. For other possible definitions see mo2 1852 and mo4 1856.
 
Theoremeuf 1835* A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition.
   =>   
 
Theoremeubid 1836 Formula-building rule for uniqueness quantifier (deduction rule).
   &       =>   
 
Theoremeubidv 1837* Formula-building rule for uniqueness quantifier (deduction rule).
   =>   
 
Theoremeubii 1838 Introduce uniqueness quantifier to both sides of an equivalence.
   =>   
 
Theoremhbeu1 1839 Bound-variable hypothesis builder for uniqueness.
 
Theoremhbeu 1840 Bound-variable hypothesis builder for "at most one." Note that and needn't be distinct (this makes the proof more difficult).
   =>   
 
Theoremhbeud 1841 Deduction version of hbeu 1840.
   &       &       =>   
 
Theoremsb8eu 1842 Variable substitution in uniqueness quantifier. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.)
   =>   
 
Theoremcbveu 1843 Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.)
   &       &       =>   
 
Theoremeu1 1844* An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110.
   =>   
 
Theoremmo 1845* Equivalent definitions of "there exists at most one."
   =>   
 
Theoremeuex 1846 Existential uniqueness implies existence. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theoremeumo0 1847* Existential uniqueness implies "at most one."
   =>   
 
Theoremeu2 1848* An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26.
   =>   
 
Theoremeu3 1849* An alternate way to express existential uniqueness.
   =>   
 
Theoremeuor 1850 Introduce a disjunct into a uniqueness quantifier.
   =>   
 
Theoremeuorv 1851* Introduce a disjunct into a uniqueness quantifier.
 
Theoremmo2 1852* Alternate definition of "at most one."
   =>   
 
Theoremsbmo 1853* Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
 
Theoremmo3 1854* Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that not occur in in place of our hypothesis.
   =>   
 
Theoremmo4f 1855* "At most one" expressed using implicit substitution.
   &       =>   
 
Theoremmo4 1856* "At most one" expressed using implicit substitution.
   =>   
 
Theoremmobid 1857 Formula-building rule for "at most one" quantifier (deduction rule).
   &       =>   
 
Theoremmobii 1858 Formula-building rule for "at most one" quantifier (inference rule).
   =>   
 
Theoremhbmo1 1859 Bound-variable hypothesis builder for "at most one."
 
Theoremhbmo 1860 Bound-variable hypothesis builder for "at most one."
   =>   
 
Theoremcbvmo 1861 Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.)
   &       &       =>   
 
Theoremeu5 1862 Uniqueness in terms of "at most one."
 
Theoremeu4 1863* Uniqueness using implicit substitution.
   =>   
 
Theoremeumo 1864 Existential uniqueness implies "at most one."
 
Theoremeumoi 1865 "At most one" inferred from existential uniqueness.
   =>   
 
Theoremexmoeu 1866 Existence in terms of "at most one" and uniqueness.
 
Theoremexmoeu2 1867 Existence implies "at most one" is equivalent to uniqueness.
 
Theoremmoabs 1868 Absorption of existence condition by "at most one."
 
Theoremexmo 1869 Something exists or at most one exists.
 
Theoremimmo 1870 "At most one" is preserved through implication (notice wff reversal).
 
Theoremimmoi 1871 "At most one" is preserved through implication (notice wff reversal).
   =>   
 
Theoremmoimv 1872* Move antecedent outside of "at most one."
 
Theoremeuimmo 1873 Uniqueness implies "at most one" through implication.
 
Theoremeuim 1874 Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (The proof was shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremmoan 1875 "At most one" is still the case when a conjunct is added.
 
Theoremmoani 1876 "At most one" is still true when a conjunct is added.
   =>   
 
Theoremmoor 1877 "At most one" is still the case when a disjunct is removed.
 
Theoremmooran1 1878 "At most one" imports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theoremmooran2 1879 "At most one" exports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theoremmoanim 1880 Introduction of a conjunct into "at most one" quantifier.
   =>   
 
Theoremeuan 1881 Introduction of a conjunct into uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
   =>   
 
Theoremmoanimv 1882* Introduction of a conjunct into "at most one" quantifier.
 
Theoremmoaneu 1883 Nested "at most one" and uniqueness quantifiers.
 
Theoremmoanmo 1884 Nested "at most one" quantifiers.
 
Theoremeuanv 1885* Introduction of a conjunct into uniqueness quantifier.
 
Theoremmopick 1886 "At most one" picks a variable value, eliminating an existential quantifier.
 
Theoremeupick 1887 Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192.
 
Theoremeupicka 1888 Version of eupick 1887 with closed formulas.
 
Theoremeupickb 1889 Existential uniqueness "pick" showing wff equivalence.
 
Theoremeupickbi 1890 Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
 
Theoremmopick2 1891 "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 1522. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theoremeuor2 1892 Introduce or eliminate a disjunct in a uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theoremmoexex 1893 "At most one" double quantification.
   =>   
 
Theoremmoexexv 1894* "At most one" double quantification.
 
Theorem2moex 1895 Double quantification with "at most one."
 
Theorem2euex 1896 Double quantification with existential uniqueness. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
 
Theorem2eumo 1897 Double quantification with existential uniqueness and "at most one."
 
Theorem2eu2ex 1898 Double existential uniqueness.
 
Theorem2moswap 1899 A condition allowing swap of "at most one" and existential quantifiers.
 
Theorem2euswap 1900 A condition allowing swap of uniqueness and existential quantifiers.
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-1914
  Copyright terms: Public domain < Previous  Next >