Sequent Calculus

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Introduction

The sequent calculus for classical logic is an efficient and simple derivation system. If a many-valued logic is defined by a matrix with finitely many truth values, i.e., $V$ source is finite, it is possible to provide a sequent calculus for it. The idea for how to do this comes from considering the meanings of sequents and the form of inference rules in the classical case.

Now recall that a sequent

!A_1, \dots, !A_n & \Sequent !B_1, \dots, !B_n \intertext{can be interpreted as the !!{formula}} (!A_1 \land \cdots \land !A_m) & \lif (!B_1 \lor \cdots \lor !B_n)

source

In other words, A valuation $\pAssign{v}$ source satisfies a sequent $\Gamma \Sequent \Delta$ source iff either $\pValue{v}(!A) = \False$ source for some $!A \in \Gamma$ source or $\pValue{v}(!A) = \True$ source for some $!A \in \Delta$ source. On this interpretation, initial sequents $!A \Sequent !A$ source are always satisfied, because either $\pValue v(!A) = \True$ source or $\pValue(!A) = \False$ source.

Here are the inference rules for the conditional in $\Log{LK}$ source, with side formulas $\Gamma$ source, $\Delta$ source left out:

Classical conditional rules

Classical left conditional rule

Proof tree. Classical left conditional rule. Premise node one: the two sided sequent with antecedent empty and succedent formula A. Premise node two: the two sided sequent with antecedent formula B and succedent empty. The label of the next inference is left conditional rule. From nodes one, and two, in that order, infer node three: the two sided sequent with antecedent the conditional from formula A to formula B and succedent empty. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\fCenter !A$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B \fCenter$ source
Step 3. Depends on step 1, step 2. Rule: left conditional rule.
$\LeftR{\lif}$ source
$!A \lif !B \fCenter$ source

source 38

hfill

Classical right conditional rule

Proof tree. Classical right conditional rule. Premise node one: the two sided sequent with antecedent formula A and succedent formula B. The label of the next inference is right conditional rule. From node one, in that order, infer node two: the two sided sequent with antecedent empty and succedent the conditional from formula A to formula B. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A \fCenter !B$ source
Step 2. Depends on step 1. Rule: right conditional rule.
$\RightR{\lif}$ source
$\fCenter !A \lif !B$ source

source 44

If we apply the above semantic interpretation of a sequent, we can read the $\LeftR{\lif}$ source rule as saying that if $\pValue v(!A) = \True$ source and $\pValue v(!B) = \False$ source, then $\pValue v(!A \lif !B) = \False$ source. Similarly, the $\RightR{\lif}$ source rule says that if either $\pValue v(!A) = \False$ source or $\pValue v(!B) = \True$ source, then $\pValue v(!A \lif !B) = \True$ source. And in fact, these conditionals are actually biconditionals. In the case of the $\LeftR{\land}$ source and $\RightR{\lor}$ source rules in their standard formulation, the corresponding conditionals would not be biconditionals. But there are alternative versions of these rules where they are:

Alternative classical conjunction and disjunction rules

Alternative classical left conjunction rule

Proof tree. Alternative classical left conjunction rule. Premise node one: the two sided sequent with antecedent formula A, followed by formula B, followed by Gamma and succedent Delta. The label of the next inference is left conjunction rule. From node one, in that order, infer node two: the two sided sequent with antecedent the conjunction of formulas A and B, followed by Gamma and succedent Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, !B, \Gamma \fCenter \Delta$ source
Step 2. Depends on step 1. Rule: left conjunction rule.
$\LeftR{\land}$ source
$!A \land !B, \Gamma \fCenter \Delta$ source

source 62

hfill

Alternative classical right disjunction rule

Proof tree. Alternative classical right disjunction rule. Premise node one: the two sided sequent with antecedent Gamma and succedent Delta, followed by formula A, followed by formula B. The label of the next inference is right disjunction rule. From node one, in that order, infer node two: the two sided sequent with antecedent Gamma and succedent Delta, followed by the disjunction of formulas A and B. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \fCenter \Delta, !A, !B$ source
Step 2. Depends on step 1. Rule: right disjunction rule.
$\RightR{\lor}$ source
$\Gamma \fCenter \Delta, !A \lor !B$ source

