Reinventing Formal Logic

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 non-arithmetical proof in Agda. We won’t use propositional equality here even once, so it might work as an introduction to non-trivial Agda proofs for those who are not scared of logic. If you know nothing at all about Agda at the moment, you will be able to understand everything in here after finishing with the “Slow start” section of BrutalDepTypes and ignoring the rest of that tutorial. Though, you should probably start reading it from the very beginning.

Another bonus is that this stuff is probably taught in class within university mathematical logic course. Doing it yourself allows much deeper understanding.

Changelog

• 2024-09-28 Version 3.0.0: edited, improved many explanations, added more flair, fixed typos, improved formula formatting
• 2024-02-19 Version 2.1.0: switched to semantic versioning
• 2024-02-16 Version 2.0.0: updated formatting a little, added a link to a follow-up
• 2012-12-11 Version 1.0.0: initial public release

Table of Contents

Goals

(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.

Some definitions

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.

If you are reading the literate source version of this in Emacs with Agda UI available, this is a good time to press C-c C-l (which calls agda2-load).

Module definition goes first:

module ReinventingFormalLogic where

Then we’ll need the 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 the ∈ 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)

A 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.

Finally, we nee the Σ-type, also known as dependently-typed pair:

  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B fst

  open Σ public

Using the above, “there exists such x of type SomeType so that SomeProperty x holds (is true)” is expressed like this: Σ SomeType (λ x → SomeProperty x), which, of course, is simply Σ SomeType SomeProperty.

Propositions and judgments

The first issue we need to solve is that most our terms will need a type for variables. Instead of trying to define such a type, we can simply introduce it as a module parameter

  module Dummy (V : Set) where

And, finally, we can start defining logical terms now.

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, so we have to use other UNICODE symbols):

    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 the above 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. Though, there are 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 a proposition you want to prove.

There is also a simple computational justification for Agda users. Suppose you’re trying to fill a hole of some type X in a term and you notice that the context of bound variables in that hole has a variable of type ⊥ in it. This means that, assuming the compiler complies your program correctly, the execution won’t ever reach this point of the program because no other part of the program could ever give you a value from an empty type. But you still need a value of type X to finish your term in the hole. Ex falso rule allows you to cheat and plug this hole for free. And it’s safe to cheat like that because that code won’t ever be run. In practice, of course, the compiler will also ensure that attempting execution of an ex falso term will cause the whole program to abort, just to be safe.

If that did not make sense, return here again after you’ve finished the rest of this article.

Hilbert-style proofs

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.

Hilbert-style sequence

Let’s think again. Proof is an axiom or a combination of a number of smaller proofs. Aha! It’s a list!

So, a proof sequence is a list where each element is either

• an axiom, or
• a logical step (made by using a certain rule) which generates a new judgment from judgments earlier in the sequence.

Then, a proof of J is a proof sequence which has J as its latest element.

In the literature that uses the traditional two-dimentional syntax, the “logical step” rules are usually written something like this:

$$\frac{A}{A ∨ B}$$

which, as a logical formula, is just A → (A ∨ B), and

$$\frac{A \quad B}{A ∧ B}$$

which, as a logical formula, is just A → (B → (A ∧ B)).

In two-dimensional 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 the bar. In other words, the bar is “meta-implication” while the 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. Relevant examples of these will be shown below.

Implication is the only logical connective in our definition of IPC⟨→⟩. The simplest logical rule for implication elimination is

$$\frac{A → B \quad A}{B}$$

which, as a logical formula, is just ((A → B) ∧ A) → B. This inference rule is called “modus ponens”.

Now, instead of using the original formulation of IPC(→) invented by Hilbert at the start of twentieth century [4], we can be clever and use a slightly simpler one by using the types of K and S combinators from SKI calculus as our axioms. (The equivalence of these systems are left as an exercise to the reader.)

Since we also have ⊥c in our language we shall add ex falso rule too.

As a result, we get 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.

In other words, our definition of IPC⟨→⟩ has three axioms which can be written as

$$\frac{}{⊥ → A}$$ and $$\frac{}{A → (B → A)}$$ and $$\frac{}{(A → B → C) → ((A → B) → (A → C))}$$

using the two-dimensional syntax.

As a side note, the point of Hilbert-style systems is an observation that for more involved logical systems, e.g. IPC⟨→⟩ with ∧ and ∨ logical operators, we can transform all inference rules except modus ponens into logical formula axioms by turning bars and meta-conjuctions into implications. For example:

$$\frac{A \quad B}{A ∧ B} \Rightarrow \frac{}{A → (B → (A ∧ B))}$$

