3
$\begingroup$

I'm looking to prove that $(P \leftrightarrow \neg P)$ is a contradiction using a natural deduction proof (which is to say, I want a proof to show $(P\leftrightarrow \neg P)\vdash Q$). In case it helps, the specific system I'm working in is as outlined in Halbach's Logic Manual (tree structure, introduction and elimination rules for each connective; see the link below), but it's the overall structure of the proof I'm struggling with.

Given a proof that shows $\vdash (P \vee \neg P)$ I can transform this into the desired proof, but that generates a very large tree given the simplicity of the sentence, because the proof for $\vdash (P \vee \neg P)$ is fairly long itself.

I can't shake the feeling there must be a more straightforward (even if still indirect) proof, but haven't been able to find it so far.


Edit: As found by lemontree, the ruleset I am using is listed here.

$\endgroup$
4
  • 1
    $\begingroup$ Would you mind recalling the facts about negation ? $\endgroup$
    – FiMePr
    Jun 29 '20 at 15:50
  • 1
    $\begingroup$ It would be useful to link to the rule set you're using, if it exists on the web. Is this it? users.ox.ac.uk/~logicman/jsslides/ll6p.pdf $\endgroup$
    – lemontree
    Jun 29 '20 at 16:05
  • $\begingroup$ @lemontree That's the set; I'll edit that link into the question. $\endgroup$
    – dbmag9
    Jun 29 '20 at 17:23
  • $\begingroup$ @FiMePr The rules for negation are on the 4th page of the PDF now linked. The introduction rule is: Given $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \psi$, you can form a proof that $\Gamma \vdash \neg \phi$ (where $\Gamma$ is a set of sentences and $\phi, \psi$ are sentences). The elimination rule just switches all the $\phi$s for $\neg\phi$s and vice versa. $\endgroup$
    – dbmag9
    Jun 29 '20 at 17:28
2
$\begingroup$

You can prove Lemma 1: $P\to\lnot P\vdash\lnot P$:

  1. $P\to\lnot P$ - assumption
  2. | $P$ - additional assumption
  3. | $\lnot P$ - modus ponens on 1. and 2.
  4. | $\bot$ - elimination of negation from 2. and 3.
  5. $\lnot P$ - introduction of negation on 2-4.

and similarly Lemma 2: $\lnot P\to P\vdash P$. Now:

  1. $P\leftrightarrow\lnot P$ - assumption
  2. $P\to\lnot P$ - elimination of equivalence from 1.
  3. $\lnot P\to P$ - elimination of equivalence from 1.
  4. $P$ - Lemma 2 and 3.
  5. $\lnot P$ - Lemma 1 and 2.
  6. $\bot$ - elimination of negation from 5. and 6.
  7. $Q$ - ex falso quodlibet from 6.
$\endgroup$
1
  • 1
    $\begingroup$ The rules for $\leftrightarrow$ in the source specified by the OP are defined such that from 1. and 4. one obtains 5. directly without the intermediate step 2. (and analogous for the other direction). $\endgroup$
    – lemontree
    Jun 29 '20 at 16:07
2
$\begingroup$

One possible route is proving $\lnot(P \leftrightarrow \lnot P)$ without premises. Following that path, this would be a Gentzen-style proof, I think.

$ \def\be\qquad\mathbf{\leftrightarrow Elim} \def\bi\qquad\mathbf{\leftrightarrow Intro} \def\ne\qquad\mathbf{\neg Elim} \def\ni\qquad\mathbf{\neg Intro} $

$ \begin{equation} \dfrac{ \dfrac{ [P] \qquad [P \leftrightarrow \lnot P] }{ \dfrac{ [P] \qquad \lnot P }{\lnot P}\ni}\be \quad \dfrac{ [\lnot P] \qquad [P \leftrightarrow \lnot P] }{ \dfrac{ [\lnot P] \qquad P }{P}\ne}\be }{\lnot(P \leftrightarrow \lnot P)}\ne \end{equation} $


EDIT:

Based on OP comments, I am adding a proof of $P \leftrightarrow \lnot P \vdash Q\\$.

$ \begin{equation} \dfrac{ \dfrac{ [P] \qquad P \leftrightarrow \lnot P }{ \dfrac{ [P] \qquad \lnot P }{\lnot P}\ni}\be \quad \dfrac{ [\lnot P] \qquad P \leftrightarrow \lnot P }{ \dfrac{ [\lnot P] \qquad P }{P}\ne}\be }{Q}\ne \end{equation} $

$\endgroup$
2
  • 1
    $\begingroup$ Thanks for this; in fact your tree can be adapted into a tree for $(P\leftrightarrow \neg P) \vdash Q$ just by taking the square brackets off the occurences of $(P\leftrightarrow \neg P)$ in the top row, and replacing the final sentence with $Q$ (using $\neg$Elim to 'discharge' an assumption of $\neg Q$ that does not feature in the tree). $\endgroup$
    – dbmag9
    Jun 30 '20 at 13:16
  • 1
    $\begingroup$ You're welcome. Good observation. I'll add it to the answer. $\endgroup$
    – F. Zer
    Jun 30 '20 at 13:46
0
$\begingroup$

(Posted after answer accepted.) Using a form of natural deduction:

enter image description here

enter image description here

$\endgroup$

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.