**Instances of Axiom 1**:

Note that in all the examples, the term instantiated into the
universal claim is *substitutable* for the variable. This is
designed to avoid the situation in which a term gets `captured', when
substituted into a quantified claim, by a quantifier for that variable
that already exists in the claim. For example, suppose the following
claim is true: *for every x, there is a y such that y is not
identical with x*. The variable *y* already appears in
this claim bound by a quantifier. Now suppose we could instantiate
the quantifier `*for every x*' in this claim to the variable
*y* (variables are terms, so they can be instantiated into
universal claims) by removing the quantifier from the claim and
replacing *y* for *x* everywhere *x* appears.
The resulting claim would be: *there is a y such that y is not
identical with y*, which is clearly false. Therefore, we would
have proven a falsehood from a truth. The problem with substituting
the variable *y* in this claim is that it was `captured' by the
quantifier `*there is a y*' that was already part of the claim.
This alters the significance of the resulting sentence upon
substitution, and the restriction that terms be substitutable for
the quantified variable avoids this situation.

**Instances of Axiom 2**:

**Instances of Axiom 3**:

**Instances of Axiom 4**:

**The Rule of Generalization**:

It is important
to mention that our logic of quantification is one in which formulas
with free variables are assertable. This simply means that logical
axioms, logical theorems, non-logical axioms and non-logical theorems
may be expressed by formulas that contain a free variable. Given our
Rule of Generalization, it is an immediate consequence that the
universal closures of these axioms and theorems are also theorems.
So, for example, the logical axiom for the logic of encoding is:
*if it is possible that x encodes F, then it is necessary that x
encodes F*. This is a formula in which the variable
*x* is free. By two applications of GEN, it follows that:
*for any property F and for any object x, if it is possible that x
encodes F, then it is necessary that x encodes F*. This universal
generalization is, therefore, a logical theorem.

**Metatheorem (The Deduction Theorem) and Derived Rule
(Conditional Proof)**:

**Derived Rules: Universal Instantiation (UI)**

**Derived Rule: Universal Generalization (UG)**

**Exercises**: Look again at the derived rules of
Existential Generalization and Instantiation. What invalid arguments
are the restrictions on the rules designed to prevent? Find an
introductory logic text and look at some examples of the rules in
action. Then use them to demonstrate the following:

**Logical Theorem:**

**Logical Theorem: **