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:

>

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.

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:

I also like to use the unboxed version of contraposition:

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

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

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:

Here's the applicative instance:

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.

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 `(<*>)`:

We can then use it and the intuitionistic identity \\(\neg \neg \neg \phi \to \neg \phi\\) to prove the final axiom:

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

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:

$$

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