… or “the missing Law of Excluded Middle”.
First things first, Law of Excluded Middle or LEM is an axiom of logic that states that either some proposition A
holds or its negation ¬A
holds, there is no third choice. LEM is one of the core tenets of formal reasoning in “classical” branches of mathematics, and for me as a classically trained mathematician this is indeed a very natural way of thinking.
Recently, I got interested in the theory of programming languages. The discipline differs a great deal from functional analysis, probability theory or other familiar branches of mathematics, and learning required starting from the very basics, including proof theory and intuitionistic logic.
Honestly, this all did feel pretty daunting and unproductive given how much effort was required even for simple proofs. So I figured that doing exercises in code instead of pencil & paper should make it more fun.
Ahead are some basic pieces of intuitionistic logic accompanied by snippets of Coq
code.