source 67

This basic idea, applied to an $n$ source-valued logic, then results in a sequent calculus with $n$ source instead of two places, one for each truth value. For a three-valued logic with $V = \{\False, \Undef, \True\}$ source, a sequent is an expression $\Gamma \mid \Pi \mid \Delta$ source. It is satisfied in a valuation $\pAssign v$ source iff either $\pValue{v}(!A) = \False$ source for some $!A \in \Gamma$ source or $\pValue{v}(!A) = \True$ source for some $!A \in \Delta$ source or $\pValue{v}(!A) = \Undef$ source for some $!A \in \Pi$ source. Consequently, initial sequents $!A \mid !A \mid !A$ source are always satisfied.

Rules and derivation

For the following, let $\Gamma, \Delta, \Pi, \Lambda$ source represent finite sequences of sentences.

Definition of an n sided sequent

[Sequent] An $n$ source-sided sequent is an expression of the form

\Gamma_1 \nSequent \dots \nSequent \Gamma_n

source

where each $\Gamma_1$ source is a finite (possibly empty) sequences of sentences of the language $\Lang L$ source.

Definition of initial sequents

[Initial Sequent] An $n$ source-sided initial sequent is an $n$ source-sided sequent of the form $!A \nSequent \dots \nSequent !A$ source for any sentence $!A$ source in the language.

If the language contains a $0$ source-place connective $\star$ source, i.e., a propositional constant, then we also take the sequent $\dots \nSequent \star \nSequent \dots$ source where $\star$ source appears in the space for the truth value associated with $\tf{\star} \in V$ source, and is empty otherwise.

For each connective of an $n$ source-valued logic $\Log{L}$ source, there is a logical rule for each truth value that this connective can take in $\Log{L}$ source. Derivations in an $n$ source-sided sequent calculus for $\Log{L}$ source are trees of sequents, where the topmost sequents are initial sequents, and if a sequent stands below one or more other sequents, it must follow correctly by a rule of inference for the connectives of $\Log{L}$ source.

Definition of theoremhood

[Theorems] A sentence $!A$ source is a theorem of an $n$ source-valued logic $\Log{L}$ source if there is a derivation of the $n$ source-sequent containing $!A$ source in each position corresponding to a designated truth value of $\Log{L}$ source. We write $\Proves[\Log{L}] !A$ source if $!A$ source is a theorem and $\Proves/[\Log{L}] !A$ source if it is not.

Definition of derivability from premises

[Derivability] A sentence $!A$ source is derivable from a set of sentences $\Gamma$ source in an $n$ source-valued logic $\Log{L}$ source, $\Gamma \Proves[\Log{L}] !A$ source, iff there is a finite subset $\Gamma_0 \subseteq \Gamma$ source and a sequence $\Gamma_0'$ source of the sentences in $\Gamma_0$ source such that the following sequent has a derivation:

\Lambda_1 \nSequent \dots \nSequent \Lambda_n

source

where $\Lambda_i$ source is $!A$ source if position $i$ source corresponds to a designated truth value, and $\Gamma_0'$ sourceotherwise. If $!A$ source is not derivable from $\Gamma$ source we write $\Gamma \Proves/ !A$ source.

For instance, $3$ source-valued L ukasiewicz logic has a $3$ source-sided sequent calculus. In a $3$ source-sided sequent $\Gamma \nSequent \Pi \nSequent \Delta$ source, $\Gamma$ source corresponds to $\False$ source, $\Delta$ source to $\True$ source, and $\Pi$ source to $\Undef$ source. Axioms are $!A \nSequent !A \nSequent !A$ source. Since only $\True$ source is designated, $\Gamma \Proves[\LogLuk[3]] !A$ source iff the sequent $\Gamma \nSequent \Gamma \nSequent !A$ source has a derivation. (If $\Undef$ source were also designated, we would need a derivation of $\Gamma \nSequent !A \nSequent !A$ source.)

