(Inspired by http://playingwithpointers.com/archives/988)

```
module Logic where
```

## Data types

In Agda, similarly to Coq, we define our universe by specifying types
which are subtypes of the universal type `Set`

and then creating their
inductive constructors. This is similar to Haskell’s GADTs and shares
a similar syntax.

For instance, we can create conjunctive (product) and disjunctive
(coproduct) types. Note that in Agda underscores specify the “mixfix”
syntax, each argument replaces an underscore to form the final
notation.

```
infix 5 _,_
data _∧_ (P Q : Set) : Set where
_,_ : P → Q → P ∧ Q
data _∨_ (P Q : Set) : Set where
injl : P → P ∨ Q
injr : Q → P ∨ Q
```

By pattern matching on the constructors for these pair types we can
create some deconstructor definitions as well. These are useful later
for creating proof objects since they encapsulate the pattern matching
needed to destruct the values of pair types.

```
both : ∀ {P Q R : Set} → P ∨ Q → (P → R) → (Q → R) → R
both (injl x) f g = f x
both (injr x) f g = g x
left : ∀ {P Q : Set} → P ∧ Q → P
left (x , _) = x
right : ∀ {P Q : Set} → P ∧ Q → Q
right (_ , x) = x
```

We also can already prove very simple lemmas such as the symmetry of
the product types. `∨-symmetry`

will be useful later.

```
∧-symmetry : ∀ {P Q : Set} → P ∧ Q → Q ∧ P
∧-symmetry (p , q) = q , p
∨-symmetry : ∀ {P Q : Set} → P ∨ Q → Q ∨ P
∨-symmetry (injl x) = injr x
∨-symmetry (injr x) = injl x
```

## Embedding

Further, we embed constructive logic by denoting the “top” and
“bottom” types in `Set`

, `⊤`

is trivially constructable and thus
always provable and `⊥`

is impossible to construct and thus is
isomorphic to unprovable statements.

```
data ⊤ : Set where tt : ⊤
data ⊥ : Set where
```

Using `⊥`

we can turn a constructable type into an unconstructable
function space and an unconstructable type into a constructable
function space—-logical negation.

```
¬_ : Set → Set
¬ P = P → ⊥
```

Logical negation works as expected, we can construct types of `¬ ⊥`

or
`⊥ → ⊥`

by rejecting the premise. In the definition of `notBot`

the
`()`

represents the assertion that the domain of `notBot`

is empty and
thus `notBot`

is a trivial function.

```
notBot : ⊥ → ⊥
notBot ()
```

We can do this more generally to create any value. `absurd`

is
absurdly useful for creating proofs later as it encapsulates the
assertion of a trivial function space.

```
absurd : ∀ {A : Set} → ⊥ → A
absurd ()
```

## Some helpers

Agda’s core is a typical functional language, so we get some of the
same basic functions and higher order functions one might be used to
from Haskell.

```
id : ∀ {P : Set} → P → P
id p = p
id₁ : ∀ {P : Set₁} → P → P
id₁ p = p
k : ∀ {X N : Set} → X → N → X
k z _ = z
```

These higher order functions are very useful for transfering from a
“pointed” to a “point-free” mental framework, for beginning to think
of wiring functions together categorically instead of as chasing
values. This is invaluable for proofs later.

```
infix 9 _∘_
infixr 0 _$_
_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)
_$_ : ∀ {A B : Set} → (A → B) → (A → B)
f $ x = f x
```

It’s also worth noting that both of these functions have far more
“dependent types” which are sometimes written instead of this basic
types as above. The dependent types are vital in times when type
constraints flow from input values to output types. For what I need
for the rest of this exploration, though, the more dependent types
only serve to obscure the meaning of the functions.

## Classical logic

Constructive logic does not contain proofs for all of the theorems of
classical logic. In particular these five are unprovable.

```
peirce : Set₁
classic : Set₁
excludedMiddle : Set₁
deMorgan : Set₁
impliesToOr : Set₁
peirce = ∀ {P Q : Set} → ((P → Q) → P) → P
classic = ∀ {P : Set} → ¬ (¬ P) → P
excludedMiddle = ∀ {P : Set} → P ∨ ¬ P
deMorgan = ∀ {P Q : Set} → ¬ (¬ P ∧ ¬ Q) → P ∨ Q
impliesToOr = ∀ {P Q : Set} → (P → Q) → (¬ P ∨ Q)
```

More interestingly, the addition of any of these 5 as an axiom
converts constructive logic to classical logic. More formally, we can
say that these five propositions are all isomorphic. Armed with an
isomorphism type

```
data _↔_ : Set₁ → Set₁ → Set₂ where
iso : ∀ {P Q : Set₁} → (P → Q) → (Q → P) → P ↔ Q
```

the remainder of this exploration will be to prove the previously
stated isomorphisms. To do so we’ll use this I will show the following
proofs

```
`P ↔ C ↔ EM ↔ I` and `C ↔ dM`
```

and then by the equivalence of `↔`

they will all be isomorphic.

```
reflexive↔ : ∀ {P : Set₁} → P ↔ P
reflexive↔ = iso id₁ id₁
symmetric↔ : ∀ {P Q : Set₁} → P ↔ Q → Q ↔ P
symmetric↔ (iso ⟶ ⟵) = iso ⟵ ⟶
transitive↔ : ∀ {P Q R : Set₁} → (P ↔ Q) → (Q ↔ R) → P ↔ R
transitive↔ (iso p→q p←q) (iso q→r q←r) =
iso (λ p → q→r (p→q p)) (λ r → p←q (q←r r))
```

`peirce`

is isomorphic to `classic`

```
module peirce↔classic where
private
⟶ : peirce → classic
⟶ pc {P} cl = { }0
```

For the context of hole 0 here we need to solve this goal

```
Goal: P
————————————
cl : (P → ⊥) → ⊥
P : Set
pc : {P₁ Q : Set} → ((P₁ → Q) → P₁) → P₁
```

To create a `P`

we have two routes, we could use
`absurd ∘ cl : (P → ⊥) → P`

but since that almost immediately
throws away our double
negative `cl`

, we’ll focus instead on `pc {P} {⊥} : ((P → ⊥) → P) → P`

.
In order to get a `P`

from that we simply need to product a
function type `((P → ⊥) → P)`

… but we already did that earlier while
examining `absurd ∘ cl`

, so the final proof is

```
⟶ pc cl = pc $ λ negp → absurd $ cl negp
```

To go the other direction

```
⟵ : classic → peirce
⟵ cl {P} {Q} pc = { }0
```

we have the goal

```
Goal: P
——————————————————————————
pc : (P → Q) → P
Q : Set
P : Set
cl : {P₁ : Set} → ((P₁ → ⊥) → ⊥) → P₁
```

it’s very tempting to use `pc`

, but to do that we need to find a
universal coercion function `P → Q`

… that seems very hard without
any readily available contradictions, so we’ll go by the route of
`cl {P} : ((P → ⊥) → ⊥) → P`

.

```
⟵ cl {P} {Q} pc = cl {P} $ { }0
```

Now our goal boils down to producing a `¬ (¬ P)`

from `pc`

. We have
the raw materials—-a `¬ P = P → ⊥`

can be transformed into `P → Q`

using `absurd`

, but we need to carefully interweave `pc`

and
`¬ (¬ P)`

. We use a λ abstraction to get access to the first `¬ P`

then use it to create `P → Q`

, which then is fed to `pc`

to get our
originally needed `P`

.

```
⟵ cl pc = cl $ λ f → f $ pc $ λ p → absurd $ f p
```

And then we just wrap up the two implications into an `iso`

.

```
peirce↔classic : peirce ↔ classic
peirce↔classic = iso ⟶ ⟵
```

Unmentioned above is that Agsy, Agda’s builtin proof search tool, is
capable of automatically finding the “only if” implication `⟵`

. While
it’s illustrative to work through the function weaving by hand, the
proof can be immediately generated in Emacs by placing the cursor in
the goal, typing the `-m`

flag and hitting “C-c C-a”.

Many of the following proofs can be found by Agsy, which suggests that
logical tautologies are often searchable (consider Coq’s `tauto`

tactic). For many of them we have to include the global environment
with the `-m`

flag otherwise Agsy gets caught on pattern
matching. This is the reason we defined the destructors above. The
implications which cannot be found by Agsy (within 5 seconds anyway)
are marked with a `*`

.

```
module classic↔demorgan where
private
⟶ : classic → deMorgan
⟶ cl {P} {Q} dm = { }0
```

to which we have the goal

```
Goal: P ∨ Q
——————————————————————————
dm : (P → ⊥) ∧ (Q → ⊥) → ⊥
Q : Set
P : Set
cl : {P₁ : Set} → ((P₁ → ⊥) → ⊥) → P₁
```

The primary trick for this implication is that the classical logicical
implication `¬ (¬ P) → P`

can be instantiated with *any*
`P₁`

… including something like `P ∨ Q`

, the goal proposition. Once
this is applied as `cl {P ∨ Q} : ((P ∨ Q → ⊥) → ⊥) → P ∨ Q`

we
generate the needed negation by packaging the negations into a pair
and passing it to `dm`

as

```
λ notporq → dm (notporq ∘ injl , notporq ∘ injr) : (P ∨ Q → ⊥) → ⊥
```

where the `injl`

constructor is used to change
`notporq : (P → ⊥) ∧ (Q → ⊥) → ⊥`

into
`notporq ∘ injl : (P → ⊥) → ⊥`

.

```
⟶ cl dm = cl $ λ notporq → dm (notporq ∘ injl , notporq ∘ injr)
```

Then we build

```
⟵* : deMorgan → classic
⟵* dm {P} cl = { }0
```

giving us the goal

```
Goal: P
——————————————————————————————————————
cl : (P → ⊥) → ⊥
P : Set
dm : {P₁ Q : Set} → ((P₁ → ⊥) ∧ (Q → ⊥) → ⊥) → P₁ ∨ Q
```
```

The “only if” implication cleverly destructs
`dm {P} {P} : ((P → ⊥) ∧ (P → ⊥) → ⊥) → P ∨ P`

using `both`

as

```
⟵* dm {P} cl = both (dm {P} {P} { }0) id id
```

The goal type remaining is of type `((P₁ → ⊥) ∧ (Q → ⊥) → ⊥)`

which
can be trivially constructed by composing an injection into a
disjuctive pair with our double negative `cl`

as `cl ∘ left`

```
⟵* dm cl = both (dm $ cl ∘ left) id id
classic↔demorgan : classic ↔ deMorgan
classic↔demorgan = iso ⟶ ⟵*
module classic↔excludedMiddle where
private
⟶ : classic → excludedMiddle
⟶ cl {P} = { }0
```

with goal

```
Goal: P ∨ (P → ⊥)
——————————————————————————
P : Set
cl : {P₁ : Set} → ((P₁ → ⊥) → ⊥) → P₁
```

The intuition for this goal is similar to the forward implication
`classic → deMorgan`

, we want to pass our entire goal type in as `P₁`

above and then produce the needed double negative.

```
cl {P} = cl {P ∨ (P → ⊥)} $ { }0
```

From here we simply need to construct our double negative or, create
`⊥`

from `notContra : P ∨ (P → ⊥) → ⊥`

. This is a fairly evident
tautology, which we can resolve by noting that
`injr $ notContra . injl : ∀ {W : Set} → W ∨ (P → ⊥)`

which is the argument to `notContra`

itself and so we are done.

```
⟶ cl = cl $ λ notContra → notContra $ injr $ notContra ∘ injl
⟵* : excludedMiddle → classic
⟵ em {P} cl = { }0
```

with goal

```
Goal: P
—————————————————————
cl : (P → ⊥) → ⊥
P : Set
em : {P₁ : Set} → P₁ ∨ (P₁ → ⊥)
```

The “only if” implication is almost painfully trivial as the left side
of `em {P}`

is the goal and the right side can be combined immediately
with `cl`

to get a contradiction. We deconstruct `em`

with `both`

and
complete the proof presently.

```
⟵* em cl = both em id (absurd ∘ cl)
classic↔excludedMiddle : classic ↔ excludedMiddle
classic↔excludedMiddle = iso ⟶ ⟵*
module excludedMiddle↔impliesToOr where
private
⟶ : excludedMiddle → impliesToOr
⟶ em {P} {Q} or2or = { }0
```

with the goal

```
Goal: (P → ⊥) ∨ Q
———————————————————————
or2or : P → Q
Q : Set
P : Set
em : {P₁ : Set} → P₁ ∨ (P₁ → ⊥)
```

This implication is basically trivial as well, using `both (em {P})`

to derive a component of the disjunctive goal from both `P`

(via
`or2or : P → Q`

) and `¬ P`

directly.

```
⟶ em or2or = both em (injr ∘ or2or) injl
```

Then we build

```
⟵ : impliesToOr → excludedMiddle
⟵ or2or {P} = { }0
```

with the goal

```
Goal: P ∨ (P → ⊥)
————————————————————————————————
P : Set
or2or : {P₁ Q : Set} → (P₁ → Q) → (P₁ → ⊥) ∨ Q
```

This proof is trivial to construct as well since we have

or2or {P} {P} id : ¬ P ∨ P

immediately so we simply apply the `∨-symmetry`

lemma proved
before massage it to the required form.

```
⟵ or2or = ∨-symmetry $ or2or id
excludedMiddle↔impliesToOr : excludedMiddle ↔ impliesToOr
excludedMiddle↔impliesToOr = iso ⟶ ⟵
open peirce↔classic
open classic↔demorgan
open classic↔excludedMiddle
open excludedMiddle↔impliesToOr
```