Axiom ax-4 1608

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 1608 through ax-7 1592 plus rule ax-gen 1593). 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 1593. Conditional forms of the converse are given by ax-12 1598, ax-15 2015, ax-16 1854, and ax-17 1605.

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

An nice alternate axiomatization uses ax467 1659 and ax-5o 1610 in place of ax-4 1608, ax-5 1590, ax-6 1591, and ax-7 1592.

This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1607. (We replaced the older ax-5o 1610 and ax-6o 1613 with newer versions ax-5 1590 and ax-6 1591 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 1584	. 2 wff A.xph
4	3, 1	wi 3	1 wff (A.xph -> ph)

This axiom is referenced by:  ax5o 1609  ax5 1611  ax6o 1612  ax6 1614  a4i 1617  a4s 1619  a4sd 1620  ax46 1653  ax67to6 1657  ax467 1659  19.8a 1665  19.3 1667  19.12 1683  19.21 1692  19.21bi 1696  19.38 1718  19.21t 1755  19.23t 1756  hbae 1786  equs4 1791  equveli 1812  sb2 1821  ax11 1865  ax11b 1866  dfsb2 1871  sbf3t 1894  hbsb4 1895  hbsb4t 1896  sb56 1913  sb6 1914  a16gb 1924  sbal1 2001  ax11indalem 2023  ax11inda2ALT 2024  mopick 2094  2eu1 2112  ra4 2406  ralcom2 2490  ceqex 2631  vtoclgft 2671  hbsbcgd 2750  intab 3428  axrep1 3597  axrep2 3598  axnulALT 3611  dtru 3662  copsex2t 3701  ssopab2 3734  eusv1 3960  eusv2OLD 3963  eusv2 3964  alxfr 3982  fununi 4582  hbfvd2 4773  dffv2 4820  fiint 5872  nd3 6459  axrepndlem2 6463  axrepnd 6464  axpowndlem2 6468  axpowndlem4 6470  axinfndlem1 6475  axacndlem4 6480  axacndlem5 6481  suppsrlem 6739  cncnplem2 9918  inficlALT 11047  bnj32 13195  bnj954 13621  bnj569 14058  bnj1073 14174  tz6.26 14558  frmin 14591  wfrlem5 14614  frrlem5 14638  imonclem 15956  inficlALTOLD 16196  prtlem14 17101  pm11.57 17170  pm11.59 17172  ax4567to6 17186  ax4567to7 17187  ax10ext 17188  ax10-16 17189  pm14.123b 17214  eubi 17226  compne 17241

Copyright terms: Public domain