Hey Juan!

Actually, I got side tracked with thinking about something you asked in another thread.

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) (.)

We have enough to start with the *Classical Logic Theorem Monad*

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:

& \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

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...