I am using a website called Carnap.io for submitting my proofs for natural deduction for TFL. It keeps telling me the proof for the following premise is wrong: ⊤ ⊢ (A ↔ ¬B) → (¬A → B) but I'm not sure why it is wrong. Am I applying the rules incorrectly? My proof is below:

1 A ↔ ¬B :AS

2 A :AS

3 | :~I1,2

4 ~A :~I2,3

5 B :<->E1,4

6 ~A -> B :->I4,5

7 --

8 (A<->~B) -> (~A -> B) :->I1,6

  • Assume ~A and ~B and derive a contradiction with the premise. – Mauro ALLEGRANZA Oct 26 '20 at 7:35

Your Answer

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

Browse other questions tagged or ask your own question.