What is this?

The Sequent Calculus Verifier (SeCaV) is a one-sided sequent calculus embedded in the logic of the Isabelle proof assistant. Sequents are represented as lists of formulas. Since the calculus is one-sided, it has rules not only for each connective, but also for the negation of each connective.

This page explains how to use SeCaV to prove formulas in first-order logic. The reader is assumed to know how proofs in sequent calculus work, see e.g. System G in Mathematical Logic for Computer Science by Mordechai (Moti) Ben-Ari.

If you are already familiar with SeCaV, or if you want to try it out immediately, click here to jump to some example proofs.

Copyright information

Copyright © 2021 Asta Halkjær From, Frederik Krogsdal Jacobsen, Emmanuel André Ryom & Jørgen Villadsen

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Source code from other authors is used and the license agreements may be viewed here.

How to use SeCaV

SeCaV requires that the Isabelle proof assistant must be installed. SeCaV is embedded in such a way that formulas that we want to prove in SeCaV are defined as lemmas in Isabelle, which verifies the SeCaV proof of the formula.

You will need the file SeCaV.thy, which defines the calculus. To use SeCaV, your Isabelle theory must import SeCaV using the following line, which should be placed at the top of your file:

theory Example imports SeCaV begin

The SeCaV file must be in the same directory as any files that use SeCaV. The name of the theory ("Example" above) must be the same as the name of the file containing it, except the extension ".thy", which should not be included.

At the end of the file, you must add a line containing the keyword end to match the keyword begin above.

You might already have noticed that Isabelle will complain and highlight some lines of your file in red if there is some mistake, such as forgetting a matching keyword or bracket. Isabelle will also highlight any proofs that it cannot verify in red to let you know there is an error.

Isabelle continuously checks whether your proofs are correct, so there is no "compile" or "commit" step like you might be used to from programming.

How to write a lemma in SeCaV

Before we can start to prove things using SeCaV, we need to know how to express the formulas we want to prove.

