Lab07 - Intuitionistic first-order 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 first-order logic via the Agda programming language. We reproduce without further comment the basic definitions for propositional logic.

module AgdaLab02 where

infixr 2 _∧_

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

  _,_ : A → B → A ∧ B

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

fst (a , _) = a

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

snd (_ , b) = b

infixr 1 _∨_ 

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

    left : A → A ∨ B

    right : B → A ∨ B

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

case f g (left x) = f x

case f g (right x) = g x

data ⊤ : Set where

  tt : ⊤

A→⊤ : {A : Set} → A → ⊤

A→⊤ _ = tt

data ⊥ : Set where

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

⊥-elim ()

infix 3 ¬_ 

¬_ : Set → Set

¬ A = A → ⊥

Dependent types in Agda

So far we have only seen (polymorphic) simple types, such as A → B for (A B : Set). There are situations where one wants to impose some additional property on the output B which depends on the particular input a : A. In order to achieve this, the output B is generalised to have type A → Set (instead of just Set). One obtains dependent function space

(a : A) → B a

Notice how the type expression B a now contains the term a, i.e., the type B a : Set depends on a. The type of B is A -> Set

Our main application and source of examples of dependent types is to model intuitionistic first-order logic.

Intuitionistic first-order logic

We show how dependent types can be used to implement universal quantification (dependent function space) and existential quantification (dependent product).

The universal quantifier ∀

In intuitionistic logic a proof of inline_formula not implemented is a function inline_formula not implemented mapping a proof inline_formula not implemented of inline_formula not implemented into a proof inline_formula not implemented of inline_formula not implemented, where we can see inline_formula not implemented as a family of types indexed by proofs of inline_formula not implemented. The universal quantifier is implemented via the dependent function space

Π : (A : Set) → (B : A → Set) → Set

Π A B = (a : A) → B a

(Note how Π is a type-level function, i.e., it maps types to types.)

The type ((a : A) → B a) generalises implication A → B, which corresponds to non-dependent function space. In this sense, in intuitionistic logic implication is a special case of universal quantification.

(Universal quantification also generalises conjunction, since the type inline_formula not implemented is isomorphic to inline_formula not implemented where inline_formula not implemented and inline_formula not implemented. For this reason, sometimes Π is called dependent product, hence the notation. However, for us dependent product is something else and it will be used below to model existential quantification.)

-- the type of the first argument of Π can be inferred from the second,

-- so we can make it implicit and save typing

Π' : {A : Set} → (B : A → Set) → Set

Π' {A} B = Π A B

-- we introduce a convenient syntax reminiscent of universal quantification in logic

infix 0 Π'

syntax Π' (λ x → B) = ∀[ x ] B

-- Π {A} (λ x → B)

-- thanks to the declaration above,

-- "∀[ x ] B" is the same as "Π' (λ x → B)"

-- dependent apply; corresponds to ∀-elimination

apply : {A : Set} → {B : A → Set} → Π A B → (a : A) → B a

apply f x = f x

-- apply is just the identity at type Π A B

Exercise (∀)

1. Show that the universal quantifier commutes with itself: inline_formula not implemented.

2. Show that one can diagonalise a universal relation: inline_formula not implemented.

-- recall that "∀[ a ] ∀[ b ] P a b" is the same as

-- "Π A (λ a → Π B (λ b → P a b))", which in turn just means

-- "(a : A) → (b : A) → P a b"

∀-comm :

  {A B : Set} {P : A → B → Set} →

  ∀[ a ] ∀[ b ] P a b →

  -------------------------------

  ∀[ b ] ∀[ a ] P a b

∀-comm f b a = ?

∀-diag :

  {A : Set} {P : A → A → Set} →

  ∀[ a ] ∀[ b ] P a b →

  ------------------------------

  ∀[ a ] P a a

∀-diag f a = ?

Exercise (∀ and →)

Show that the universal quantifier distributes over implication: inline_formula not implemented.

-- recall that "∀[ a ] P a" is the same as

-- "Π A (λ a → P a)", which in turn just means

-- "(a : A) → P a"

