Modal Sequent Calculus

Reading preferences

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

Editorial

Draft chapter on sequent calculi for modal logic. Needs more examples, soundness and completeness proofs.

Introduction

The sequent calculus for propositional logic can be extended by additional rules that deal with $\Box$ source and $\Diamond$ source . For instance, for $\Log{K}$ source, we have LogLK plus:

\Axiom$\Gamma \fCenter \Delta, !A$ \RightLabel{$\Box$} \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta, \Box!A$ \DisplayProof \qquad \Axiom$!A, \Gamma \fCenter \Delta$ \RightLabel{$\Diamond$} \UnaryInf$\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$ \DisplayProof

source

K box-rule schema in the introduction

Source premise node one: Gamma yields Delta comma formula A. The next inference is labeled box rule. From node one, infer node two: box Gamma yields diamond Delta comma box formula A. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
Gamma yields Delta comma formula A
Step 2. Depends on step 1. Rule: box rule.
box Gamma yields diamond Delta comma box formula A

source 20

K diamond-rule schema in the introduction

Source premise node one: formula A comma Gamma yields Delta. The next inference is labeled diamond rule. From node one, infer node two: diamond formula A comma box Gamma yields diamond Delta. The root conclusion is node two. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
formula A comma Gamma yields Delta
Step 2. Depends on step 1. Rule: diamond rule.
diamond formula A comma box Gamma yields diamond Delta

source 25

For extensions of $\Log{K}$ source, additional rules have to be added as well.

Not every modal logic has such a sequent calculus. Even $\Log{S5}$ source, which is semantically simple (it can be defined without using accessibility relations at all) is not known to have a sequent calculus that results from $\Log{LK}$ source which is complete without the rule cut. However, it has a cut-free complete hypersequent calculus.

Rules for LogK

The rules for the regular propositional connectives are the same as for regular sequent calculus $\Log{LK}$ source. Axioms are also the same: any sequent of the form $!A \Sequent !A$ source counts as an axiom.

For the modal operator s $\Box$ source and $\Diamond$ source , we have the following additional rules :

\Axiom$\Gamma \fCenter \Delta, !A$ \RightLabel{$\Box$} \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta, \Box!A$ \DisplayProof \qquad \Axiom$!A, \Gamma \fCenter \Delta$ \RightLabel{$\Diamond$} \UnaryInf$\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$ \DisplayProof

source

K box-rule schema

Step 1. No premises. Rule: source axiom or displayed premise.
Gamma yields Delta comma formula A
Step 2. Depends on step 1. Rule: box rule.
box Gamma yields diamond Delta comma box formula A

source 22

K diamond-rule schema

Step 1. No premises. Rule: source axiom or displayed premise.
formula A comma Gamma yields Delta
Step 2. Depends on step 1. Rule: diamond rule.
diamond formula A comma box Gamma yields diamond Delta

source 27

Here, $\Box\Gamma$ source means the sequence of formulas resulting from $\Gamma$ source by putting $\Box$ source in front of every formula in $\Gamma$ source and $\Diamond\Delta$ source is the sequence of formulas resulting from $\Delta$ source by putting $\Diamond$ source in front of every formula in $\Delta$ source .

$\Gamma$ source and $\Delta$ source may be empty; in that case the corresponding part $\Box\Gamma$ source and $\Diamond\Delta$ source of the conclusion sequent is empty as well.

The restriction of adding a $\Box$ source on the right and $\Diamond$ source on the left to a single formula $!A$ source is necessary. If we allowed to add $\Box$ source to any number of formulas on the right or to add $\Diamond$ source to any number of formulas on the left we would be able to derive:

