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).