∀→-distr :

  {A : Set} {P Q : A → Set} →

  ∀[ a ] (P a → Q a) →

  ∀[ a ] P a →

  ---------------------------

  ∀[ a ] Q a

∀→-distr = ?

Exercise (∀ and ∧)

Prove the following intuitionistic tautologies.

1. inline_formula not implemented.

2. inline_formula not implemented.

-- 1.

∀∧-distr :

  {A : Set} {B C : A → Set} →

  ∀[ a ] B a ∧ C a →

  ----------------------------

  (∀[ a ] B a) ∧ (∀[ a ] C a)

∀∧-distr = ?

{-

The notation "∀[ a ] B a" is just syntactic sugaring for "Π A (λ a → B a)"

(where A is inferred automatically from the type of B),

which in turn is defined to be "(a : A) → (λ a → B a) a",

i.e., "(a : A) → B a".

Using "∀[ a ] B a" instead of "(a : A) → B a" makes the syntax closer to logic.

-}

-- 2.

∧∀-distr :

  {A : Set} {B C : A → Set} →

  (∀[ a ] B a) ∧ (∀[ a ] C a) →

  -----------------------------

  ∀[ a ] B a ∧ C a

∧∀-distr = ?

Exercise (∀ and ∨)

Which of the following are intuitionistic tautologies? Which are classic tautologies? Which are neither? Prove the intuitionistic ones.

1. inline_formula not implemented.

2. inline_formula not implemented, where inline_formula not implemented does not occur in inline_formula not implemented.

3. inline_formula not implemented.

Hint: If you cannot easily program a solution, then most likely there is no solution.

-- 1.

∀∨-distr :

  {A : Set} {B C : A → Set} →

  ∀[ a ] B a ∨ C a →

  ----------------------------

  (∀[ a ] B a) ∨ (∀[ a ] C a)

∀∨-distr = ?

-- 2.

∀∨-distr' :

  {A C : Set} {B : A → Set} →

  ∀[ a ] (B a ∨ C) →

  ---------------------------

  (∀[ a ] B a) ∨ C

∀∨-distr' f = ?

-- ∀∨-distr' would hold if A is a finite set A = {a1, ..., an}

-- f a1? : Ba1

-- f a2? : Ba2

-- ...

-- f an? : Ban

-- --> ∀[ a ] B a

-- 3.

∨∀-distr :

  {A : Set} {B C : A → Set} →

  (∀[ a ] B a) ∨ (∀[ a ] C a) →

  -----------------------------

  ∀[ a ] B a ∨ C a

∨∀-distr = ?

Exercise (∀ and ¬)

The double negation shift (DNS) is the following classical tautology: inline_formula not implemented. While DNS does not hold intuitionistically, prove that its converse does.

-- converse double negation shift

cdns :

  {A : Set} {P : A -> Set} →

  ¬ ¬ (∀[ a ] P a) →

  --------------------------

  ∀[ a ] ¬ ¬ P a

cdns = ?

The existential quantifier ∃

In intuitionistic logic, 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. Like in universal quantification, we can see inline_formula not implemented as a family of types indexed by proofs of inline_formula not implemented. The existential quantifier is implemented with the dependent product:

data Σ (A : Set) (B : A → Set) : Set where

    _,_ : (a : A) → B a → Σ A B

Compare this with conjunction, which corresponds to non-dependent product inline_formula not implemented:

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

		_,_ : A → B → A ∧ B

In this sense, in intuitionistic logic existential quantification Σ generalises conjunction, which justifies the name dependent product. (This can create confusion because Π is sometimes called dependent product too, since also Π generalises conjunction...)

(Existential quantification also generalises disjunction, since the type inline_formula not implemented is isomorphic to inline_formula not implemented with inline_formula not implemented and inline_formula not implemented. For this reason, Σ is sometimes called dependent sum. However, we will not follow this terminology here.)

Σ' : ∀ {A : Set} (B : A → Set) → Set

Σ' {A} B = Σ A B

infix 0 Σ'

syntax Σ' (λ x → B) = ∃[ x ] B

-- ∃[ x ] B is a shortcut for Σ' (λ x → B) and Σ _ (λ x → B)

-- aka uncurry

∃-elim : {A : Set} {B : A → Set} {C : Set} → (∀ (a : A) → B a → C) → Σ A B → C

