Axiom ax-12 965

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 1353, 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 1371.

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 952	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 952	. . . . 5 class x
5	2, 4	wceq 953	. . . 4 wff z = x
6	5, 1	wal 951	. . 3 wff ∀z z = x
7	6	wn 2	. 2 wff ¬ ∀z z = x
8		vy	. . . . . . 7 set y
9	8	cv 952	. . . . . 6 class y
10	2, 9	wceq 953	. . . . 5 wff z = y
11	10, 1	wal 951	. . . 4 wff ∀z z = y
12	11	wn 2	. . 3 wff ¬ ∀z z = y
13	4, 9	wceq 953	. . . 4 wff x = y
14	13, 1	wal 951	. . . 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 1122  hbae 1141  dvelimfALT 1149  equvini 1164  hbequid 1165  ax17eq 1207  hbsb4 1243  sbcom 1253  sbal1 1341  ax11eq 1356  ax11indalem 1361  a12stdy4 1368  a12lem1 1369  axrepndlem2 4917  axacndlem4 4934  axacnd 4936

Copyright terms: Public domain