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

Question

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.

Answer 1

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

Answer 2

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.

Answer 3

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