Structural Rules

The structural rules for $n$ source-sided sequent calculus operate as in the classical case, except for each position $i$ source.

Indexed structural rules

Weakening at an arbitrary position

Proof tree. Weakening at an arbitrary position. Premise node one: the n sided sequent containing Gamma sub one through Gamma sub n, with Gamma sub i in position i; the phantom formula is alignment space only. The label of the next inference is weakening rule at position i. From node one, in that order, infer node two: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains formula A followed by Gamma sub i. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma_1 \nSequent \dots \nSequent \phantom{!A,}\Gamma_i \nSequent \dots \nSequent \Gamma_n$ source
Step 2. Depends on step 1. Rule: weakening rule at position i.
$\iR{\Weakening}{i}$ source
$\Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n$ source

source 18

\\[2ex]

Contraction at an arbitrary position

Proof tree. Contraction at an arbitrary position. Premise node one: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains two consecutive copies of formula A followed by Gamma sub i. The label of the next inference is contraction rule at position i. From node one, in that order, infer node two: the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains one visible copy of formula A followed by Gamma sub i; the phantom copy is alignment space only. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma_1 \nSequent \dots \nSequent !A, !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n$ source
Step 2. Depends on step 1. Rule: contraction rule at position i.
$\iR{\Contraction}{i}$ source
$\Gamma_1 \nSequent \dots \nSequent \phantom{!A,}!A, \Gamma_i \nSequent \dots \nSequent \Gamma_n$ source

source 23

\\[2ex]

Exchange at an arbitrary position

Proof tree. Exchange at an arbitrary position. Premise node one: the n sided sequent with position i containing Gamma sub i, formula A, formula B, then Gamma sub i prime; all other positions retain their respective Gamma sequences. The label of the next inference is exchange rule at position i. From node one, in that order, infer node two: the n sided sequent with position i containing Gamma sub i, formula B, formula A, then Gamma sub i prime; all other positions retain their respective Gamma sequences. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma_1 \nSequent \dots \nSequent \Gamma_i, !A, !B, \Gamma_i' \nSequent \dots \nSequent \Gamma_n$ source
Step 2. Depends on step 1. Rule: exchange rule at position i.
$\iR{\Exchange}{i}$ source
$\Gamma_1 \nSequent \dots \nSequent \Gamma_i, !B, !A, \Gamma_i' \nSequent \dots \nSequent \Gamma_n$ source

source 29

A series of weakening, contraction, and exchange inferences will often be indicated by double inference lines.

The cut rule comes in several forms, one for every combination of distinct positions in the sequent $i \neq j$ source:

Cut at distinct positions

Cut at two distinct positions

Cut rule at distinct positions i and j. The first premise is the n sided sequent with formula A followed by Gamma sub i in position i and Gamma sub k in every other position k. The second premise has formula A followed by Delta sub j in position j and Delta sub k in every other position k. From both premises, in this order, infer the n sided sequent whose position k contains Gamma sub k followed by Delta sub k. Formula A is removed from the two distinguished positions. End cut rule.

Step 1. No premises. Rule: premise of the displayed rule.
the n sided sequent containing Gamma sub one through Gamma sub n, except that position i contains formula A followed by Gamma sub i
Step 2. No premises. Rule: premise of the displayed rule.
the n sided sequent containing Delta sub one through Delta sub n, except that position j contains formula A followed by Delta sub j
Step 3. Depends on step 1, step 2. Rule: cut rule at position i and j.
$\AxiomC{$ \Gamma_1 \nSequent \dots \nSequent !A, \Gamma_i \nSequent \dots \nSequent \Gamma_n $} \AxiomC{$ \Delta_1 \nSequent \dots \nSequent !A, \Delta_j \nSequent \dots \nSequent \Delta_n $} \RightLabel{$\iR{\Cut}{i,j}$} \BinaryInfC{$\Gamma_1,\Delta_1 \nSequent \dots \nSequent \Gamma_n, \Delta_n$} \DisplayProof$ source
the n sided sequent whose position k contains Gamma sub k followed by Delta sub k, for each position k from one through n

