**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 1692
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 1814 and ax9from9o 1816. A more convenient form of this axiom is a9e 1817,
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 1684 can be proved from a weaker version requiring
that the variables be
distinct; see theorem ax9 1683.
ax-9 1684 can also be proved from the Axiom of
Separation (in the form that
we use that axiom, where free variables are not universally quantified).
See theorem ax9vsep 4105. (Contributed by NM,
5-Aug-1993.) |