by Jan Malakhovski, v. 2.1, published , last updated Literate Source
Have you ever wondered why there is the deduction theorem [1] which is a theorem, yet implication introduction [2] is an axiom?
Obviously, the answer can be deduced from the Wikipedia articles. But it’s much more interesting to find it the hard way. Let’s reinvent basic formal logic ourselves!
We’ll do this in Agda (which is kind of funny, because Agda is already a fine formal logic system). The result would be a simple example of a nontrivial nonarithmetical proof in Agda. We won’t use propositional equality here even once, so it might work as an introduction to Agda for those who are not scared of logic.
Another bonus is that this stuff is probably taught in class within university mathematical logic course. Doing it yourself allows much deeper understanding.
(This is a TL;DR for the logic theoreticians. Ignore everything you don’t understand yet, all will be explained later in the article.)
For the sake of simplicity we shall restrict ourselves to inventing only Hilbert- and Gentzen-style intuitionistic propositional logics. Even first-order systems require substitutions and all the stuff that comes with them, yet everything is fascinatingly simple in propositional setting.
I don’t particularly like to dig through libraries, so I’m just going to write out every piece of Agda code we’ll need. Fortunately, there isn’t much.
Module definition goes first:
Then we’ll need List
type
infixr 40 _∷_
data List (A : Set) : Set where
[] : List A -- an empty list
_∷_ : (a : A) → (as : List A) → List A -- "cons" -- creates a new list with "a" in the head
-- and "as" in the tail
-- appending two lists
_++_ : ∀ {A} → List A → List A → List A
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)
and ∈
relation
data _∈_ {A : Set} : A → List A → Set where
Z : {a : A}{as : List A} → a ∈ (a ∷ as) -- "a" is in a head of a list
S : {a b : A}{as : List A} → a ∈ as → a ∈ (b ∷ as) -- "a" is in a tail somewhere
-- if x is in as then it is in bs appended to as
relax-right : ∀ {A} {x : A} {as bs} → x ∈ as → x ∈ (as ++ bs)
relax-right Z = Z
relax-right (S y) = S (relax-right y)
-- similarly, but if x is in bs
relax-left : ∀ {A} {x : A} as {bs} → x ∈ bs → x ∈ (as ++ bs)
relax-left [] p = p
relax-left (a ∷ as) p = S (relax-left as p)
Value of type x ∈ as
is very similar to a natural number. It’s a position of x
in a list as
counting from list’s head.
And a Σ
-type (dependent pair).
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
fst : A
snd : B fst
open Σ public
“There exists such x
of type SomeType
so that SomeProperty
holds (is true)” expressed with dependent pair becomes: Σ SomeType (λ x → SomeProperty)
.
Most our terms will need a type of variables. It’s a common trick to introduce such a type as a module parameter
What is simplest possible proposition? A variable! What is a simplest logical connectivity? “If-then”, i.e. implication! What is a simples way to say that something is not true? Use proposition that is always false (called “bottom” by brainy mathematicians)! Well, actually, negation is not really that necessary for us here, but it’s fun to have.
So, in implicational intuitionistic propositional calculus (abbreviated IPC(→)) formulas (called “judgments” by brainy mathematicians) have three constructors: variables, implication and bottom. Let’s write that down (in Agda we can’t use parentheses in the name of IPC(→), also we can’t or don’t want to use →
and ⊥
as a constructor names, that’s a pity):
data IPC⟨→⟩ : Set where
⋆_ : V → IPC⟨→⟩ -- variable
_⊃_ : IPC⟨→⟩ → IPC⟨→⟩ → IPC⟨→⟩ -- implication
⊥c : IPC⟨→⟩ -- "bottom" -- formula that has no proof
Given a variable a : V
we have (⋆ a) ⊃ (⋆ a) : IPC⟨→⟩
— a formula expressing “a
implies a
”.
The only sacred knowledge about this definition is bottom usage. Negation ¬ J
(J
is false) for some judgment J
is encoded by J → ⊥
. The idea is that ⊥ → X
is always true for any X
— so called “ex falso” rule — “from a contradiction, anything follows”, it’s an axiom in any formal system build around bottom (there’re other design choices, see e.g. [3]). ⊥
is always false, so proving J → ⊥
we prove that J
is isomorphic (J → ⊥ ∧ ⊥ → J
) to ⊥
. Which means that J
is false (i.e. ¬ J
is true) too because it could be substituted instead of bottom everywhere.
You might wonder about a justification behind “ex falso” rule. There’s an textbook explanation by Bertrand Russell: “If 2 * 2 ≡ 5
then I’m the Pope. 2 * 2 ≡ 2 + (1 * 2) ≡ 2 + 2
, 2 + 3 ≡ 5
, by transitivity and reflexivity 2 + 2 ≡ 2 + 3
, thus 2 ≡ 3
, 1 ≡ 2
. Now assume a two element set {Bertrand, Pope}. 2 ≡ 1
. So Bertrand ≡ Pope
.” Which roughly says that you could always rearrange your proof so that from a contradictional proposition follows a proposition which implies proposition you want to prove.
There is another “computational” justification for Agda users by me. Suppose you’re writing an expression of some type X
and there’s a variable of type isomorphic to ⊥
in a context. This means that execution won’t reach this point of a program anytime soon (assuming correct compiler) because nobody could give you a value from an empty type. But you still need a value of type X
. Ex falso allows you to plug this hole for free. It’s safe to cheat like that because nobody is ever going to look at you here at run-time.
If you haven’t understood that, return here again after you finished this article.
What is a proof of a judgment J
? Well, there are judgments that are always true, e.g. A → (B → A)
. These are called “axioms”. How do we prove a thing that is not an axiom? We combine smaller proofs into a larger proof.
Let’s think again. Proof is an axiom or a combination of a number of smaller proofs. Aha! It’s a list! Proof of J
is a list (proof sequence) which has J
as a lastest element, whereas each element of the sequence is either
Using traditional two-dimentional syntax, rule preconditions (stuff already in a proof sequence) are written above the bar whereas rule conclusions (stuff to append to a sequence) are placed below, e.g.: , . In other words, bar is “meta-implication” while spaces between preconditions are “meta-conjuctions”.
Note, that an axiom is just a rule that allows to introduce a certain judgments without preconditions, i.e. without using any earlier judgments from a proof sequence.
Implication is the only logical connective in our definition of IPC⟨→⟩. Simplest logical rule for implication elimination is ((A → B) ∧ A) → B
rewritten into two-dimensional rule with simple IPC(→) terms as judgments gives us inference rule called “modus ponens”.
Being clever we could use types of K
and S
combinators from SKI calculus as our axioms. Since we also have ⊥c
in our language we shall add ex falso rule too.
As a result we have the following set of axioms:
⊥ → A
for any A
— ex falso, ⊥-elimination axiom;A → (B → A)
for any A
and B
— K combinator;(A → B → C) → ((A → B) → (A → C))
for any A
, B
and C
— S combinator.Hurray! We have just reinvented a formal proof system, invented by Hilbert at the start of twentieth century [4]. Except SKI was not yet invented and Hilbert’s original system used a slightly different set of axioms.
The trick is that we can transform all rules into axioms by turning bars into implications: . If we can formulate all our axioms in terms of implication we won’t need to invent other inference rules except modus ponens. For instance, for ∧
and ∨
connectives we just need to add a bunch of axioms to our set (for appropriate “for anys”):
A → (B → (A ∧ B))
(A ∧ B) → A
(A ∧ B) → B
A → (A ∨ B)
B → (A ∨ B)
(A ∨ B) → ((A → C) → ((B → C) → C))
Except this wouldn’t be called IPC(→) but IPC (without an arrow, signifying that there are other logical connectivities except implication). In that case we’d need to add ∧ and ∨ constructors to our definition in Agda.
Another useful thing we have missed is “assumptions”. Assumptions are just local user-defined axioms and we could formalize them as such, adding
A
for any assumption A
— assumption axiomto our set of axioms.
Okay, let’s implement this. Our system doesn’t have any explicit quantifiers, but our axioms are “polymorphic” (they work for all A
’s, B
’s and so on’s). Thus it’s much easier to encode them directly into syntax than to track them separately as a set.
We shall define a certificate Γ hl⊢ L
which says that a list L
of IPC⟨→⟩
terms is a valid proof sequence if we assume Γ
.
data _hl⊢_ (Γ : List IPC⟨→⟩) : List IPC⟨→⟩ → Set where
H-EM : Γ hl⊢ [] -- empty list is a valid
-- proof sequence
H-AΓ : ∀ {A pl} → A ∈ Γ → Γ hl⊢ pl → Γ hl⊢ (A ∷ pl) -- assumption
H-AB : ∀ {A pl} → Γ hl⊢ pl → Γ hl⊢ ((⊥c ⊃ A) ∷ pl) -- ex falso
H-AK : ∀ {A B pl} → Γ hl⊢ pl → Γ hl⊢ ((A ⊃ (B ⊃ A)) ∷ pl) -- K
H-AS : ∀ {A B C pl} → Γ hl⊢ pl → Γ hl⊢ (((A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))) ∷ pl) -- S
H-IM : ∀ {A B pl} → (A ⊃ B) ∈ pl → A ∈ pl → Γ hl⊢ pl → Γ hl⊢ (B ∷ pl) -- modus ponens
Now, how do we say that a judgment is provable? Judgment is provable iff there exists a proof sequence that ends with a needed judgment:
Let’s prove A → A
within this system:
H-AI : ∀ {Γ A} → Γ h⊢ (A ⊃ A)
H-AI {A = A} = ((A ⊃ (A ⊃ A)) ⊃ (A ⊃ A)) ∷ (A ⊃ (A ⊃ A))
∷ ((A ⊃ ((A ⊃ A) ⊃ A)) ⊃ ((A ⊃ (A ⊃ A)) ⊃ (A ⊃ A)))
∷ (A ⊃ ((A ⊃ A) ⊃ A)) ∷ []
, H-IM Z (S Z) (H-IM (S Z) (S (S Z)) (H-AK (H-AS (H-AK H-EM))))
Pretty tiring.
Note that since all the links between list elements go strictly back into the list we could forget about the list structure and build a tree (possibly dublicating some list elements on the way).
Let’s define a datatype for this tree:
data _t⊢_ (Γ : List IPC⟨→⟩) : IPC⟨→⟩ → Set where
T-AΓ : ∀ {A} → A ∈ Γ → Γ t⊢ A
T-AB : ∀ {A} → Γ t⊢ (⊥c ⊃ A)
T-AK : ∀ {A B} → Γ t⊢ (A ⊃ (B ⊃ A))
T-AS : ∀ {A B C} → Γ t⊢ ((A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C)))
T-IM : ∀ {A B} → Γ t⊢ (A ⊃ B) → Γ t⊢ A → Γ t⊢ B
Advantage of this definition is that we don’t need an explicit sequence of judgments to build a proof. This time the proof of A → A
is much more short and readable:
T-AI : ∀ {Γ A} → Γ t⊢ (A ⊃ A)
T-AI {A = A} = T-IM (T-IM (T-AS {A = A} {B = A ⊃ A} {C = A}) T-AK) T-AK
Now we a going to prove that this representation has exactly the same expressive power as h⊢, i.e. if we can prove something with h⊢, then we could do the same with t⊢ and vice versa.
connect-var : ∀ {Γ L A} → Γ hl⊢ L → A ∈ L → Γ t⊢ A
connect-var H-EM ()
connect-var (H-AΓ y y') Z = T-AΓ y
connect-var (H-AB y) Z = T-AB
connect-var (H-AK y) Z = T-AK
connect-var (H-AS y) Z = T-AS
connect-var (H-IM y y' y0) Z = T-IM (connect-var y0 y) (connect-var y0 y')
connect-var (H-AΓ y y') (S y0) = connect-var y' y0
connect-var (H-AB y) (S y') = connect-var y y'
connect-var (H-AK y) (S y') = connect-var y y'
connect-var (H-AS y) (S y') = connect-var y y'
connect-var (H-IM y y' y0) (S y1) = connect-var y0 y1
h→t : ∀ {Γ A} → Γ h⊢ A → Γ t⊢ A
h→t (pl , p) = connect-var p Z
++-proofs : ∀ {Γ L M} → Γ hl⊢ L → Γ hl⊢ M → Γ hl⊢ (L ++ M)
++-proofs H-EM p2 = p2
++-proofs (H-AΓ y y') p2 = H-AΓ y (++-proofs y' p2)
++-proofs (H-AB y) p2 = H-AB (++-proofs y p2)
++-proofs (H-AK y) p2 = H-AK (++-proofs y p2)
++-proofs (H-AS y) p2 = H-AS (++-proofs y p2)
++-proofs (H-IM y y' y0) p2 = H-IM (relax-right y) (relax-right y') (++-proofs y0 p2)
t→h : ∀ {Γ A} → Γ t⊢ A → Γ h⊢ A
t→h (T-AΓ y) = [] , H-AΓ y H-EM
t→h T-AB = [] , H-AB H-EM
t→h T-AK = [] , H-AK H-EM
t→h T-AS = [] , H-AS H-EM
t→h (T-IM {A = A} {B = B} y y') = (((A ⊃ B) ∷ fst hA⊃B) ++ (A ∷ fst hA))
, H-IM Z (relax-left ((A ⊃ B) ∷ fst hA⊃B) Z)
(++-proofs (snd hA⊃B) (snd hA)) where
hA⊃B = t→h y
hA = t→h y'
How do we usually prove A → B
in mathematics? We assume A
and then prove B
. Does this work in our systems? Yes, and it’s called “The Deduction Theorem”.
deduction-t : ∀ {Γ A B} → (A ∷ Γ) t⊢ B → Γ t⊢ (A ⊃ B)
deduction-t (T-AΓ Z) = T-AI
deduction-t (T-AΓ (S y)) = T-IM T-AK (T-AΓ y)
deduction-t T-AB = T-IM T-AK T-AB
deduction-t T-AK = T-IM T-AK T-AK
deduction-t T-AS = T-IM T-AK T-AS
deduction-t (T-IM y y') = T-IM (T-IM T-AS (deduction-t y)) (deduction-t y')
deduction-h : ∀ {Γ A B} → (A ∷ Γ) h⊢ B → Γ h⊢ (A ⊃ B)
deduction-h p = t→h (deduction-t (h→t p))
It’s fun to dissect deduction-t
proof. Comment right-hand sides of sentences, insert holes after =
and inspect types.
With deduction-h
A → A
becomes a cake:
You can inspect the proof it generates by C-c C-n in the following hole:
Compare it to the proof we wrote above.
Proving things with a help from the deduction theorem is much more easy. What if we drop K
and S
and add the deduction theorem as a rule?
data _⊩_ (Γ : List IPC⟨→⟩) : IPC⟨→⟩ → Set where
G-A : ∀ {A} → A ∈ Γ → Γ ⊩ A
G-B : ∀ {A} → Γ ⊩ ⊥c → Γ ⊩ A
G-I : ∀ {A B} → (A ∷ Γ) ⊩ B → Γ ⊩ (A ⊃ B)
G-E : ∀ {A B} → Γ ⊩ (A ⊃ B) → Γ ⊩ A → Γ ⊩ B
Note that we also rewrote ⊥-elimination a bit, so that all rules have one precondition on top of the bar. Let’s check that it’s a valid transformation.
This ⊩ is a Gentzen-style “Natural Deduction” system invented by Gentzen in 1935 [5]. It becomes simply typed lambda calculus with bottom elimination if you look through Curry-Howard lens: G-A
is a variable occurrence, G-I
is an abstraction, G-E
is an application, G-B
is a bottom elimination.
Is this system still of equal expressive power to Hilbert-style systems? Yes.
t→g : ∀ {Γ A} → Γ t⊢ A → Γ ⊩ A
t→g (T-AΓ y) = G-A y
t→g T-AB = G-B-is-ok
t→g T-AK = G-I (G-I (G-A (S Z))) -- λ x y . x
t→g T-AS = G-I (G-I (G-I
(G-E
(G-E (G-A (S (S Z))) (G-A Z))
(G-E (G-A (S Z)) (G-A Z))))) -- λ x y z . x z (y z)
t→g (T-IM y y') = G-E (t→g y) (t→g y')
g→t : ∀ {Γ A} → Γ ⊩ A → Γ t⊢ A
g→t (G-A y) = T-AΓ y
g→t (G-B y) = T-IM T-AB (g→t y)
g→t (G-I y) = deduction-t (g→t y)
g→t (G-E y y') = T-IM (g→t y) (g→t y')
h→g : ∀ {Γ A} → Γ h⊢ A → Γ ⊩ A
h→g p = t→g (h→t p)
g→h : ∀ {Γ A} → Γ ⊩ A → Γ h⊢ A
g→h p = t→h (g→t p)
Note the deduction theorem usage in g→t
.
I hope you had as much fun while inspecting this as I had while writing.
Homework:
h→g
and g→h
directly?h→t (t→h p) ≡ p
t→h (h→t p) ≡ p
g→t (t→g p) ≡ p
t→g (g→t p) ≡ p
The deduction theorem isn’t only about philosophical justification of “hipothetical reasoning” [1]. It’s a meat of the proof of equivalence between Hilbert- and Gentzen-style systems.
If you want more there’s an awesome book about logical systems through Curry-Howard isomorphism lens by Sørensen and Urzyczyn [3]. It’s not written in Agda, though.
∈
relation stolen from Rob Simmons’ Agda library [6].1. Wikipedia. Deduction theorem. https://en.wikipedia.org/wiki/Deduction_theorem.
2. Wikipedia. Natural deduction. Hypothetical derivations. https://en.wikipedia.org/wiki/Natural_deduction#Hypothetical_derivations.
3. Sørensen M.H.B., Urzyczyn P. Lectures on the Curry-Howard isomorphism. 1998. https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385.
4. Wikipedia. Hilbert system. https://en.wikipedia.org/wiki/Hilbert_system.
5. Wikipedia. Natural deduction. https://en.wikipedia.org/wiki/Natural_deduction.
6. Simmons R. Agda-lib. https://bitbucket.org/robsimmons/agda-lib.