\Axiom$!A \fCenter !A$ \RightLabel{\RightR{\lnot}} \UnaryInf$\fCenter !A, \lnot !A$ \RightLabel{$\Box*$} \UnaryInf$\fCenter \Box!A, \Box\lnot !A$ \doubleLine \RightLabel{\RightR{\lor}} \UnaryInf$\fCenter \Box!A \lor \Box \lnot !A$ \DisplayProof \qquad \Axiom$!A \fCenter !A$ \RightLabel{\LeftR{\lnot}} \UnaryInf$\lnot !A, !A \fCenter$ \RightLabel{$\Diamond*$} \UnaryInf$\Diamond\lnot !A,\Diamond!A \fCenter $ \RightLabel{\RightR{\lnot}} \UnaryInf$\Diamond!A \fCenter \lnot\Diamond\lnot !A$ \RightLabel{\RightR{\lif}} \UnaryInf$ \fCenter \Diamond!A \lif \lnot\Diamond\lnot !A$ \DisplayProof

source

Hypothetical invalid starred-box derivation

Source premise node one: formula A yields formula A. The next inference is labeled negation right rule. From node one, infer node two: yields formula A comma not formula A. The next inference is labeled invalid starred box rule. From node two, infer node three: yields box formula A comma box not formula A. The source prints a double inference line; any compressed structural steps remain omitted. The next inference is labeled disjunction right rule. From node three, infer node four: yields box formula A or box not formula A. The root conclusion is node four. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
formula A yields formula A
Step 2. Depends on step 1. Rule: negation right rule.
yields formula A comma not formula A
Step 3. Depends on step 2. Rule: invalid starred box rule.
yields box formula A comma box not formula A
Step 4. Depends on step 3. Rule: disjunction right rule.
yields box formula A or box not formula A

source 68

Hypothetical invalid starred-diamond derivation

Source premise node one: formula A yields formula A. The next inference is labeled negation left rule. From node one, infer node two: not formula A comma formula A yields. The next inference is labeled invalid starred diamond rule. From node two, infer node three: diamond not formula A comma diamond formula A yields. The next inference is labeled negation right rule. From node three, infer node four: diamond formula A yields not diamond not formula A. The next inference is labeled conditional right rule. From node four, infer node five: yields diamond formula A implies not diamond not formula A. The root conclusion is node five. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
formula A yields formula A
Step 2. Depends on step 1. Rule: negation left rule.
not formula A comma formula A yields
Step 3. Depends on step 2. Rule: invalid starred diamond rule.
diamond not formula A comma diamond formula A yields
Step 4. Depends on step 3. Rule: negation right rule.
diamond formula A yields not diamond not formula A
Step 5. Depends on step 4. Rule: conditional right rule.
yields diamond formula A implies not diamond not formula A

source 79

But $\Box!A \lor \Box \lnot !A$ source and $\Diamond!A \lif \lnot\Diamond\lnot !A$ source are not valid in $\Log{K}$ source.

If we allowed side formulas in addition to $!A$ source in the premise, and allowed the $\Box$ source rule to add $\Box$ source to only $!A$ source on the right , or allowed the $\Diamond$ source rule to add $\Diamond$ source to only $!A$ source on the left (but do nothing to the side formulas) we would be able to derive:

\Axiom$!A \fCenter !A$ \RightLabel{\RightR{\lnot}} \UnaryInf$\fCenter !A, \lnot !A$ \RightLabel{\RightR{\Exchange}} \UnaryInf$\fCenter \lnot !A, !A$ \RightLabel{$\Box*$} \UnaryInf$\fCenter \lnot!A, \Box !A$ \doubleLine \RightLabel{\RightR{\lor}} \UnaryInf$\fCenter \lnot!A \lor \Box !A$ \DisplayProof \qquad \Axiom$!A \fCenter !A$ \RightLabel{\LeftR{\lnot}} \UnaryInf$\lnot !A, !A \fCenter$ \RightLabel{$\Diamond*$} \UnaryInf$\Diamond\lnot !A, !A \fCenter $ \RightLabel{\RightR{\lnot}} \UnaryInf$!A \fCenter \lnot\Diamond\lnot !A$ \RightLabel{\RightR{\lif}} \UnaryInf$ \fCenter !A \lif \lnot\Diamond\lnot !A$ \DisplayProof

source

Hypothetical invalid side-formula box derivation

