The Sequent Calculus — Read

Proof

The initial sequent $!A \Sequent !A$source 84 is derivable, and $\{!A\} \subseteq \Gamma$source 84.

End of proof.

Proof

Suppose $\Gamma \Proves !A$source 95, i.e., there is a finite $\Gamma_0 \subseteq \Gamma$source 95 such that $\Gamma_0 \Sequent !A$source 96 is derivable. Since $\Gamma \subseteq \Delta$source 97, then $\Gamma_0$source 97 is also a finite subset of $\Delta$source 98. The derivation of $\Gamma_0 \Sequent !A$source 98 thus also shows $\Delta \Proves !A$source 99.

End of proof.

Proof

If $\Gamma \Proves !A$source 109, there is a finite $\Gamma_0 \subseteq \Gamma$source 109 and a derivation $\pi_0$source 110 of $\Gamma_0 \Sequent !A$source 110. If $\{!A\} \cup \Delta \Proves !B$source 110, then for some finite subset $\Delta_0 \subseteq \Delta$source 111, there is a derivation $\pi_1$source 112 of $!A, \Delta_0 \Sequent !B$source 112. Consider the following derivation:

Since $\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta$source 124, this shows $\Gamma \cup \Delta \Proves !B$source 125.

End of proof.

Proof

Exercise.

End of proof.

Proof

1. If $\Gamma \Proves !A$source 159, then there is a finite subset $\Gamma_0 \subseteq \Gamma$source 160 such that the sequent $\Gamma_0 \Sequent !A$source 160 has a derivation. Consequently, $\Gamma_0 \Proves !A$source 161.

2. If $\Gamma$source 163 is inconsistent, there is a finite subset $\Gamma_0 \subseteq \Gamma$source 164 such that $\Log{LK}$source 164 derives $\Gamma_0 \Sequent \quad$source 165. But then $\Gamma_0$source 165 is a finite subset of $\Gamma$source 166 that is inconsistent.

End of proof.

Proof

There are finite $\Gamma_0$source 25 and $\Gamma_1 \subseteq \Gamma$source 25 such that $\Log{LK}$source 26 derives $\Gamma_0 \Sequent !A$source 26 and $!A, \Gamma_1 \Sequent \quad$source 26. Let the $\Log{LK}$source 27-derivation of $\Gamma_0 \Sequent !A$source 27 be $\pi_0$source 28 and the $\Log{LK}$source 28-derivation of $\Gamma_1, !A \Sequent \quad$source 28 be $\pi_1$source 29. We can then derive

Since $\Gamma_0 \subseteq \Gamma$source 41 and $\Gamma_1 \subseteq \Gamma$source 41, $\Gamma_0 \cup \Gamma_1 \subseteq \Gamma$source 42, hence $\Gamma$source 42 is inconsistent.

End of proof.

Proof

First suppose $\Gamma \Proves !A$source 51, i.e., there is a derivation $\pi_0$source 52 of $\Gamma \Sequent !A$source 52. By adding a $\LeftR{\lnot}$source 53 rule, we obtain a derivation of $\lnot !A, \Gamma \Sequent \quad$source 53, i.e., $\Gamma \cup \{\lnot !A\}$source 54 is inconsistent.

If $\Gamma \cup \{\lnot !A\}$source 56 is inconsistent, there is a derivation $\pi_1$source 57 of $\lnot !A, \Gamma \Sequent \quad$source 57. The following is a derivation of $\Gamma \Sequent !A$source 58:

End of proof.

Proof

Suppose $\Gamma \Proves !A$source 81 and $\lnot !A \in \Gamma$source 81. Then there is a derivation $\pi$source 82 of a sequent $\Gamma_0 \Sequent !A$source 82. The sequent $\lnot !A, \Gamma_0 \Sequent \quad$source 83 is also derivable:

Since $\lnot !A \in \Gamma$source 96 and $\Gamma_0 \subseteq \Gamma$source 96, this shows that $\Gamma$source 97 is inconsistent.

End of proof.

Proof

There are finite sets $\Gamma_0 \subseteq \Gamma$source 106 and $\Gamma_1 \subseteq \Gamma$source 106 and $\Log{LK}$source 107-derivations $\pi_0$source 107 and $\pi_1$source 107 of $!A, \Gamma_0 \Sequent \quad$source 108 and $\lnot !A, \Gamma_1 \Sequent \quad$source 108, respectively. We can then derive

