# 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