**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 1288
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 *x* and *y* 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 1410 and ax9 1412. Another name for this theorem is a9e 1409,
which has
additional remarks. (Contributed by Mario Carneiro,
31-Jan-2015.) |