Hey Juan!

I wanted to share because I'm sort of proud of this wackiness, but I'll get back to working through Conal's paper soon!

----------------------------------------

In [Lecture 9 - Chapter 1: Adjoints and the Logic of Subsets](https://forum.azimuthproject.org/discussion/comment/16866/#Comment_16866)

> @Matthew, I don't know if I have understood exactly what you meant with _|_, but my answer is this:
>

type Bottom = forall t. t

hilbertExplosion :: Bottom -> a
hilbertExplosion bottom = id bottom


Oh, _|_ is just me trying to be cute and represent \$$\bot\$$. The symbol \$$\bot\$$ denotes \$$\bigvee\\{\\}\$$ or "the [minimal element](https://en.wikipedia.org/wiki/Maximal_and_minimal_elements) in a preorder".

> Why is it called hilbertExplosion?

David Hilbert derived this rule in his essay [The Foundations of Mathematics (1927)](https://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm). It is the first consequence he gives after stating his 12 axioms.

Philosophers also call this rule *ex falso (sequiter) quadlibet* in Latin and *The Principle Of Pseudo-Scotus*.

Now that we have Bottom (I prefer Falsum so I will use that), we can plug it into John's definition of negation, and combine it with [Glivenko's Theorem](https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog).

This gives us a *monad* in Haskell which re-purposes Haskell's type checker as a simple proof checker for classical logic!

I will be following Hilbert's formalism for logic.

Haskell lacks [*impredicative polymorphism*](https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism) sadly. This means if we want to do anything fancy with the type system we have to box stuff all over the place.


{-# LANGUAGE Rank2Types #-}

module Classical where

newtype Falsum = Falsum { efq :: forall a . a } -- efq stands for *ex falso quodlibet*

-- John Baez's definition of negation
newtype Not a = Not { unNot :: a -> Falsum }


The first thing to note is that John's negation gives rise to a *contravariant* functor, which is a functor with a rule contramap :: (a -> b) -> f b -> f a. This map has an old name in logic - [contraposition](https://en.wikipedia.org/wiki/Contraposition)

$$\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$$

Here's how we construct it:


contraposition :: (a -> b) -> Not b -> Not a
contraposition = (flip . curry . (Not .) . uncurry . ((.) .)) unNot


I also like to use the unboxed version of contraposition:


contraposition' :: (a -> b) -> (b -> Falsum) -> a -> Falsum
contraposition' = (flip . curry . uncurry) (.)



newtype Classical a = Thm { getProof :: Not (Not a) }


The first thing to show is that this is a *functor*. Here is the instance:


instance Functor Classical where
fmap = ( flip
. curry
. (Thm .)
. uncurry
. (flip (contraposition . contraposition) .)
) getProof


Next, we want to show it is an *Applicative*. The pure operation reflects that intuitionistic logic (captured by the Identity functor in Haskell, as per the celebrated [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)) is a sublogic of classical logic.

Apply <*> for this monad reflects the rule philosophers traditionally call *modus ponens*:

$$\vdash \phi \to \psi \Longrightarrow\; \vdash \phi \Longrightarrow \; \vdash \psi$$

My instance uses the unboxed definitions for Classical, which are given by:


toDoubleNeg :: Classical a -> (a -> Falsum) -> Falsum
toDoubleNeg = flip (flip (unNot . getProof) . Not)

fromDoubleNeg :: ((a -> Falsum) -> Falsum) -> Classical a
fromDoubleNeg = Thm . Not . contraposition' unNot


Here's the applicative instance:


instance Applicative Classical where
pure  = Thm . Not . flip unNot
(<*>) = ( curry
. (fromDoubleNeg .)
. uncurry
. (. toDoubleNeg)
. flip
. (. toDoubleNeg)
. (contraposition' .)
. flip
. (contraposition' .)
. flip
) contraposition'


Along with *modus ponens*, classical logic has several axioms. The axiomatization varies amongst logicians, but one system commonly used is:

$$\begin{eqnarray} & \vdash \phi \to \psi \to \phi & \\\\ & \vdash (\phi \to \psi \to \chi) \to (\phi \to \psi) \to \phi \to \chi & \\\\ & \vdash \neg \neg \phi \to \phi \end{eqnarray}$$

And we can indeed construct and check proofs for all three axioms.

The first two correspond to the [**K** and **S** combinators](https://en.wikipedia.org/wiki/SKI_combinator_calculus), which are pure and <*> for the (->) e functor. See Conor McBride's [*Idioms: applicative programming with effects* (2009)](http://www.staff.city.ac.uk/~ross/papers/Applicative.html) for a discussion of this.


ax1 :: Classical (a -> b -> a)
ax1 = pure const  -- or ax1 = pure const

ax2 :: Classical ((a -> b -> c) -> (a -> b) -> a -> c)
ax2 = pure (<*>) -- or ax2 = pure (\f x -> f x x)


Finally, what's left is to show \$$\vdash \neg\neg \phi \to \phi\$$. I like to follow Dirk van Dalen's presentation on page 159 of [Logic and Structure (2013)](https://www.researchgate.net/file.PostFileLoader.html?id=5518f022d5a3f25c318b4611&assetKey=AS%3A273746110156809%401442277566498).

First, we can write unApply, which is the inverse of (<*>):


unApply :: (Classical a -> Classical b) -> Classical (a -> b)
unApply = ( fromDoubleNeg
. ((<*>) (<*>) ((<*>) pure))
. ( curry
. flip
) ( ( flip
. uncurry
. flip
. (flip ($) .) ) (. (efq .)) . (. pure) ) ) . (toDoubleNeg .) . (. fromDoubleNeg)  We can then use it and the intuitionistic identity \$$\neg \neg \neg \phi \to \neg \phi\$$ to prove the final axiom:  ax3 :: Classical ((Not (Not a)) -> a) ax3 = (. (toDoubleNeg . Thm)) <$> unApply ( fromDoubleNeg
. flip ((flip (\$)) . toDoubleNeg . pure)
. toDoubleNeg)


All that's left to show is that this is Monad. This isn't super hard, but I'll leave it as an exercise for anyone reading who wants to try...