You are here
Homededuction theorem holds for first order logic
Primary tabs
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, 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:
1. 2. $\forall xA\to A[a/x]$, where $x\in V$, $a\in V(\Sigma)$, and $a$ is free for $x$ in $A$
3. $\forall x(A\to B)\to(A\to\forall xB)$, where $x\in V$ is not free in $A$
with modus ponens and generalization as inference rules. A deduction of a wff $A$ from a set $\Delta$ is a finite sequence of wff’s, where each wff is either an axiom, an element of $\Delta$, or the result of an application of an inference rule.
Theorem 1.
(Modified Deduction Theorem). If $\Delta,A\vdash B$, then $\Delta\vdash A\to B$, provided that there is a deduction $\mathcal{E}$ of $B$ from $\Delta\cup\{A\}$ that contains no applications of universal generalization

either to a variable occurring free in $A$, or

to a wff whose deduction in $\mathcal{E}$ contains $A$ as a premise
A big portion of the proof is the same as the one given for the deduction theorem for propositional logic, namely, the cases that $B$ is an axiom, an element of $\Delta$, or as the result of an application of modus ponens. We will not repeat the proof here, but refer the reader to this entry for that. In this entry, we will concentrate on the proof of the last case: when $B$ is the result of an application of universal generalization.
Proof.
Let us first rephrase the conditions in the theorem. We are given a deduction $\mathcal{E}$ of $B$ from $\Delta\cup\{A\}$, that is, sequence of wff’s
$A_{1},\ldots,A_{n}$ 
such that if $A_{i}$ is $\forall xA_{j}$ (where $j<i$), then either
As mentioned, we assume that $B$ is $\forall xA_{k}$, where $A_{k}$ is in $\mathcal{E}$.
We induct on the length $n$ of $\mathcal{E}$. By the assumption on $B$, $n$ is at least $2$. If $n=2$, then $\mathcal{E}$ is
$A_{1},\forall xA_{1}.$ 
Then $A_{1}$ is either an axiom, or an element of $\Delta\cup\{A\}$. Furthermore, $x$ does not occur free in $A_{1}$. If $A_{1}$ is either an axiom or in $\Delta$, then
$A_{1},\forall xA_{1},\forall xA_{1}\to(A\to\forall xA_{1}),A\to\forall xA_{1}$  (1) 
is a deduction of $A\to B$ from $\Delta$. If $A_{1}$ is $A$, then
$\cdots,A\to A,\forall x(A\to A),\forall x(A\to A)\to(A\to\forall xA),A\to% \forall xA$  (2) 
is a deduction of $A\to B$ from $\Delta$, where $\cdots,A\to A$ is a deduction of the tautology $A\to A$ (see here).
Now assume the length of $\mathcal{E}$ is $n>2$. Furthermore, we may assume that it has the form
$A_{1},\ldots,A_{{n1}},\forall xA_{{n1}}$ 
from $\Delta\cup\{A\}$. Then none of $A_{1},\ldots,A_{{n1}}$ contain $x$ free. Now, let us look at the conditions above:

$x$ is not free in $A$. As $A_{1},\ldots,A_{{n1}}$ is a deduction of $A_{{n1}}$ of length $n1$, by induction, there is a deduction of
$B_{1},\ldots,B_{m}$ of $A\to A_{{n1}}$ from $\Delta$. Since $x$ does not occur free in $A$,
$B_{1},\ldots,B_{m},\forall x(A\to A_{{n1}}),\forall x(A\to A_{{n1}})\to(A\to% \forall xA_{{n1}}),A\to\forall xA_{{n1}}$ (3) is a deduction of $A\to\forall xA_{{n1}}$.

the deduction of $A_{j}$ in the sequence $A_{1},\ldots,A_{j}$ does not contain $A$. Let
$B_{1},\ldots,B_{m}$ be this deduction of $A_{j}$ in $\mathcal{E}$. Then
$B_{1},\ldots,B_{m},\forall xA_{{n1}},\forall xA_{{n1}}\to(A\to\forall xA_{{n% 1}}),A\to\forall xA_{{n1}}$ (4) is a deduction of $A\to\forall xA_{{n1}}$.
In both cases, since $A$ does not occur in the deduction, $\Delta\vdash A\to B$. ∎
Note that the last three steps of deductions $(1)$ and $(4)$ use generalization, the axiom schema $A\to(B\to A)$, and modus ponens, and the last steps of deductions $(2)$ and $(3)$ use generalization, the axiom schema $\forall x(A\to B)\to(A\to\forall xB)$, and modus ponens.
As a corollary, we have
Corollary 1.
If $\Delta,A\vdash B$, and $A$ a sentence, then $\Delta\vdash A\to B$.
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 $A_{1},\ldots,A_{n}$ is a deduction of $A$, and $A$ is $\forall xA_{i}$, the result of an application of generalization to an earlier wff $A_{i}$, then $x$ does not occur free in any of the wff’s in the deduction. With this change, we have the original version:
Theorem 2.
(Deduction Theorem). If $\Delta,A\vdash B$, then $\Delta\vdash A\to B$.
This is an immediate consequence of the following fact: if $B$ can be deduced with $A$ as a hypothesis, then $A\to B$ can be deduced without $A$ as a hypothesis, which can be easily proved using induction.
Mathematics Subject Classification
03B10 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections