Building a Sequent Calculus Toolbox

After finishing the first section of this tutorial, I realized it was getting quite long and therefore decided to split it into multiple posts. Part two of the tutorial can be found here.

This article is a small tutorial on the use of the calculus toolbox for defining and generating Isabelle theory files and a graphical interface for a logic calculus. This tutorial is similar to the introduction guide to the calculus toolbox, however here I will try to showcase the work flow and the decisions and modifications that needed to be made, to formalize a new or different version of a calculus, starting from a template calculus.

In this tutorial, we will be taking a look at the LK (or "klassische Prädikatenlogik") sequent calculus, described in this wikipedia article. Due to the current restriction of the toolbox, namely the lack of support for quantifiers in calculi, only a fragment of the LK calculus without the \(\exists\) and \(\forall\) quantifiers will be formalized in this article.

Formally defining the LK calculus terms

To begin, we need a formal definition of the terms of this calculus. Looking at the rules of the LK system we can define the formulae of this sequent calculus fragment in the following manner:

\(F:= ap \in \mathsf{AtProp} \mid F \land F \mid F \rightarrow F \mid \neg F\)

The following section describes the sequents that are built up from formulas.

• \(\vdash\) known as the turnstile, separates the assumptions on the left from the propositions on the right
• A and B denote formulae of first-order predicate logic (one may also restrict this to propositional logic),
• \(\Gamma\), \(\Delta\), \(\Sigma\), and \(\Pi\) are finite (possibly empty) sequences of formulae (in fact, the order of formulae do not matter; see subsection Structural Rules), called contexts,
• when on the left of the \(\vdash\), the sequence of formulas is considered conjunctively (all assumed to hold at the same time),
• while on the right of the \(\vdash\), the sequence of formulas is considered disjunctively (at least one of the formulas must hold for any assignment of variables),

Formally we can write this definition as:

\(S:= F \mid S , S\)

where the inductively defined formulas \(F\) are composed into structures \(S\). Two structures on either side of a turnstyle then make up sequents:

\(S \vdash S\)

Note that our formal definition of the LK fragment's terms differs somewhat from the wikipedia article definition, in that it builds the sequences of formulas as trees rather than sequences/lists. This means that the rules of the calculus will have to handle associativity explicitly, and therefore, this formalization will include additional rules not found in the wikipedia article.

However, before trying to formalize these extra rules, we first need to formalize the structure of the terms in a such a way, that the toolbox can parse and create the necessary Isabelle theories and Scala code. In order to do this, we can start with a template JSON file, which encodes DCPL (display classical propositional logic), similar to the LK fragment in its terms and some rules. Even though DCPL is a display calculus, little modification of the JSON file is needed to encode the Sequent calculus.

Encoding the terms in the JSON description file

To encode the LK calculus fragent into a format which the toolbox can use, we need to make/download a copy of the template calculus, which we will be modifying.

Next, change the name of the calculus, encoded in this line, to "SequentCalc".

Having done the previous two steps, we can focus on the section of the JSON file encoding the terms of the calculus, found right underneath the above code, which needs to be modified to correspond to our earlier inductive definition of the calculus terms.

Looking at a code snippet below, it is clear that the DCPL terms are very similar to the Sequent calculus terms:

