Natural deduction proof that $(P\leftrightarrow \neg P)$ is a contradiction, without first deriving $(P\vee \neg P)$

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.

• Would you mind recalling the facts about negation ? Jun 29 '20 at 15:50
• 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 Jun 29 '20 at 16:05
• @lemontree That's the set; I'll edit that link into the question. Jun 29 '20 at 17:23
• @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. Jun 29 '20 at 17:28

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}$$

$$$$\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$$$$

EDIT:

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

$$$$\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$$$$

• 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). Jun 30 '20 at 13:16
• You're welcome. Good observation. I'll add it to the answer. Jun 30 '20 at 13:46

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.
• 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). Jun 29 '20 at 16:07

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