Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-4 GIF version

Axiom ax-4 1392
 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 x is free in ∀yx = y.) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1392 through ax-7 1338 plus rule ax-gen 1339). 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 1339. Conditional forms of the converse are given by ax-12 1393, ax-15 1807, ax-16 1644, and ax-17 1402. 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 1619. An nice alternate axiomatization uses ax467 1455 and ax-5o 1425 in place of ax-4 1392, ax-5 1336, ax-6 1337, and ax-7 1338. This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1423. (We replaced the older ax-5o 1425 and ax-6o 1428 with newer versions ax-5 1336 and ax-6 1337 in order to prove this redundancy.)
Assertion
Ref Expression
ax-4 (xφφ)

Detailed syntax breakdown of Axiom ax-4
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 set x
31, 2wal 1335 . 2 wff xφ
43, 1wi 4 1 wff (xφφ)
 Colors of variables: wff set class This axiom is referenced by:  ax-12  1393  hbequid  1397  ax5o  1424  ax5  1426  ax6o  1427  ax6  1429  a4i  1432  a4s  1433  a4sd  1434  hbnt  1435  hbim  1439  ax46  1449  ax67to6  1453  ax467  1455  19.3  1461  19.21  1464  19.21bi  1467  hbimd  1475  19.21t  1477  a6e  1527  19.12  1535  19.38  1540  ax9o  1557  hbae  1578  drex1  1588  equveli  1603  sb2  1611  ax11  1655  ax11b  1656  dfsb2  1661  sbf3t  1685  hbsb4  1686  hbsb4t  1687  sb56  1704  sb6  1705  a16gb  1714  sbal1  1793  ax11indalem  1815  ax11inda2ALT  1816  mopick  1886  2eu1  1904
 Copyright terms: Public domain W3C validator