# Given premise ~(P↔Q) how can one derive (~P↔Q) using Fitch?

Given premise ~(P↔Q) derive (~P↔Q) using Fitch-style natural deduction. I thought of simplifying the premise but I am still not able to find an answer. Can someone please help me?

• – virmaior Jul 22 '19 at 5:09
• @virmaior I wasn't able to construct a natural deduction proof using the link you mentioned, but I did provide an alternate answer there using the technique I used below: math.stackexchange.com/a/3300974/312852 The questions are similar but the one on Math SE is looking for an equivalence proof. – Frank Hubeny Jul 22 '19 at 23:02

One way to approach this is to think of the goal, ¬P ↔ Q, not as a biconditional but as this conjunction of disjunctions: (P ∨ Q) ∧ (¬P ∨ ¬Q). This will allow one to access more inference rules. Then the first step would be to assume the negation of that to derive a contradiction with the premise. (See lines 2-27 below.) Once this contradiction is obtained one can derive the desired biconditional.

Here is how this looks in the forallx proof checker. The proof checker you are using may look different but a similar approach should work. Details of the inference rules and the proof checker are linked below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

• I'm pretty sure Fitch does not have DeMorgan's rule. Without which it's going to be brutal to slog through this. – virmaior Jul 23 '19 at 1:27

Here's a skeleton to start you out

`````` |_ ~(P ↔ Q)       Premise
|  |_ P           Assume
|  |  |_ Q        Assume
|  |  |  |_ P     Assume
|  |  |  |  Q     Reit
|  |  |  P → Q    Cond. Intro.
|  |  |  |_ ...   Assume
|  |  |  |  ...   ...
|  |  |  ...      ...
|  |  |  ...      ...
|  |  |  ┴        Neg. Elim.
|  |  ~Q          Neg. Intro
|  P → ~Q         Cond. Intro.
|  |_ ~Q          Assume
|  |  |_ ~P       Assume
|  |  |  |_ ...   Assume
|  |  |  |  ┴     Neg.Elim.
|  |  |  |  ...   Ex Falso Quodlibet
|  |  |  ...      ...
|  |  |  |_ ...   ...
|  |  |  |  ...   ...
|  |  |  |  ...   ...
|  |  |  ...      ...
|  |  |  ...      ...
|  |  |  ┴        Neg. Elim.
|  |  ~~P         Neg. Intro.
|  |  P           Double Neg. Elim.
|  ~Q → P         Cond. Intro.
|  P ↔ ~Q         Bicond. Intro.
``````