Axiom ax-12 966

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 1358, 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 1376.

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 953	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 953	. . . . 5 class x
5	2, 4	wceq 954	. . . 4 wff z = x
6	5, 1	wal 952	. . 3 wff ∀z z = x
7	6	wn 2	. 2 wff ¬ ∀z z = x
8		vy	. . . . . . 7 set y
9	8	cv 953	. . . . . 6 class y
10	2, 9	wceq 954	. . . . 5 wff z = y
11	10, 1	wal 952	. . . 4 wff ∀z z = y
12	11	wn 2	. . 3 wff ¬ ∀z z = y
13	4, 9	wceq 954	. . . 4 wff x = y
14	13, 1	wal 952	. . . 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 1124  hbae 1143  dvelimfALT 1151  equvini 1166  hbequid 1167  ax17eq 1209  hbsb4 1246  sbcom 1256  sbal1 1344  dvelimALT 1351  ax11eq 1361  ax11indalem 1366  a12stdy4 1373  a12lem1 1374  axrepndlem2 4925  axacndlem4 4942  axacnd 4944

Copyright terms: Public domain