Leftovers

• The logic described here is intuitionistic logic (“IL”)

• It is weaker than classical logic (“CL”)

• For example, it does not prove

p ∨ ¬p

• (It does prove ¬¬(p ∨ ¬p))

• Another theorem of classical logic that it doesn't prove is:

((p → q) → p) → p

• If you add this to IL as an axiom, IL proves everything that CL does

• This is the type of call/cc!

• If you add to Haskell a call/cc function, it becomes a classical logic

• You can then construct a value of type p ∨ ¬p