Axiom ax-4 970

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 960. Conditional forms of the converse are given by ax-12 965, ax-15 1353, ax-16 1206, and ax-17 968.

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 1181.

An alternate axiomatization could use ax467 1019 and ax-5o 972 in place of ax-4 970, ax-5o 972, ax-6o 975, and ax-7 959.

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

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 951	. 2 wff ∀xφ
4	3, 1	wi 3	1 wff (∀xφ → φ)

This axiom is referenced by:  ax5o 971  ax5 973  ax6o 974  ax6 976  a4i 979  a4s 981  a4sd 982  ax46 1013  ax67to6 1017  ax467 1019  19.8a 1025  19.3 1027  19.12 1043  19.21 1052  19.21bi 1056  19.38 1077  19.21t 1111  19.23t 1112  hbae 1141  equs4 1146  sb2 1173  sbied 1191  ax11 1214  ax11b 1215  dfsb2 1220  hbsb4 1243  hbsb4t 1244  sb56 1261  sb6 1262  a16gb 1272  sbal1 1341  ax11indalem 1361  ax11inda2ALT 1362  mopick 1426  2eu1 1442  ra4 1686  ralcom2 1768  ceqex 1877  abidhb 1903  hbsbc1gd 1973  hbsbcgd 1974  disjssun 2316  intab 2550  axrep1 2684  axrep2 2685  axnul2 2698  dtruALT 2738  ssopab2 2811  alxfr 2886  fununi 3549  hbfvd2 3716  fiint 4534  nd3 4912  axrepndlem2 4917  axrepnd 4918  axpowndlem2 4922  axpowndlem4 4924  axinfndlem1 4929  axacndlem4 4934  axacndlem5 4935  suppsrlem 5193  cncnplem2 7714  imonclem 10583

Copyright terms: Public domain