source 43

Propositional Rules for Selected Logics

The inference rules for a connective in an $n$ source-sided sequent calculus only depend on the characteristic truth function for the connective. Thus, if some connective is defined by the same truth function in different logics, these $n$ source-sided sequent rules for the connective are the same in those logics.

subsectionRules for $\lnot$ source

The following rules for $\lnot$ source apply to L ukasiewicz and Kleene logics, and their variants.

Negation for Lukasiewicz and Kleene logics

False position negation rule for Lukasiewicz and Kleene logics

Proof tree. False position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is negation rule at position false. From node one, in that order, infer node two: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 2. Depends on step 1. Rule: negation rule at position false.
$\iR{\lnot}{\False}$ source
$\lnot !A, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 26

\\[2ex]

Middle position negation rule for Lukasiewicz and Kleene logics

Proof tree. Middle position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta. The label of the next inference is negation rule at position middle. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position the negation of formula A, followed by Pi; and true position Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, \Pi \nSequent \Delta$ source
Step 2. Depends on step 1. Rule: negation rule at position middle.
$\iR{\lnot}{\Undef}$ source
$\Gamma \nSequent \lnot !A, \Pi \nSequent \Delta$ source

source 31

\\[2ex]

True position negation rule for Lukasiewicz and Kleene logics

Proof tree. True position negation rule for Lukasiewicz and Kleene logics. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is negation rule at position true. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 2. Depends on step 1. Rule: negation rule at position true.
$\iR{\lnot}{\True}$ source
$\Gamma \nSequent \Pi \nSequent \Delta, \lnot !A$ source

source 36

The following rules for $\lnot$ source apply to Gödel logic.

Negation for Goedel logic

False position negation rule for Goedel logic

Proof tree. False position negation rule for Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. The label of the next inference is negation rule at position false in Goedel logic. From node one, in that order, infer node two: the three sided sequent with false position the negation of formula A, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, \Pi \nSequent \Delta, !A$ source
Step 2. Depends on step 1. Rule: negation rule at position false in Goedel logic.
$\iR{\lnot}{\False}[\LogGod]$ source
$\lnot !A, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 46

hfill

True position negation rule for Goedel logic

Proof tree. True position negation rule for Goedel logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is negation rule at position true in Goedel logic. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the negation of formula A. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 2. Depends on step 1. Rule: negation rule at position true in Goedel logic.
$\iR{\lnot}{\True}[\LogGod]$ source
$\Gamma \nSequent \Pi \nSequent \Delta, \lnot !A$ source

source 51

hfill

(In Gödel logic, $\lnot !A$ source can never take the value $\Undef$ source, so there is no rule for the middle position.)

subsectionRules for $\land$ source

These are the rules for $\land$ source in L ukasiewicz, strong Kleene, and Gödel logic.

Conjunction rules for the three selected logics

False position conjunction rule

Proof tree. False position conjunction rule. Premise node one: the three sided sequent with false position formula A, followed by formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conjunction rule at position false. From node one, in that order, infer node two: the three sided sequent with false position the conjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, !B, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 2. Depends on step 1. Rule: conjunction rule at position false.
$\iR{\land}{\False}$ source
$!A \land !B, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 68

\\[2ex]

Middle position conjunction rule

Proof tree. Middle position conjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position formula A, followed by Delta. Premise node two: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position formula B, followed by Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. The label of the next inference is conjunction rule at position middle. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the conjunction of formulas A and B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, \Pi \nSequent !A, \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !B, \Pi \nSequent !B, \Delta$ source
Step 3. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$ source
Step 4. Depends on step 1, step 2, step 3. Rule: conjunction rule at position middle.
$\iR\land\Undef$ source
$\Gamma \nSequent !A \land !B, \Pi \nSequent \Delta$ source

