People keep getting hung up on material implication but it can not understand why. It's more than an encoding hack--falsity (i.e. the atomic logical statement equivalent to 0=1) indicates that a particular case is unreachable and falsity elimination (aka "from falsity follows everything") expresses that you have reached such a case as part of the case distinctions happening in every proof.

Or more poetically, "if my grandmother had wheels she would have been a bike[1]" is a folk wisdom precisely because it makes so much sense.

1: https://www.youtube.com/watch?v=A-RfHC91Ewc

Material implication was not the default implication historically; it came as a useful hack by people who hoped that by enforcing it they could formalize the whole math and knowledge and have a sort of a "single source of truth" for any statement, and evaluate all statements purely syntactically. This proved to be futile as incompleteness theorem showed, and which material implication directly enabled by allowing self-referential non-sense as valid statements. There were many attempts to reconcile this with different logics but they all ended up weaker and unable to formalize all statements. We are now entering the next phase of this attempt, by using hugely complex reasoning function approximators as our "single source of truth" in the form of AI/LLMs.

I used to do a lot of proofs coming all the way from Peano arithmetics, successor operators and first-order tableaux method.