0

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?

2

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.

enter image description here

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 at 1:27
2

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.