Building a Sequent Calculus Toolbox - Extra

This the final part of a tutorial on building a sequent calculus toolbox in Isabelle and Scala. There is part one, two and three if you have not read those yet.

This is an extra aside to the tutorial on the calculus toolbox, where we will focus on the shallow embedding of the calculus, produced by the calculus-toobox build script along with the deep embedding used by the UI (which was discussed in the previous part of this guide). I will not discuss the difference between the shallow and the deep embedding, and will instead refer you to the documentation, which discusses this topic is some detail.

I will instead focus on showcasing the use of the shallow embedding, by formalizing the wikipedia article version of the Sequent calculus fragment and the prove it equivalent to our own version.

Just to recap, the main point of difference between our formalization of the Sequent calculus and the one found in the wikipedia article arises from the encoding of structures. In the wiki calculus, sequents are made up of two lists of formulas separated by the turnstile \(\vdash\). Our version of the calculus uses trees of formulas instead, which, amongst other things, means we have to handle associativity explicitly. We have also introduced four reversible rules for the nullary connective \(I\), which acts like the empty list in our calculus.

The definition of the shallow terms of our sequent calculus can be found in the calculus folder under src/isabelle/SequentCalc_Core_SE.thy and the formalization wiki calculus can be found in /extras/SequentCalculus.thy.

As this part of the tutorial is mostly an aside, the extras folder has not been included in the files downloadable for this tutorial. All of the files are instead available in the precompiled version of the sequent calculus toolbox in the github repository.

Defining the shallow embedding of the wiki Sequent calculus

Since the calculus in the wikipedia article is pretty much the same as our implementation, we can make our lives easier by reusing as many definitions of the calculus terms as possible. This practically means we only have to redefine sequents to be lists of formulas rather than trees (as is the case in our version of the calculus).

Since we do not want to have duplicate definitions of formulas, we import SequentCalc_Core_SE.thy at the begining of the /extras/SequentCalculus.thy file and then define a new datatype sequent, that corresponds to the wiki calculus definition:

datatype sequent = sequent "Formula list" "Formula list" (infix "⊢" 300)

Here, we make use of Isabelle's implementation of lists (part of Isabelle core libraries), which means we automatically have many lemmas about the general properties of lists available to us, These will come in handy when proving equality between the two versions of the sequent calculus.

The next definition in /extras/SequentCalculus.thy introduces the comma as sugar notation for the concat/append function on lists:

definition concat :: "Formula list ⇒ Formula list ⇒ Formula list" (infix ";" 400) where
  "concat list1 list2 = list1 @ list2"

This function serves a purely visual function, making our sequent terms look closer to the notation introduced in the wikipedia article.

Note however that there are still slight differences between the presentation of the terms of this calculus to the wikipedia version. In the wikipedia article, the comma is used ambiguously, for example in the term \(\Gamma \vdash \Delta_1, A , B, \Delta_2\), different commas inside the term could have all of the type signatures below:

Because we did not want the comma to be ambiguous, we chose one type signature for the comma, namely:

\[, :: [Formula] \Rightarrow [Formula] \Rightarrow [Formula]\]

As a result, we enclose any singleton formulas in a list, so that \(\Gamma \vdash \Delta_1, A , B, \Delta_2\) becomes \(\Gamma \vdash \Delta_1, [A] , [B], \Delta_2\).


The rest of the theory file contains the rules of the wiki sequent calculus.

Equality proof

Now that we have a definition of the wiki sequent calculus, we can open up another theory file in the extras folder called SequentCalculusEq.thy. This theory file, as the name suggests, contains the proofs of equality between our version of the calculus and the wiki version.

The proof of equality is split into two lemmas, corresponding to a proof of derivability of all sequents in our version of the calculus in the wiki version and vice versa:

lemma sequentCalc_SE_to_sequentCalculus_derivable:
    fixes loc f
    assumes "loc ⊢d seq"
    and "loc = [CutFormula f]"
    shows "[f] ⊢D (>> seq)"
  
lemma sequentCalculus_to_sequentCalc_SE_derivable:
    fixes loc
    assumes "loc ⊢D seq"
    and "loc = [f]"
    shows "[CutFormula f] ⊢d (<< seq)"

Prerequisites

In order to formulate the equality lemmas between the two versions of the caclulus, we need to defines the functions that translate a term in one version of the calculus to a term in the other. These functions are used in the lemmas formulated above, \(>> \ \Psi\) standing for a function that takes a sequent \(\Psi\) from our version of the calculus and produces the wiki calculus term and the \(<< \ \Theta\) doing the converse for a term \(\Theta\) in the wiki calculus.

One should bear in mind that composing \(>>\) and \(<<\) does not always yield an identity function, for example applying \(<< \circ >>\) (this composed function takes a term in our calculus and produces a term of our calculus) to the following bracketed term \((\Delta, \Sigma), \Gamma \vdash \Pi\) will yield \(\Delta, (\Sigma, \Gamma) \vdash \Pi\).

However, the opposite direction, namely \(>> \circ <<\), is in fact the identity function.