Lab06 - Intuitionistic propositional logic in Agda

LICENCE: This tutorial contains adaptations of material from Programming Language Foundations in Agda by Phil Wadler and Wen Kokke. It is licensed under Creative Commons Attribution 4.0 International.

SYNTAX: You can enter → by writing \-> and pressing TAB. Similar useful combinations include \lambda, \neg, \top, \bot, \and, \or, \forall, \exists, \Pi, \Sigma, ...

In this lab we will explore intuitionistic propositional logic via the Agda programming language. Agda can be seen as Haskell on steroids with a more powerful type system.

Implication

Intuitionistic implication is implemented as function space inline_formula not implemented. The idea is that a proof of inline_formula not implemented is a (terminating) program inline_formula not implemented that, given a proof inline_formula not implemented of inline_formula not implemented, always terminates and produces a proof inline_formula not implemented of inline_formula not implemented.

For instance, the following Agda program id proves the intuitionistic tautology inline_formula not implemented:

module AgdaLab01 where

id : {A : Set} -> A -> A

id a = a

-- the same with λ-abstraction:

id' id'' : {A : Set} -> A -> A

id' = λ a → a

id'' = \ a -> a -- alternative non-unicode syntax

Compare this with the equivalent Haskell definition:

id :: A → A

id x = x

In Agda we need to explicitly say what A is with the implicit argument {A : Set}. (In Agda, Set means type.) Thus id is a higher order function that takes as (implicit) input a type A, a value of type A, and returns a value also of type A. This shows how already such a simple function uses a dependent type.

The inline_formula not implemented-elimination rule from natural deduction is function application and the inline_formula not implemented-introduction rule is inline_formula not implemented-abstraction:

→-elim : {A B : Set} → (A → B) → A → B

→-elim a→b a = a→b a

SPACING: Agda allows us to be very flexible in the variable names, which can be strings such as x, idλ, a→b, &&true, or even arbitrary unicode symbols 💔, provided there is no space in-between. As a consequence, spaces in Agda have a syntactic meaning as separators, and we need to be very generous with them.

Exercise

Prove in Agda following theorems of intuitionistic propositional logic:

inline_formula not implemented

How many proofs does inline_formula not implemented have?

A1 : {A B : Set} → A → B → A

A1 a b = ?

A2 : {A B C : Set} → (A → B → C) → (A → B) → A → C

A2 a→b→c a→b a = ?

diamond : {A B C D : Set} → (A → B) → (A → C) → (B → C → D) → A → D

diamond = ?

proj : {A : Set} → A → A → A

proj = ?

True and false

The two truth values inline_formula not implemented and inline_formula not implemented are implemented via Agda's data type mechanism. The intuition is that the type inline_formula not implemented has precisely one inhabitant (called tt below) and that inline_formula not implemented has no inhabitants at all.

data ⊤ : Set where

  tt : ⊤

data ⊥ : Set where

The ⊥-elimination rule is implemented via the absurd pattern "()":

⊥-elim : {A : Set} → ⊥ → A

⊥-elim ()

f : {A B : Set} → B → ⊥ → A

f _ absurd = ⊥-elim absurd

Negation

Negation is not a primitive in intuitionistic logic. In intuitionistic logic inline_formula not implemented means that, if we had a proof of inline_formula not implemented, then we could derive a contradiction inline_formula not implemented:

inline_formula not implemented

infix 3 ¬_

¬_ : Set → Set

¬ A = A → ⊥

Note how ¬_ is a type-level function, i.e., a function mapping types to types!

Exercise

Use ⊥-elim to prove inline_formula not implemented:

exfalso : {A B : Set} → ¬ A → A → B

exfalso = ?

Exercise

The logic of Agda is intuitionistic. In particular, in Agda the following double negation law does not hold:

inline_formula not implemented

Which one of the two directions holds in intuitionistic logic?

• Formalise this and prove it in Agda. Recall that ¬ ¬ A = (A → ⊥) → ⊥.

• Does the proof (i.e., program) resemble something we have already seen?

¬¬-elim : {A : Set} → ¬ ¬ A → A

¬¬-elim f = ?

¬¬-intro : {A : Set} → A → ¬ ¬ A

¬¬-intro a f = ?

Exercise

Show that the following triple negation law holds intuitionistically.

triple-negation : {A : Set} → ¬ ¬ ¬ A → ¬ A

triple-negation = ?

Exercise

The contrapositive of an implication inline_formula not implemented is inline_formula not implemented. In classical logic an implication and its contrapositive are logically equivalent, i.e., the following is a tautology:

inline_formula not implemented

Prove which, if any, of the two directions above holds in intuitionistic logic.

contrapositive : ?

contrapositive = ?

Conjunction

According to the BHK interpretation, a proof of inline_formula not implemented is a pair inline_formula not implemented, where inline_formula not implemented is a proof of inline_formula not implemented and inline_formula not implemented is a proof of inline_formula not implemented. This intuition translates immediately into the following product datatype:

infix 2 _∧_ 

-- _∧_ is the cartesian product operator ×

