Axiom ax-4 951

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. Unlike the more typical 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 1168. 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 955. Conditional forms of the converse are given by ax-12 1104, ax-15 1109, ax-16 1194, and ax-17 1190.

General remarks: Predicate calculus, or first-order logic, introduces quantifiers to make statements such as "for all individuals, such-and-such is true" and "there exist individuals such that... ." We introduce a new kind of variable, called an "individual variable," that ranges over individuals. (Actually, in Metamath we are introducing "metavariables" that range over the individual variables of textbook predicate calculus, but the theorems look the same. This is a technical point you should be aware of when studying standard textbooks.) In addition, predicate calculus introduces one or more "predicate symbols" that combine individual variables to form wff"s. We will be concerned with two predicate symbols, the equality sign = used in all of mathematics and the stylized epsilon e. used to express "is an element of" in set theory.

Our axioms look quite different from those in standard textbooks, but the rules for manipulating the symbols end up being considerably simpler. The axioms of standard textbooks are derived as theorems stdpc4 1168 and stdpc5 1034.

We will work with the axioms for predicate calculus in four phases. Phase 1 introduces "pure" predicate calculus, which has no predicate symbols. Phase 2, starting at ax-8 1101, introduces the predicate symbol for equality. Phase 3, starting at ax-13 1107, introduces the stylized epsilon predicate symbol for set theory (without specifying any of its properties that are peculiar to set theory). Phase 4, starting at ax-17 1190, introduces the concept of distinct variables (our first use of the $d statement).

In phase 3, we will define (df-sb 1155) and develop the concept of proper substitution. In standard textbooks, substitution is introduced immediately with a somewhat complex recursive definition, since it is needed to state the axioms. Instead, we will define it in terms of concepts contained in the axioms so that in principle it can be eliminated from the language entirely.

Finally, we will define existential uniqueness (df-eu 1359) and develop some basic facts about it.

ax-4 951 through ax-7 954 are the axioms of what we call "pure" predicate calculus. These are valid even when their quantified variables x and y occur ("free" or not) in wff's ph and ps. Thus we do not have to worry about "free" variable restrictions that complicate the traditional textbook axioms.

An alternate axiomatization could use ax467 997 in place of ax-4 951, ax-6 953, and ax-7 954.

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

This axiom is referenced by:  a4i 958  a4s 960  a4sd 961  ax46 991  ax67to6 995  ax467 997  ax6-3 1002  19.8a 1005  19.3 1007  19.12 1023  19.21 1032  19.21bi 1036  19.38 1057  19.21t 1091  19.23t 1092  hbae 1128  equs4 1133  sb2 1160  sbied 1178  ax11 1203  ax11b 1204  dfsb2 1209  hbsb4 1232  hbsb4t 1233  sb56 1250  sb6 1251  a16gb 1259  sbal1 1328  ax11indalem 1345  ax11inda2ALT 1346  mopick 1410  2eu1 1426  ra4 1670  ralcom2 1752  ceqex 1858  abidhb 1884  hbsbc1gd 1954  hbsbcgd 1955  disjssun 2297  intab 2528  axrep1 2662  axrep2 2663  axnul2 2676  dtruALT 2716  ssopab2 2784  alxfr 2859  fununi 3503  hbfvd2 3670  fiint 4486  nd3 4863  axrepndlem2 4868  axrepnd 4869  axpowndlem2 4873  axpowndlem4 4875  axinfndlem1 4880  axacndlem4 4885  axacndlem5 4886  suppsrlem 5144  cncnplem2 7662  imonclem 8933

Copyright terms: Public domain