Description: Axiom of Existence. One
of the equality and substitution axioms of
predicate calculus with equality. This axiom in effect tells us that at
least one thing exists. In this form (not requiring that and
be distinct) it was used in an axiom system of Tarski (see Axiom B7' in
footnote 1 of [KalishMontague] p.
81.) It is equivalent to axiom scheme
C10' in [Megill] p. 448 (p. 16 of the
preprint); the equivalence is
established by ax9 1110 and ax9a 1111. A more convenient form of this
axiom
is a9e 1112, which has additional remarks.
Raph Levien proved the independence of this axiom from the others on
12-Apr-2005. See item 16 at
http://us.metamath.org/award2003.html. |