« Section 2.4: Problem 4 Solution

Section 2.4: Problem 6 Solution »

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:
  1. If , then and .
  2. If , then does not occur free in , and with two additional steps in the deduction .
  3. 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.