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

1.1.1 Linux

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

sudo apt-get install agda

in order to install Agda.

1.1.2 Permission denied in Ubuntu

If you have a permission denied problem with Ubuntu, you have probably hit a known bug in the package for the standard library (agda-stdlib version 1.7.3-1). Make sure that we are talking about the incriminated package by typing

apt-cache policy agda-stdlib

and check that the installed version is 1.7.3-1. If this is the case, you can to the following in order to circumvent it. Type as root:

cd /usr/share/agda-stdlib
echo "name: standard-library-1.7.1" > standard-library.agda-lib
echo "flags: -WnoUnsupportedIndexedMatch" >> standard-library.agda-lib
mkdir _build
chmod 777 _build

1.1.3 MacOS

On MacOS, you can install Agda via Homebrew with

brew install agda

Beware, you should also follow the instructions displayed in the end in order to properly install the standard library.

1.1.4 Windows

On Windows, you should use Windows subsystem for Linux (aka WSL) and refer to the above documentation for Linux.

1.1.5 None of the above

If you cannot manage to install Agda on your machine, ask for help. In the meantime, you can work via ssh on the machines from the computer room in the Turing building:

ssh -J samuel.mimram@login.dix.polytechnique.fr samuel.mimram@ablette.dix.polytechnique.fr

(obviously, you need to replace samuel.mimram by you own login above, twice).

1.2 Editors

The following editors support 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

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.

Note: if you are using VS Code, the \ should be replaced by *

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: you should change (A B : Set) to {A B : Set} and remove the arguments A and B in the last line.

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 diag of \(A\Rightarrow A\land A\).

4.3 Commutativity

Show that conjunction is commutative in a proof ∧-comm: \((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 in a proof →distrib: \[ (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 (or-comm).

5.3 Distributivity

Show that conjunction distributes over disjunction (and-or-distrib).

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