Timeline for How to prove ¬(p→q) ⊢ p &¬q
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 28, 2018 at 17:58 | vote | accept | Diego Ruiz Haro | ||
| Aug 13, 2018 at 15:51 | comment | added | Dan Christensen | I see. I wasn't familiar with your notation. Makes sense now. Thanks. | |
| Aug 13, 2018 at 15:25 | comment | added | Frank Hubeny | @DanChristensen Line 2 is an assumption starting a subproof. I will have to discharge that assumption (end the subproof) before I finish. That subproof ends with a contradiction on line 9 which allows me to discharge the assumption (close the subproof) with an indirect proof (IP). That step on line 10 is also the desired conclusion and so the proof completes. Line 2 is not coming from a definition of the conditional statement in line 1, but from negating the conclusion. | |
| Aug 13, 2018 at 15:15 | comment | added | Dan Christensen | Line 2 assumes a definition for --> that wasn't in the OP's list of rules. | |
| Aug 3, 2018 at 8:37 | comment | added | Frank Hubeny | @MauroALLEGRANZA Thank you. I don't think this particular proof checker's rules will allow me to proceed in that manner, but I can see that the result is the same. | |
| Aug 3, 2018 at 8:25 | comment | added | Mauro ALLEGRANZA | Tomassi's system has no ⊥ symbol and thus neither (⊥I) rule. But your proof is easily "adapted" to the system. Replace step 6 with (∧I) to get ¬(P∧¬Q) ∧ (P∧¬Q) and then use RAA to get ¬¬Q from 4 and 6. Then derive Q with DNE (Double Negation Elim). The same for steps 9-10. In this way, the total number of steps are 12, as required by the OP. | |
| Aug 2, 2018 at 21:39 | history | answered | Frank Hubeny | CC BY-SA 4.0 |