We work with sequents , and interpret the propositions (and ) as subsets of some universe set . We interpret the sequent itself as .
While writing the previous post, there was the temptation to introduce the sequent calculus rules for existential and universal quantification. But the subset interpretation with a fixed universe set didn’t seem helpful for free variables and quantification. But what if we allow different universe sets for different sequents? One way would be to augment the sequent rules to change the universe sets in a well defined way. However, the cut rule and two of the four quantification rules (those that replace an arbitrary term by a quantified variable) are a bit problematic. For them, the universe can sometimes be shrunk down, since a formula or a term was eliminated. Therefore, we just add two separate rules for changing the universe, and apply the sequent rules themselves only with respect to a fixed universe set.
This is the last planed post on the sequent calculus for the moment. (There might be an additional post in this series, extending the subset interpretation to natural deduction.) Since this post will remain vague and unsatisfactory in many ways, a list of related online materials on the sequent calculus seems appropriate: I often consulted the wikipedia article while writing these posts. (I never consulted Sequent Calculus Primer, but it looks nice and has exercises.) This MathOverflow question on introductions to sequent calculus suggests the chapter on Sequent Calculus from Frank Pfenning’s manuscript on Automated Theorem Proving, which I really liked. It also suggests Proofs and Types by Jean-Yves Girard, which was my first introduction to the sequent calculus. It left me unsatisfied, and I agree with Charles Stewart:
A warning: Girard’s style is a little slippery, and it is common for students to say they have read it, who turn out to have absorbed the opinions but little of the results.
I am still slightly ashamed that one of my first questions – when I met a group of academic logicians (with a focus on proof assistants) – was whether they found Girard easy to understand. Girard claims that the sequent calculus is generally ignored by computer scientists, an exception being Logic For Computer Science Foundations of Automatic Theorem Proving by Jean H. Gallier. A nice text, but who has time to read those 500+ pages? This is one reason why I like An Introduction to Proof Theory by Samuel R. Buss.
The sequent calculus rules for predicate logic
We are interested in normal first order predicate logic with predicates and functions. Here a signature with a finite number of predicate and function symbols is given, which include the arity for each of the symbols. The sequent calculus rules for quantification are:
|Left quantification rules||Right quantification rules|
Those rules look simple, but what do they mean? What is the difference between and ? And how to interpret a sequent with formulas containing free variables? First, is a free variable not occurring in , , or . And means that each free occurrence of in is replaced by . Next, is an arbitrary term, with no restrictions at all on the variables occurring in it. A term is just any reasonable combination of function symbols (from the signature) and variables, like where both and are binary function symbols.
There are many possible interpretations of predicate logic, but that answer just avoids answering the question. The interpretation of a formula or sequent with free variables can be controversial. My previous effort at a subset based interpretations of predicate logic compatible with non-classical logic left out equality, functions and constants. Even so we are talking only about classical logic here, the goal of the following interpretation is to be also applicable more generally. That interpretation will follow naturally once we clarify which models we want to allow.
Models and interpretations of predicate calculus
For the typical interpretations, a model consists of a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol. A straightforward interpretation in that context is that a formula with free variables is a subset of , and a formula without free variables (i.e. a sentence) is either true or false. And for any set of variables, we can interpret any formula whose free variables are included in that set as a subset of . A sequent in this interpretation is true, iff for the subsets formed by the formulas interpreted relative to the set of all free variables in the sequent, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.
This straightforward interpretation above is already a subset interpretation, but we want a slightly more general subset interpretation. For propositional logic, the possible models were given by a set and a subset of for each propositional variable . In predicate logic, the 0-ary predicates take the role of the propositional variables, so we want them to be subsets of . For our generalised interpretation, a model consists of a set (whose subsets are the truth values) and a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol.
The way will enter into the model is to have some implicit context such that formulas like in the formal syntax become in the model. So for any set of free variables, we can interpret any formula whose free variables are included in that set as a subset of . For a given set of variables and a sequent for which the free variables of the formulas are contained in that subset, the a sequent is true, iff for the subsets formed by the formulas interpreted relative that set of variables, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.
(If we have a formula like , we would like to interpret it as a subset of , so we normally use and then just omit it. Here the element is called unit, the set represents truth, and the empty set represents falsehood.)
Context morphisms give life to the subset interpretation
If we have (a sequent of) subsets over , then a (partial) function from to gives us (a sequent of) subsets over by taking inverse images of the subsets. We have
The direct translation into the language of sequences reads
This just tells us that global substitution is unproblematic. (But is required in case is a partial function, which is easily missed.) However, the more typical function for our purpose is similar to , i.e. a function from to . It is typical, since the expressions grow in complexity for most rules of sequent calculus. Here is an example:
This example also shows, how we can separately change the universe set, and apply the sequent rules only with respect to a fixed universe set. After applying the or rule, we can shrink the universe set. To illustrate, let us first apply the and rule, where we cannot always shrink the universe set:
Here we cannot shrink the universe set.
Now we can shrink the universe set, but only after checking that the sequent no longer depends on . But when we apply , we can always shrink the universe set:
How can we justify this shrinking in terms of images or inverse images? The inverse image under for an arbitrary function (constant) could be a justification. But we don’t really write , and is arbitrary and irrelevant. So the image under might be a nicer justification. But we only have
However, if we assume , then and hence
Doubts about context morphisms and substitutions
Let us apply the above to propositional logic. Surely, from we can deduce . But we cannot justify it from in terms of inverse images. Can we justify it from ? Yes, take the map with . Here and can be arbitrary and . Note that we only need .
How justified are those substitutions into the expressions? Here, we used
Can we justify this? Can such substitutions go wrong? Yes, if is a partial function:
Here fails, but it would work if were a total function. We could have omitted , but then it would fail because of . That was actually the point were I noticed that the restriction is required for partial functions.
The substitutions are justified, because they work for each operation individually:
Treating equality without special rules
Equality can be given by a binary predicate which is a congruence relation for the functions, and compatible with the other predicates. There are different ways to treat equality, and it is important for most interesting applications of predicate logic. A canonical approach is to write the axioms on the left side of the sequent, and use normal deductions. Concrete examples for the required axioms were already given in the last post in the section “Axiomatic theories in predicate logic without falsehood” for the theory of groups and in the section “Axiomatic theories in predicate logic without falsehood” for Robinson arithmetic.
Part of the reason for presenting a subset interpretation for predicate logic was to better understand how predicate logic could work in case of non-classical logics. There are theories like Heyting arithmetic (and Gentzen’s own work), which seem to fit nicely with the interpretation above. But there are also intuitionistic dependent type theories with special rules and equality types, whose possible interpretations remain unclear to me, despite the nice subset interpretation explained above. Maybe Per Martin Löf is right: In the end, everybody must understand for himself (p.166)
This post was hard for me to write. This is the classical problem when explaining something obvious (predicate calculus). You have to make a lot of words for something which seems obvious, but where the language is missing to properly write down what is going on behind the scenes. I didn’t solve that language problem, but I came up with a natural example of how the obvious thing can fail to be true. That might help the reader to understand for himself.
The content above already became clear to me while writing the previous post. But only after this current post was nearly finished did I notice the restriction in case is a partial function. Which is funny, after I clarified the notion of context morphism which makes sense of that logic without truth from the first post (in this series), I find out that there is an additional restriction that the antecedent should never be empty. My first reaction was that I don’t like this. Maybe I should look for a transformation which turns this logic about partial functions into the logic without negation or falsehood. But my second reaction was that it could make sense, perhaps any logical deduction needs assumptions.
Still the question remains whether there is a reasonable transformation from the logic without truth (and partial functions) to the logic without negation and falsehood. Probably that question will be easy to answer. Somehow one has to take complements, and hope that the structure of the predicate calculus remains intact. It seems to work, but I still have trouble to intuitively understand it. And I want to finish this post now.