Axiom ax-4 971

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 961. Conditional forms of the converse are given by ax-12 966, ax-15 1358, ax-16 1208, and ax-17 969.

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

An alternate axiomatization could use ax467 1021 and ax-5o 973 in place of ax-4 971, ax-5o 973, ax-6o 976, and ax-7 960.

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

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

This axiom is referenced by:  ax5o 972  ax5 974  ax6o 975  ax6 977  a4i 980  a4s 982  a4sd 983  ax46 1015  ax67to6 1019  ax467 1021  19.8a 1027  19.3 1029  19.12 1045  19.21 1054  19.21bi 1058  19.38 1079  19.21t 1113  19.23t 1114  hbae 1143  equs4 1148  sb2 1175  sbied 1193  ax11 1217  ax11b 1218  dfsb2 1223  hbsb4 1246  hbsb4t 1247  sb56 1264  sb6 1265  a16gb 1275  sbal1 1344  ax11indalem 1366  ax11inda2ALT 1367  mopick 1431  2eu1 1447  ra4 1691  ralcom2 1773  ceqex 1882  abidhb 1908  hbsbc1gd 1979  hbsbcgd 1980  disjssun 2322  intab 2555  axrep1 2689  axrep2 2690  axnul2 2703  dtruALT 2743  ssopab2 2817  alxfr 2891  fununi 3555  hbfvd2 3722  fiint 4540  nd3 4920  axrepndlem2 4925  axrepnd 4926  axpowndlem2 4930  axpowndlem4 4932  axinfndlem1 4937  axacndlem4 4942  axacndlem5 4943  suppsrlem 5201  cncnplem2 7725  imonclem 10619

Copyright terms: Public domain