jspha (An exploration of constructive and classical logics in Agda)

6 months ago

An exploration of constructive and classical logics in Agda

(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