Home | Intuitionistic Logic ExplorerTheorem List (p. 19 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | dveeq1 1801* | Quantifier introduction when one pair of variables is distinct. |

Theorem | dveeq1ALT 1802* | Version of dveeq1 1801 using ax-16 1644 instead of ax-17 1402. |

Theorem | dveel1 1803* | Quantifier introduction when one pair of variables is distinct. |

Theorem | dveel2 1804* | Quantifier introduction when one pair of variables is distinct. |

Theorem | sbal2 1805* | Move quantifier in and out of substitution. |

Theorem | ax15 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. |

Axiom | ax-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. |

Theorem | ax17el 1808* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-17 1402 considered as a metatheorem.) |

Theorem | dveel2ALT 1809* | Version of dveel2 1804 using ax-16 1644 instead of ax-17 1402. |

Theorem | ax11eq 1810 | Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Atomic formula for equality predicate. |

Theorem | ax11el 1811 | Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Atomic formula for membership predicate. |

Theorem | ax11f 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. |

Theorem | ax11indn 1813 | Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Negation case. |

Theorem | ax11indi 1814 | Induction step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Implication case. |

Theorem | ax11indalem 1815 | Lemma for ax11inda2 1817 and ax11inda 1818. |

Theorem | ax11inda2ALT 1816* | A proof of ax11inda2 1817 that is slightly more direct. |

Theorem | ax11inda2 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. |

Theorem | ax11inda 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.) |

Theorem | a12stdy1 1819 | Part of a study related to ax-12 1393. The consequent introduces a new variable . There are no distinct variable restrictions. |

Theorem | a12stdy2 1820 | Part of a study related to ax-12 1393. The consequent is quantified with a different variable. There are no distinct variable restrictions. |

Theorem | a12stdy3 1821 | Part of a study related to ax-12 1393. The consequent introduces two new variables. There are no distinct variable restrictions. |

Theorem | a12stdy4 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. |

Theorem | a12lem1 1823 | Proof of first hypothesis of a12study 1825. |

Theorem | a12lem2 1824 | Proof of second hypothesis of a12study 1825. |

Theorem | a12study 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. |

Theorem | a12studyALT 1826 | Alternate proof of a12study 1825, also without using ax-12 1393. |

Theorem | a12study2 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.) |

Theorem | a12study3 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 | ||

Syntax | weu 1829 | Extend wff definition to include existential uniqueness ("there exists a unique such that "). |

Syntax | wmo 1830 | Extend wff definition to include uniqueness ("there exists at most one such that "). |

Theorem | eujust 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.) |

Theorem | eujustALT 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. |

Definition | df-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). |

Definition | df-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. |

Theorem | euf 1835* | A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. |

Theorem | eubid 1836 | Formula-building rule for uniqueness quantifier (deduction rule). |

Theorem | eubidv 1837* | Formula-building rule for uniqueness quantifier (deduction rule). |

Theorem | eubii 1838 | Introduce uniqueness quantifier to both sides of an equivalence. |

Theorem | hbeu1 1839 | Bound-variable hypothesis builder for uniqueness. |

Theorem | hbeu 1840 | Bound-variable hypothesis builder for "at most one." Note that and needn't be distinct (this makes the proof more difficult). |

Theorem | hbeud 1841 | Deduction version of hbeu 1840. |

Theorem | sb8eu 1842 | Variable substitution in uniqueness quantifier. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.) |

Theorem | cbveu 1843 | Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.) |

Theorem | eu1 1844* | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. |

Theorem | mo 1845* | Equivalent definitions of "there exists at most one." |

Theorem | euex 1846 | Existential uniqueness implies existence. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | eumo0 1847* | Existential uniqueness implies "at most one." |

Theorem | eu2 1848* | An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. |

Theorem | eu3 1849* | An alternate way to express existential uniqueness. |

Theorem | euor 1850 | Introduce a disjunct into a uniqueness quantifier. |

Theorem | euorv 1851* | Introduce a disjunct into a uniqueness quantifier. |

Theorem | mo2 1852* | Alternate definition of "at most one." |

Theorem | sbmo 1853* | Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | mo3 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. |

Theorem | mo4f 1855* | "At most one" expressed using implicit substitution. |

Theorem | mo4 1856* | "At most one" expressed using implicit substitution. |

Theorem | mobid 1857 | Formula-building rule for "at most one" quantifier (deduction rule). |

Theorem | mobii 1858 | Formula-building rule for "at most one" quantifier (inference rule). |

Theorem | hbmo1 1859 | Bound-variable hypothesis builder for "at most one." |

Theorem | hbmo 1860 | Bound-variable hypothesis builder for "at most one." |

Theorem | cbvmo 1861 | Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.) |

Theorem | eu5 1862 | Uniqueness in terms of "at most one." |

Theorem | eu4 1863* | Uniqueness using implicit substitution. |

Theorem | eumo 1864 | Existential uniqueness implies "at most one." |

Theorem | eumoi 1865 | "At most one" inferred from existential uniqueness. |

Theorem | exmoeu 1866 | Existence in terms of "at most one" and uniqueness. |

Theorem | exmoeu2 1867 | Existence implies "at most one" is equivalent to uniqueness. |

Theorem | moabs 1868 | Absorption of existence condition by "at most one." |

Theorem | exmo 1869 | Something exists or at most one exists. |

Theorem | immo 1870 | "At most one" is preserved through implication (notice wff reversal). |

Theorem | immoi 1871 | "At most one" is preserved through implication (notice wff reversal). |

Theorem | moimv 1872* | Move antecedent outside of "at most one." |

Theorem | euimmo 1873 | Uniqueness implies "at most one" through implication. |

Theorem | euim 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.) |

Theorem | moan 1875 | "At most one" is still the case when a conjunct is added. |

Theorem | moani 1876 | "At most one" is still true when a conjunct is added. |

Theorem | moor 1877 | "At most one" is still the case when a disjunct is removed. |

Theorem | mooran1 1878 | "At most one" imports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | mooran2 1879 | "At most one" exports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | moanim 1880 | Introduction of a conjunct into "at most one" quantifier. |

Theorem | euan 1881 | Introduction of a conjunct into uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | moanimv 1882* | Introduction of a conjunct into "at most one" quantifier. |

Theorem | moaneu 1883 | Nested "at most one" and uniqueness quantifiers. |

Theorem | moanmo 1884 | Nested "at most one" quantifiers. |

Theorem | euanv 1885* | Introduction of a conjunct into uniqueness quantifier. |

Theorem | mopick 1886 | "At most one" picks a variable value, eliminating an existential quantifier. |

Theorem | eupick 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. |

Theorem | eupicka 1888 | Version of eupick 1887 with closed formulas. |

Theorem | eupickb 1889 | Existential uniqueness "pick" showing wff equivalence. |

Theorem | eupickbi 1890 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |

Theorem | mopick2 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.) |

Theorem | euor2 1892 | Introduce or eliminate a disjunct in a uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | moexex 1893 | "At most one" double quantification. |

Theorem | moexexv 1894* | "At most one" double quantification. |

Theorem | 2moex 1895 | Double quantification with "at most one." |

Theorem | 2euex 1896 | Double quantification with existential uniqueness. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | 2eumo 1897 | Double quantification with existential uniqueness and "at most one." |

Theorem | 2eu2ex 1898 | Double existential uniqueness. |

Theorem | 2moswap 1899 | A condition allowing swap of "at most one" and existential quantifiers. |

Theorem | 2euswap 1900 | A condition allowing swap of uniqueness and existential quantifiers. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |