| 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 y is
free in ∀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 869. 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 677. Conditional forms of the converse are given
by ax-12 802,
ax-15 806, ax-16 922, and ax-17 925. |
Home