Prove that and are logically equivalent without truth tables
. . I call it "Alternate Definition of Implication" (ADI).
Start with the right side:
This is fine, but expressing as misses an important subtlety. One can define as where denotes a contradiction (e.g., 0 = 1). Indeed, and imply by Modus Ponens, and deriving from proves by Deduction theorem (or implication introduction).
Then becomes . Now, it is surprising that this formula is implied by without using the fact that is a contradiction. I.e.,
is the transitivity of , and it is derivable for any using only basic rules about implication.
This suggests that implies in a much stronger sense than just in Boolean logic.