# Propositional calculus. If there is a deduction of $t$ from $S\cup\{s\}$ in $n$ lines,

... then there is a deduction of $(s\Rightarrow t)$ in at most $3n+2$ lines.

So I think this should be done by induction. The cases with $t$ being an axiom or a member of $S$ or $t=s$ can be proved by explicitly deducing $(s\Rightarrow t)$ in 5 lines or fewer. But what happens if $t$ is deduced from previous lines using Modus Ponens?

The axioms I am using are $$(s\Rightarrow (t \Rightarrow s)) \\((s\Rightarrow(t\Rightarrow u))\Rightarrow((s\Rightarrow t)\Rightarrow(s\Rightarrow u))) \\ (((s\Rightarrow \bot)\Rightarrow \bot)\Rightarrow s)$$

In a deduction every step is either an axiom or deduced by modus ponens.

-
You should state your axiom system explicitly, since many are in common use. – Chris Eagle Nov 6 '12 at 23:31
Have you seen a proof of the deduction theorem? If you analyse the proof you should be able to extract this upper bound. – Zhen Lin Nov 6 '12 at 23:34
@ZhenLin If in deducing $t$ from $S\cup\{s\}$, $t$ comes from MP from previous lines $r$ and $r\Rightarrow t$ then the proof I have seen writes down the deduction of $s\Rightarrow r$ and $s\Rightarrow (r\Rightarrow t)$ and write down $(s\Rightarrow (r\Rightarrow t))\Rightarrow((s \Rightarrow r)\Rightarrow (s \Rightarrow t)$ and apply MP two more times. But if I use induction then the induction hypothesis on the number of lines in which I can write down the deduction of $s\Rightarrow r$ and $s\Rightarrow (r\Rightarrow t)$ is not strong enough. – Montez Nov 7 '12 at 12:20

"If in deducing $\tau$ from $\Gamma \cup \{ \sigma \}$, $\tau$ comes by MP from previous lines $\phi$ and $\phi ⇒ \tau$ then the proof proceed as follows:

(a) write down the deduction of $\sigma ⇒ \phi$

(b) write down the deduction of $\sigma ⇒ (\phi ⇒ \tau)$

(c) write down $(\sigma ⇒ (\phi ⇒ \tau)) ⇒ ((\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau))$

and apply MP twice"

is sound.

Because the "upper bound" $3n+2$ is relative to the number $n$ of lines in the derivation, we have to prove it by induction on $n$.

(A) --- The induction start from the base case, i.e. $n=1$. But a one-line derivation of $\tau$ from $\Gamma \cup \{ \sigma \}$ is possible only if $\tau$ is in $\Gamma$ or it is an axiom or it is $\sigma$ itself.

If $\tau$ is in $\Gamma$ or $\tau$ is a logical axiom, we need a $3$ lines derivation :

(i) $\tau$ --- in $\Gamma$ or axiom

(ii) $\sigma ⇒ (\tau ⇒ \sigma)$ --- axiom

(iii) $\tau ⇒ \sigma$ --- by MP.

If $\tau$ is $\sigma$, we need the "standard" derivation : $\vdash \tau ⇒ \tau$, which is $5$ lines long.

Thus, in both cases, we have a resulting derivation $\le 5=3 \times n +2$, with $n=1$.

(B) --- Now we need the induction hypothesis, i.e. that $\sigma ⇒ \phi$ and $\sigma ⇒ (\phi ⇒ \tau)$ have both "resulting" derivations $\le 3 \times (n-1) +2$ lines, and we want to show that the resulting derivation for $\sigma ⇒ \tau$ has $\le 3 \times n +2$ lines.

In the "initial" derivation we add only the line $k$-th line :

(k) $\quad \tau$ --- from previous lines $i, j$ (with $1 \le i, j, < k$) by MP,

as "justification".

Now, we have to add the axiom instance (a) above :

(l) $(\sigma ⇒ (\phi ⇒ \tau)) ⇒ ((\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau))$ --- axiom

(l+1) $(\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau)$ --- from (i) and (l) by MP

(l+2) $\sigma ⇒ \tau$ --- from (j) and (l+1) by MP.

The "resulting" derivation of $\sigma ⇒ \tau$ has $\le 3 \times (n-1) +2 +3 = 3n + 2$ lines.

-