Sequent: A Fitch-Style First-Order Logic Proof Language

I recently deployed the Sequent proof language!

For many years, even after earning my master’s degree in computer science, I have been a teaching assistant on the course Logic in Computer Science at the University of Copenhagen. Historically, the course has used BoxProver for the first part of the course concerning natural deduction in first-order logic. While I love BoxProver, the fact that it is basically a frontend built on Twelf often results in students struggling with the syntax, error messages, and proof composition. So I decided to design and implement a language specifically for teaching Fitch-style natural deduction.

Sequent is a small proof language for natural deduction in propositional and first-order logic. The web application provides a proof checker, script formatter, proof renderer, and clickable diagnostics.

The main goals of the Sequent language are:

Being syntactically close to the notation used in various textbooks.
Supporting proof composition and custom rule declaration as first-class language features.
Abstracting away low-level machinery by inferring substitutions from conclusions and rule applications.
Providing helpful and user-friendly error/warning messages.

Web Interface#

The quickest way to try out Sequent is through the accompanying web application. The web application provides:

Editor with Sequent syntax highlighting.
Check Format, and Share actions.
Rendered proof tabs with closed/open/failed status.
Clickable proof lines and diagnostic locations.
Hidden proofs omitted from the proof tab bar with %hide.
Inline proof rendering with %inline.
An extensive help page with various examples.
An illustrative starter program on first visit.

While the editor is focused, Ctrl+Enter (or Cmd+Enter on MacOS) runs the proof checker. If all proofs are sound, the proof renderer becomes focused and ←/→ lets you navigate through the different proofs. If there are one or more errors, the first error location is automatically highlighted in the editor. Clicking on a rendered proof line moves the editor’s cursor to the corresponding source line.

Local Proof Checking#

If you want to try out Sequent on your local machine, you can download prebuilt binaries for all major platforms here, or build it from source as described in the README.

If you want to contribute, please follow the associated branching model.

Language Overview#

A Sequent program contains declarations and directives. A proof declaration has a name, a sequent, and a bracketed proof body:

identity : p |- p [
    l1: p  by premise;
    l2: p  by copy l1;
]

Each proof line includes a label, a derived formula or sequent, the by marker, a rule name, zero or more references, and a semicolon.

Boxes introduce local assumptions:

self_implication : |- p => p [
    @box [
        l1: p    by assumption;
        l2: p    by copy l1;
    ]
    l3: p => p   by imp_i @box;
]

Boxes can also introduce an arbitrary variable for first-order rules:

universal_identity : all x. P(x) |- all y. P(y) [
    l1: all x. P(x)  by premise;
    @any [ var y0;
        l2: P(y0)    by all_e l1;
        l3: P(y0)    by copy l2;
    ]
    l4: all y. P(y)  by all_i @any;
]

Formula Syntax#

Meaning	Syntax
Negation	`~p`
Conjunction	`p /\ q`
Disjunction	`p \/ q`
Implication	`p => q`
Falsity	`bot`
Truth	`top`
Universal quantifier	`all x. P(x)`
Existential quantifier	`exi x. P(x)`
Equality	`a = b`
Predicate application	`P(a, f(b))`
Sequent	`p, q \|- r`
Rule judgment	`(p \|- q), (\|- p) \|\|- q`

Predicate and function symbols use parentheses for arguments. Nullary symbols do not need parentheses.

Built-In Rules#

Common rules include:

premise, assumption, copy
con_i, con_e1, con_e2
dis_i1, dis_i2, dis_e
imp_i, imp_e
neg_i, neg_e, bot_e
all_i, all_e, exi_i, exi_e
eq_i, eq_e

Classical mode adds classical rules such as dne.

Composition#

You can define a reusable rule with ||-:

imp_e_from_box : (p |- q), (|- p) ||- q [
    l1: p |- q  by premise;
    l2: |- p    by premise;
    l3: p => q  by imp_i l1;
    l4: q       by imp_e l2 l3;
]

