Axiom ax-12 972

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 1364, 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 1382.

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 959	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 959	. . . . 5 class x
5	2, 4	wceq 960	. . . 4 wff z = x
6	5, 1	wal 958	. . 3 wff ∀z z = x
7	6	wn 2	. 2 wff ¬ ∀z z = x
8		vy	. . . . . . 7 set y
9	8	cv 959	. . . . . 6 class y
10	2, 9	wceq 960	. . . . 5 wff z = y
11	10, 1	wal 958	. . . 4 wff ∀z z = y
12	11	wn 2	. . 3 wff ¬ ∀z z = y
13	4, 9	wceq 960	. . . 4 wff x = y
14	13, 1	wal 958	. . . 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 1130  hbae 1149  dvelimfALT 1157  equvini 1172  hbequid 1173  ax17eq 1215  hbsb4 1252  sbcom 1262  sbal1 1350  dvelimALT 1357  ax11eq 1367  ax11indalem 1372  a12stdy4 1379  a12lem1 1380  axrepndlem2 4965  axacndlem4 4982  axacnd 4984

Copyright terms: Public domain