Source premise node one: formula A yields formula A. The next inference is labeled negation right rule. From node one, infer node two: yields formula A comma not formula A. The next inference is labeled exchange right rule. From node two, infer node three: yields not formula A comma formula A. The next inference is labeled invalid starred box rule. From node three, infer node four: yields not formula A comma box formula A. The source prints a double inference line; any compressed structural steps remain omitted. The next inference is labeled disjunction right rule. From node four, infer node five: yields not formula A or box formula A. The root conclusion is node five. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
formula A yields formula A
Step 2. Depends on step 1. Rule: negation right rule.
yields formula A comma not formula A
Step 3. Depends on step 2. Rule: exchange right rule.
yields not formula A comma formula A
Step 4. Depends on step 3. Rule: invalid starred box rule.
yields not formula A comma box formula A
Step 5. Depends on step 4. Rule: disjunction right rule.
yields not formula A or box formula A

source 101

Hypothetical invalid side-formula diamond derivation

Source premise node one: formula A yields formula A. The next inference is labeled negation left rule. From node one, infer node two: not formula A comma formula A yields. The next inference is labeled invalid starred diamond rule. From node two, infer node three: diamond not formula A comma formula A yields. The next inference is labeled negation right rule. From node three, infer node four: formula A yields not diamond not formula A. The next inference is labeled conditional right rule. From node four, infer node five: yields formula A implies not diamond not formula A. The root conclusion is node five. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
formula A yields formula A
Step 2. Depends on step 1. Rule: negation left rule.
not formula A comma formula A yields
Step 3. Depends on step 2. Rule: invalid starred diamond rule.
diamond not formula A comma formula A yields
Step 4. Depends on step 3. Rule: negation right rule.
formula A yields not diamond not formula A
Step 5. Depends on step 4. Rule: conditional right rule.
yields formula A implies not diamond not formula A

source 114

But $\lnot!A \lor \Box !A$ source (which is equivalent to $!A \lif \Box!A$ source) and $!A \lif \lnot\Diamond\lnot !A$ source are not valid in $\Log{K}$ source.

Sequent derivation for LogK

Example: box preserves conjunction

We give a sequent calculus derivation that shows $\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$ source.

Sequent proof that box preserves conjunction

Source premise node one: formula A yields formula A. The source prints a double inference line; any compressed structural steps remain omitted. From node one, infer node two: formula B comma formula A yields formula A. Source premise node three: formula B yields formula B. The source prints a double inference line; any compressed structural steps remain omitted. From node three, infer node four: formula B comma formula A yields formula B. The next inference is labeled conjunction right rule. From nodes two, then four, infer node five: formula B comma formula A yields formula A and formula B. The next inference is labeled box rule. From node five, infer node six: box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis. The next inference is labeled conjunction left rule. From node six, infer node seven: box formula A and box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis. The next inference is labeled exchange left rule. From node seven, infer node eight: box formula A comma box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis. The next inference is labeled conjunction left rule. From node eight, infer node nine: box formula A and box formula B comma box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis. The next inference is labeled contraction left rule. From node nine, infer node ten: box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis. The next inference is labeled conditional right rule. From node ten, infer node eleven: yields open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis. The root conclusion is node eleven. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$!A \fCenter !A$ source
Step 2. Depends on step 1. Rule: compressed source inference marked by a double line.
$!B, !A \fCenter !A$ source
Step 3. No premises. Rule: source axiom or displayed premise.
$!B \fCenter !B$ source
Step 4. Depends on step 3. Rule: compressed source inference marked by a double line.
$!B, !A \fCenter !B$ source
Step 5. Depends on step 2, step 4. Rule: conjunction right rule.
$!B, !A \fCenter !A \land !B$ source
Step 6. Depends on step 5. Rule: box rule.
$\Box$ source
$\Box!B, \Box!A \fCenter \Box (!A \land !B)$ source
Step 7. Depends on step 6. Rule: conjunction left rule.
$\Box!A \land \Box!B, \Box!A \fCenter \Box (!A \land !B)$ source
Step 8. Depends on step 7. Rule: exchange left rule.
$\Box!A, \Box!A \land \Box!B \fCenter \Box (!A \land !B)$ source
Step 9. Depends on step 8. Rule: conjunction left rule.
$\Box!A \land \Box!B, \Box!A \land \Box!B \fCenter \Box (!A \land !B)$ source
Step 10. Depends on step 9. Rule: contraction left rule.
$\Box!A \land \Box!B \fCenter \Box (!A \land !B)$ source
Step 11. Depends on step 10. Rule: conditional right rule.
$\fCenter (\Box!A \land \Box!B) \lif \Box (!A \land !B)$ source

