Axiom ax-4 972

Description: Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for φ). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only y is free in ∀xx = y.) This is one of the 4 axioms of what we call "pure" predicate calculus. Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 962. Conditional forms of the converse are given by ax-12 967, ax-15 1359, ax-16 1209, and ax-17 970.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. That is dealt with later when substitution is introduced - see stdpc4 1184.

An alternate axiomatization could use ax467 1022 and ax-5o 974 in place of ax-4 972, ax-5o 974, ax-6o 977, and ax-7 961.

This axiom is redundant, as shown by theorem ax4 971.

Assertion

Ref	Expression
ax-4	⊢ (∀xφ → φ)

Detailed syntax breakdown of Axiom ax-4

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3	1, 2	wal 953	. 2 wff ∀xφ
4	3, 1	wi 3	1 wff (∀xφ → φ)

This axiom is referenced by:  ax5o 973  ax5 975  ax6o 976  ax6 978  a4i 981  a4s 983  a4sd 984  ax46 1016  ax67to6 1020  ax467 1022  19.8a 1028  19.3 1030  19.12 1046  19.21 1055  19.21bi 1059  19.38 1080  19.21t 1114  19.23t 1115  hbae 1144  equs4 1149  sb2 1176  sbied 1194  ax11 1218  ax11b 1219  dfsb2 1224  hbsb4 1247  hbsb4t 1248  sb56 1265  sb6 1266  a16gb 1276  sbal1 1345  ax11indalem 1367  ax11inda2ALT 1368  mopick 1432  2eu1 1448  ra4 1692  ralcom2 1774  ceqex 1883  abidhb 1909  hbsbc1gd 1980  hbsbcgd 1981  disjssun 2323  intab 2556  axrep1 2690  axrep2 2691  axnul2 2704  dtruALT 2744  ssopab2 2818  alxfr 2892  fununi 3559  hbfvd2 3726  fiint 4543  nd3 4923  axrepndlem2 4928  axrepnd 4929  axpowndlem2 4933  axpowndlem4 4935  axinfndlem1 4940  axacndlem4 4945  axacndlem5 4946  suppsrlem 5204  cncnplem2 7735  imonclem 10655

Copyright terms: Public domain