Since $\Gamma_0 \subseteq \Gamma$source 122 and $\Gamma_1 \subseteq \Gamma$source 122, $\Gamma_0 \cup \Gamma_1 \subseteq \Gamma$source 123. Hence $\Gamma$source 123 is inconsistent.

End of proof.

Proof

1. Both sequents $!A \land !B \Sequent !A$source 37 and $!A \land !B \Sequent !B$source 37 are derivable:

   Proof diagram: Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 43

   Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A — line 43. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are left conjunction rule. Its last stated proof component is: From the immediately preceding branch using the left conjunction rule, infer antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled left conjunction rule.
   3. From the immediately preceding branch using the left conjunction rule, infer antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A.
   4. The source ends this displayed proof segment here.

   Proof diagram: Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B — line 39

   Proof tree concluding antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B — line 39. This source proof tree has 7 explicitly ordered components. Its inference labels, in order, are left conjunction rule, then left conjunction rule. Its last stated proof component is: From the immediately preceding branch using the left conjunction rule, infer antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled left conjunction rule.
   3. From the immediately preceding branch using the left conjunction rule, infer antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula A.
   4. The source ends this displayed proof segment here.
   5. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   6. The next inference is labeled left conjunction rule.
   7. From the immediately preceding branch using the left conjunction rule, infer antecedent containing the conjunction of formula A and formula B; sequent arrow; succedent containing formula B.

   1. $!A \fCenter !A$source 40
   2. $!A \land !B \fCenter !A$source 42
   3. $!B \fCenter !B$source 44
   4. $!A \land !B \fCenter !B$source 46

   source 39

2. Here is a derivation of the sequent $!A, !B \Sequent !A \land !B$source 48:

   Proof diagram: Proof tree concluding antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B — line 49

   Proof tree concluding antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B — line 49. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are right conjunction rule. Its last stated proof component is: From the two immediately preceding branches using the right conjunction rule, infer antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   3. The next inference is labeled right conjunction rule.
   4. From the two immediately preceding branches using the right conjunction rule, infer antecedent containing first formula A, then formula B; sequent arrow; succedent containing the conjunction of formula A and formula B.

   1. $!A \fCenter !A$source 50
   2. $!B \fCenter !B$source 51
   3. $!A, !B \fCenter !A \land !B$source 53

   source 49

End of proof.

Proof

1. We give a derivation of the sequent $!A \lor !B, \lnot !A, \lnot !B \Sequent$source 67:

   Proof diagram: Proof tree concluding antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas — line 69

   Proof tree concluding antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas — line 69. This source proof tree has 12 explicitly ordered components. Its inference labels, in order, are left negation rule, then left negation rule, then left disjunction rule. Its last stated proof component is: From the two immediately preceding branches using the left disjunction rule, infer antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled left negation rule.
   3. From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas.
   4. A double inference line abbreviates one or more weakening, contraction, or exchange steps.
   5. From the immediately preceding branch, infer antecedent containing first formula A, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas.
   6. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   7. The next inference is labeled left negation rule.
   8. From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula B, then formula B; sequent arrow; succedent containing no formulas.
   9. A double inference line abbreviates one or more weakening, contraction, or exchange steps.
   10. From the immediately preceding branch, infer antecedent containing first formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas.
   11. The next inference is labeled left disjunction rule.
   12. From the two immediately preceding branches using the left disjunction rule, infer antecedent containing first the disjunction of formula A and formula B, then the negation of formula A, and finally the negation of formula B; sequent arrow; succedent containing no formulas.

   1. $!A \fCenter !A$source 70
   2. $\lnot !A, !A \fCenter$source 72
   3. $!A, \lnot !A, \lnot !B \fCenter$source 74
   4. $!B \fCenter !B$source 75
   5. $\lnot !B, !B \fCenter$source 77
   6. $!B, \lnot !A, \lnot !B \fCenter$source 79
   7. $!A \lor !B, \lnot !A, \lnot !B \fCenter$source 81

   source 69

   (Recall that double inference lines indicate several weakening, contraction, and exchange inferences.)

