Axiom ax-12 1004

Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases.

An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax-15 1399, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 1417.

Assertion

Ref	Expression
ax-12	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

Detailed syntax breakdown of Axiom ax-12

Step	Hyp	Ref	Expression
1		vz	. . . . . 6 set z
2	1	cv 991	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 991	. . . . 5 class x
5	2, 4	wceq 992	. . . 4 wff z = x
6	5, 1	wal 990	. . 3 wff ∀z z = x
7	6	wn 2	. 2 wff ¬ ∀z z = x
8		vy	. . . . . . 7 set y
9	8	cv 991	. . . . . 6 class y
10	2, 9	wceq 992	. . . . 5 wff z = y
11	10, 1	wal 990	. . . 4 wff ∀z z = y
12	11	wn 2	. . 3 wff ¬ ∀z z = y
13	4, 9	wceq 992	. . . 4 wff x = y
14	13, 1	wal 990	. . . 4 wff ∀z x = y
15	13, 14	wi 3	. . 3 wff (x = y → ∀z x = y)
16	12, 15	wi 3	. 2 wff (¬ ∀z z = y → (x = y → ∀z x = y))
17	7, 16	wi 3	1 wff (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

This axiom is referenced by:  equid 1162  equidALT 1163  hbae 1182  dvelimfALT 1190  equvini 1205  hbequid 1206  ax17eq 1248  hbsb4 1286  sbcom 1296  sbal1 1385  dvelimALT 1392  ax11eq 1402  ax11indalem 1407  a12stdy4 1414  a12lem1 1415  axrepndlem2 5099  axacndlem4 5116  axacnd 5118

Copyright terms: Public domain