Axiom ax-9 962

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 970 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 1118 and ax9 1120. A more convenient form of this axiom is a9e 1121, 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.

Assertion

Ref	Expression
ax-9	⊢ ¬ ∀x ¬ x = y

Detailed syntax breakdown of Axiom ax-9

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 952	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 952	. . . . 5 class y
5	2, 4	wceq 953	. . . 4 wff x = y
6	5	wn 2	. . 3 wff ¬ x = y
7	6, 1	wal 951	. 2 wff ∀x ¬ x = y
8	7	wn 2	1 wff ¬ ∀x ¬ x = y

This axiom is referenced by:  ax4 969  ax9o 1118  a9e 1121  a16g 1271

Copyright terms: Public domain