Propositional logic in Agda

Samuel Mimram

1 Getting started

Starting from today we are going to use Agda. In case you have a problem, you are encouraged to read the official documentation.

1.1 Installing Agda on your own computer

This section is useful in order to install Agda on your personal computer, skip it if you are using the PCs of the TD room.

1.1.1 Linux

If you have a Linux distribution such as Ubuntu or Debian simply type

sudo apt-get install emacs agda

in order to install Agda and Emacs.

1.1.2 MacOS

Install brew by following these instructions (brew is a package manager for MacOS) and type

brew install agda emacs
agda-mode setup

1.1.3 Windows

The easiest way is to use Windows subsystem for Linux (aka WSL) and follow the above installation instructions for Linux.

1.2 Editors

The recommended editor is Emacs, which is already installed and configured in the TD rooms.

Some other editors however also have support for Agda:

1.3 Shortcuts

We recall that the most useful shortcuts are

Shortcut Effect
C-c C-l typecheck and highlight the current file
C-c C-, get information about the hole under the cursor
C-c C-. show both the type of the current hole and of the proposed filling
C-c C-space give a solution
C-c C-c case analysis on a variable (≈ an elimination rule)
C-c C-r refine the hole (≈ an introduction rule)
C-c C-a automatic fill
middle click definition of the term

Note: if some e appears when you type C-c C-., you should run ibus-setup and disable the C-. shortcut here (it is used in order to type emoji…).

1.4 Symbols

Agda heavily resorts to UTF-8 notations. The Emacs mode has some great support for it, allowing to enter symbols generally as you would do in LaTeX. Some useful ones are

\and \top \to
\or \bot ¬ \neg
\all Π \Pi λ \Gl
\ex Σ \Sigma \Equiv
\bN × \times \le
\in \uplus \::
\qed \_1 \=>
\< \>

Many other symbols can be found here.

2 Our first proof

Try to do by yourself the first proof of the course. Create a file named TD5.agda and type (or copy) the following (recall that “×” is entered with \times and “→” with \to):

open import Data.Product

×-comm : (A B : Set)  (A × B)  (B × A)
×-comm A B p = ?

Then

  1. Use C-c C-l to load the file.
  2. Use C-c C-, to obtain the type of the hole.
  3. Use C-c C-c then p to observe the argument.
  4. Use C-c C-r to refine the hole.
  5. Enter the answers in the two holes and use C-c C-space.

In this example, you could have directly defined the λ-term, but in general you will see that it is necessary to use the holes.

Modify the proof so that the arguments A and B are implicit.

3 Implication

We will now do some proofs in propositional logic. We recall that, under the Curry-Howard correspondence the implication \(\Rightarrow\) corresponds to the arrow → of Agda. For instance, if we want to prove \(A\Rightarrow A\), we will construct a term of type A → A. For instance,

id : {A : Set}  A  A
id a = a

3.1 First projection

Give a proof of \(A\Rightarrow B\Rightarrow A\):

K : {A B : Set}  A  B  A

3.2 Application

Give a proof of \((A\Rightarrow B)\Rightarrow A\Rightarrow B\):

app : {A B : Set}  (A  B)  A  B

3.3 Flip

Give a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow B\Rightarrow A\Rightarrow C\)

flip : {A B C : Set}  (A  B  C)  B  A  C

3.4 Transitivity / composition

Give a proof of \((A\Rightarrow B)\Rightarrow(B\Rightarrow C)\Rightarrow(A\Rightarrow C)\):

comp : {A B C : Set}  (A  B)  (B  C)  (A  C)

3.5 S

Give a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow(A\Rightarrow B)\Rightarrow A\Rightarrow C\):

S : {A B C : Set}  (A  B  C)  (A  B)  A  C

4 Conjunction

The conjunction is defined in the module Data.Product which you can use with

open import Data.Product renaming (_×_ to __)

By default, following the Curry-Howard correspondence, the conjunction \(\land\) is noted as a product × on types in Agda. However, since we focus on logic here, we use the renaming command in order to change the notation to the usual .

4.1 Projections

Give a proof of \((A\land B)\Rightarrow A\):

proj1 : {A B : Set}  (A ∧ B)  A

and a proof proj2 of \((A\land B)\Rightarrow B\).

4.2 Diagonal

Give a proof of \(A\Rightarrow A\land A\).

4.3 Commutativity

Show that conjunction is commutative: \((A\land B)\Rightarrow(B\land A)\).

4.4 Currying

Most functional programming languages support Currying which is a principle according to which a function taking a pair of arguments can be transformed into one with two arguments and vice versa. For instance, in OCaml the functions of type

'a * 'b -> 'c

are in correspondence with those of type

'a -> 'b -> 'c

Show that we have \((A\land B\Rightarrow C)\Rightarrow(A\Rightarrow B\Rightarrow C)\):

curry1 : {A B C : Set}  (A ∧ B  C)  (A  B  C)

and the converse implication

curry2 : {A B C : Set}  (A  B  C)  (A ∧ B  C)

All connectives are defined in Agda. For instance, following the usual definition

\[ A \Leftrightarrow B \qquad=\qquad (A\Rightarrow B)\land(B\Rightarrow A) \]

we can define equivalence in Agda by

equiv : (A B : Set)  Set
equiv A B = (A  B)(B  A)

