Let $\mathcal{L}_0=\mathcal{L}[\{\neg, \rightarrow\}]$. Define the system $L_0$ as follows:

An axiom of $L_0$ is any formula of $\mathcal{L}_0$ of the form

  • (A1) $(\alpha \rightarrow ( \beta \rightarrow \alpha))$
  • (A2) $((\alpha \rightarrow ( \beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow ( \beta \rightarrow \gamma)))$
  • (A3) $((\neg \beta \rightarrow \neg \alpha ) \rightarrow (\alpha \rightarrow \beta))$

The only rule of inference in $L_0$ is modus ponens, i.e. from $\alpha$ and $(\alpha \rightarrow \beta)$ infer $\beta$.

A formula of $\mathcal{L}_0$, $\phi$, is provable from a set of formulas $\Gamma$ in the system $SQ$, if there exists a finite sequence of sequents where each follows from the next according to the following set of rules:

  • (Ass) If $\psi \in \Delta$, we infer $\Delta \vdash_{SQ} \psi$
  • (MP) If $\Delta \vdash_{SQ} \psi$ and $\Delta ' \vdash_{SQ} (\psi \rightarrow \phi)$ then infer $\Delta \cup \Delta ' \vdash_{SQ} \phi$
  • (DT) If $\Delta \cup \{\psi \} \vdash_{SQ} \chi$ we infer $\Delta \vdash_{SQ} (\psi \rightarrow \chi)$
  • (PC) If $\Delta \cup \{ \neg \psi \} \vdash_{SQ} \chi$ and $\Delta ' \cup \{ \neg \psi \} \vdash_{SQ} \neg \chi$ infer that $\Delta \cup \Delta ' \vdash_{SQ} \psi$

Prove that the systems $SQ$ and $L_0$ are equivalent, i.e. that $\Gamma \vdash_{L_0} \phi$ iff $\Gamma \vdash_{SQ} \phi$.

Ideally the legwork for this has been done elsewhere, in which case a link will be gratefully received.

Is the idea then to show that $\emptyset \vdash_{SQ} (A1)$, $\emptyset \vdash_{SQ} (A2)$, $\emptyset \vdash_{SQ} (A3)$ and that $SQ$ somehow implies (MP) in $L_0$, and then to do the reverse, i.e. show that $L_0$ proves each of the sequents of $SQ$? I don't quite see how that would be formalised.

  • $\begingroup$ Basically, you are on the right track; in $SQ$ you have the rule (MP) that is already modus ponens; thus, it is enough to "rewrite" (MP) with $\Delta = \Delta' = \emptyset$. For the other "direction", you need Deduction Theorem (provable from (A1)-(A3) with the help of $\vdash \alpha \rightarrow \alpha$, which is easily derivable from them), i.e. from $\Gamma \cup \alpha \vdash \beta$, infer $\Gamma \vdash (\alpha \rightarrow \beta)$: this will play the role of (DT). About (PC), it is "simply" (A3) in sequent-form. $\endgroup$ – Mauro ALLEGRANZA Apr 15 '14 at 13:45
  • 1
    $\begingroup$ You have to "consult" a textbook which use the same $L_0$ axiom system, like Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997) : page 35, with "deduction from $\Gamma$ and Deduction Theorem (page 37). They are the "ingredients" for deriving in it (Ass) (trivial) and (MP) (see comment above) and (DT) and (PC) (as above). I suggest you also : Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012) : Chapter 3 (page 49-on); the "mechanism" is explained but, unfortunately, the sequent calculus system is different... $\endgroup$ – Mauro ALLEGRANZA Apr 15 '14 at 14:19
  • $\begingroup$ See Wiki for an on-line resource regarding how to prove Deduction Theorem with your $L_0$. $\endgroup$ – Mauro ALLEGRANZA Apr 15 '14 at 14:59

I suppose there is a mistake; your (A2) must be :

$(α→(β→γ)) \rightarrow ((α→β)→(α→γ))$.

From $SQ$ to $\mathsf L_0$ we have :


1) --- $\alpha, \beta \vdash \alpha$ --- by (Ass)

2) --- $\alpha \vdash \beta \rightarrow \alpha$ --- from 1) by (DT)

3) --- $\vdash \alpha \rightarrow (\beta \rightarrow \alpha)$ --- from 2) by (DT).


1) --- $\alpha \rightarrow (\beta \rightarrow \gamma) \vdash \alpha \rightarrow (\beta \rightarrow \gamma)$ --- by (Ass)

2) --- $\alpha \vdash \alpha $ --- by (Ass)

3) --- $\alpha, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \beta \rightarrow \gamma$ --- from 1), 2) by (MP)

4) --- $\alpha \rightarrow \beta \vdash \alpha \rightarrow \beta $ --- by (Ass)

5) --- $\alpha, \alpha \rightarrow \beta \vdash \beta $ --- from 2), 4) by (MP)

6) --- $\alpha, \alpha \rightarrow \beta, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \gamma$ --- from 3), 5) by (MP)

7) --- $\alpha \rightarrow \beta, \alpha \rightarrow (\beta \rightarrow \gamma) \vdash \alpha \rightarrow \gamma$ --- from 6) by (DT)

8) --- $\alpha \rightarrow (\beta \rightarrow \gamma) \vdash (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma)$ --- from 7) by (DT)

9) --- $\vdash (\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma))$ --- from 8) by (DT).


1) --- $\lnot \beta \rightarrow \lnot \alpha \vdash \lnot \beta \rightarrow \lnot \alpha$ --- by (Ass)

2) --- $\lnot \beta \vdash \lnot \beta$ --- by (Ass)

3) --- $\lnot \beta, \lnot \beta \rightarrow \lnot \alpha \vdash \lnot \alpha$ --- from 1), 2) by (MP)

4) --- $\alpha, \lnot \beta \vdash \alpha$ --- by (Ass)

5) --- $\alpha, \lnot \beta \rightarrow \lnot \alpha \vdash \beta$ --- from 4), 5) by (PC)

6) --- $\lnot \beta \rightarrow \lnot \alpha \vdash \alpha \rightarrow \beta$ --- from 5) by (DT)

7) --- $\vdash (\lnot \beta \rightarrow \lnot \alpha) \rightarrow (\alpha \rightarrow \beta$) --- from 6) by (DT).

The only rule of inference of $\mathsf L_0$ is modus ponens; we derive it from (MP) simply with $\Delta = \Delta' = \emptyset$.


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.