∃-elim a→b→c (a , b) = a→b→c a b

We can also define projection functions for dependent pairs.

dfst : {A : Set} {B : A → Set} → Σ A B → A

dfst (a , _) = a

-- notice how the *type* of the second projection dsnd needs to use the first projection dfst!

dsnd : {A : Set} {B : A → Set} → (p : Σ A B) → B (dfst p)

dsnd (_ , b) = b

-- dsnd : {A : Set} {B : A → Set} → ((a , _) : Σ A B) → B a ??

We note how the definition of the functions dfst and dsnd is exactly as before with non-dependent pairs, however the type of these functions is much more precise now.

Exercise (∃)

1. Show that the existential quantifier commutes with itself: inline_formula not implemented.

∃-comm :

  {A B : Set} {P : A → B → Set} →

  ∃[ a ] ∃[ b ] P a b →

  -------------------------------

  ∃[ b ] ∃[ a ] P a b

∃-comm = ?

Exercise (∃ and →)

Consider the following two implications (where inline_formula not implemented is not free in inline_formula not implemented):

1. inline_formula not implemented, and

2. inline_formula not implemented.

They are both valid in classical logic. Find out which one is valid in intuitionistic logic, and prove it.

∃→1 :

  {A : Set} {P : Set} {Q : A → Set} →

  ∃[ a ] (P → Q a) →

  P →

  -----------------------------------

  ∃[ a ] Q a

∃→1 = ?

∃→2 :

  {A : Set} {P : Set} {Q : A → Set} →

  (P → ∃[ a ] Q a) →

  ------------------------------------

  ∃[ a ] (P → Q a)

∃→2 = ?

Exercise (∃ and ∀)

-- 1

duncurry :

  {A : Set} {B : A → Set} {C : Set} →

  ∀[ a ] (B a → C) →

  ∃[ a ] B a →

  ------------------------------------

  C

duncurry = ?

dcurry :

  {A : Set} {B : A → Set} {C : Set} →

  (∃[ a ] B a  → C) →

  -----------------------------------

  ∀[ a ] (B a → C)

dcurry = ?

Exercise (∃, ∧, and ∨)

Establish whether the following are intuitionistic tautologies and prove it for the positive cases:

1. inline_formula not implemented.

2. inline_formula not implemented.

3. inline_formula not implemented.

4. inline_formula not implemented.

5. inline_formula not implemented, where inline_formula not implemented does not occur in inline_formula not implemented.

-- 1

∃∨-distr :

  {A : Set} {B C : A → Set} →

  ∃[ a ] B a ∨ C a →

  ---------------------------

  (∃[ a ] B a) ∨ (∃[ a ] C a)

∃∨-distr = ?

-- 2

∨∃-distr :

  {A : Set} {B C : A → Set} →

  (∃[ a ] B a) ∨ (∃[ a ] C a) →

  -----------------------------

  ∃[ a ] B a ∨ C a

∨∃-distr = ?

-- 3

∃∧-distr :

  {A : Set} {B C : A → Set} →

  ∃[ a ] B a ∧ C a →

  ---------------------------

  (∃[ a ] B a) ∧ (∃[ a ] C a)

∃∧-distr = ?

-- 4

∧∃-distr :

  {A : Set} {B C : A → Set} →

  (∃[ a ] B a) ∧ (∃[ a ] C a) →

  -----------------------------

  ∃[ a ] B a ∧ C a

∧∃-distr = ?

-- 5

∧∃-distr' :

  {A : Set} {B : A → Set} {C : Set} →

  (∃[ a ] B a) ∧ C →

  -----------------------------------

  ∃[ a ] B a ∧ C

∧∃-distr' = ?

Exercise (∀, ∃, and ¬)

Which of the following holds in intuitionistic logic? Prove those that hold.

1. inline_formula not implemented, where inline_formula not implemented depends on inline_formula not implemented and inline_formula not implemented.

2. inline_formula not implemented, where inline_formula not implemented depends on inline_formula not implemented.

3. inline_formula not implemented, where inline_formula not implemented depends on inline_formula not implemented.