\RightR{\land}

source

\LeftR{\land}

source

\LeftR{\Exchange}

source

\LeftR{\land}

source

\LeftR{\Contraction}

source

\RightR{\lif}

source

source 18

Example: diamond distributes over disjunction

We give a sequent calculus derivation that shows $\Proves \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond!B)$ source.

Sequent proof that diamond distributes over disjunction

Source premise node one: formula A yields formula A. The source prints a double inference line; any compressed structural steps remain omitted. From node one, infer node two: formula A yields formula A comma formula B. Source premise node three: formula B yields formula B. The source prints a double inference line; any compressed structural steps remain omitted. From node three, infer node four: formula B yields formula A comma formula B. The next inference is labeled disjunction left rule. From nodes two, then four, infer node five: formula A or formula B yields formula A comma formula B. The next inference is labeled diamond rule. From node five, infer node six: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula B. The next inference is labeled disjunction right rule. From node six, infer node seven: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula A or diamond formula B. The next inference is labeled exchange right rule. From node seven, infer node eight: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B comma diamond formula A. The next inference is labeled disjunction right rule. From node eight, infer node nine: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B comma diamond formula A or diamond formula B. The next inference is labeled contraction right rule. From node nine, infer node ten: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B. The next inference is labeled conditional right rule. From node ten, infer node eleven: yields diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or diamond formula B close parenthesis. The root conclusion is node eleven. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$!A \fCenter !A$ source
Step 2. Depends on step 1. Rule: compressed source inference marked by a double line.
$!A \fCenter !A, !B$ source
Step 3. No premises. Rule: source axiom or displayed premise.
$!B \fCenter !B$ source
Step 4. Depends on step 3. Rule: compressed source inference marked by a double line.
$!B \fCenter !A, !B$ source
Step 5. Depends on step 2, step 4. Rule: disjunction left rule.
$!A \lor !B \fCenter !A, !B$ source
Step 6. Depends on step 5. Rule: diamond rule.
$\Diamond$ source
$\Diamond(!A \lor !B) \fCenter \Diamond !A, \Diamond!B$ source
Step 7. Depends on step 6. Rule: disjunction right rule.
$\Diamond(!A \lor !B) \fCenter \Diamond !A, \Diamond !A \lor \Diamond!B$ source
Step 8. Depends on step 7. Rule: exchange right rule.
$\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B, \Diamond !A$ source
Step 9. Depends on step 8. Rule: disjunction right rule.
$\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B, \Diamond !A \lor \Diamond!B$ source
Step 10. Depends on step 9. Rule: contraction right rule.
$\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B$ source
Step 11. Depends on step 10. Rule: conditional right rule.
$\fCenter \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond!B)$ source

\LeftR{\lor}

source

\RightR{\lor}

source

\RightR{\Exchange}

source

\RightR{\lor}

source

\RightR{\Contraction}

source

\RightR{\lif}

source

source 51

Here is a derivation of Dual.

Sequent derivation of modal duality

