4
$\begingroup$

On this and this pages, there are proofs presented for this rule, but what confuses me though is that I think we actually need to show that $\bot\vdash Q$ holds, not $(P\wedge\neg P)\vdash Q$ or $\vdash(P\wedge\neg P)\rightarrow Q$. I know that $P\wedge\neg P$ is an obvious contradiction and in the natural deduction system I have seen you introduce a $\bot$ from $P$ and $\neg P$ on two separate lines, but still I don't think this necessarily means that $\bot$ is equivalent to $P\wedge\neg P$!

$\endgroup$
  • 1
    $\begingroup$ In Natural Deduction we have two basic possibilities: (i) $\bot$ as primitive, with the rule $\bot \vdash \varphi$ and $\lnot$ defiend. In this case, the intro- and elimination-rules for $\lnot$ are derived from those for $\to$ using the abbreviation: $\lnot P := P \to \bot$. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '17 at 11:44
  • 1
    $\begingroup$ (ii) $\lnot$ as primitive with the "usual" intro- and elimination-rules. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '17 at 11:45
  • $\begingroup$ @MauroALLEGRANZA So I guess in first case you don't need to derive this rule you just take it for accepted, and in the second one you don't even use $\bot$ symbol instead you use something like $P\wedge\neg P$ and those proofs are for this second case? $\endgroup$ – Pooria Sep 25 '17 at 12:22
  • 1
    $\begingroup$ Correct; in the second case, the Ex falso "axiom" will be like: $\lnot A \to (A \to B)$. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '17 at 19:03

Your Answer

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

Browse other questions tagged or ask your own question.