deduction theorem holds for first order logic
In this entry, we show that the deduction theorem holds for first order logic. Actually, depending on the axiom systems, some modifications to the deduction theorem may be necessary. If we use the system given in the beginning of this entry (http://planetmath.org/AxiomSystemForFirstOrderLogic), no modifications are necessary, and the proof is mutatis mutandis the same as the one for propositional logic. However, if we instead use the system given in the remark of that entry, the deduction theorem needs to be revised. For convenience, we briefly state the axiom system here:
, where , , and is free for in
, where is not free in
with modus ponens and generalization as inference rules. A deduction of a wff from a set is a finite sequence of wff’s, where each wff is either an axiom, an element of , or the result of an application of an inference rule.
A big portion of the proof is the same as the one given for the deduction theorem for propositional logic, namely, the cases that is an axiom, an element of , or as the result of an application of modus ponens. We will not repeat the proof here, but refer the reader to this entry (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic) for that. In this entry, we will concentrate on the proof of the last case: when is the result of an application of universal generalization.
Let us first rephrase the conditions in the theorem. We are given a deduction of from , that is, sequence of wff’s
such that if is (where ), then either
the variable is not free in , or
the deduction of in the sequence does not contain
As mentioned, we assume that is , where is in .
We induct on the length of . By the assumption on , is at least . If , then is
Then is either an axiom, or an element of . Furthermore, does not occur free in . If is either an axiom or in , then
is a deduction of from . If is , then
is a deduction of from , where is a deduction of the tautology (see here (http://planetmath.org/AxiomSystemForPropositionalLogic)).
Now assume the length of is . Furthermore, we may assume that it has the form
from . Then none of contain free. Now, let us look at the conditions above:
is not free in . As is a deduction of of length , by induction, there is a deduction of
of from . Since does not occur free in ,
is a deduction of .
the deduction of in the sequence does not contain . Let
be this deduction of in . Then
is a deduction of .
In both cases, since does not occur in the deduction, . ∎
Note that the last three steps of deductions and use generalization, the axiom schema , and modus ponens, and the last steps of deductions and use generalization, the axiom schema , and modus ponens.
As a corollary, we have
If , and a sentence, then .
Remark. If we want to restore the modified deduction theorem to its original version (Theorem 2 below), and we want keep the axiom system stated above, the way deductions are constructed needs to be modified. In this case, the modification is: if is a deduction of , and is , the result of an application of generalization to an earlier wff , then does not occur free in any of the wff’s in the deduction. With this change, we have the original version:
(Deduction Theorem). If , then .
|Title||deduction theorem holds for first order logic|
|Date of creation||2013-03-22 19:32:31|
|Last modified on||2013-03-22 19:32:31|
|Last modified by||CWoo (3771)|