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

I recently deployed the web interface for 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 web UI 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 is focused, and Left/Right lets you navigate through the different proofs. Clicking on a rendered proof line moves the editor’s cursor to the corresponding source line.

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#

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;

Use bodyless declarations only when the exercise or library explicitly grants them, since the checker trusts their declared type.

Language Features for the Web Application#

%hide keeps helper proofs available to the checker but removes them from the proof tabs:

%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;
]

You can also ask the renderer to expand a call with %inline:

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.