Source premise node one: formula A yields formula A. The next inference is labeled negation right rule. From node one, infer node two: not formula A comma formula A yields. The next inference is labeled diamond rule. From node two, infer node three: diamond not formula A comma box formula A yields. The next inference is labeled negation right rule. From node three, infer node four: box formula A yields not diamond not formula A. The next inference is labeled conditional right rule. From node four, infer node five: yields box formula A implies not diamond not formula A. Source premise node six: formula A yields formula A. The next inference is labeled negation right rule. From node six, infer node seven: yields formula A comma not formula A. The next inference is labeled exchange right rule. From node seven, infer node eight: yields not formula A comma formula A. The next inference is labeled box rule. From node eight, infer node nine: yields diamond not formula A comma box formula A. The next inference is labeled exchange right rule. From node nine, infer node ten: yields box formula A comma diamond not formula A. The next inference is labeled negation right rule. From node ten, infer node eleven: not diamond not formula A yields box formula A. The next inference is labeled conditional right rule. From node eleven, infer node twelve: yields not diamond not formula A implies box formula A. The next inference is labeled conjunction right rule. From nodes five, then twelve, infer node thirteen: yields box formula A if and only if not diamond not formula A. The root conclusion is node thirteen. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$!A \fCenter !A$ source
Step 2. Depends on step 1. Rule: negation right rule.
$\lnot !A, !A \fCenter$ source
Step 3. Depends on step 2. Rule: diamond rule.
$\Diamond$ source
$\Diamond\lnot !A, \Box !A \fCenter$ source
Step 4. Depends on step 3. Rule: negation right rule.
$\Box !A \fCenter \lnot\Diamond\lnot !A$ source
Step 5. Depends on step 4. Rule: conditional right rule.
$\fCenter \Box !A \lif \lnot\Diamond\lnot !A$ source
Step 6. No premises. Rule: source axiom or displayed premise.
$!A \fCenter !A$ source
Step 7. Depends on step 6. Rule: negation right rule.
$\fCenter !A, \lnot !A$ source
Step 8. Depends on step 7. Rule: exchange right rule.
$\fCenter \lnot !A, !A$ source
Step 9. Depends on step 8. Rule: box rule.
$\Box$ source
$\fCenter \Diamond\lnot !A, \Box !A$ source
Step 10. Depends on step 9. Rule: exchange right rule.
$\fCenter \Box !A, \Diamond\lnot !A$ source
Step 11. Depends on step 10. Rule: negation right rule.
$\lnot\Diamond\lnot !A \fCenter \Box !A$ source
Step 12. Depends on step 11. Rule: conditional right rule.
$\fCenter \lnot \Diamond \lnot !A \lif \Box !A$ source
Step 13. Depends on step 5, step 12. Rule: conjunction right rule.
$\fCenter \Box !A \liff \lnot\Diamond\lnot !A$ source

\RightR{\lnot}

source

\RightR{\lnot}

source

\RightR{\lif}

source

\RightR{\lnot}

source

\RightR{\Exchange}

source

\RightR{\Exchange}

source

\RightR{\lnot}

source

\RightR{\lif}

source

\RightR{\land}

source

source 83

Exercises in modal sequent calculus for K

Find sequent calculus proofs in $\Log{K}$ source for the following formulas:

$\Box \lnot p \lif \Box(p \lif q)$ source
$(\Box p \lor \Box q) \lif \Box(p \lor q)$ source
$\Diamond p \lif \Diamond(p \lor q)$ source
$\Box(p \land q) \lif \Box p$ source

Rules for Other Accessibility Relations

In order to deal with logics determined by special accessibility relations, we consider the additional rules in the table of additional modal sequent rules.

Table

defarraystretch3

Inner table: more modal rules

More modal rules, inner source table. The source prints no column-heading row; the following cells are read top to bottom and left to right. Row one, unlabelled first cell. Source premise node one: formula A comma Gamma yields Delta. The next inference is labeled T box rule. From node one, infer node two: box formula A comma Gamma yields Delta. The root conclusion is node two. End proof tree. Row one, unlabelled second cell. Source premise node one: Gamma yields Delta comma formula A. The next inference is labeled T diamond rule. From node one, infer node two: Gamma yields Delta comma diamond formula A. The root conclusion is node two. End proof tree. Row two, one cell spanning both source columns. Source premise node one: Gamma yields Delta. The next inference is labeled D rule. From node one, infer node two: box Gamma yields diamond Delta. The root conclusion is node two. End proof tree. Row three, unlabelled first cell. Source premise node one: Gamma comma diamond Pi yields box Delta comma Lambda comma formula A. The next inference is labeled B box rule. From node one, infer node two: box Gamma comma Pi yields Delta comma diamond Lambda comma box formula A. The root conclusion is node two. End proof tree. Row three, unlabelled second cell. Source premise node one: formula A comma diamond Gamma comma Pi yields box Lambda comma Delta. The next inference is labeled B diamond rule. From node one, infer node two: diamond formula A comma Gamma comma box Pi yields Lambda comma diamond Delta. The root conclusion is node two. End proof tree. Row four, unlabelled first cell. Source premise node one: box Gamma yields diamond Delta comma formula A. The next inference is labeled four box rule. From node one, infer node two: box Gamma yields diamond Delta comma box formula A. The root conclusion is node two. End proof tree. Row four, unlabelled second cell. Source premise node one: formula A comma box Gamma yields diamond Delta. The next inference is labeled four diamond rule. From node one, infer node two: diamond formula A comma box Gamma yields diamond Delta. The root conclusion is node two. End proof tree. Row five, unlabelled first cell. Source premise node one: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma formula A. The next inference is labeled five box rule. From node one, infer node two: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma box formula A. The root conclusion is node two. End proof tree. Row five, unlabelled second cell. Source premise node one: formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda. The next inference is labeled five diamond rule. From node one, infer node two: diamond formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda. The root conclusion is node two. End proof tree. End table.