use_rule : p, p => q |- q [
    l1: p        by premise;
    l2: p => q   by premise;
    @box [
        l3: p    by assumption;
        l4: q    by imp_e l3 l2;
    ]
    l5: q        by imp_e_from_box @box l1;
]

You can call a proved theorem as a rule with proof:

and_flip : p /\ q |- q /\ p [
    l1: p /\ q  by premise;
    l2: q       by con_e2 l1;
    l3: p       by con_e1 l1;
    l4: q /\ p  by con_i l2 l3;
]

use_helper : a /\ b |- b /\ a [
    l1: a /\ b  by premise;
    l2: b /\ a  by proof and_flip l1;
]

Declarations without proof bodies act as given facts or imported theorems:

given_commutativity : p /\ q |- q /\ p;

Language Features for the Web Application#

%hide keeps helper proofs available to the checker but removes them from the proof tabs, and %expand asks the renderer to expand a subproof:

%hide and_flip : p /\ q |- q /\ p [
    l1: p /\ q  by premise;
    l2: q       by con_e2 l1;
    l3: p       by con_e1 l1;
    l4: q /\ p  by con_i l2 l3;
]

use_helper_inline : a /\ b |- b /\ a [
    l1: a /\ b  by premise;
    l2: b /\ a  by %inline proof and_flip l1;
]

%hide declaration ... hides a declaration from the web proof tabs.
%inline and %noinline can be used on individual rule applications.

Directives#

Directives affect later declarations.

%mode cfl;
%mode ifl;
%alias right con_e2;

%mode cfl; enables classical first-order logic.
%mode ifl; switches back to intuitionistic first-order logic.
%alias new_name existing_rule; introduces a rule alias.

Term Parameters and Fresh Boxes#

First-order Fitch proofs often need a temporary arbitrary object, sometimes called an eigenvariable. In Sequent, those variables are introduced explicitly inside boxes:

@any [ var a;
    l1: P(a)   by assumption;
    l2: P(a)   by copy l1;
]

The box above is inferred to have a sequent type with a term parameter:

[var a] P(a) |- P(a)

That type matters when boxes are passed to rules. For example, universal introduction can generalize a formula proved with a fresh term:

universal_equality : |- all x. x = x [
    @any [ var a;
        l1: a = a      by eq_i;
        l2: a = a      by copy l1;
    ]
    l3: all x. x = x   by all_i @any;
]

Rule declarations can also mention term parameters in their premise sequents. This makes wrappers for first-order rules possible:

double_all_i : ([var x, y] |- P(x, y)) ||- all x. all y. P(x, y) [
    p  : [var x, y] |- P(x, y)       by premise;
    l1 : [var x] |- all y. P(x, y)   by all_i p;
    l2 : all x. all y. P(x, y)       by all_i l1;
]

The [var x, y] part is not an extra assumption. It says that x and y are fresh term parameters for the box proof. When the rule is used, the checker matches the inferred box type against the rule premise type and substitutes the caller’s fresh names coherently.

For now, term parameters belong in boxes and in rule premise sequents, not in standalone sequent declarations. A declaration such as [var x] |- P(x) is therefore rejected at the top level; write a rule judgment with a term-parameter premise when you want reusable arbitrary-object structure.

By contrast, ordinary constants that simply appear in a proof body are inferred as global terms:

body_constant : |- P(t) => P(t) [
    @box [
        l1: P(t)       by assumption;
        l2: P(t)       by copy l1;
    ]
    l3: P(t) => P(t)   by imp_i @box;
]

Here t is not arbitrary in the eigenvariable sense. It is just a term symbol used by the proof. This keeps proofs lightweight while preserving the important side condition for quantifier rules: fresh, scoped eigenparameters still have to be introduced explicitly with var (or the alias term).

The Implementation#

Sequent was implemented in Haskell. Even the web application (frontend excluded) is built in Haskell, specifically with Scotty.

Though my dayjob is developing software in C/C++, Haskell has a special place in my heart from my university days. Haskell shines especially when it comes to implementation of programming languages, with its algebraic datatypes and support for monadic computation.

