# Section 2.4: Problem 5 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

Find a function
such that if a formula
has a deduction of length
from a set
, and if
does not occur free in
, then
has a deduction from
of length
. The more slowly your function grows, the better.

If
does not occur free in
, we can use axiom 4 and add
to the end. However, in general,
may contain
as a free variable. What we will try to do is to change every formula
in a deduction of
to
, and evaluate
, the number of additional steps needed in the worst case scenario, by induction:

- If , then and .
- If , then does not occur free in , and with two additional steps in the deduction .
- Otherwise, is deduced from and , where by induction we have already changed them to and , accordingly, and we need three steps instead of one previous MP-rule, namely, , and two new MP-rules.

Overall, we see that, in the worst case scenario when no axioms are used, we need three formulas in a deduction instead of each one. Of course, there could be some shortcuts even if there are no axioms in the deduction, for example, as noted at the very beginning of the solution, but in the worst case scenario,
.

A more precise function would be one in two variables, where for a deduction of
of length
using
axioms and
other rules (
or MP), there is always a deduction of
of length
using
axioms and
other rules (
or MP). Then,

*Example*(p. 122). A deduction for : , , , , , a deduction of length 5. According to our derived function , should require no more than steps. However, here we have two free variables, 3 axioms, and 2 MP-rules. Hence, the formula in two variables gives us , , for , and , , for . As mentioned on page 122, the length of is indeed the best we can achieve in this case.