Axiom ax-4 1157

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 x is free in A.yx = y.) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1157 through ax-7 1142 plus rule ax-gen 1143). 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 1143. Conditional forms of the converse are given by ax-12 1148, ax-15 1589, ax-16 1418, and ax-17 1155.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1388.

An nice alternate axiomatization uses ax467 1208 and ax-5o 1159 in place of ax-4 1157, ax-5 1140, ax-6 1141, and ax-7 1142.

This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1156. (We replaced the older ax-5o 1159 and ax-6o 1162 with newer versions ax-5 1140 and ax-6 1141 in order to prove this redundancy.)

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 1134	. 2 wff A.xph
4	3, 1	wi 3	1 wff (A.xph -> ph)

This axiom is referenced by:  ax5o 1158  ax5 1160  ax6o 1161  ax6 1163  a4i 1166  a4s 1168  a4sd 1169  ax46 1202  ax67to6 1206  ax467 1208  19.8a 1214  19.3 1216  19.12 1232  19.21 1241  19.21bi 1246  19.38 1270  19.21t 1311  19.23t 1312  hbae 1343  equs4 1348  sb2 1379  sbiedOLD 1402  ax11 1427  ax11b 1428  dfsb2 1433  sbf3t 1457  hbsb4 1458  hbsb4t 1459  hbsb4tOLD 1460  sb56 1481  sb6 1482  a16gb 1493  sbal1 1575  ax11indalem 1597  ax11inda2ALT 1598  mopick 1670  2eu1 1690  ra4 1989  ralcom2 2078  ralcom2OLD 2079  ceqex 2224  hbsbc1gdOLD 2349  hbsbcgd 2350  hbsbcgdOLD 2351  disjssunOLD 2757  intab 3069  axrep1 3244  axrep2 3245  axnulALT 3258  dtru 3313  ssopab2 3388  eualeq 3634  euexeqOLD 3637  euexaleq 3638  alxfr 3647  fununi 4292  hbfvd2 4499  dffv2 4545  fiint 5460  nd3 5888  axrepndlem2 5893  axrepnd 5894  axpowndlem2 5898  axpowndlem4 5900  axinfndlem1 5905  axacndlem4 5910  axacndlem5 5911  suppsrlem 6169  cncnplem2 8847  bnj32 12190  bnj111OLD 12248  bnj228OLD 12310  bnj954 12642  bnj569 13079  bnj1073 13195  tz6.26 13705  frmin 13730  wfrlem5 13753  imonclem 14844  inficlALT 15054  prtlem14 15959  pm11.57 16028  pm11.59 16030  ax4567to6 16044  ax4567to7 16045  ax10ext 16046  ax10-16 16047  pm14.123b 16072  eubi 16084  compne 16099

Copyright terms: Public domain