4
$\begingroup$

About that natural deduction system that is used in the beginning of Chiswell&Hodges. Can I introduce the sequent $\{a,\neg a\} \vdash b$ where $b$ is an arbitrary proposition? In other words this rule says that from absurdity anything follows.

What confuses me is that the rule in the book says that if there are $a$ and $\neg a$, and you have some assumption, for example $\neg c$, you can remove the negation sign from the assumption and introduce $c$. But the proposition $b$ is not an assumption in my system, it is arbitrary. I think I can put $\neg b$ as an vacuous assumption in the derivation, but is it legit to let it appear out of the blue?


EDIT: If I want to prove an arbitrary statement $\psi$ from absurdity, I don't think this way will work (what rule should I apply?):

enter image description here

I have come up with this. Here I have found a way to put $\psi$ as an assumption:

enter image description here

$\endgroup$
  • $\begingroup$ I suspect that in the rule you're quoting, "there are $a$ and $\neg a$" means these two formulas are conclusions, not assumptions. In any case, your statement of this rule isn't clear enough for useful discussion. $\endgroup$ – Andreas Blass Jun 22 '14 at 21:05
3
$\begingroup$

It might be clearer if you look at the rules for negation in their sequent forms on pp. 26/27 of their Mathematical Logic. Two of them, simplified, are

($\neg$E) If $\Gamma\vdash\phi$ and $\Gamma\vdash\neg\phi$ are both correct, then $\Gamma\vdash\bot$ is correct.

(RAA) If $\Gamma\cup\{(\neg\phi)\} \vdash\bot$ is correct, then so is $\Gamma \vdash\phi$

So we have the following argument

$A, \neg A, \neg B \vdash A$ and also $A, \neg A, \neg B \vdash \neg A$ [two applications of the basic property of $\vdash$, the Axiom Rule of p. 8]

$A, \neg A, \neg B \vdash \bot$ [by $\neg$E]

$A, \neg A, \vdash B$ [by RAA]

So that's how the RAA gets used [in C&H's system in its sequent version] to derive any conclusion you like from a contradictory pair.

Now think how this is reflected in the natural deduction version of their system.

$\endgroup$
  • $\begingroup$ Please, check the edit to my question. I gave the simplest derivation that I could think of. $\endgroup$ – Graduate Jun 23 '14 at 11:45
  • 1
    $\begingroup$ Your derivation works. But in fact C&H (if you look very carefully) allow you to discharge "assumptions" that actually appear nowhere, so the bottom three lines of your proof already suffice! $\endgroup$ – Peter Smith Jun 23 '14 at 12:38

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.