source 73

\\[2ex]

True position conjunction rule

Proof tree. True position conjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula B. The label of the next inference is conjunction rule at position true. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conjunction of formulas A and B. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 2. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !B$ source
Step 3. Depends on step 1, step 2. Rule: conjunction rule at position true.
$\iR\land\True$ source
$\Gamma \nSequent \Pi \nSequent \Delta, !A \land !B$ source

source 80

subsectionRules for $\lor$ source

These are the rules for $\lor$ source in L ukasiewicz, strong Kleene, and Gödel logic.

Disjunction rules for the three selected logics

False position disjunction rule

Proof tree. False position disjunction rule. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is disjunction rule at position false. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the disjunction of formulas A and B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 3. Depends on step 1, step 2. Rule: disjunction rule at position false.
$\iR\lor\False$ source
$!A \lor !B, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 95

\\[2ex]

Middle position disjunction rule

Proof tree. Middle position disjunction rule. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. The label of the next inference is disjunction rule at position middle. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the disjunction of formulas A and B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent !B, \Pi \nSequent \Delta$ source
Step 3. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$ source
Step 4. Depends on step 1, step 2, step 3. Rule: disjunction rule at position middle.
$\iR\lor\Undef$ source
$\Gamma \nSequent !A \lor !B, \Pi \nSequent \Delta$ source

source 101

\\[2ex]

True position disjunction rule

Proof tree. True position disjunction rule. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A, followed by formula B. The label of the next inference is disjunction rule at position true. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the disjunction of formulas A and B. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A, !B$ source
Step 2. Depends on step 1. Rule: disjunction rule at position true.
$\iR\lor\True$ source
$\Gamma \nSequent \Pi \nSequent \Delta, !A \lor !B$ source

source 108

subsectionRules for $\lif$ source

These are the rules for $\lif$ source in L ukasiewicz logic.

Conditional rules for three valued Lukasiewicz logic

False position conditional rule for three valued Lukasiewicz logic

Proof tree. False position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position false in three valued Lukasiewicz logic.
$\iR\lif\False[\LogLuk[3]]$ source
$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 121

\\[2ex]

Middle position conditional rule for three valued Lukasiewicz logic

Proof tree. Middle position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position middle in three valued Lukasiewicz logic.
$\iR\lif\Undef[\LogLuk[3]]$ source
$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$ source

source 127

\\[2ex]

True position conditional rule for three valued Lukasiewicz logic

Proof tree. True position conditional rule for three valued Lukasiewicz logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B. Premise node two: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in three valued Lukasiewicz logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent !B, \Pi \nSequent \Delta, !B$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta, !B$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position true in three valued Lukasiewicz logic.
$\iR{\lif}{\True}[\LogLuk[3]]$ source
$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$ source

source 133

These are the rules for $\lif$ source in strong Kleene logic.

Conditional rules for strong Kleene logic

False position conditional rule for strong Kleene logic

Proof tree. False position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in strong Kleene logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position false in strong Kleene logic.
$\iR\lif\False[\LogKs]$ source
$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 145

\\[2ex]

Middle position conditional rule for strong Kleene logic

Proof tree. Middle position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position formula B, followed by Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position Gamma; middle position formula A, followed by formula B, followed by Pi; and true position Delta. Premise node three: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in strong Kleene logic. From nodes one, and two, and three, in that order, infer node four: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node four. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent !B, \Pi \nSequent \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, !B, \Pi \nSequent \Delta$ source
Step 3. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, \Pi \nSequent \Delta, !A$ source
Step 4. Depends on step 1, step 2, step 3. Rule: conditional rule at position middle in strong Kleene logic.
$\iR\lif\Undef[\LogKs]$ source
$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$ source

source 151

\\[2ex]

True position conditional rule for strong Kleene logic

