Content-Type: text/shitpost

Even after all these years, the implicational fragment of logic still has the ability to surprise me. Today I was surprised to observe that:

$$((a\to b)\to a) \to (a\to b) \to b$$

is a theorem of logic. It was no longer surprising after I thought about it: if !!a\to b!! implies !!a!!, then it also implies formula that is implied by !!a!!, but !!a\to b!! itself shows that !!b!! is one of those formulas.

(As a term of combinatory logic, this is simply !!S I!!, so I wonder how I never noticed before.)