Propositional Logic Theorem Proof Help: (¬(P↔Q)↔(P↔¬Q))

Can anyone help me prove this theorem via natural deduction for my class?

$$(¬(P↔Q)↔(P↔¬Q))$$

I can solve one side of the biconditional quite easily using conditional derivation, but have no idea how to solve the other way. Below is my proof for one direction of the biconditional.

I am not allowed to use any other theorems in my proof (De Morgan's Laws etc.) The only tools we are allowed to use are: modus ponens, modus tollens, disjunctive syllogism, addition, adjunction, conditional derivation, indirect derivation/reductio, bicondition, reiterate/repeat.

The language used is from DeLancey's "A Concise Introduction to Logic": https://milnepublishing.geneseo.edu/concise-introduction-to-logic/front-matter/about-the-textbook/

Any geniuses who want to give this a crack?

• I think this question should be reopened. The answers in that similar post don't use natural deduction, which is the formalism required here. Apr 20 at 9:23

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\iff{\leftrightarrow}$$ You wish to derive $$~\neg(P\iff Q)\vdash P\iff\neg Q~$$.
$$\qquad\fitch{\neg(P\iff Q)}{\fitch{P}{\fitch{Q}{~\vdots\\P\iff Q\\\neg(P\iff Q)}\\\neg Q}\\\fitch{\neg Q}{\fitch{\lnot P}{~\vdots\\P\iff Q\\\neg(P\iff Q)}\\P}\\P\iff\neg Q}$$
• Ah. In many natural deduction systems, $\bot$ is the symbol for contradiction (also called 'bottom', 'falsity' or similar names). It looks like your system just uses two contradictory statements, so just reiterate the assumed $\lnot(P\leftrightarrow Q)$ at that point. Apr 20 at 9:02
• $\vdash$ is the symbol for "syntactic entailment". $\phi,\ldots,\psi\vdash \chi$ says, "from the list of assumptions , $\phi,\ldots,\psi$, you can derive $\chi$". Apr 20 at 9:11
• $~\vdots~$ is a vertical ellipsis; just indicating missing derivation for you to complete on your own. This is merely a skeleton of a proof to get you started. @milfordcubicle2 Apr 20 at 9:12