Axiom ax-4 973

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 ph). (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 A.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 963. Conditional forms of the converse are given by ax-12 968, ax-15 1360, ax-16 1210, and ax-17 971.

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

An alternate axiomatization could use ax467 1023 and ax-5o 975 in place of ax-4 973, ax-5o 975, ax-6o 978, and ax-7 962.

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

Assertion

Ref	Expression
ax-4	|- (A.xph -> ph)

Detailed syntax breakdown of Axiom ax-4

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	wal 954	. 2 wff A.xph
4	3, 1	wi 3	1 wff (A.xph -> ph)

This axiom is referenced by:  ax5o 974  ax5 976  ax6o 977  ax6 979  a4i 982  a4s 984  a4sd 985  ax46 1017  ax67to6 1021  ax467 1023  19.8a 1029  19.3 1031  19.12 1047  19.21 1056  19.21bi 1060  19.38 1081  19.21t 1115  19.23t 1116  hbae 1145  equs4 1150  sb2 1177  sbied 1195  ax11 1219  ax11b 1220  dfsb2 1225  hbsb4 1248  hbsb4t 1249  sb56 1266  sb6 1267  a16gb 1277  sbal1 1346  ax11indalem 1368  ax11inda2ALT 1369  mopick 1433  2eu1 1449  ra4 1694  ralcom2 1776  ceqex 1886  abidhb 1912  hbsbc1gd 1983  hbsbcgd 1984  disjssun 2326  intab 2560  axrep1 2694  axrep2 2695  axnul2 2708  dtruALT 2748  ssopab2 2822  alxfr 2896  fununi 3563  hbfvd2 3731  fiint 4559  fiintOLD 4560  nd3 4940  axrepndlem2 4945  axrepnd 4946  axpowndlem2 4950  axpowndlem4 4952  axinfndlem1 4957  axacndlem4 4962  axacndlem5 4963  suppsrlem 5221  cncnplem2 7775  imonclem 10741

Copyright terms: Public domain