Inner table: more modal rules
unlabelled first source column	unlabelled second source column
T box-rule schema Source premise node one: formula A comma Gamma yields Delta. The next inference is labeled T box rule. From node one, infer node two: box formula A comma Gamma yields Delta. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $!A, \Gamma \fCenter \Delta$ source Step 2. Depends on step 1. Rule: T box rule. $\Box$ source $\Box!A, \Gamma \fCenter \Delta$ source	T diamond-rule schema Source premise node one: Gamma yields Delta comma formula A. The next inference is labeled T diamond rule. From node one, infer node two: Gamma yields Delta comma diamond formula A. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $\Gamma \fCenter \Delta, !A$ source Step 2. Depends on step 1. Rule: T diamond rule. $\Diamond$ source $\Gamma \fCenter \Delta, \Diamond!A$ source
D rule schema Source premise node one: Gamma yields Delta. The next inference is labeled D rule. From node one, infer node two: box Gamma yields diamond Delta. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $\Gamma \fCenter \Delta$ source Step 2. Depends on step 1. Rule: D rule. $\Box\Gamma \fCenter \Diamond\Delta$ source
B box-rule schema Source premise node one: Gamma comma diamond Pi yields box Delta comma Lambda comma formula A. The next inference is labeled B box rule. From node one, infer node two: box Gamma comma Pi yields Delta comma diamond Lambda comma box formula A. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Lambda, !A$ source Step 2. Depends on step 1. Rule: B box rule. $\Box$ source $\Box\Gamma, \Pi \fCenter \Delta, \Diamond\Lambda, \Box!A$ source	B diamond-rule schema Source premise node one: formula A comma diamond Gamma comma Pi yields box Lambda comma Delta. The next inference is labeled B diamond rule. From node one, infer node two: diamond formula A comma Gamma comma box Pi yields Lambda comma diamond Delta. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $!A, \Diamond\Gamma, \Pi \fCenter \Box\Lambda, \Delta$ source Step 2. Depends on step 1. Rule: B diamond rule. $\Diamond$ source $\Diamond!A, \Gamma, \Box\Pi \fCenter \Lambda, \Diamond\Delta$ source
Four box-rule schema Source premise node one: box Gamma yields diamond Delta comma formula A. The next inference is labeled four box rule. From node one, infer node two: box Gamma yields diamond Delta comma box formula A. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $\Box\Gamma \fCenter \Diamond\Delta, !A$ source Step 2. Depends on step 1. Rule: four box rule. $\Box$ source $\Box\Gamma \fCenter \Diamond\Delta, \Box!A$ source	Four diamond-rule schema Source premise node one: formula A comma box Gamma yields diamond Delta. The next inference is labeled four diamond rule. From node one, infer node two: diamond formula A comma box Gamma yields diamond Delta. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $!A, \Box\Gamma \fCenter \Diamond\Delta$ source Step 2. Depends on step 1. Rule: four diamond rule. $\Diamond$ source $\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$ source
Five box-rule schema Source premise node one: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma formula A. The next inference is labeled five box rule. From node one, infer node two: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma box formula A. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Diamond\Lambda, !A$ source Step 2. Depends on step 1. Rule: five box rule. $\Box$ source $\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Diamond\Lambda, \Box!A$ source	Five diamond-rule schema Source premise node one: formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda. The next inference is labeled five diamond rule. From node one, infer node two: diamond formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda. The root conclusion is node two. End proof tree. Step 1. No premises. Rule: source axiom or displayed premise. $!A, \Diamond\Gamma, \Box\Pi \fCenter \Diamond\Delta, \Box\Lambda$ source Step 2. Depends on step 1. Rule: five diamond rule. $\Diamond$ source $\Diamond!A,\Diamond\Gamma,\Box\Pi \fCenter \Diamond\Delta,\Box\Lambda$ source