2. Both sequents $!A \Sequent !A \lor !B$source 85 and $!B \Sequent !A \lor !B$source 85 have derivations:

   Proof diagram: Proof tree concluding antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B — line 91

   Proof tree concluding antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B — line 91. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are right disjunction rule. Its last stated proof component is: From the immediately preceding branch using the right disjunction rule, infer antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled right disjunction rule.
   3. From the immediately preceding branch using the right disjunction rule, infer antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B.
   4. The source ends this displayed proof segment here.

   Proof diagram: Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B — line 87

   Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B — line 87. This source proof tree has 7 explicitly ordered components. Its inference labels, in order, are right disjunction rule, then right disjunction rule. Its last stated proof component is: From the immediately preceding branch using the right disjunction rule, infer antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled right disjunction rule.
   3. From the immediately preceding branch using the right disjunction rule, infer antecedent containing formula A; sequent arrow; succedent containing the disjunction of formula A and formula B.
   4. The source ends this displayed proof segment here.
   5. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   6. The next inference is labeled right disjunction rule.
   7. From the immediately preceding branch using the right disjunction rule, infer antecedent containing formula B; sequent arrow; succedent containing the disjunction of formula A and formula B.

   1. $!A \fCenter !A$source 88
   2. $!A \fCenter !A \lor !B$source 90
   3. $!B \fCenter !B$source 92
   4. $!B \fCenter !A \lor !B$source 94

   source 87

End of proof.

Proof

1. The sequent $!A \lif !B, !A \Sequent !B$source 109 is derivable:

   Proof diagram: Proof tree concluding antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B — line 110

   Proof tree concluding antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B — line 110. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are left conditional rule. Its last stated proof component is: From the two immediately preceding branches using the left conditional rule, infer antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   3. The next inference is labeled left conditional rule.
   4. From the two immediately preceding branches using the left conditional rule, infer antecedent containing first the conditional whose antecedent is formula A; and whose consequent is formula B, then formula A; sequent arrow; succedent containing formula B.

   1. $!A \fCenter !A$source 111
   2. $!B \fCenter !B$source 112
   3. $!A \lif !B, !A \fCenter !B$source 114

   source 110

2. Both sequents $\lnot !A \Sequent !A \lif !B$source 116 and $!B \Sequent !A \lif !B$source 116 are derivable:

   Proof diagram: Proof tree concluding antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 128

   Proof tree concluding antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 128. This source proof tree has 10 explicitly ordered components. Its inference labels, in order, are left negation rule, then left exchange rule, then right weakening rule, then right conditional rule. Its last stated proof component is: From the immediately preceding branch using the right conditional rule, infer antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled left negation rule.
   3. From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas.
   4. The next inference is labeled left exchange rule.
   5. From the immediately preceding branch using the left exchange rule, infer antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas.
   6. The next inference is labeled right weakening rule.
   7. From the immediately preceding branch using the right weakening rule, infer antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B.
   8. The next inference is labeled right conditional rule.
   9. From the immediately preceding branch using the right conditional rule, infer antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B.
   10. The source ends this displayed proof segment here.

   Proof diagram: Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 118

   Proof tree concluding antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B — line 118. This source proof tree has 15 explicitly ordered components. Its inference labels, in order, are left negation rule, then left exchange rule, then right weakening rule, then right conditional rule, then left weakening rule, then right conditional rule. Its last stated proof component is: From the immediately preceding branch using the right conditional rule, infer antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B.

   1. Premise or initial sequent: antecedent containing formula A; sequent arrow; succedent containing formula A.
   2. The next inference is labeled left negation rule.
   3. From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula A, then formula A; sequent arrow; succedent containing no formulas.
   4. The next inference is labeled left exchange rule.
   5. From the immediately preceding branch using the left exchange rule, infer antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing no formulas.
   6. The next inference is labeled right weakening rule.
   7. From the immediately preceding branch using the right weakening rule, infer antecedent containing first formula A, then the negation of formula A; sequent arrow; succedent containing formula B.
   8. The next inference is labeled right conditional rule.
   9. From the immediately preceding branch using the right conditional rule, infer antecedent containing the negation of formula A; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B.
   10. The source ends this displayed proof segment here.
   11. Premise or initial sequent: antecedent containing formula B; sequent arrow; succedent containing formula B.
   12. The next inference is labeled left weakening rule.
   13. From the immediately preceding branch using the left weakening rule, infer antecedent containing first formula A, then formula B; sequent arrow; succedent containing formula B.
   14. The next inference is labeled right conditional rule.
   15. From the immediately preceding branch using the right conditional rule, infer antecedent containing formula B; sequent arrow; succedent containing the conditional whose antecedent is formula A; and whose consequent is formula B.

   1. $!A \fCenter !A$source 119
   2. $\lnot !A, !A \fCenter$source 121
   3. $!A, \lnot !A \fCenter$source 123
   4. $!A, \lnot !A \fCenter !B$source 125
   5. $\lnot !A \fCenter !A \lif !B$source 127
   6. $!B \fCenter !B$source 129
   7. $!A, !B \fCenter !B$source 131
   8. $!B \fCenter !A \lif !B$source 133

   source 118

