**Description: **Axiom of Existence. One
of the equality and substitution axioms of
predicate calculus with equality. One thing this axiom tells us is that
at least one thing exists (although ax-4 1392
and possibly others also tell
us that, i.e. they are not valid in the empty domain of a "free
logic").
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
ax9o 1557 and ax9 1559. A more convenient form of this
axiom is a9e 1556, which
has additional remarks.
Raph Levien proved the independence of this axiom from the other logical
axioms on 12-Apr-2005. See item 16 at
http://us.metamath.org/award2003.html.
ax-9 1418 can be proved from a weaker version requiring
that the variables be
distinct; see theorem a9wa9 1415. |