T

source

T

source

D

source

B

source

B

source

4

source

4

source

5

source

5

source

source 20

captionMore modal rules.

Adding these rules results in systems that are sound and complete for the logics given in the table matching modal logics, accessibility conditions, and sequent rules.

Table

Inner table: sequent rules for modal logics

Modal logics, accessibility conditions, and sequent rules, inner source table. Header row. First column: Logic. Second column: accessibility relation R is followed by an ellipsis. Third column: Rules. Row T. Logic modal system T equals modal system K T. Accessibility condition: reflexive. Rules in source order: box, T box, and T diamond. Row D. Logic modal system D equals modal system K D. Accessibility condition: serial. Rules in source order: box and D. Row K four. Logic modal system K four. Accessibility condition: transitive. Rules in source order: box, four box, and four diamond. Row B. Logic modal system B equals modal system K T B. Accessibility conditions, printed on successive source lines: reflexive, then symmetric. Rules in source order: box, T box, T diamond, B box, and B diamond. Row S four. Logic modal system S four equals modal system K T four. Accessibility conditions, printed on successive source lines: reflexive, then transitive. Rules in source order: box, T box, T diamond, four box, and four diamond. Row S five. Logic modal system S five equals modal system K T five. Accessibility conditions, printed on successive source lines: reflexive, transitive, and Euclidean. Rules in source order: box, T box, T diamond, five box, and five diamond. The final Euclidean source line has no additional rule entry. End table.

Inner table: sequent rules for modal logics
Logic	$R$ source is followed by an ellipsis	Rules
$\Log{T} = \Log{KT}$ source	reflexive	$\Box$ source $\Box$ source $\Diamond$ source
$\Log{D} = \Log{KD}$ source	serial	$\Box$ source
$\Log{K4}$ source	transitive	$\Box$ source $\Box$ source $\Diamond$ source
$\Log{B} = \Log{KTB}$ source	reflexive, then symmetric	$\Box$ source $\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source
$\Log{S4} = \Log{KT4}$ source	reflexive, then transitive	$\Box$ source $\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source
$\Log{S5} = \Log{KT5}$ source	reflexive, transitive, then Euclidean	$\Box$ source $\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source

source 170

captionSequent rules for various modal logics.

Example deriving axiom four in K four

We give a sequent derivation that shows $\Log{K4} \Proves \Ax{4}$ source, i.e., $\Box!A \lif \Box\Box!A$ source.

K four proof of axiom four

Source premise node one: box formula A yields box formula A. The next inference is labeled four box rule. From node one, infer node two: box formula A yields box box formula A. The next inference is labeled conditional right rule. From node two, infer node three: yields box formula A implies box box formula A. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$\Box!A \fCenter \Box!A$ source
Step 2. Depends on step 1. Rule: four box rule.
$\Box$ source
$\Box!A \fCenter \Box\Box!A$ source
Step 3. Depends on step 2. Rule: conditional right rule.
$\fCenter \Box!A \lif \Box\Box!A$ source

4

source

\RightR{\lif}

source

source 226

Example deriving axiom five in S five

We give a sequent derivation that shows $\Log{S5} \Proves \Ax{5}$ source, i.e., $\Diamond!A \lif \Box\Diamond!A$ source.

S five proof of axiom five

