Need help to Proof ~(A->B) :- A ^ ~B

I was following William Rose proof from 1 to 33. but I am stuck on this.


1 Answer 1


I was too tired, and I was actually at line 10 without aware of the contradiction of line 10.

enter image description here

  • 1
    Your answer is the correct version with the right sequence of assumptions, though it should be noted since you invoked double negation in your last step so this proof/conclusion only works in classic not intuitionistic logic... Feb 23, 2022 at 4:32
  • Thank Double Knot. Unfortunately, I only taught Fitch style. May I ask how should the proof go in intuitionistic logic?
    – Keith Lam
    Feb 23, 2022 at 5:44
  • Intuitionistic logic is more conservative (weaker) than common classic logic and extensively used in contemporary constructive mathematics, internal logic of topos in categorical logic, type theory, automated theorem prover, and computer science, etc, and it has nothing to do with Fitch style which is a popular style of natural deduction calculus system of many logics, including classic, intuitionistic and modal logics, there's also Gentzen tree style. In IL, you just remain at line 11... Feb 23, 2022 at 5:51

Not the answer you're looking for? Browse other questions tagged .