"Atprop" : {
    "Atprop" : {
       "type" : "string",
       "ascii" : "_",
       "latex" : "_"
    },
    "Atprop_Freevar" : {
       "type" : "string",
       "isabelle" : "?\\<^sub>A _",
       "ascii" : "A? _",
       "latex" : "_",
       "precedence": [320, 320]
    }
  },
  
  "Formula" : {
    "Formula_Atprop" : {
       "type": "Atprop",
       "isabelle" : "_ \\<^sub>F",
       "precedence": [320, 330]
    },
    "Formula_Freevar" : {
       "type" : "string",
       "isabelle" : "?\\<^sub>F _",
       "ascii" : "F? _",
       "latex" : "_",
       "precedence": [340, 330]
    },
  .
  .
  .
  

The only differences between the terms of the template calculus and the sequent calculus are in fact the following:

• The formulae of the template calculus don't include the unary \(\lnot\) operator
• The template calculus includes two structural connectives, the comma \(;\) and the implication \(>>\) , whereas the sequent caculus only uses the comma.

To address the first difference, we add a Formula_Un constructor to the type Formula:

"Formula_Un" : {
    "type" : ["Formula_Un_Op", "Formula"],
    "isabelle" : "U\\<^sub>F _",
    "isabelle_se" : "_",
    "precedence": [330, 331]
  }
  

To explain what the entries in the JSON encoding mean, have a look at the calculus encoding page of the documentation.

Once we define the Formula_Un constructor, we need to define the actual not operator:

"Formula_Un_Op" : {
    "Formula_Not" : {
      "isabelle" : "\\<not>\\<^sub>F",
      "ascii" : "-",
      "latex" : "\\lnot"
    }
  }
  

match_Formula (Formula_Bin var11 op1 var12) x = (case x of 
    (Formula_Bin var21 op2 var22) ⇒ 
      (if op1 = op2 then 
        (match var11 var21) @m (match var12 var22) 
      else []) | 
    _ ⇒ [])
  

To address the second difference to the template calculus, namely the extra structural connective, we simply delete the Structure_ImpR entry under Structure_Bin_Op in the JSON file.

Encoding the rules of the LK fragment

Now that the terms of out Sequent calculus fragment are defined, we can move on to the rule encoding. Following the template, the rules first need to be declared in the calc_structure_rules section of the file and then encoded using the ASCII defined terms in the latter part of the JSON file. We will take a look at a few key rules to demonstrate the encoding.

Logical rules

The first interesting rule is the \(\vee L\) rule:

\[\frac{\Gamma , A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \vee B \vdash \Delta , \Pi} (\vee L)\]

To encode thus rule, we need to do two things. firstly, we need to declare the rule in calc_structure_rules section of the JSON decription file. We create a new section for logical rules in calc_structure_rules, called RuleL:

"calc_structure_rules" : {
    "RuleL" : { }
  }
  

Now add the folowing entry to RuleL:

"Or_L" : {
    "ascii" : "Or_L",
    "latex" : "\\vee L"
  }
  

This encodes the name of the rule and the sugar used for LaTeX typesetting of the rule label. The ASCII encodes the reserved name for the rule, used for generating the ASCII parser and to-string functions (the parser and the to-string functions are used to store and retrieve prooftrees generated by the calculus toolbox UI).

We can now proceed formalizing the rule itself by adding RuleL to the rule section of the JSON file and encoding Or_L. After adding the \(\vee L\) rule, the JSON file should look something like this:

"rules" : {
    "RuleL" : {
      "Or_L" : ["(?X, ?Z), F?A \\/ F?B |- ?Y, ?W",  "?X, F?A |- ?Y", "?Z, F?B |- ?W"]
    }
  }
  

The rest of the logical rules were formalized in a similar fashion and can be found in the following section of the Sequent.json file.

Structural rules

We now turn our attention to the structural rules of the calculus. We deviate from the wikipedia formalization of the structural rules, relaxing them somewhat, by replacing the formulas \(A\) and \(B\) by structures, \(\Lambda\) and \(\Phi\). I will not discuss the motivation for this change in great detail here, but will dedicate a section on this later, where I will also show that these rules are interchangeable with the ones formalized in the wikipedia article. The short answer I will give now boils down to: it makes things easier and more consistent, as we have already introduced two structural rules \(A_L\) and \(A_R\), which follow this convention.

The first structural rule we take a closer look at, is the \(CL\) rule of the Sequent calculus:

\[\frac{\Gamma , A , A \vdash \Delta}{\Gamma , A \vdash \Delta} (CL)\]

Since we decided to allow replace the single formula \(A\) with a structure, the rule becomes:

\[\frac{\Gamma , \Lambda , \Lambda \vdash \Delta}{\Gamma , \Lambda \vdash \Delta} (CL)\]

As with the \(\vee L\) rule, the \(CL\) rule contains an ambiguous case of bracketing in the term \(\Gamma , \Lambda , \Lambda\). The rule was encoded with the term bracketed in the following way: \(\Gamma , (\Lambda , \Lambda)\).

This bracketing will hopefully seem intuitive after looking at the parse trees, corresponding to the \(CL\) rule, below.

The last rule we will look at in detail is the \(PL\) rule, rewritten below, with \(A\) and \(B\) already replaced with the structural variables \(\Lambda\) and \(\Phi\).

\[\frac{\Gamma_1 , \Lambda, \Phi, \Gamma_2 \vdash \Delta}{\Gamma_1 , \Phi, \Lambda, \Gamma_2 \vdash \Delta} (PL)\]

Our well-bracketed version of this rule is the following one:

\[\frac{(\Gamma_1 , \Lambda), (\Phi, \Gamma_2) \vdash \Delta}{(\Gamma_1 , \Phi), (\Lambda, \Gamma_2) \vdash \Delta} (PL)\]

The intuition behind this bracketing comes from the way this rule manipulates the terms. The bracketing above makes the parse trees look symmetric, manipulating the two subtrees \(\Lambda\) and \(\Phi\) at the same level in the tree:

Additional rules

As was mentioned earlier, due to the way we defined our structural terms, we need to add extra rules to our version of the calculus on top of the ones defined in the wikipedia article.

We have already seen two of these rules, the \(A_L\) and \(A_R\). Next, we need to introduce rules for the structural connective \(I\).

At this point, you might say, hang on, what is \(I\)? Where was it introduced and defined? Well, the answer is that I snuck the \(I\) in without telling you. The reason for the nullary connective \(I\) is to simulate the empty list in a way. Let's say we have a sequent '\(\vdash A \vee \lnot A\)' seen in the section of the article showing some example derivations in the LK calculus.

At first sight, this sequent is not a valid term in our calculus, since the right hand side contains a structure whilst the left hand side appears to be empty. Now, according to our definition, a sequent consists of two structures, one on either side of the turnstile. However, if we look at the article's definition of a sequent, we can see that the turnstile separates sequences (or, as I prefer, lists) of formulas. Since a list can be empty, it is perfectly fine to have (an empty) one on either side of the turnstile. (Note to self: Does that mean that '\(\ \vdash\ \)' is technically a well formed, albeit slightly useless, term of the LK calculus?)

Since we do not have lists, but rather trees of formulas, we introduce the nullary \(I\) to represent the notion of an empty tree rather than an empty list. We therefore have to modify the definition of structures to include the \(I\):

\(S:= F \mid S , S \mid I\)

The sequent '\(\vdash A \vee \lnot A\)' , rewritten in our calculus thus becomes '\(I \vdash A \vee \lnot A\)'.

The following rules involving the \(I\) were added to our calculus (all the rules below are reversible):

\[\frac{\Gamma \vdash \Delta}{I, \Gamma \vdash \Delta} (I_{LL})\] \[\frac{\Gamma \vdash \Delta}{\Gamma, I \vdash \Delta} (I_{LR})\] \[\frac{\Gamma \vdash \Delta}{\Gamma \vdash I, \Delta} (I_{RL})\] \[\frac{\Gamma \vdash \Delta}{\Gamma \vdash \Delta, I} (I_{LR})\]

The motivation for the above rules comes from the following property of lists: \([] + A = A = A + []\) which states that the empty list is the neutral or the identity element which, if concatenated with a list \(A\), produces \(A\) again.

To show why these rules are necessary, let's have a look at the proof of derivability of '\(\vdash A \vee \lnot A\)' in the sequent calculus. The fist step of the proof uses the \(CR\) rule to duplicate the formula \(A \vee \lnot A\) on the right hand side:

\[\frac{\displaystyle \frac{\vdots}{\vdash A \vee \lnot A, A \vee \lnot A}}{\vdash A \vee \lnot A} (CR)\]

The \(CR\) rule in the article calculus can be applied to a sequent of the shape \(\Gamma \vdash A, \Delta\). As we have already stated, this formalization uses lists so '\(\vdash A \vee \lnot A\)' can actually be rewritten as '\([] \vdash A \vee \lnot A, []\)'. In order to be able to apply the \(CR\) rule in our calculus, we have to do something similar:

\[\frac{\displaystyle \frac{\displaystyle \frac{\displaystyle \frac{\vdots} {I \vdash A \vee \lnot A, A \vee \lnot A}} {I \vdash (A \vee \lnot A, A \vee \lnot A), I}} {I \vdash A \vee \lnot A, I} } {I \vdash A \vee \lnot A}\]

First, we introduce the \(I\) on the right side of the right structure (rule \(I\_{RR}\)), only then we can apply the \(CR\) rule. Finally, we apply the reverse of the \(I_{RR}\) rule to get rid of the \(I\) on the right.

For now, we will omit the \(Cut\) rule from our formalization and revisit it in the next section.

This concludes the first part of the tutorial. In part two, we will have a look at how to use the calculus description file we created (available here for reference) to compile a Sequent calculus toolbox.