Source premise node one: diamond formula A yields diamond formula A. The next inference is labeled five box rule. From node one, infer node two: diamond formula A yields box diamond formula A. The next inference is labeled conditional right rule. From node two, infer node three: yields diamond formula A implies box diamond formula A. The root conclusion is node three. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$\Diamond!A \fCenter \Diamond!A$ source
Step 2. Depends on step 1. Rule: five box rule.
$\Box$ source
$\Diamond!A \fCenter \Box\Diamond!A$ source
Step 3. Depends on step 2. Rule: conditional right rule.
$\fCenter \Diamond!A \lif \Box\Diamond!A$ source

5

source

\RightR{\lif}

source

source 252

S five example requiring cut

The sequent calculus for LogS5 is not complete without the cut rule; e.g., $\Diamond\Box !A \lif !A$ source , which is valid in $\Log{S5}$ source, has no proof without cut. Here is a derivation using cut:

S five cut derivation of the displayed implication

Source premise node one: box formula A yields box formula A. The next inference is labeled five diamond rule. From node one, infer node two: diamond box formula A yields box formula A. Source premise node three: formula A yields formula A. The next inference is labeled T box rule. From node three, infer node four: box formula A yields formula A. The next inference is labeled cut rule. From nodes two, then four, infer node five: diamond box formula A yields formula A. The next inference is labeled conditional right rule. From node five, infer node six: yields diamond box formula A implies formula A. The root conclusion is node six. End proof tree.

Step 1. No premises. Rule: source axiom or displayed premise.
$\Box !A \fCenter \Box!A$ source
Step 2. Depends on step 1. Rule: five diamond rule.
$\Diamond$ source
$\Diamond\Box!A \fCenter \Box!A$ source
Step 3. No premises. Rule: source axiom or displayed premise.
$!A \fCenter !A$ source
Step 4. Depends on step 3. Rule: T box rule.
$\Box$ source
$\Box!A \fCenter !A$ source
Step 5. Depends on step 2, step 4. Rule: cut rule.
$\Diamond\Box!A \fCenter !A$ source
Step 6. Depends on step 5. Rule: conditional right rule.
$\fCenter \Diamond\Box!A \lif !A$ source

5

source

T

source

\Cut

source

\RightR{\lif}

source

source 298

Exercises on additional modal rules

Give sequent derivations that show the following:

$\Log{KT5} \Proves \Ax{B}$ source;
$\Log{KT5} \Proves \Ax{4}$ source;
$\Log{KDB4} \Proves \Ax{T}$ source;
$\Log{KB4} \Proves \Ax{5}$ source;
$\Log{KB5} \Proves \Ax{4}$ source;
$\Log{KT} \Proves \Ax{D}$ source.

Reading preferences

Source file content/normal-modal-logic/sequent-calculus/sequent-calculus.tex

Editorial

Source file content/normal-modal-logic/sequent-calculus/introduction.tex

Introduction

K box-rule schema in the introduction

K diamond-rule schema in the introduction

Source file content/normal-modal-logic/sequent-calculus/rules-for-K.tex

Rules for LogK

K box-rule schema

K diamond-rule schema

Hypothetical invalid starred-box derivation

Hypothetical invalid starred-diamond derivation

Hypothetical invalid side-formula box derivation

Hypothetical invalid side-formula diamond derivation

Source file content/normal-modal-logic/sequent-calculus/proofs-in-K.tex

Sequent derivation for LogK

Example: box preserves conjunction

Sequent proof that box preserves conjunction

Example: diamond distributes over disjunction

Sequent proof that diamond distributes over disjunction

Sequent derivation of modal duality

Exercises in modal sequent calculus for K

Source file content/normal-modal-logic/sequent-calculus/more-rules.tex

Rules for Other Accessibility Relations

Table

Inner table: more modal rules

T box-rule schema

T diamond-rule schema

D rule schema

B box-rule schema

B diamond-rule schema

Four box-rule schema

Four diamond-rule schema

Five box-rule schema

Five diamond-rule schema

Table

Inner table: sequent rules for modal logics

Example deriving axiom four in K four

K four proof of axiom four

Example deriving axiom five in S five

S five proof of axiom five

S five example requiring cut

S five cut derivation of the displayed implication

Exercises on additional modal rules