While it is possible to write SeCaV formulas and proofs directly into Isabelle, the SeCaV Unshortener makes this process much easier. The SeCaV Unshortener allows you to write multiple proofs in the same window by separating them with minuses (-) or hashes (#). The Unshortener has an integrated prover that adds a warning if it finds a mistake in your proof, but for formal verification you must still copy and paste the proofs into Isabelle. An optional comment in quotes may follow either of these symbols, and will then be included in the generated SeCaV Isabelle proof text as either a piece of text (for minuses) or a section header (for hashes). It is also possible to insert comments delimited by (* and *) at any point, though these comments will not be included in the output.

Terms: functions, constants and variables

The syntax of SeCaV consists of terms and formulas. A predicate must be applied to a list of terms, and we will begin by explaining how to write these, as they are simpler than the formulas.

In SeCaV, terms are either function applications, which consist of a function name and a list of terms to apply the function to, or variables, which are written as numbers for reasons that will be explained later. In SeCaV, functions do not have names like we are used to from mathematics or programming, but are instead identified by a (natural) number. The SeCaV Unshortener will automatically convert the function names we use into appropriate numbers. Names must start with a letter, but the rest of the name can contain numbers, underscores (_) and ticks ('). Functions are always applied to a list of arguments, which must also be terms. Lists are written using the syntax [a, b, c].

A constant may be represented as a function applied to no arguments, i.e. a function applied to the empty list of terms, which may be written as [] or simply omitted.

Let's look at some examples. A constant may be written as a. The name a is completely arbitrary. A different constant could thus be written as b, and these two constants could be used in the same formula. Note that a and A are different constants, since the names are case sensitive.

It is of course also possible to write functions which are not constants. As an example, consider the following expression: f[a, b]. This expression applies function f, which is a function with two arguments, to functions a and b, which are both constants since they do not take any arguments. To use the same function twice in a formula, just write the same name in both places.

The variables in SeCaV are meant to be used with the first-order quantifiers of the logic. We will thus return to variables when we introduce the quantifiers.

Both constants (i.e. functions with no arguments) and variables are meant to represent values in some domain, while functions represent functions over the domain. The domain can be any non-empty set, e.g. the natural numbers or the lines in a program.

Formulas: predicates, logical connectives, and quantifiers

To state a lemma in SeCaV we need to write a formula, which can be either a predicate or a number of subformulas connected by logical connectives and quantifiers.

The basic building block of SeCaV formulas are predicates, which take a list of terms as arguments, and are written by writing their names. Predicates represent mappings from the arguments of the predicate to truth values. Since the arguments are terms, we may think of predicates as mappings from domain values to truth values. Just like with functions, it is possible to define constant predicates (relative to the domain) by letting the list of arguments be the empty list or by omitting it.

Like functions, predicates do not have names as such, but are instead identified by a number. Again, the SeCaV Unshortener will automatically convert the predicate names we use into appropriate numbers. These names are completely separate from the names used to identify functions, so it is not an issue to have both a function and a predicate named e.g. a, though this may lead to some confusion.

An interpretation in SeCaV contains a domain of values, an environment mapping variables to elements of the domain, a mapping from the identifier of each function to a function (which might be a constant) over the domain, and a mapping from the identifier of each predicate to a predicate over the domain. The interpretation we choose determines the truth value of each of the predicates in a formula. Whatever domain we are currently working in is often called the universe because it contains everything that we might want to consider in our formulas.

Logical connectives

Formulas can be combined using logical connectives. All of these connectives are applied to two existing formulas except the negation operator, which is only applied to one. A list of the connectives available in SeCaV can be found in the first part of the table below. We note that these connectives are more than enough to define any other connective one might want. Note also that the connectives are applied in the style of functional programming, i.e. by writing Imp A B and not by writing Imp(A, B).

Using these connectives and the syntax described above, we may write any formula of propositional logic as a lemma. A simple example is the formula P → P, which may be written as Imp P P. Notice that propositional variables are simply predicates with no arguments, i.e. predicates which are assigned a truth value independently of the domain used in the interpretation. The lemma ⊢ P → P (which means "P → P can be proved") can be written in the SeCaV Unshortener by simply writing down the formula.

If you write this into the SeCaV Unshortener, it will give you an error saying that it expects a proof rule. Proof rules are the steps that you can instruct the SeCaV system to take when proving a lemma. We will return to these shortly.

Quantifiers

To go from propositional logic to first-order logic, we now introduce first-order quantifiers, which are special operators that specify the quantity of elements in the domain that satisfy some formula. In the logic of SeCaV, we have only two quantifiers, those being the universal and existential quantifiers.

The universal quantifier is written using the symbol ∀ in usual notation, and it specifies that all elements of the domain satisfy the formula following the quantifier.

The existential quantifier is written using the symbol ∃ in usual notation, and it specifies that some (i.e. at least one) element of the domain satisfies the formula following the quantifier.

You have probably already seen these quantifiers in various other contexts. The quantifiers in SeCaV are essentially the usual quantifiers known from mathematics, except the quantifiers in SeCaV always quantify over the entire domain. It is thus not necessary to note which set we are quantifying over (by writing e.g. ∀ x ∈ S for some set S), since this is implicitly known to be the entire domain.

A quantifier binds a variable, which represents the elements of the domain that the quantifier specifies in the formula following the quantifier. In usual notation we might for example write ∀ x . P(x) to mean that some predicate P is true for all elements of the domain or ∃ x . ∀ y . P(x) → Q(y) to mean that there is some element of the domain, which we bind to the variable name x, for which it holds that, if the predicate P holds for that element, the predicate Q holds for all elements of the domain.

In SeCaV, we do not want to have to keep track of the names of variables, so instead of identifying variables by conventional names, we will identify them by numbers. The numbering system we use for variables is a bit complicated, since we need to keep track of the quantifier that binds each variable. To do this we use so-called de Bruijn indices to identify the variables. The idea is to number the variables "from the inside out" so that the variable with index 0 is always bound by the innermost quantifier, and so on. Using de Bruijn indices, the formula

∀ x . ∀ y . ∀ z . P(x) → Q(y) → R(z)

∀ ∀ ∀ (P(2) → Q(1) → R(0)) .

Note that the same index may be used for different variables if we have multiple "branches" within the formula, just like how we may usually use the same variable name in several places as long as their scopes do not overlap. Consider for example the formula

∃ x . (∀ y . P(y) ∧ Q(x)) → (∀ y . Q(x) ∧ P(y))

∃ (∀ (P(0) ∧ Q(1))) → (∀ (Q(1) ∧ P(0)))

As mentioned previously, the reason for using de Bruijn indices is that we don't want to keep track of variable names. One reason for this is that the semantics of the SeCaV system depend on being able to identify variables. Recall that an interpretation in SeCaV contains an environment which maps variables to elements of the domain. The environment changes whenever we encounter a quantifier, since the newly quantified variable must be added to the environment. If we had used usual variable names, we would have to keep track of all of the names that are currently defined to construct this mapping. Since we use de Bruijn indices to represent variables, we can simply increment the index of every existing variable by one to make room for the new variable as the new innermost variable with index 0. Once we leave the scope of a quantifier, the variable it binds no longer exists, we decrement the index of every other variable to make the new innermost variable return to index 0. The environment is then simply a mapping from the natural numbers to elements of the domain.

Another benefit of using de Bruijn indices is that they make it very easy to identify equivalent formulas containing quantifiers. Consider for example the formulas ∀ x . P(x) and ∀ y . P(y). These formulas clearly have exactly the same meaning, but they are not syntactically identical, so we would need some rule that allows us to prove that they are equivalent. With de Bruijn indices however, both of these formulas are written ∀ P(0), so there is no need to introduce an additional rule to prove the equivalence between the formulas. This allows us to easily prove formulas such as (∀ x . P(x)) → (∀ y . P(y)).

In the SeCaV Unshortener syntax, the universal quantification ∀ A is written Uni A, while the existential quantification ∃ A is written Exi A.

The table above contains an overview of the logical connectives and quantifiers available in SeCaV.

The rules of SeCaV

Now that we know how to write lemmas in SeCaV, we can begin attempting to prove them. SeCaV is a sequent calculus, which means that each step of a SeCaV proof consists of a number of formulas which must be derived by the following steps. One might consider the lemma itself as the "first step" of a proof, since it must be derived by the rest of the proof. Since the proof must eventually end, we end the proof with a special step which needs no further derivations to apply.

SeCaV is a one-sided sequent calculus, which means that any formulas we assume to be true to prove a set of formulas are added to the set itself as negated formulas. We may do this because it can be proven that a statement Γ ⊢ Δ can be proven in a standard sequent calculus if and only if ⊢ ¬ Γ, Δ can be proven in the corresponding one-sided sequent calculus.

This leads us to the first rule of SeCaV, which in usual logic notation says that ⊢ P, ¬ P, Γ is true. Here and in the rest of the rules, Γ represents any formulas that are part of the set, but which are not relevant to the rule in question. If we convert the one-sided statement ⊢ P, ¬ P, Γ back to a "normal" statement, it becomes obvious that the rule is true: ¬ Γ, P ⊢ P means "if we assume P is true (and possibly some other things), then P is true". The actual rule is slightly different, but has essentially the same meaning:

Basic: ⊩ p # z if member (Neg p) z

The Basic rule is the only rule that can end a proof, since all of the other rules depend on the derivations of other formulas. Note that the right hand side of the rule is not a SeCaV formula, but a purely computational condition that can be proven by simply looking at the asserted formulas. Note also that this rule can only be used for the first formula, since p is explicitly the head of the list of formulas. We will return to the question of what to do if we want to use another formula at the end of this section.

Since the Basic rule is the only rule that can end a proof, every other rule will be followed by a list of formulas which is the result of applying the rule to the previous list of formulas. We will see how this is done in more detail in the examples below.

Another very simple, but very important rule is the double negation rule, which is named NegNeg in the SeCaV system. In usual logic notation, this rule says that ⊢ ¬ ¬ P, Γ if ⊢ P, Γ, and essentially means that negation cancels itself. Here is the rule:

NegNeg: ⊩ Neg (Neg p) # z if ⊩ p # z

Before we look at the rules for proving formulas involving logical connectives, let's look at a final obvious rule called Ext. This rule says that to prove a number of formulas ⊢ A, B, C, …, you may instead prove any subset of the original formulas, in any order. The mentioned list of formulas could thus be replaced by e.g. ⊢ A, ⊢ C, B, A, or ⊢ B, C. Here is the rule:

Ext: ⊩ y if ⊩ z and ext y z

ext y z ↔ set z ⊆ set y

α- and β-rules

The rules we have seen so far do not tell us anything about how to handle the logical connectives, but there are of course also rules to prove formulas involving them. We will see that these rules can be divided into two categories depending on the number of formulas that must be derived to use them. Rules in the first category are called α-rules, and rules in this category depend on only one derivation. Rules in the second category are called β-rules, and rules in this category depend on two derivations.

In each category there is exactly one rule for disjunction, one rule for implication, and one rule for conjunction. In total there are thus six rules, one for each connective, and one for the negation of each connective. There are no further rules about the negation operator, so formulas involving the negation operator must be proven either using the double negation rule or in connection with another logical connective using the α- or β-rules.

The α-rules are about formulas of the forms A ∨ B, A → B, and ¬ (A ∧ B), while the β-rules are about formulas of the forms A ∧ B, ¬ (A → B), and ¬ (A ∨ B).

The first α-rule is called AlphaDis and says that ⊢ A ∨ B, Γ is true if ⊢ A, B, Γ is true. This should be obvious, since the rule just moves the connective from the object language into the metalanguage (remember that there is an implicit disjunction between the asserted formulas in a sequent calculus). Here is the rule:

AlphaDis: ⊩ Dis p q # z if ⊩ p # q # z

The second α-rule is called AlphaImp and says that ⊢ A → B, Γ is true if ⊢ ¬ A, B, Γ is true. This rule is less intuitive, but becomes obvious when you consider the truth table definition of implication. Here is the rule:

AlphaImp: ⊩ Imp p q # z if ⊩ Neg p # q # z

The third and final α-rule is called AlphaCon and says that ⊢ ¬ (A ∧ B), Γ is true if ⊢ ¬ A, ¬ B, Γ is true. The meaning of this rule is that at least one of the two propositions A and B must be false for the negated conjunction of the propositions to be false. Here is the rule:

AlphaCon: ⊩ Neg (Con p q) # z if ⊩ Neg p # Neg q # z

Notice that the conclusions of all of the α-rules depend on only a single derivation. We will now look at the β-rules, whose conclusions all depend on two derivations that must both be true.

The first β-rule is called BetaCon and says that ⊢ A ∧ B, Γ is true if both ⊢ A, Γ and ⊢ B, Γ are true. Here is the rule:

BetaCon: ⊩ Con p q # z if ⊩ p # z and ⊩ q # z

The second β-rule is called BetaImp and says that ⊢ ¬ (A → B), Γ is true if both ⊢ A, Γ and ⊢ ¬ B, Γ are true. This should again be obvious from the truth table for implication. Here is the rule:

BetaImp: ⊩ Neg (Imp p q) # z if ⊩ p # z and ⊩ Neg q # z

The third and final β-rule is called BetaDis and says that ⊢ ¬ (A ∨ B), Γ is true if both ⊢ ¬ A, Γ and ⊢ ¬ B, Γ are true. Again, the connective is essentially just moved into the metalanguage. Here is the rule:

BetaDis: ⊩ Neg (Dis p q) # z if ⊩ Neg p # z and ⊩ Neg q # z

You may have noticed that the β-rules all carry any additional formulas Γ (or z in the code syntax) into both branches of the derivation. This suggests that, like in the method of tableaux, one should always strive to use as many α-rules as possible before using any β-rules to avoid duplication of work.

γ- and δ-rules

We now know how to prove formulas involving logical connectives, but we still haven't seen how to handle quantified formulas. When we encounter a formula starting with a quantifier, we want to eliminate the quantifier so we can continue using rules on the inner formula. When we eliminate a quantifier we also need to do something about the variable bound by the quantifier. Since quantifiers generalize formulas by replacing terms with variables, we will replace the bound variable by a term when we eliminate the quantifier. The rules for eliminating quantifiers can be divided into two categories depending on which term we are allowed to replace the variable with. There are two rules in each category, one for each of the quantifiers.

The simplest of these categories contains formulas where there are no restrictions on which term we are allowed to replace the variable with. The rules in this category are called γ-rules, and concern formulas of the forms ∃ x . A(x) and ¬ ∀ x . A(x).

The first γ-rule is called GammaExi and says that ⊢ ∃ x . A(x), Γ is true if ⊢ A, Γ, with the variable x replaced by some term t in A, is true. The idea is that, if we want to prove that the formula A(x) is true for some x, we need to provide a proof of the formula with x replaced by some concrete term t, which is commonly called a witness. If we have a proof that the formula is true for t, the formula is obviously true for some term (that term being t), so we have proven ∃ x . A(x). Here is the rule:

GammaExi: ⊩ Exi p # z if ⊩ sub 0 t p # z

The other γ-rule is called GammaUni and says that ⊢ ¬ ∀ x . A(x), Γ is true if ⊢ ¬ A, Γ, with the variable x replaced by some term t in A, is true. The idea is that, if we want to prove that the formula A(x) is not true for every x, we need to provide a term t for which the formula does not hold. Here is the rule:

GammaExi: ⊩ Neg (Uni p) # z if ⊩ Neg (sub 0 t p) # z

The γ-rules are fairly simple, but Isabelle will sometimes need help using the rules because we can replace the bound variable by any term. This can make Isabelle confused about which part of the new formula is our witness. In the SeCaV Unshortener syntax, we can specify which term we are replacing the bound variable with by writing an annotation e.g. GammaExi[t] to mean that we want to apply rule GammaExi, replacing the bound variable by the term t. This is not necessary, but it never hurts, as the annotation will automatically be added in the generated Isabelle proof anyways.

The other category contains formulas where we must replace the variable with a fresh constant. A fresh constant is one which does not occur anywhere else in the list of formulas in our current proof step. The rules in this category are called δ-rules, and concern formulas of the forms ∀ x . A(x) and ¬ ∃ x . A(x).

The first δ-rule is called DeltaUni and says that ⊢ ∀ x . A(x), Γ is true if ⊢ A, Γ, with the variable x replaced by a fresh constant c in A, is true. The idea is that, if we want to prove that the formula A(x) is true for every x, we can do so by proving the formula A for a fresh constant. Since the fresh constant is not mentioned anywhere else, it could be replaced by any term without changing the meaning of the formula. The formula is thus true for any term, which is what we wanted to prove. Here is the rule:

DeltaUni: ⊩ Uni p # z if ⊩ sub 0 f p # z and news f (p # z)

The second δ-rule is called DeltaExi and says that ⊢ ¬ ∃ x . A(x) is true if ⊢ ¬ A, Γ, with the variable x replaced by a fresh constant c in A, is true. The idea is that, if we want to prove that there is no x such that A(x) is true, we can do so by proving the formula ¬ A for a fresh constant. Since the fresh constant is not mentioned anywhere else, it could be replaced by any term without changing the meaning of the formula. There is thus no term for which the formula is true, which is what we wanted to prove. Here is the rule:

DeltaExi: ⊩ Neg (Exi p) # z if ⊩ Neg (sub 0 f p) # z and news f (p # z)

We have now seen every rule in SeCaV, so we are ready to begin proving lemmas. The rules of SeCaV can prove any lemma in first-order logic, but unlike proofs in propositional logic, proofs in first-order logic require planning. This is mainly because of the γ-rules, which require the user to choose a term to substitute into the formula when eliminating the quantifier. If the user chooses the wrong term, it may not be possible to continue the proof, and it is not always obvious what to choose.

Note also that all of the γ- and δ-rules remove the quantified formula from the list of formulas. It may sometimes be necessary to use the GammaUni or GammaExi rule multiple times on the same universally quantified formula to obtain several versions of the same formula with different terms substituted in for the variable.

Additionally, the user might choose to eliminate quantifiers at an unfortunate step in the proof. When a β-rule is used, the proof splits in two branches. If a quantifier is eliminated before this happens, the term replacing the bound variable will be the same in both branches, but if the user waits to do this until the β-rule has been used, the variable can be replaced by different terms in the two branches.

These difficulties mean that you should expect to spend a few attempts before successfully proving a formula.

Some example proofs

This section contains a number of example proofs in the SeCaV Unshortener syntax. To try these proofs, simply copy them into the SeCaV Unshortener, then copy the output into your Isabelle file. Remember to add the required header and footer to the Isabelle file as described above.

You can copy multiple examples in at once separated by minuses (-) or hashes (#) as described above.

Example 1

The formula P(a,b) ∨ ¬ P(a,b) may be stated and proved as follows in the SeCaV Unshortener:

# "Example 1"
      
Dis p[a, b] (Neg p[a, b])

AlphaDis
  p[a, b]
  Neg p[a, b]
Basic

Example 2

The formula (∀x . ∀y . P(x,y)) → P(a,a) may be stated and proved as follows in the SeCaV Unshortener:

# "Example 2"

Imp (Uni (Uni (p[1, 0]))) p[a, a]

AlphaImp
  Neg (Uni (Uni p[1, 0]))
  p[a, a]
GammaUni
  Neg (Uni p[a, 0])
  p[a, a]
GammaUni
  Neg p[a, a]
  p[a, a]
Ext
  p[a, a]
  Neg p[a, a]
Basic

Example 3

The formula (∀x . P(x) → Q(x)) → ((∃x . P(x)) → (∃x . Q(x))) may be stated and proved as follows in the SeCaV Unshortener:

# "Example 3"

Imp (Uni (Imp p[0] q[0])) (Imp (Exi p[0]) (Exi q[0]))

AlphaImp
  Neg (Uni (Imp p[0] q[0]))
  Imp (Exi p[0]) (Exi q[0])
Ext
  Imp (Exi p[0]) (Exi q[0])
  Neg (Uni (Imp p[0] q[0]))
AlphaImp
  Neg (Exi p[0])
  Exi q[0]
  Neg (Uni (Imp p[0] q[0]))
DeltaExi
  Neg p[a]
  Exi q[0]
  Neg (Uni (Imp p[0] q[0]))
Ext
  Neg (Uni (Imp p[0] q[0]))
  Neg p[a]
  Exi q[0]
GammaUni
  Neg (Imp p[a] q[a])
  Neg p[a]
  Exi q[0]
BetaImp
  p[a]
  Neg p[a]
  Exi q[0]
+
  Neg q[a]
  Neg p[a]
  Exi q[0]
Basic
  Neg q[a]
  Neg p[a]
  Exi q[0]
Ext
  Exi q[0]
  Neg q[a]
GammaExi
  q[a]
  Neg q[a]
Basic