Then, using such a formulation appears to simplify things, since if our formal system has all axioms formulated in terms of implication alone, then modus ponens is the only inference rule it will ever need.

For instance, if in the future we would want to extend our IPC⟨→⟩ with ∧ and ∨ connectives, we’d need to add _∧_ and _∨_ constructors to our definition of logical terms in Agda above, and then we’d add a bunch more axioms to the set above (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))

without adding any new inference rules. Except the resulting system wouldn’t be called IPC(→) but IPC, without an arrow, signifying that there are other logical connectivities except implication. (Doing this is left as an exercise to the reader.)

Getting back on track, the last thing we need to make it all work we have not discussed yet is “assumptions”. Assumptions are just local user-defined axioms and we could formalize them as such, adding

• A for any assumption A — assumption axiom

to 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)      -- axiom: ex falso
      H-AK : ∀ {A B pl}       → Γ hl⊢ pl → Γ hl⊢ ((A ⊃ (B ⊃ A)) ∷ pl) -- axiom: K
      H-AS : ∀ {A B C pl}     → Γ hl⊢ pl → Γ hl⊢ (((A ⊃ (B ⊃ C)) ⊃ ((A ⊃ B) ⊃ (A ⊃ C))) ∷ pl) -- axiom: 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:

    _h⊢_ : (Γ : List IPC⟨→⟩) → IPC⟨→⟩ → Set
    Γ h⊢ A = Σ (List IPC⟨→⟩) (λ pl → Γ hl⊢ (A ∷ pl))

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))))

Immediately, we can see this system is pretty tiring to use, yes.

Hilbert-style tree

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 duplicating 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

The 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 shorter and more 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'

The Deduction theorem

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 out right-hand sides of the sentences above, insert holes after the = symbols and inspect the types by pressing C-c C-t in Emacs Agda UI (which calls agda2-goal-type).

With deduction-h the scary proof of A → A we saw above becomes cake:

    H-AI‵ : ∀ {Γ A} → Γ h⊢ (A ⊃ A)
    H-AI‵ = deduction-h ([] , H-AΓ Z H-EM)

In Emacs Agda UI, you can inspect the proof it generates by pressing C-c C-n (which calls agda2-compute-normalised-maybe-toplevel function) in the following hole:

    check-me : ∀ {Γ A} → Γ h⊢ (A ⊃ A)
    check-me {A = A} = {!H-AI‵ {A = A}!}

Compare it to the proof we wrote above.

Gentzen-style proofs

Proving things by using the deduction theorem seems to be much easier than doing things by hand. So, what if we drop K and S and add the deduction theorem as a rule instead? Would such a system be expressive enough to prove everything we could prove before? Let’s try!

    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 our new rules have one precondition on top of the bar. That is, in two-dimensional syntax, our previous axiom rule of

$$\frac{}{⊥ → A}$$

became

$$\frac{⊥}{A}$$

inference rule instead.

Let’s check that it’s a valid transformation:

    G-B-is-ok : ∀ {Γ A} → Γ ⊩ (⊥c ⊃ A)
    G-B-is-ok = G-I (G-B (G-A Z))

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.

But, is this system still of equal expressive power to Hilbert-style systems? Wikipedia claims so, let’s prove it:

    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.

Homework

• What is the answer to the very first question of this article?
• Try to understand both logical and computational (proof sequences/trees transformations) semantics of the proofs above.
• Note how we proved equivalence of Hilbert-style sequence and Gentzen-style tree by moving through Hilbert-style tree. Can you prove h→g and g→h directly?
• Does any of the following hold?
  • h→t (t→h p) ≡ p
  • t→h (h→t p) ≡ p
  • g→t (t→g p) ≡ p
  • t→g (g→t p) ≡ p
  Do we care? What can we do about it?
• Open an empty Emacs buffer and try to reimplement everything from scratch without peeking at the code here.
• Extend IPC⟨→⟩ with ∧ and ∨ connectives and extend the above proofs to work in the resulting system.
• Prove that our formulation of IPC⟨→⟩ is equivalent to the original one of Hilbert [4].

Conclusions

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.

Also, Hilbert-style formulation of only using modus ponens as an inference rule indeed only appears to simplify things. In practice, it makes things much harder. Which is why most modern logical systems are Gentzen-style.

I hope you had as much fun while inspecting these proofs as I had while writing them.

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.

Credits

• ∈ relation was stolen from Rob Simmons’ Agda library [6].
• First version of these proofs was done in collaboration with Alex Kasatkin on TTFV implementation meeting. The current version is a from-scratch reimplementation (I did my own homework) with simplified proofs.

Follow-ups

• @mietek on GitHub published his extension of this to the complete IPC, also in Agda.

References