Do you understand this notation? (if not, ask). Or better, since we like UTF-8 symbols and infix notations:

__ : (A B : Set)  Set
A ↔ B = (A  B)(B  A)

where ↔︎ is typed \<->. With this notation, currying can now be expressed as

currying : {A B C : Set}  (A ∧ B  C)(A  B  C)

prove it (you can use previous proofs).

4.5 Distributivity

Show that conjunction on the target distributes over implication: \((A\Rightarrow(B\land C))\Leftrightarrow((A\Rightarrow B)\land(A\Rightarrow C))\).

5 Disjunction

Disjunction is defined in Agda in the module Data.Sum. However, in order to see how it works, we define it by hand (and use more usual notations):

data __ (A B : Set) : Set where
  left  : A  A ∨ B
  right : B  A ∨ B

It is an inductive type, which takes two parameters (A and B of type Set) and returns a Set. It has two constructors left and right which respectively take an element of type A and B as argument.

5.1 Elimination rule

Show the elimination rule for disjunction:

or-elim : {A B C : Set}  (A ∨ B)  (A  C)  (B  C)  C

5.2 Commutativity

Show that disjunction is commutative.

5.3 Distributivity

Show that conjunction distributes over disjunction.

dist : {A B C : Set}  (A ∧ (B ∨ C))  (A ∧ B)(A ∧ C)

6 Negation

6.1 Falsity

We define falsity as

data: Set where

which is an inductive type with no constructor.

Show the elimination rule

⊥-elim : {A : Set}  A

6.2 Negation

Define negation as a function

¬ : Set  Set

6.3 Contradiction

Show the principle of contradiction:

contr : {A B : Set}  (A  B)  (¬ B  ¬ A)

6.4 Non-contradiction

Show the principle of non-contradiction:

non-contr : {A : Set}  ¬ (A ∧ ¬ A)

6.5 Double negation introduction

Show the rule of introduction of double negation:

nni : {A : Set}  A  ¬ (¬ A)

6.6 Double negation elimination on \(\bot\)

Show that the principle of elimination of double negation is valid on \(\bot\):

⊥-nne : ¬ (¬ ⊥) 

6.7 Elimination of negation

Show the principle of elimination of negation:

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

6.8 De Morgan laws

Show the De Morgan laws

dm∧ : {A B : Set}  ¬ A ∧ ¬ B  ¬ (A ∨ B)

and

dm∨ : {A B : Set}  ¬ A ∨ ¬ B  ¬ (A ∧ B)

Can you manage to prove the converse implications?

6.9 Non-falsifiability of the law of excluded middle

Show that the law of excluded middle is not falsifiable:

nnlem : {A : Set}  ¬ (¬ (A ∨ (¬ A)))

6.10 Russell’s paradox

Show the following logical counterpart of Russell’s paradox:

rp : {A : Set}  (A  ¬ A)  ((¬ A)  A) 

(Hint: there is a solution which does not require any previously defined function).

7 Truth

7.1 Definition

Define truth as an inductive type.

7.2 ⊤-strengthening

Show that the hypothesis \(\top\) is always superfluous:

ti : {A : Set}  ( A)  A

7.3 De Morgan laws

Show the de Morgan laws

dmnt : ¬ ⊤ 

and

dmtn : ¬ ⊤

8 Classical logic

8.1 Equivalence between excluded middle and double negation elimination

We define the excluded middle principle by

lem : Set₁
lem = (A : Set)  A ∨ (¬ A)

and double negation elimination by

nne : Set₁
nne = (A : Set)  ¬ (¬ A)  A

Show that lem implies nne:

nne-lem : nne  lem

Show the converse implication:

lem-nne : lem  nne

It can be useful to first show:

lem-nne' : (A : Set)  (A ∨ ¬ A)  ¬ (¬ A)  A

8.2 Pierce law

Show that the two above principles are equivalent to the Pierce law:

pierce : Set₁
pierce = {A B : Set}  ((A  B)  A)  A

9 First-order logic (optional)

Suppose fixed a set U, which will act as the universe where variables range over. This can be achieved with

postulate U : Set

A predicate \(P(x)\) will be encoded as a function P of type U → Set which, given an element \(x\) of U returns a truth value. The formula \(\forall x. P(x)\) can then be encoded as the type of (dependent) functions

(x : U)  (P x)

and the formula \(\exists x. P(x)\) will be encoded as

 x  P x)

(we will not detail what this notation means exactly for now, but a witness is a pair consisting of an element t of U, and an element of P t).

9.1 Commutation of connectives

Given a predicate \(P(x,y)\), which depends on two variables, show the formula \[\forall x.\forall y.P(x,y)\Rightarrow \forall y.\forall x.P(x,y)\] by defining

∀-comm : {P : U  U  Set} 
         ((x : U)  (y : U)  P x y)  ((y : U)  (x : U)  P x y)

Similarly, show that existential quantifications commute, i.e. \[\exists x.\exists y.P(x,y)\Rightarrow \exists y.\exists x.P(x,y)\] by defining

∃-comm : {P : U  U  Set}  x  y  P x y))  y  x  P x y))

Show the formula

\[\exists x.\forall y.P(x,y)\Rightarrow \forall y.\exists x.P(x,y)\]

9.2 Interaction with other connectives

Show the following formulas