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.

  • 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.2019-04-18

1 Answers 1

1

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.