The Sequent Calculus — Read

Example: Every initial sequent, e.g., antecedent containing formula C; sequent arrow; succedent… — line 37

Every initial sequent, e.g., $!C \Sequent !C$source 38 is a derivation. We can obtain a new derivation from this by applying, say, the $\LeftR{\Weakening}$source 40 rule,

The rule, however, is meant to be general: we can replace the $!A$source 46 in the rule with any sentence, e.g., also with $!D$source 47. If the premise matches our initial sequent $!C \Sequent !C$source 48, that means that both $\Gamma$source 49 and $\Delta$source 49 are just $!C$source 49, and the conclusion would then be $!D, !C \Sequent !C$source 50. So, the following is a derivation:

We can now apply another rule, say $\LeftR{\Exchange}$source 56, which allows us to switch two sentences on the left. So, the following is also a correct derivation:

In this application of the rule, which was given as

both $\Gamma$source 72 and $\Pi$source 72 were empty, $\Delta$source 72 is $!C$source 72, and the roles of $!A$source 73 and $!B$source 73 are played by $!D$source 73 and $!C$source 73, respectively. In much the same way, we also see that

is a derivation. Now we can take these two derivations, and combine them using $\RightR{\land}$source 81. That rule was

In our case, the premises must match the last sequents of the derivations ending in the premises. That means that $\Gamma$source 89 is $!C, !D$source 90, $\Delta$source 90 is empty, $!A$source 90 is $!C$source 90 and $!B$source 90 is $!D$source 90. So the conclusion, if the inference should be correct, is $!C, !D \Sequent !C \land !D$source 91.

Of course, we can also reverse the premises, then $!A$source 105 would be $!D$source 106 and $!B$source 106 would be $!C$source 106.

source 37

Example: Give an L K derivation for the sequent antecedent containing the conjunction of formula A and… — line 15

Give an $\Log{LK}$source 16-derivation for the sequent $!A \land !B \Sequent !A$source 16.

We begin by writing the desired end-sequent at the bottom of the derivation.

Next, we need to figure out what kind of inference could have a lower sequent of this form. This could be a structural rule, but it is a good idea to start by looking for a logical rule. The only logical connective occurring in the lower sequent is $\land$source 27, so we're looking for an $\land$source 28 rule, and since the $\land$source 28 symbol occurs in the antecedent, we're looking at the left conjunction rule.

There are two options for what could have been the upper sequent of the left conjunction rule inference: we could have an upper sequent of $!A \Sequent !A$source 37, or of $!B \Sequent !A$source 38. Clearly, $!A \Sequent !A$source 38 is an initial sequent (which is a good thing), while $!B \Sequent !A$source 39 is not derivable in general. We fill in the upper sequent:

We now have a correct $\Log{LK}$source 46-derivation of the sequent $!A \land !B \Sequent !A$source 46.

source 15

Example: Give an L K derivation for the sequent antecedent containing the disjunction of the negation of… — line 50

Give an $\Log{LK}$source 51-derivation for the sequent $\lnot !A \lor !B \Sequent !A \lif !B$source 51.

Begin by writing the desired end-sequent at the bottom of the derivation.

To find a logical rule that could give us this end-sequent, we look at the logical connectives in the end-sequent: $\lnot$source 60, $\lor$source 60, and $\lif$source 61. We only care at the moment about $\lor$source 61 and $\lif$source 61 because they are main operators of sentences in the end-sequent, while $\lnot$source 63 is inside the scope of another connective, so we will take care of it later. Our options for logical rules for the final inference are therefore the left disjunction rule and the right conditional rule. We could pick either rule, really, but let's pick the right conditional rule (if for no reason other than it allows us to put off splitting into two branches). According to the form of right conditional rule inferences which can yield the lower sequent, this must look like:

If we move $\lnot !A \lor !B$source 76 to the outside of the antecedent, we can apply the left disjunction rule. According to the schema, this must split into two upper sequents as follows:

Remember that we are trying to wind our way up to initial sequents; we seem to be pretty close! The right branch is just one weakening and one exchange away from an initial sequent and then it is done:

Now looking at the left branch, the only logical connective in any sentence is the $\lnot$source 111 symbol in the antecedent sentences, so we're looking at an instance of the left negation rule.