Proof tree. True position conditional rule for strong Kleene logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in strong Kleene logic. From node one, in that order, infer node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent \Pi \nSequent \Delta, !B$ source
Step 2. Depends on step 1. Rule: conditional rule at position true in strong Kleene logic.
$\iR{\lif}{\True}[\LogKs]$ source
$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$ source

source 158

These are the rules for $\lif$ source in Gödel logic.

Conditional rules for three valued Goedel logic

False position conditional rule for three valued Goedel logic

Proof tree. False position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula A. Premise node two: the three sided sequent with false position formula B, followed by Gamma; middle position Pi; and true position Delta. The label of the next inference is conditional rule at position false in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position the conditional from formula A to formula B, followed by Gamma; middle position Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !A, \Pi \nSequent \Delta, !A$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!B, \Gamma \nSequent \Pi \nSequent \Delta$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position false in three valued Goedel logic.
$\iR\lif\False[\LogGod[3]]$ source
$!A \lif !B, \Gamma \nSequent \Pi \nSequent \Delta$ source

source 169

\\[2ex]

Middle position conditional rule for three valued Goedel logic

Proof tree. Middle position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position Gamma; middle position formula B, followed by Pi; and true position Delta. Premise node two: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by formula A. The label of the next inference is conditional rule at position middle in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position the conditional from formula A to formula B, followed by Pi; and true position Delta. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent !B, \Pi \nSequent \Delta$ source
Step 2. No premises. Rule: premise of the displayed rule.
$\Gamma \nSequent \Pi \nSequent \Delta, !A$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position middle in three valued Goedel logic.
$\iR\lif\Undef[\LogGod[3]]$ source
$\Gamma \nSequent !A \lif !B, \Pi \nSequent \Delta$ source

source 175

\\[2ex]

True position conditional rule for three valued Goedel logic

Proof tree. True position conditional rule for three valued Goedel logic. Premise node one: the three sided sequent with false position formula A, followed by Gamma; middle position formula B, followed by Pi; and true position Delta, followed by formula B. Premise node two: the three sided sequent with false position formula A, followed by Gamma; middle position formula A, followed by Pi; and true position Delta, followed by formula B. The label of the next inference is conditional rule at position true in three valued Goedel logic. From nodes one, and two, in that order, infer node three: the three sided sequent with false position Gamma; middle position Pi; and true position Delta, followed by the conditional from formula A to formula B. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent !B, \Pi \nSequent \Delta, !B$ source
Step 2. No premises. Rule: premise of the displayed rule.
$!A, \Gamma \nSequent !A, \Pi \nSequent \Delta, !B$ source
Step 3. Depends on step 1, step 2. Rule: conditional rule at position true in three valued Goedel logic.
$\iR{\lif}{\True}[\LogGod[3]]$ source
$\Gamma \nSequent \Pi \nSequent \Delta, !A \lif !B$ source

source 181

Worked Lukasiewicz derivation figure

Worked branched derivation in three valued Lukasiewicz logic

