Axiom ax-16 1208

Description: Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 969 to be a metatheorem and not an axiom). Axiom scheme C16' 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. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 2768), but nonetheless it is technically necessary as you can see from its uses.

This axiom is redundant if we include ax-17 969; see theorem ax16 1207. Alternately, ax-17 969 becomes logically redundant in the presence of this axiom, but without ax-17 969 we lose the more powerful metalogic that results from being able to express the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). We retain ax-16 1208 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-17 969, which might be easier to study for some theoretical purposes.

Assertion

Ref	Expression
ax-16	⊢ (∀x x = y → (φ → ∀xφ))

Distinct variable group:   x,y

Detailed syntax breakdown of Axiom ax-16

Step	Hyp	Ref	Expression
1		vx	. . . . 5 set x
2	1	cv 953	. . . 4 class x
3		vy	. . . . 5 set y
4	3	cv 953	. . . 4 class y
5	2, 4	wceq 954	. . 3 wff x = y
6	5, 1	wal 952	. 2 wff ∀x x = y
7		wph	. . 3 wff φ
8	7, 1	wal 952	. . 3 wff ∀xφ
9	7, 8	wi 3	. 2 wff (φ → ∀xφ)
10	6, 9	wi 3	1 wff (∀x x = y → (φ → ∀xφ))

This axiom is referenced by:  ax17eq 1209  ax11v 1263  a16g 1274  hbs1 1330  hbsb 1331  sbal1 1344  ax17el 1359  exists2 1456  hbab 1465  hbabd 1466

Copyright terms: Public domain