Content-Type: text/shitpost


Subject: The implicational fragment of logic
Path: you​!your-host​!walldrug​!epicac​!ihnp4​!hal9000​!plovergw​!plover​!shitpost​!mjd
Date: 2018-08-27T19:18:50
Newsgroup: alt.binaries.implicational-fragment
Message-ID: <3c14f4b8728f9d4b@shitpost.plover.com>
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.)