In the future, I might do a writeup on the design and implementation details of Sequent, or maybe on Haskell in general. Until then, you’re welcome to browse the Sequent repository (though it might not yet be fully polished). (☞ﾟヮﾟ)☞

Demo: The Drinker’s Paradox 🍺#

A small, nontrivial demonstration would probably be appropriate, so here is a proof for the famous drinker’s paradox written in Sequent. ( ´ ∀ `)ノ

%mode cfl;

drinkers_paradox : |- exi x. (P(x) => all y. P(y)) [
    @refute_goal [
        l1  : ~(exi x. (P(x) => all y. P(y)))           by assumption;
        @candidate [
            l2  : P(t)                                  by assumption;
            @arbitrary_y [ var y0;
                @refute_py [
                    l3 : ~P(y0)                         by assumption;
                    @vacuous_candidate [
                        l4 : P(y0)                      by assumption;
                        l5 : bot                        by neg_e l4 l3;
                        l6 : all y. P(y)                by bot_e l5;
                    ]
                    l7 : P(y0) => all y. P(y)           by imp_i @vacuous_candidate;
                    l8 : exi x. (P(x) => all y. P(y))   by exi_i l7;
                    l9 : bot                            by neg_e l8 l1;
                ]
                l10 : ~~P(y0)                           by neg_i @refute_py;
                l11 : P(y0)                             by dne l10;
            ]
            l12 : all y. P(y)                           by all_i @arbitrary_y;
        ]
        l13 : P(t) => all y. P(y)                       by imp_i @candidate;
        l14 : exi x. (P(x) => all y. P(y))              by exi_i l13;
        l15 : bot                                       by neg_e l14 l1;
    ]
    l16 : ~~(exi x. (P(x) => all y. P(y)))              by neg_i @refute_goal;
    l17 : exi x. (P(x) => all y. P(y))                  by dne l16;
]

Exercises for the Reader#

As a final note, here are some exercises for the reader. (・_・ヾ

// First-order logic exercises
// Solve the exercises by defining the proof bodies.
// (H&R = Logic in Computer Science by Huth and Ryan)

// H&R Exercise 1.2.1(b)
ex_1_2_1_b : p /\ q |- q /\ p;

// H&R Exercise 1.2.1(f)
ex_1_2_1_f : |- (p /\ q) => p;

// H&R Exercise 1.2.1(h)
ex_1_2_1_h : p |- (p => q) => q;

// H&R Exercise 1.2.1(l)
ex_1_2_1_l : p => q, r => s |- (p \/ r) => (q \/ s);

// H&R Exercise 1.2.3(c)
ex_1_2_3_c : p \/ q, ~q |- p;

// H&R Exercise 1.2.1(y)
ex_1_2_1_y : (p /\ q) \/ (p /\ r) |- p /\ (q \/ r);

// H&R Exercise 1.2.3(n)
ex_1_2_3_n : p /\ q |- ~(~p \/ ~q);

// H&R Exercise 1.2.3(q), using LEM
ex_1_2_3_q : |- (p => q) \/ (q => r);

// H&R Exercise 2.3.1(a)
ex_2_3_1_a : (y = 0) /\ (y = x) |- 0 = x;

// H&R Exercise 2.3.7(c)
ex_2_3_7_c : exi x. all y. P(x, y) |- all y. exi x. P(x, y);

// H&R Exercise 2.3.9(a)
ex_2_3_9_a : exi x. (S => Q(x)) |- S => exi x. Q(x);

// H&R Exercise 2.3.9(k)
ex_2_3_9_k : all x. (P(x) /\ Q(x)) |- (all x. P(x)) /\ (all x. Q(x));

// H&R Exercise 2.3.11(c)
ex_2_3_11_c : exi x. exi y. (H(x, y) \/ H(y, x)),
              ~(exi x. H(x, x))
              |- exi x. exi y. ~x = y;

you've reached the end of the post
bye for now ~ (๑˃ᴗ˂)ﻭ