Proof tree. Worked branched derivation in three valued Lukasiewicz logic. Initial sequent node one: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node one, in that order, infer node two: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position middle. From node two, in that order, infer node three: the three sided sequent with false position formula A; middle position formula B, followed by formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position middle. From node three, in that order, infer node four: the three sided sequent with false position formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B, followed by formula A. Initial sequent node five: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node five, in that order, infer node six: the three sided sequent with false position formula A; middle position formula A; and true position formula A, followed by formula A. The label of the next inference is weakening rule at position true. From node six, in that order, infer node seven: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A. The label of the next inference is weakening rule at position false. From node seven, in that order, infer node eight: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A, followed by formula A. The label of the next inference is conditional rule at position middle. From nodes four, and eight, in that order, infer node nine: the three sided sequent with false position formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B, followed by formula A. Initial sequent node ten: the three sided sequent with false position formula B; middle position formula B; and true position formula B. The label of the next inference is weakening rule at position middle. From node ten, in that order, infer node eleven: the three sided sequent with false position formula B; middle position formula A, followed by formula B; and true position formula B. The label of the next inference is exchange rule at position middle. From node eleven, in that order, infer node twelve: the three sided sequent with false position formula B; middle position formula B, followed by formula A; and true position formula B. The label of the next inference is weakening rule at position middle. From node twelve, in that order, infer node thirteen: the three sided sequent with false position formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B. The label of the next inference is weakening rule at position false. From node thirteen, in that order, infer node fourteen: the three sided sequent with false position formula A, followed by formula B; middle position formula A, followed by formula B, followed by formula A; and true position formula B. The label of the next inference is exchange rule at position false. From node fourteen, in that order, infer node fifteen: the three sided sequent with false position formula B, followed by formula A; middle position formula A, followed by formula B, followed by formula A; and true position formula B. Initial sequent node sixteen: the three sided sequent with false position formula A; middle position formula A; and true position formula A. The label of the next inference is weakening rule at position true. From node sixteen, in that order, infer node seventeen: the three sided sequent with false position formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position false. From node seventeen, in that order, infer node eighteen: the three sided sequent with false position formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is weakening rule at position false. From node eighteen, in that order, infer node nineteen: the three sided sequent with false position formula B, followed by formula B, followed by formula A; middle position formula A; and true position formula B, followed by formula A. The label of the next inference is conditional rule at position middle. From nodes fifteen, and nineteen, in that order, infer node twenty: the three sided sequent with false position formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B. The label of the next inference is conditional rule at position false. From nodes nine, and twenty, in that order, infer node twenty one: the three sided sequent with false position the conditional from formula A to formula B, followed by formula A; middle position the conditional from formula A to formula B, followed by formula A; and true position formula B. The root conclusion is node twenty one. End proof tree.

Step 1. No premises. Rule: initial sequent.
$A \nSequent A \nSequent A$ source
Step 2. Depends on step 1. Rule: weakening rule at position true.
$\iR \Weakening \True$ source
$A \nSequent A \nSequent B, A$ source
Step 3. Depends on step 2. Rule: weakening rule at position middle.
$\iR \Weakening \Undef$ source
$A \nSequent B, A \nSequent B, A$ source
Step 4. Depends on step 3. Rule: weakening rule at position middle.
$\iR \Weakening \Undef$ source
$A \nSequent A, B, A \nSequent B, A$ source
Step 5. No premises. Rule: initial sequent.
$A \nSequent A \nSequent A$ source
Step 6. Depends on step 5. Rule: weakening rule at position true.
$\iR \Weakening \True$ source
$A \nSequent A \nSequent A, A$ source
Step 7. Depends on step 6. Rule: weakening rule at position true.
$\iR \Weakening \True$ source
$A \nSequent A \nSequent B, A, A$ source
Step 8. Depends on step 7. Rule: weakening rule at position false.
$\iR \Weakening \False$ source
$B, A \nSequent A \nSequent B, A, A$ source
Step 9. Depends on step 4, step 8. Rule: conditional rule at position middle.
$\iR\lif\Undef$ source
$A \nSequent A \lif B, A \nSequent B, A$ source
Step 10. No premises. Rule: initial sequent.
$B \nSequent B \nSequent B$ source
Step 11. Depends on step 10. Rule: weakening rule at position middle.
$\iR \Weakening \Undef$ source
$B \nSequent A, B \nSequent B$ source
Step 12. Depends on step 11. Rule: exchange rule at position middle.
$\iR \Exchange \Undef$ source
$B \nSequent B, A \nSequent B$ source
Step 13. Depends on step 12. Rule: weakening rule at position middle.
$\iR \Weakening \Undef$ source
$B \nSequent A, B, A \nSequent B$ source
Step 14. Depends on step 13. Rule: weakening rule at position false.
$\iR \Weakening \False$ source
$A, B \nSequent A, B, A \nSequent B$ source
Step 15. Depends on step 14. Rule: exchange rule at position false.
$\iR \Exchange \False$ source
$B, A \nSequent A, B, A \nSequent B$ source
Step 16. No premises. Rule: initial sequent.
$A \nSequent A \nSequent A$ source
Step 17. Depends on step 16. Rule: weakening rule at position true.
$\iR \Weakening \True$ source
$A \nSequent A \nSequent B, A$ source
Step 18. Depends on step 17. Rule: weakening rule at position false.
$\iR \Weakening \False$ source
$B, A \nSequent A \nSequent B, A$ source
Step 19. Depends on step 18. Rule: weakening rule at position false.
$\iR \Weakening \False$ source
$B, B, A \nSequent A \nSequent B, A$ source
Step 20. Depends on step 15, step 19. Rule: conditional rule at position middle.
$\iR\lif\Undef$ source
$B, A \nSequent A \lif B, A \nSequent B$ source
Step 21. Depends on step 9, step 20. Rule: conditional rule at position false.
$\iR\lif\False$ source
$A \lif B, A \nSequent A \lif B, A \nSequent B$ source