data _∧_ (A : Set) (B : Set) : Set where

  _,_ : A → B → A ∧ B

The datatype _∧_ is parametrised by two types, A and B, and it is written A ∧ B or, using prefix notation, _∧_ A B. It has only one constructor _,_, corresponding to the ∧-introduction rule: Given elements a : A and b : B, a , b has type A ∧ B (notice the mandatory spaces!). The term above can also be written in prefix notation as _,_ A B.

We can then define the two projection functions, which correspond to the two ∧-elimination rules:

fst : {A B : Set} → A ∧ B → A

fst (a , _) = a

snd : {A B : Set} → A ∧ B → B

snd (_ , b) = b

Exercise

Formalise and prove the following:

1. Conjunction is commutative.

1. Curry/uncurry: The formula/type inline_formula not implemented is "the same" as inline_formula not implemented.

∧-commutative : ?

∧-commutative = ?

uncurry : {A B C : Set} → (A → B → C) → A ∧ B → C

uncurry = ?

curry : {A B C : Set} → (A ∧ B → C) → A → B → C

curry = ?

Disjunction

According to the BHK interpretation, a proof of inline_formula not implemented is a pair inline_formula not implemented, where inline_formula not implemented specifies that we are proving inline_formula not implemented and inline_formula not implemented is a proof thereof. Since the first component is finite, disjunction can be implemented with two constructors. Each constructor corresponds to a ∨-introduction rule.

-- we give disjunction lower priority than conjunction

-- so we can omit parenthesis from (A ∧ B) ∨ C and write A ∧ B ∨ C instead.

infix 1 _∨_ 

data _∨_ (A : Set) (B : Set) : Set where

    left : A → A ∨ B

    right : B → A ∨ B

We can do case analysis by pattern matching on the constructor. This corresponds to the ∨-elimination rule:

case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C

case f g (left a) = f a

case f g (right b) = g b

Exercise

In classical logic we have the following law of excluded middle:

inline_formula not implemented

1. Why there is no Agda program of the corresponding type {A : Set} → A ∨ ¬ A?

2. Challenge: Write an Agda program for the irrefutability of the law of excluded middle: inline_formula not implemented

   Hint: Expand the definition of inline_formula not implemented. You will need: left, right, and inline_formula not implemented-abstraction.

-- ¬ ¬ (A ∨ ¬ A) = ((A ∨ (A → ⊥)) → ⊥) → ⊥ 

irrefutability : {A : Set} → ¬ ¬ (A ∨ ¬ A)

irrefutability = ?

Exercise (De Morgan Laws)

Are the following laws valid in intuitionistic logic? If so, write a proof in Agda.

inline_formula not implemented

de_morgan1-1 : {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B

de_morgan1-1 = ?

de_morgan1-2 : {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)

de_morgan1-2 = ?

de_morgan2 : {A B : Set} → ¬ A ∨ ¬ B → ¬ (A ∧ B)

de_morgan2 = ?

de_morgan3 : {A B : Set} → ¬ (A ∧ B) → ¬ A ∨ ¬ B

de_morgan3 f = ?

Exercise

In classical logic, inline_formula not implemented is logically equivalent to inline_formula not implemented. Which of the following two directions hold in intuitionistic logic? Prove it in Agda.

inline_formula not implemented

-- your solution here

Challenges

The following exercises are entirely optional and not mandatory to be completed. Nonetheless, they show that very interesting phenomena happen in intuitionistic logic already at the propositional level.

Weak Peirce's law

We know that Peirce's law is not an intuitionistic tautology. Show that the following related formula is an intuitionistic tautology:

inline_formula not implemented

wp : {A B : Set} → ((((A → B) → A) → A) → B) → B

wp f = ?

Intuitionistically equivalent LEM formulations

In the previous exercises we have seen that the following principles are not intuitionistic tautologies:

1. Law of excluded middle: A∨¬A.

2. Elimination of double negation: ¬¬A→A.

3. Implication as disjunction: (A→B)→¬A∨B.

4. The Negated De Morgan's law: ¬(¬A∧¬B)→A∨B.

5. Peirce's Law: ((A→B)→A)→A.

Show that all principles above are logically equivalent in intuitionistic logic. Each propositional variable A,B is universally quantified in each principle.

Hint: Prove the following sequence of implications:

• 1→2.

• 2→3: Use irrefutability of (A→B)→¬A∨B, proved earlier: ¬¬((A→B)→¬A∨B).

• 3→1.

• 1→4: Use the excluded middle for 𝐴 and for 𝐵.

• 4→1: Use ¬(¬A∧¬B)→A∨B with B≡¬A.

• 1→5.

• 5→1: Use Peirce's law ((A′→B′)→A′)→A′ with A′≡A∨¬A and 𝐵′≡⊥.

1→2 : ?

1→2 = ?

2→3 : ?

2→3 = ?

3→1 : ?

3→1 = ?

1→4 : ?

1→4 = ?

4→1 : ?

4→1 = ?

1→5 : ?

1→5 = ?

5→1 : ?

5→1 = ?