I'm can't solve Exercise 2 on page 30 on Rautenberg (Chapter 1.4 - A calculus of Natural Deduction), which reads:

Augment the signature $\{\lnot, \land\}$ by $\lor$ and prove the completeness of the calculus obtained by supplementing the basic rules used so far (see at the bottom of my question) with the rules:

$(\lor1)$ $\dfrac{X \vdash \alpha}{X \vdash \alpha \lor \beta, \beta \lor \alpha}$

$(\lor2)$ $\dfrac{X,\alpha \vdash \gamma \ \mid \ X,\beta\vdash \gamma}{X,\alpha \lor \beta \vdash , \gamma}$

The solution and hints reads:

Prove that $X \vdash \alpha \lor \beta \iff X\vdash \alpha$ or $X\vdash \beta$. It is clear to me why this is needed, however I can't prove $\Rightarrow$. If you could please help. Thank-you

These are the inference rules for the system (+ the two above)

(IS) $\dfrac{}{\alpha\vdash\alpha}$

(MR) $\dfrac{X\vdash\alpha}{X'\vdash\alpha}$, if $X\subseteq$ X'

($\land$1) $\dfrac{X\vdash\alpha,\beta}{X\vdash\alpha\land\beta}$

($\land$2) $\dfrac{X\vdash\alpha\land\beta}{X\vdash\alpha,\beta}$

($\lnot$1) $\dfrac{X\vdash\alpha,\lnot\alpha}{X\vdash\beta}$

($\lnot$2) $\dfrac{X,\alpha \vdash \beta \ \mid \ X,\lnot\alpha\vdash \beta}{X\vdash \beta}$

  • $\begingroup$ Can you write down all the inference rules of your system? $\endgroup$ – Taroccoesbrocco Aug 10 '18 at 15:23
  • $\begingroup$ Please find the inference rules at the bottom of my question. Thanks $\endgroup$ – Lorenzo Gandini Aug 10 '18 at 17:53

You cannot prove in any classical logic: $X \vdash α \vee β$ iff $X \vdash α$ or $X \vdash β$ in general. Here is a counter example:

$$p \vee \neg p \vdash p \vee \neg p$$

But you don't have neither:

$$p \vee \neg p \nvdash p$$

$$p \vee \neg p \nvdash \neg p$$

You can argue semantically $p \vee \neg p$, as a Tautology, has two models $p=0$ and $p=1$. But the model $p=0$ prevents a consequence $p$. And the model $p=1$ prevents a consequence $\neg p$.

Edit: What Routenbergs Exercise Nr. 2 on Page 30 is about, is showing completness. So you would proceed with a consistent X and construct a maximally consistent X' (like in his Theorem 4.6), where you would indeed then have if $α \vee β \in X'$, then either $α \in X'$ or $β \in X'$.


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.