# Section 2.5: Problem 3 Solution

Working problems is a crucial part of learning mathematics. No one can learn... merely by poring over the definitions, theorems, and examples that are worked out in the text. One must work part of it out for oneself. To provide that opportunity is the purpose of the exercises.

James R. Munkres

Assume that
and that
is a predicate symbol which occurs neither in
nor in
. Is there a deduction of
from
in which
nowhere occurs?

*Suggestion*: There are two very different approaches to this problem. The “soft” approach makes use of two languages, one that contains and one that does not. The “hard” approach considers the question whether can be systematically eliminated from a given deduction of from .
“Soft”.
implies
. For every structure
for the language without
and
such that
, consider corresponding structure
for the language with
, which extends
by defining
. Then
(as no wff in
uses
), and, hence,
, implying
(for the same reason). Therefore,
in the language without
, and
.

“Hard”.
implies that there is a deduction of
from
that may use
. We show that the deduction can be changed to one not containing
. Every occurrence of
in the deduction is an atomic subformula, which is a part of the modus ponens rule or a valid logical axiom, so that we can hope to change it to another atomic formula throughout the deduction and preserve the validity of reasoning. So, suppose that we change every occurrence of
to
in every formula
of the deduction, we call it
, and we will see, what properties of such substitution we need to ensure. First, we consider logical axioms.

- is a tautology. Then, by substituting an atomic formula by another one in all places, remains a tautology.
- is where is substitutable for in . is where must be substitutable for in . The only case where is not substitutable for in , is where there is a subformula such that , is free in , and occurs in . If (containing ) is substitutable in , then is not free in . Therefore, to ensure that our substitution does not create a substitutability problem, we just need to make sure that does not contain new (free) variables that occur anywhere as the subject of substitution. For example, we may use the same terms as in (if we have another -place predicate ), or use variables that do not occur in the deduction at all.
- becomes .
- If is where does not occur free in , then becomes where does not occur free in if does not contain new (free) variables that occur anywhere as a quantified variable.
- remains the same.
- remains the same if , otherwise it becomes where we need to define the meaning of . We will get back to this later.

Second, if
is obtained by modus ponens, then it must have been derived from some
and
, which become
and
, respectively, implying
by modus ponens, as long as
is the same as
.

Overall, we need to ensure the following properties of substitution: in substitution of
by
, we need that a)
does not introduce any new (compared to
) free variable
that occurs anywhere in
or
, and b) the substitution is carried out in such a way that
is

*always*the same as , and similar for and . In particular, this concerns all axioms. We can see that the only potentially problematic axiom group is axiom group 6, where we need to ensure that always equals , i.e. if is obtained from by substituting for at some places, then is also obtained from by substituting for at some places.
In fact, it seems that if, for example, the language has the equality symbol, we can do something as simple, as substituting
for all
regardless of the terms, where
is a variable that does not occur in any wffs in the deduction. Indeed,
does not introduce any new free variables that were used at any places in the deduction, and any non-prime formula of axiom group 6 becomes
, which is fine. If the equality is not in the language, then we may use any other predicate symbol
and substitute
for
(there has to be at least one
different from
, as otherwise, there would not be any atomic formulas in which
does not occur).