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:

1. tautologies

2. $\forall xA\to A[a/x]$, where $x\in V$, $a\in V(\mathrm{\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 $\mathrm{\Delta }$ is a finite sequence of wff’s, where each wff is either an axiom, an element of $\mathrm{\Delta }$, or the result of an application of an inference rule.

Theorem 1.

(Modified Deduction Theorem). If $\mathrm{\Delta }\mathrm{,}A\mathrm{⊢}B$, then $\mathrm{\Delta }\mathrm{⊢}A\mathrm{\to }B$, provided that there is a deduction $\mathrm{E}$ of $B$ from $\mathrm{\Delta }\mathrm{\cup }\mathrm{\{}A\mathrm{\}}$ that contains no applications of universal generalization

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

• to a wff whose deduction in $ℰ$ 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 $\mathrm{\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 (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic) 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 $ℰ$ of $B$ from $\mathrm{\Delta }\cup \{A\}$, that is, sequence of wff’s

$$A_1,\mathrm{\dots },A_n$$

such that if $A_i$ is $\forall x{A}_j$ (where ), then either

• the variable $x$ is not free in $A$, or

• the deduction of $A_j$ in the sequence $A_1,\mathrm{\dots },A_j$ does not contain $A$

As mentioned, we assume that $B$ is $\forall x{A}_k$, where $A_k$ is in $ℰ$.

We induct on the length $n$ of $ℰ$. By the assumption on $B$, $n$ is at least $2$. If $n=2$, then $ℰ$ is

$$A_1,\forall x{A}_1.$$

Then $A_1$ is either an axiom, or an element of $\mathrm{\Delta }\cup \{A\}$. Furthermore, $x$ does not occur free in $A_1$. If $A_1$ is either an axiom or in $\mathrm{\Delta }$, then

$$A_1,\forall x{A}_1,\forall x{A}_1\to (A\to \forall x{A}_1),A\to \forall x{A}_1$$ (1)

is a deduction of $A\to B$ from $\mathrm{\Delta }$. If $A_1$ is $A$, then

$$\mathrm{\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 $\mathrm{\Delta }$, where $\mathrm{\cdots },A\to A$ is a deduction of the tautology $A\to A$ (see here (http://planetmath.org/AxiomSystemForPropositionalLogic)).

Now assume the length of $ℰ$ is $n>2$. Furthermore, we may assume that it has the form

$$A_1,\mathrm{\dots },A_{n-1},\forall x{A}_{n-1}$$

from $\mathrm{\Delta }\cup \{A\}$. Then none of $A_1,\mathrm{\dots },A_{n-1}$ contain $x$ free. Now, let us look at the conditions above:

• $x$ is not free in $A$. As $A_1,\mathrm{\dots },A_{n-1}$ is a deduction of $A_{n-1}$ of length $n-1$, by induction, there is a deduction of

  $$B_1,\mathrm{\dots },B_m$$

  of $A\to A_{n-1}$ from $\mathrm{\Delta }$. Since $x$ does not occur free in $A$,

  $$B_1,\mathrm{\dots },B_m,\forall x(A\to A_{n-1}),\forall x(A\to A_{n-1})\to (A\to \forall x{A}_{n-1}),A\to \forall x{A}_{n-1}$$ (3)

  is a deduction of $A\to \forall x{A}_{n-1}$.

• the deduction of $A_j$ in the sequence $A_1,\mathrm{\dots },A_j$ does not contain $A$. Let

  $$B_1,\mathrm{\dots },B_m$$

  be this deduction of $A_j$ in $ℰ$. Then

  $$B_1,\mathrm{\dots },B_m,\forall x{A}_{n-1},\forall x{A}_{n-1}\to (A\to \forall x{A}_{n-1}),A\to \forall x{A}_{n-1}$$ (4)

  is a deduction of $A\to \forall x{A}_{n-1}$.

In both cases, since $A$ does not occur in the deduction, $\mathrm{\Delta }⊢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 $\mathrm{\Delta }\mathrm{,}A\mathrm{⊢}B$, and $A$ a sentence, then $\mathrm{\Delta }\mathrm{⊢}A\mathrm{\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,\mathrm{\dots },A_n$ is a deduction of $A$, and $A$ is $\forall x{A}_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 $\mathrm{\Delta }\mathrm{,}A\mathrm{⊢}B$, then $\mathrm{\Delta }\mathrm{⊢}A\mathrm{\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.

Title	deduction theorem holds for first order logic
Canonical name	DeductionTheoremHoldsForFirstOrderLogic
Date of creation	2013-03-22 19:32:31
Last modified on	2013-03-22 19:32:31
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	26
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B10