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?
-
1See math.stackexchange.com/questions/2301286/…– virmaiorJul 22, 2019 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 HubenyJul 22, 2019 at 23:02
Add a comment
|
2 Answers
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
answered Jul 22, 2019 at 19:46
-
I'm pretty sure Fitch does not have DeMorgan's rule. Without which it's going to be brutal to slog through this.– virmaiorJul 23, 2019 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.
