A Guide for the Agda's FOL Plug-in

Introduction

The Agda's FOL plug-in provides a means to access the Gandalf first-order logic prover from Agda. By using this plugin, it can be much easier to prove first-order logic propositions in Agda.

How to Install

The binary packages of Agda for Windows and Machintosh already bundle the Gandalf prover, the auxiliary tool Santa, and the plugin itself. At the moment, Windows users must install cygwin before they can use this plugin. Instructions for installation under Linux are here.

Preparation

Download the following files to a directory and open foltest.alfa with the Emacs Agda interface:

Getting Started

Example 1: Prove that: P ∧ Q → P ∨ Q

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test1 (P,Q::Prop) :: And P Q -> Or P Q
  = external "fol"
If you typecheck the above code, you obtain the following message in the buffer "* External Info *":
Proved by FOL
And P Q -> Or P Q
This means that Gandalf proved that for all propositions P and Q, it is the case that P ∧ Q → P ∨ Q. Observe how this formula is represented as a type. The type Prop is assumed to contain all propositions. The above occurrence of the expression external "fol" can be regarded as a proof term. For example, \(h :: And P Q) -> introOr_lft P Q (elimAnd_fst P Q h) where introOr_lft and elimAnd_fst are constants defined in the library LogicSet.alfa.

Should you get the message "Plugin error: FOL could not prove" instead of the above message, at least one of Gandalf, Santa, and the Agda's plugin feature is not installed correctly. If you have installed Agda using the Windows binary installer, it is likely that you have not yet installed cygwin.

Example 2: Prove that: P(a) → ∃x. P(x)

To express an existentially quantified formula, we write Exists P. Here, P must be a predicate on a set A, that is, a function of the type A -> Prop which sends each element of the set A to a proposition.
--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test2 (A::Set) (P::A -> Prop) (a::A) :: P a -> Exists P
  = external "fol"
If you typecheck the above code, you obtain the following message:
Proved by FOL
P a -> Exists |A P
This means that Gandalf proved that for any set A, any predicate P on A, and any element a of A, it is the case that P(a) → ∃x. P(x).

Example 3: Prove that: ∀a. (∀x. P(x)) → P(a)

We write a dependent function type (x :: A) -> P x to express a universally quantified formula. Here, P must have the type A -> Prop.
--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test3 (A::Set) (P::A -> Prop) :: (a::A) -> ((x::A) -> P x) -> P a
  = external "fol"
Proved by FOL
(a::A) -> ((x::A) -> P x) -> P a

Example 4: We, of course, cannot prove that: ∃x. P(x)

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test4 (A::Set) (P::A -> Prop) :: Exists |A P
  = external "fol"
You will get the following message because ∃x. P(x) is not provable for arbitrary A and P.
Plugin error: FOL could not prove
Exists |A P
In this case, the message "Type correct" will not be displayed in the info bar of the Emacs buffer. This means that some proofs have not been found.

The Prover Uses Classical Logic

The logic of the plugin is classical. Hence, it is users' responsibility not to use the plugin where constructive proofs are requested.

Example 5: We can prove that: P ∨ ¬P

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test5 :: (P::Prop) -> Or P (Not P)
  = external "fol"
Proved by FOL
(P::Set) -> Or P (Not P)

Example 6: We can prove that: ¬∀x. P(x) → ∃x. ¬P(x)

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test6 (A::Set) (P::A -> Prop) :: Not ((x::A) -> P x) ->
                                 Exists (\(x::A) -> Not (P x))
  = external "fol"
Proved by FOL
Not ((x::A) -> P x) -> Exists |X (\(x::A) -> Not (P x))

The Prover Assumes the Domain is Non-empty

The plugin presumes that the domain of each individual variable is non-empty. It is users' responsibility not to forget it.

Example 7: We can prove that: ∀x. P(x) → ∃x. P(x)

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
test7 (X::Set) (P::X -> Prop) :: ((x::X) -> P x) -> Exists P
  = external "fol"
Proved by FOL
((x::X) -> P x) -> Exists |X P
Since the prover has assumed that X is nonempty, you should never give the empty datatype Absurd to test7, which would result in a proof of contradiction:
proof_of_contradiction :: Absurd
  = (test7 |Absurd |(\(x::Absurd) -> Absurd) (\(x::Absurd) -> x)).snd
The selector .snd extracts the proof part of the dependent pair representing the bogus witness.

Syntax

Connectives

Proposition Agda Representation
¬ P Not P
P ∧ Q And P Q
P ∨ Q Or P Q
P → Q P -> Q
T Taut
Absurd
∀x∈P. Q (x :: P) -> Q
∃x∈P. Q Exists (\(x :: P) -> Q)

Sets of Individuals

To introduce a set of individuals, you can declare a variable or a postulated constant of the type Set:
postulate Man :: Set

Symbols

To declare a name for a new predicate/constant/function symbol, you can just postulate a constant of that name with an appropriate type:
postulate IsFatherOf :: Man -> Man -> Prop    -- a predicate symbol
postulate fatherOf   :: Man -> Man            -- a function symbol

Axioms

Axioms or assumptions can be introduced either as variables bound in the telescope or as postulated constants. In the latter case, you may need to write those postulated constants as extra arguments to the external "fol" expressions so that the plugin can use them. These extra arguments can be supplied as many as you want.
postulate fatherLaw :: (x::Man) -> IsFatherOf x (fatherOf x)
hasFather :: (x::Man) -> Exists (IsFatherOf x)
  = external "fol" fatherLaw

Lemmas

It is convenient to give names to lemmas or theorems and this is done by defining new constants. For example, the constant hasFather defined above expresses a lemma. Lemmas can be passed as extra arguments to the external "fol" expressions so that the plugin can use them. In fact, the plugin does not distinguish between lemmas and axioms in the extra arguments; it just looks at their types.

A Larger Example

Example 8: No Men Are Barbers

--#include "LogicSet.alfa"
open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists
postulate Man :: Set                    -- Man is a set of human beings in this village
postulate Shaves :: Man -> Man -> Prop  -- Shaves x y means that x shaves the beard of y
postulate Barber :: Man -> Prop         -- Barber x means that x is a barber

postulate barberLaw1 :: (x::Man) -> Barber x ->
                        (y::Man) -> Not (Shaves y y) -> Shaves x y
postulate barberLaw2 :: (x::Man) -> Barber x ->
                        (y::Man) -> Shaves y y -> Not (Shaves x y)

noBarbers :: Not (Exists Barber)
noBarbers = external "fol" barberLaw1 barberLaw2
Proved by FOL
Not (Exists |Man Barber)

Written by Norio KATO on March 7, 2007.