HomeHome Intuitionistic Logic Explorer
Theorem List (p. 20 of 20)
< Previous  Wrap >
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 - 1901-1914   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem2exeu 1901 Double existential uniqueness implies double uniqueness quantification.
 
Theorem2mo 1902* Two equivalent expressions for double "at most one."
 
Theorem2mos 1903* Double "exists at most one", using implicit substitition.
   =>   
 
Theorem2eu1 1904 Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one.
 
Theorem2eu2 1905 Double existential uniqueness.
 
Theorem2eu3 1906 Double existential uniqueness.
 
Theorem2eu4 1907* This theorem provides us with a definition of double existential uniqueness ("exactly one and exactly one "). Naively one might think (incorrectly) that it could be defined by . See 2eu1 1904 for a condition under which the naive definition holds and 2exeu 1901 for a one-way implication. See 2eu5 1908 and 2eu8 1911 for alternate definitions.
 
Theorem2eu5 1908* An alternate definition of double existential uniqueness (see 2eu4 1907). A mistake sometimes made in the literature is to use to mean "exactly one and exactly one ." (For example, see Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining as an additional condition. The correct definition apparently has never been published. ( means "exists at most one.")
 
Theorem2eu6 1909* Two equivalent expressions for double existential uniqueness.
 
Theorem2eu7 1910 Two equivalent expressions for double existential uniqueness.
 
Theorem2eu8 1911 Two equivalent expressions for double existential uniqueness. Curiously, we can put on either of the internal conjuncts but not both. We can also commute using 2eu7 1910.
 
Theoremeuequ1 1912* Equality has existential uniqueness. (Contributed by Stefan Allan, 4-Dec-2008.)
 
Theoremexists1 1913* Two ways to express "only one thing exists." The left-hand side requires only one variable to express this. Both sides are false in set theory.
 
Theoremexists2 1914 A condition implying that at least two things exist. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
    < Previous  Wrap >

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  Wrap >