The puzzle asks us to prove (A->B)->False |- A & (B->False).
My solution is to split via TND on A & (B -> False) and deal with the non-obvious branch (on the bottom) by deducing A->B and applying it to the only axiom we have. The unusual trick is even though there is A & (B -> False) in the middle of the scheme, it's only used to deduce False so we can feed it into the blocks after. That way both A -> False and B cases are handled in the same branch.
My previous solution had 15 blocks and it split on A first, then on B, which resulted in a very simply A & (B -> False) in the middle, but almost identical branches on the sides. So I decided to merge them together.
The puzzle asks us to prove
(A->B)->False |- A & (B->False).My solution is to split via TND on
A & (B -> False)and deal with the non-obvious branch (on the bottom) by deducingA->Band applying it to the only axiom we have. The unusual trick is even though there isA & (B -> False)in the middle of the scheme, it's only used to deduceFalseso we can feed it into the blocks after. That way bothA -> FalseandBcases are handled in the same branch.My previous solution had 15 blocks and it split on
Afirst, then onB, which resulted in a very simplyA & (B -> False)in the middle, but almost identical branches on the sides. So I decided to merge them together.