source 192

captionExample derivation in $\LogLuk[3]$ source

Source disclosures

TR049-SAR-001: The source lists the antecedent through A sub n in the sequent but through A sub m in the interpreting formula. The index mismatch is retained and disclosed. This edition does not silently assert an equivalence after choosing one endpoint. source
TR049-SAR-002: The final value expression in this sentence omits the valuation argument after the value macro. The surrounding sentence discusses valuation v, but the omission remains visible in source and is explicitly named in the reading. source
TR049-SAR-003: The source says each Gamma sub one and uses the plural sequences after a singular subject. Its displayed n sided list and definition concern one finite sequence at each position. These wording defects are retained with this note. source

Reading preferences

Source file content/many-valued-logic/sequent-calculus/sequent-calculus.tex

Source file content/many-valued-logic/sequent-calculus/introduction.tex

Introduction

Classical conditional rules

Classical left conditional rule

Classical right conditional rule

Alternative classical conjunction and disjunction rules

Alternative classical left conjunction rule

Alternative classical right disjunction rule

Source file content/many-valued-logic/sequent-calculus/rules-and-proofs.tex

Rules and derivation

Definition of an n sided sequent

Definition of initial sequents

Definition of theoremhood

Definition of derivability from premises

Source file content/many-valued-logic/sequent-calculus/structural-rules.tex

Structural Rules

Indexed structural rules

Weakening at an arbitrary position

Contraction at an arbitrary position

Exchange at an arbitrary position

Cut at distinct positions

Cut at two distinct positions

Source file content/many-valued-logic/sequent-calculus/propositional-rules.tex

Propositional Rules for Selected Logics

Negation for Lukasiewicz and Kleene logics

False position negation rule for Lukasiewicz and Kleene logics

Middle position negation rule for Lukasiewicz and Kleene logics

True position negation rule for Lukasiewicz and Kleene logics

Negation for Goedel logic

False position negation rule for Goedel logic

True position negation rule for Goedel logic

Conjunction rules for the three selected logics

False position conjunction rule

Middle position conjunction rule

True position conjunction rule

Disjunction rules for the three selected logics

False position disjunction rule

Middle position disjunction rule

True position disjunction rule

Conditional rules for three valued Lukasiewicz logic

False position conditional rule for three valued Lukasiewicz logic

Middle position conditional rule for three valued Lukasiewicz logic

True position conditional rule for three valued Lukasiewicz logic

Conditional rules for strong Kleene logic

False position conditional rule for strong Kleene logic

Middle position conditional rule for strong Kleene logic

True position conditional rule for strong Kleene logic

Conditional rules for three valued Goedel logic

False position conditional rule for three valued Goedel logic

Middle position conditional rule for three valued Goedel logic

True position conditional rule for three valued Goedel logic

Worked Lukasiewicz derivation figure

Worked branched derivation in three valued Lukasiewicz logic

Source disclosures