4. inline_formula not implemented, where inline_formula not implemented depends on inline_formula not implemented.

5. inline_formula not implemented, where inline_formula not implemented depends on inline_formula not implemented.

-- 1

-- (B cannot depend on (a : A) for the swap to be possible!)

∃∀-distr :

  {A : Set} {B : Set} {C : A → B → Set} →

  ∃[ a ] ∀[ b ] C a b →

  ---------------------------------------

  ∀[ b ] ∃[ a ] C a b

∃∀-distr = ?

-- 2

¬∃→∀¬ :

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

  ¬ (∃[ a ] B a) →

  -------------------------

  ∀[ a ] ¬ B a

¬∃→∀¬ = ?

-- 3

∀¬→¬∃ :

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

  ∀[ a ] ¬ B a →

  -------------------------

  ¬ (∃[ a ] B a)

∀¬→¬∃ = ?

-- 4

∃¬→¬∀ :

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

  ∃[ a ] ¬ B a →

  -------------------------

  ¬ (∀[ a ] B a)

∃¬→¬∀ = ?

-- 5

¬∀→∃¬ :

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

  ¬ (∀[ a ] B a) →

  -------------------------

  ∃[ a ] ¬ B a

¬∀→∃¬ = ?

Exercise (∀, ∃, and →)

Show that one can always push the existential quantifier inside an implication: inline_formula not implemented.

However, the converse implication does not hold intuitionistically, even when inline_formula not implemented does not contain inline_formula not implemented free: inline_formula not implemented.

∃∀→ :

  {A : Set} {P Q : A → Set} →

  (∃[ a ] (P a → Q a)) →

  (∀[ a ] P a) →

  ---------------------------

  (∃[ a ] (Q a))

∃∀→ = ?

Relations - optional

The exercises in this section are optional.

We apply first-order logic to study some properties of binary relations. We first define what is a binary relation.

Rel : Set → Set → Set1

Rel A B = A → B → Set

(The type of Rel A B is Set1, which is the type of Set : Set1, which in turn is the same as Set0. We do not need to bother anymore with type levels.)

For example, we can express common properties of binary relations.

reflexive : ∀ {A : Set} → Rel A A → Set

reflexive R = ∀[ x ] R x x

symmetric : ∀ {A : Set} → Rel A A → Set

symmetric R = ∀[ x ] ∀[ y ] (R x y → R y x)

transitive : ∀ {A : Set} → Rel A A → Set

transitive R = ∀[ x ] ∀[ y ] ∀[ z ] (R x y → R y z → R x z)

Exercise (Total relations)

1. Define what it means for a relation inline_formula not implemented to be total: inline_formula not implemented.

2. Formalise and prove that every relation inline_formula not implemented which is symmetric, transitive, and total, it is also necessarily reflexive.

total : ∀ {A B : Set} → Rel A B → Set

total R = ?

sym∧trans∧tot→refl : (A : Set) (R : Rel A A) → ?

sym∧trans∧tot→refl = ?

Composition of relations

We can define the composition of binary relations.

_∘_ : ∀ {A B C : Set} → Rel A B → Rel B C → Rel A C

(R ∘ S) a c = ∃[ b ] (R a b ∧ S b c)

Exercise

Show that the composition of reflexive relations is also reflexive.

∘-refl : ∀ {A : Set} {R S : Rel A A} → reflexive R → reflexive S → reflexive (R ∘ S)

∘-refl = ?

Inclusion

We can define that one relation is included into another.

_⊆_ : ∀ {A B : Set} → Rel A B → Rel A B → Set

R ⊆ S = ∀[ x ] ∀[ y ] (R x y → S x y)

With this in hand, we can define that one relation commutes with another.

commute : ∀ {A : Set} (R S : Rel A A) → Set

commute R S = (R ∘ S) ⊆ (S ∘ R)

Exercise

Prove that if inline_formula not implemented and inline_formula not implemented are transitive binary relations and moreover inline_formula not implemented commutes over inline_formula not implemented, then their composition inline_formula not implemented is also transitive.

∘-trans : ∀ (A : Set) (R S : Rel A A) → transitive R → transitive S → commute S R → transitive (R ∘ S)

∘-trans = ?