... 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
    $\begingroup$ You should state your axiom system explicitly, since many are in common use. $\endgroup$ – Chris Eagle Nov 6 '12 at 23:31
  • $\begingroup$ Have you seen a proof of the deduction theorem? If you analyse the proof you should be able to extract this upper bound. $\endgroup$ – Zhen Lin Nov 6 '12 at 23:34
  • $\begingroup$ @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. $\endgroup$ – Spook Nov 7 '12 at 12:20

Your argument :

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.