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?
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.
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
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.