End of proof.

Proof

Let $\pi$source 58 be a derivation of $\Theta \Sequent \Xi$source 58. We proceed by induction on the number of inferences $n$source 59 in $\pi$source 59.

If the number of inferences is $0$source 61, then $\pi$source 61 consists only of an initial sequent. Every initial sequent $!A \Sequent !A$source 62 is obviously valid, since for every $\pAssign{v}$source 63, either $\pSat/{v}{!A}$source 64 or $\pSat{v}{!A}$source 65.

If the number of inferences is greater than 0, we distinguish cases according to the type of the lowermost inference. By induction hypothesis, we can assume that the premises of that inference are valid, since the number of inferences in the derivation of any premise is smaller than $n$source 71.

First, we consider the possible inferences with only one premise.

1. The last inference is a weakening. Then $\Theta \Sequent \Xi$source 75 is either $!A, \Gamma \Sequent \Delta$source 76 (if the last inference is left weakening rule) or $\Gamma \Sequent \Delta, !A$source 77 (if it's right weakening rule), and the derivation ends in one of

   Proof diagram: Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 84

   Proof tree concluding antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 84. This source proof tree has 5 explicitly ordered components. Its inference labels, in order, are left weakening rule. Its last stated proof component is: From the immediately preceding branch using the left weakening rule, infer antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing Gamma; sequent arrow; succedent containing capital Delta.
   3. The next inference is labeled left weakening rule.
   4. From the immediately preceding branch using the left weakening rule, infer antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta.
   5. The source ends this displayed proof segment here.

   Proof diagram: Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A — line 79

   Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A — line 79. This source proof tree has 9 explicitly ordered components. Its inference labels, in order, are left weakening rule, then right weakening rule. Its last stated proof component is: From the immediately preceding branch using the right weakening rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing Gamma; sequent arrow; succedent containing capital Delta.
   3. The next inference is labeled left weakening rule.
   4. From the immediately preceding branch using the left weakening rule, infer antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta.
   5. The source ends this displayed proof segment here.
   6. An upper premise slot is intentionally blank in this staged diagram.
   7. Previously derived premise with its intervening derivation omitted: antecedent containing Gamma; sequent arrow; succedent containing capital Delta.
   8. The next inference is labeled right weakening rule.
   9. From the immediately preceding branch using the right weakening rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A.

   1. $\Gamma \fCenter \Delta$source 81
   2. $!A, \Gamma \fCenter \Delta$source 83
   3. $\Gamma \fCenter \Delta$source 86
   4. $\Gamma \fCenter \Delta, !A$source 88

   source 79

   By induction hypothesis, $\Gamma \Sequent \Delta$source 90 is valid, i.e., for every valuation $\pAssign{v}$source 92, either there is some $!C \in \Gamma$source 93 such that $\pSat/{v}{!C}$source 94 or there is some $!C \in \Delta$source 94 such that $\pSat{v}{!C}$source 95.

   If $\pSat/{v}{!C}$source 97 for some $!C \in \Gamma$source 97, then $!C \in \Theta$source 98 as well since $\Theta = !A, \Gamma$source 98, and so $\pSat/{v}{!C}$source 99 for some $!C \in \Theta$source 99. Similarly, if $\pSat{v}{!C}$source 100 for some $!C \in \Delta$source 100, as $!C \in \Xi$source 101, $\pSat{v}{!C}$source 101 for some $!C \in \Xi$source 102. Consequently, $\Theta \Sequent \Xi$source 102 is valid.

2. The last inference is left negation rule: Then the premise of the last inference is $\Gamma \Sequent \Delta, !A$source 104 and the conclusion is $\lnot !A, \Gamma \Sequent \Delta$source 105, i.e., the derivation ends in

   Proof diagram: Proof tree concluding antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 106

   Proof tree concluding antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta — line 106. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are left negation rule. Its last stated proof component is: From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A.
   3. The next inference is labeled left negation rule.
   4. From the immediately preceding branch using the left negation rule, infer antecedent containing first the negation of formula A, then Gamma; sequent arrow; succedent containing capital Delta.

   1. $\Gamma \fCenter \Delta, !A$source 108
   2. $\lnot !A, \Gamma \fCenter \Delta$source 110

   source 106

   and $\Theta = \lnot !A, \Gamma$source 112 while $\Xi = \Delta$source 112.

   The induction hypothesis tells us that $\Gamma \Sequent \Delta, !A$source 114 is valid, i.e., for every $\pAssign{v}$source 115, either (a) for some $!C \in \Gamma$source 116, $\pSat/{v}{!C}$source 117, or (b) for some $!C \in \Delta$source 117, $\pSat{v}{!C}$source 118, or (c) $\pSat{v}{!A}$source 119. We want to show that $\Theta \Sequent \Xi$source 119 is also valid. Let $\pAssign{v}$source 121 be a valuation. If (a) holds, then there is $!C \in \Gamma$source 122 so that $\pSat/{v}{!C}$source 123, but $!C \in \Theta$source 123 as well. If (b) holds, there is $!C \in \Delta$source 124 such that $\pSat{v}{!C}$source 125, but $!C \in \Xi$source 125 as well. Finally, if $\pSat{v}{!A}$source 126, then $\pSat/{v}{\lnot !A}$source 127. Since $\lnot !A \in \Theta$source 127, there is $!C \in \Theta$source 128 such that $\pSat/{v}{!C}$source 129. Consequently, $\Theta \Sequent \Xi$source 129 is valid.

3. The last inference is right negation rule: Exercise.

4. The last inference is left conjunction rule: There are two variants: $!A \land !B$source 132 may be inferred on the left from $!A$source 133 or from $!B$source 133 on the left side of the premise. In the first case, the $\pi$source 134 ends in

   Proof diagram: Proof tree concluding antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 135

   Proof tree concluding antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta — line 135. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are left conjunction rule. Its last stated proof component is: From the immediately preceding branch using the left conjunction rule, infer antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing capital Delta.
   3. The next inference is labeled left conjunction rule.
   4. From the immediately preceding branch using the left conjunction rule, infer antecedent containing first the conjunction of formula A and formula B, then Gamma; sequent arrow; succedent containing capital Delta.

   1. $!A, \Gamma \fCenter \Delta$source 137
   2. $!A \land !B, \Gamma \fCenter \Delta$source 139

   source 135

   and $\Theta = !A \land !B, \Gamma$source 141 while $\Xi = \Delta$source 141. Consider a valuation $\pAssign{v}$source 143. Since by induction hypothesis, $!A, \Gamma \Sequent \Delta$source 144 is valid, (a) $\pSat/{v}{!A}$source 145, (b) $\pSat/{v}{!C}$source 146 for some $!C \in \Gamma$source 146, or (c) $\pSat{v}{!C}$source 147 for some $!C \in \Delta$source 147. In case (a), $\pSat/{v}{!A \land !B}$source 148, so there is $!C \in \Theta$source 149 (namely, $!A \land !B$source 149) such that $\pSat/{v}{!C}$source 150. In case (b), there is $!C \in \Gamma$source 150 such that $\pSat/{v}{!C}$source 151, and $!C \in \Theta$source 152 as well. In case (c), there is $!C \in \Delta$source 152 such that $\pSat{v}{!C}$source 153, and $!C \in \Xi$source 153 as well since $\Xi = \Delta$source 154. So in each case, $\pAssign{v}$source 155 satisfies $!A \land !B, \Gamma \Sequent \Delta$source 155. Since $\pAssign{v}$source 156 was arbitrary, $\Gamma \Sequent \Delta$source 157 is valid. The case where $!A \land !B$source 157 is inferred from $!B$source 158 is handled the same, changing $!A$source 158 to $!B$source 159.

5. The last inference is right disjunction rule: There are two variants: $!A \lor !B$source 160 may be inferred on the right from $!A$source 161 or from $!B$source 161 on the right side of the premise. In the first case, $\pi$source 162 ends in

   Proof diagram: Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B — line 163

   Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B — line 163. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are right disjunction rule. Its last stated proof component is: From the immediately preceding branch using the right disjunction rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then formula A.
   3. The next inference is labeled right disjunction rule.
   4. From the immediately preceding branch using the right disjunction rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the disjunction of formula A and formula B.

   1. $\Gamma \fCenter \Delta, !A$source 165
   2. $\Gamma \fCenter \Delta, !A \lor !B$source 167

   source 163

   Now $\Theta = \Gamma$source 169 and $\Xi = \Delta, !A \lor !B$source 169. Consider a valuation $\pAssign{v}$source 170. Since $\Gamma \Sequent \Delta, !A$source 171 is valid, (a) $\pSat{v}{!A}$source 172, (b) $\pSat/{v}{!C}$source 173 for some $!C \in \Gamma$source 173, or (c) $\pSat{v}{!C}$source 174 for some $!C \in \Delta$source 174. In case (a), $\pSat{v}{!A \lor !B}$source 175. In case (b), there is $!C \in \Gamma$source 176 such that $\pSat/{v}{!C}$source 177. In case (c), there is $!C \in \Delta$source 177 such that $\pSat{v}{!C}$source 178. So in each case, $\pAssign{v}$source 179 satisfies $\Gamma \Sequent \Delta, !A \lor !B$source 180, i.e., $\Theta \Sequent \Xi$source 180. Since $\pAssign{v}$source 181 was arbitrary, $\Theta \Sequent \Xi$source 182 is valid. The case where $!A \lor !B$source 182 is inferred from $!B$source 183 is handled the same, changing $!A$source 183 to $!B$source 183.

6. The last inference is right conditional rule: Then $\pi$source 184 ends in

   Proof diagram: Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B — line 185

   Proof tree concluding antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B — line 185. This source proof tree has 4 explicitly ordered components. Its inference labels, in order, are right conditional rule. Its last stated proof component is: From the immediately preceding branch using the right conditional rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B.

   1. An upper premise slot is intentionally blank in this staged diagram.
   2. Previously derived premise with its intervening derivation omitted: antecedent containing first formula A, then Gamma; sequent arrow; succedent containing first capital Delta, then formula B.
   3. The next inference is labeled right conditional rule.
   4. From the immediately preceding branch using the right conditional rule, infer antecedent containing Gamma; sequent arrow; succedent containing first capital Delta, then the conditional whose antecedent is formula A; and whose consequent is formula B.

   1. $!A, \Gamma \fCenter \Delta, !B$source 187
   2. $\Gamma \fCenter \Delta, !A \lif !B$source 189

   source 185

   Again, the induction hypothesis says that the premise is valid; we want to show that the conclusion is valid as well. Let $\pAssign{v}$source 193 be arbitrary. Since $!A, \Gamma \Sequent \Delta, !B$source 193 is valid, at least one of the following cases obtains: (a) $\pSat/{v}{!A}$source 195, (b) $\pSat{v}{!B}$source 196, (c) $\pSat/{v}{!C}$source 197 for some $~!C \in \Gamma$source 197, or (d) $\pSat{v}{!C}$source 198 for some $!C \in \Delta$source 198. In cases (a) and (b), $\pSat{v}{!A \lif !B}$source 199 and so there is a $!C \in \Delta, !A \lif !B$source 200 such that $\pSat{v}{!C}$source 201. In case (c), for some $!C \in \Gamma$source 201, $\pSat/{v}{!C}$source 202. In case (d), for some $!C \in \Delta$source 203, $\pSat{v}{!C}$source 203. In each case, $\pAssign{v}$source 204 satisfies $\Gamma \Sequent \Delta, !A \lif !B$source 204. Since $\pAssign{v}$source 206 was arbitrary, $\Gamma \Sequent \Delta, !A \lif !B$source 206 is valid.