1
$\begingroup$

... 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.

  • 3
    You should state your axiom system explicitly, since many are in common use.2012-11-06
  • 0
    Have you seen a proof of the deduction theorem? If you analyse the proof you should be able to extract this upper bound.2012-11-06
  • 0
    @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.2012-11-07

1 Answers 1