Similarly to how we finished off the right branch, we are just one weakening and one exchange away from finishing off this left branch as well.

source 50

Example: Give an L K derivation of the sequent antecedent containing the disjunction of the negation of… — line 154

Give an $\Log{LK}$source 155-derivation of the sequent $\lnot !A \lor \lnot !B \Sequent \lnot (!A \land !B)$source 155

Using the techniques from above, we start by writing the desired end-sequent at the bottom.

The available main connectives of sentences in the end-sequent are the $\lor$source 165 symbol and the $\lnot$source 165 symbol. It would work to apply either the left disjunction rule or the right negation rule here, but we start with the right negation rule because it avoids splitting up into two branches for a moment:

Now we have a choice of whether to look at the left conjunction rule or the left disjunction rule. Let's see what happens when we apply the left conjunction rule: we have a choice to start with either the sequent $!A, \lnot !A \lor !B \Sequent \quad$source 177 or the sequent $!B, \lnot !A \lor !B \Sequent \quad$source 178. Since the derivation is symmetric with regards to $!A$source 180 and $!B$source 180, let's go with the former:

Continuing to fill in the derivation, we see that we run into a problem:

The top of the right branch cannot be reduced any further, and it cannot be brought by way of structural inferences to an initial sequent, so this is not the right path to take. So clearly, it was a mistake to apply the left conjunction rule above. Going back to what we had before and carrying out the left disjunction rule instead, we get

Completing each branch as we've done before, we get

(We could have carried out the $\land$source 248 rules lower than the $\lnot$source 248 rules in these steps and still obtained a correct derivation).

source 154

Example: So far we haven't used the contraction rule, but it is sometimes required — line 252

So far we haven't used the contraction rule, but it is sometimes required. Here's an example where that happens. Suppose we want to prove $\quad \Sequent !A \lor \lnot !A$source 255. Applying $\RightR{\lor}$source 255 backwards would give us one of these two derivations:

Neither of these of course ends in an initial sequent. The trick is to realize that the contraction rule allows us to combine two copies of a sentence into one—and when we're searching for a proof, i.e., going from bottom to top, we can keep a copy of $!A \lor \lnot !A$source 273 in the premise, e.g.,

Now we can apply $\RightR{\lor}$source 283 a second time, and also get $\lnot !A$source 283, which leads to a complete derivation.

source 252

Example: Give an L K derivation of the sequent antecedent containing for some variable x, the negation… — line 13

Give an $\Log{LK}$source 14-derivation of the sequent $\lexists[x][\lnot !A(x)] \Sequent \lnot \lforall[x][!A(x)]$source 14.

When dealing with quantifiers, we have to make sure not to violate the eigenvariable condition, and sometimes this requires us to play around with the order of carrying out certain inferences. In general, it helps to try and take care of rules subject to the eigenvariable condition first (they will be lower down in the finished proof). Also, it is a good idea to try and look ahead and try to guess what the initial sequent might look like. In our case, it will have to be something like $!A(a) \Sequent !A(a)$source 24. That means that when we are “reversing” the quantifier rules, we will have to pick the same term—what we will call $a$source 26—for both the $\lforall$source 26 and the $\lexists$source 27 rule. If we picked different terms for each rule, we would end up with something like $!A(a) \Sequent !A(b)$source 28, which, of course, is not derivable.

Starting as usual, we write

We could either carry out the exists rule or the right negation rule. Since the exists rule is subject to the eigenvariable condition, it's a good idea to take care of it sooner rather than later, so we'll do that one first.

Applying the left negation rule and right negation rule rules backwards, we get

At this point, our only option is to carry out the forall rule. Since this rule is not subject to the eigenvariable restriction, we're in the clear. Remember, we want to try and obtain an initial sequent (of the form $!A(a) \Sequent !A(a)$source 62), so we should choose $a$source 62 as our argument for $!A$source 63 when we apply the rule.

It is important, especially when dealing with quantifiers, to double check at this point that the eigenvariable condition has not been violated. Since the only rule we applied that is subject to the eigenvariable condition was exists rule, and the eigenvariable $a$source 80 does not occur in its lower sequent (the end-sequent), this is a correct derivation.

source 13