**Instances of Axiom 1**:

- ∀
*xPx*→ (*a*↓ →*Pa*) - ∀
*xPx*→ (*z*↓ →*Pz*) - ∀
*F*(*Fa*) → (*P*↓ →*Pa*) - ∀
*F*(*Fa*) → (*H*↓ →*Pa*) - ∀
*xPx*→ (℩*xQx*↓ →*P*℩*xQx*) - ∀
*F*(*Fa*) → ([λ*y**Ry*℩*xQx*]↓ → [λ*y**Ry*℩*xQx*]*a*)

The first example asserts: if everything exemplifies the property
*P*, then if *a* exists, then *a*
exemplifies *P*. The second example says something similar.
In formal terms, these examples tell us that we may instantiate the
name *a* or variable *z* into a universal quantifier if
we know that the constant *a* or the variable *z*
denotes something. And we know both of these by axiom (45.2)
above.

The third example asserts: if *a* exemplifies every property,
then if *P* exists, then *a* exemplifies *P*. The
fourth example says something similar. In formal terms, examples 3 and
4 tell us that we may instantiate names of, and variables for,
properties into universal claims if we know that a simple property name or
variable has a denotation. And we know that they do by axiom (45.2)
above.

The fifth example asserts: if everything exemplifies *P*, then
if the *x* that exemplifies *Q* exists, then the *x*
that exemplifies *Q* exemplifies *P*. Intuitively, we may
not instantiate a description into a universal claim unless we know
that the description denotes something.

The sixth example asserts: if *a* exemplifies every property, then if
*being a y that bears R to the x that exemplifies Q* exists,
then *a* exemplifies *being a y that bears R to the x that
exemplifies Q*. In this case, we know that the property
*being a y that bears R to the x that exemplifies Q* exists,
i.e., [λ*y* *Ry*℩*xQx*]↓, by
axiom (45.2), since the λ. doesn bind a variable in any
encoding formula that is a subterm of the λ-expression.

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 guaranteed to denote, 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**:

[Examples were discussed in the examples of Axiom 1.]

**Instances of Axiom 3**:

- ∀
*x*(*Pa*→*Qx*) → (*Pa*→ ∀*xQx*) - ∀
*F*(*Pa*→*Fb*) → (*Pa*→ ∀*F**Fb*)

The first example asserts: if, for every *x*, if *a*
exemplifies *P*, then *x* exemplifies *Q*, then
if *Pa*, then every *x* exemplifies *Q*. In formal
terms, we can move a universal quantifier across the antecedent of a
conditional if the variable bound by the quantifier is not free in the
antecedent. The restriction that the antecedent of the conditional
contain no free occurences of the quantified variable prevents us from
deriving a falsehood from a truth. For example, it is logically true
that: every *x* is such that if *x* exemplifies *P*
then *x* exemplifies *P*. But if we could move the
quantifier across this conditional, we could conclude: if *x*
exemplifies *P*, then every *x* exemplifies *P*. This
is not a logical truth. It is false in those domains in which not all
the elements are in the extension of *P*; in such domains, the
sentence would be false when something that exemplifies *P* is
assigned to *x*, for then the antecedent is true and the
conclusion, *every x exemplifies P*, is false.

**Instances of Axiom 4**:

[Exercise.]

**Instances of Axiom 5(a)**:

*P*℩*xQx*→ ℩*xQx*↓- [λ
*y**Ry*℩*xQx*]*a*→ [λ*y**Ry*℩*xQx*]↓

The first example asserts: If the *x* that exemplifies *Q*
exemplifies *P*, then *the x that exemplifies Q* exists.
In formal terms, this tells us that if a definite description appears
in a true atomic formula, then the description has a denotation. The
second example asserts: if *a* exemplifies the property *being
a y such that y bears R to the x that exemplifies Q*, then the
property *being a y such that y bears R to the x that exemplifies
Q* exists. In formal terms, this tells us that the complex
predicate itself must have a denotation if it appears in a true atomic
formula, even if it has a definite description as a component.

We leave examples of Axiom 5(b) as exercises.

**The Rule of Generalization** (GEN):

It is
important to mention that our logic of quantification is one in which
formulas with free variables are assertable. This simply means that
claims (logical axioms, logical theorems, non-logical axioms, and
non-logical theorems) may be asserted even if contain a free variable.
Given the derived metarule GEN, 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* (◊*xF* → □*xF*).
This is a formula in which the variables
*x* and *F* are 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*, i.e.,
∀*F*∀*x*(◊*xF* →
□*xF*). This universal generalization is, therefore, a
logical theorem.

**Metarule/Derived Rule: Universal Elimination (∀E)**

Let us justify the (.2) version of the rule, where τ meets the following two preconditions, namely, (a) it is a primitive constant, a variable, or a λ-expression in which the initial λ does not bind any variable in any encoding formula subterm, and (b) it is substitutable for α in φ:

1. ∀αφ Premise 2. ∀αφ → (τ↓ → φ[τ/α]) Instance, axiom (45.2), given the preconditions on τ 3. τ↓ → φ[τ/α] from 1, 2, by Rule MP 4. τ↓ instance, axiom (45.2), given the preconditions on τ 5. φ[τ/α] from 3, 4 by Rule MP 6. ∀αφ → φ[τ/α] from 1–5, by Rule CP (conditional proof)

This justifies the second version of Rule ∀E: (a) it is a finite sequence, line 1 is a premise, line 2 is the first axiom of quantificational logic, line 3 results from lines 1 and 2 by MP, line 4 is the second axiom of quantificational logic, line 5 results from lines 3 and 4 by MP, and line 6 follows from lines 1–5 by the metarule of conditional proof.

**Metarule/Deriverd Rule of Universal Introduction
(∀I)**

In this rule, **Λ** is the set of axioms of object
theory, where these may be expressed using open formulas. So this
rule can't be applied to universally generalize on a variable that
occurs free in one of the axioms cited in the proof.

∀Consider the following sequence of formulas:x(Px→Qx), ∀xPx⊢ ∀xQx

1. ∀ x(Px→Qx)Premise 2. ∀ xPxPremise 3. Pa→Qafrom 1, by Rule ∀E, with aarbitrary4. Pafrom 2, by Rule ∀E 5. Qafrom 3, 4, by Rule MP 6. ∀ xQxfrom 5, by Rule ∀I

Notice that this constitutes a proof of
*everything exemplifies Q* from *everything that exemplifies
P exemplifies Q* and *everything exemplifies P*: it is a
finite sequence, lines 1 and 2 are members of the premise set, lines 3
and 4 and results from lines 1 and 2, respectively, by a justified
rule of inference, line 5 results from previous lines by MP, and line
6 results from line 5 by a justified rule. Notice also that in this
proof, the constant symbol *a* did not occur in the premises
and that the variable *x* does not occur in *a exemplifies
Q*. So the Rule ∀I applies and we are entitled to conclude
that *everything exemplifies Q* is derivable from the two given
premises.

**Fact:** ⊢ ∀*xPx* → *Px*

This asserts that: it is a theorem that if everything
exemplifies *P*, then *x* exemplifies *P*. Exercise:
Demonstrate that this is true.

**Fact:** ⊢ ∀*x*(*Px* → *Qx*)
→ ∀*x*(¬*Qx* → ¬*Px*)

If we assume the rule of Contraposition from sentential logic, then we may demonstrate this fact as follows. Consider first the following sequence of formulas:

1. ∀ x(Px→Qx)Premise 2. Pa→Qafrom 1, by ∀E, with a arbitrary3. ¬ Qa→ ¬Pafrom 2, by contraposition 4. ∀ x(¬Qx→ ¬Px)from 3, by Universal Introduction (Rule ∀I) 5. ∀ x(Px→Qx) → ∀x(¬Qx→ ¬Px)from 1–4, by Conditional Proof

In this derivation, line 4 follows from lines 2 by the Rule of
Contraposition. Given this derivation, notice that the conditions for
applying the rule of Universal Generalization are met. So by UG, we
know that there is a proof of “everything is such that if it
doesn't exemplify *Q* it doesn't exemplify *P*” from
“everything is such that if it exemplifies *P* then it
exemplifies *Q*”. But by the Deduction Theorem, it
follows that if we conditionalize the former on the latter, the result
is a theorem of logic.