Normal Modal Logics

Modal Sequent Calculus

Equation form expr-075b55206a955ee4

□A∧□B⇒□(A∧B)\Box!A \land \Box!B \fCenter \Box (!A \land !B)

Read as: box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis

Means: box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-07ea89381935676e

S4=KT4\Log{S4} = \Log{KT4}

Read as: modal system S four equals modal system K T four

Means: modal system S four equals modal system K T four

1 occurrence in this chapter

Equation form expr-092317f4ffe738ba

KT5⊢B\Log{KT5} \Proves \Ax{B}

Read as: modal system K T five derives axiom B

Means: modal system K T five derives axiom B

1 occurrence in this chapter

Equation form expr-0965332ddfce1eba

A⇒A⇒A,¬A negation right rule⇒¬A,A exchange right rule⇒¬A,□A invalid starred box rule⇒¬A∨□A disjunction right ruleA⇒A¬A,A⇒ negation left rule◇¬A,A⇒ invalid starred diamond ruleA⇒¬◇¬A negation right rule⇒A→¬◇¬A conditional right rule\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

Read as: Two hypothetical side-formula derivations, in source order. First, formula A yields formula A. Negation-right gives the empty antecedent yields formula A, not formula A; exchange gives the empty antecedent yields not formula A, formula A. The invalid starred box rule changes only formula A and gives the empty antecedent yields not formula A, box formula A. A double inference line and disjunction-right give the empty antecedent yields not formula A or box formula A. Second, formula A yields formula A. Negation-left gives not formula A, formula A yields the empty succedent. The invalid starred diamond rule changes only the first formula and gives diamond not formula A, formula A yields the empty succedent. Negation-right gives formula A yields not diamond not formula A. Conditional-right gives the empty antecedent yields formula A implies not diamond not formula A.

Means: Two hypothetical side-formula derivations, in source order. First, formula A yields formula A. Negation-right gives the empty antecedent yields formula A, not formula A; exchange gives the empty antecedent yields not formula A, formula A. The invalid starred box rule changes only formula A and gives the empty antecedent yields not formula A, box formula A. A double inference line and disjunction-right give the empty antecedent yields not formula A or box formula A. Second, formula A yields formula A. Negation-left gives not formula A, formula A yields the empty succedent. The invalid starred diamond rule changes only the first formula and gives diamond not formula A, formula A yields the empty succedent. Negation-right gives formula A yields not diamond not formula A. Conditional-right gives the empty antecedent yields formula A implies not diamond not formula A.

1 occurrence in this chapter

Equation form expr-0adcf3b28e16c022

D=KD\Log{D} = \Log{KD}

Read as: modal system D equals modal system K D

Means: modal system D equals modal system K D

1 occurrence in this chapter

Equation form expr-0c7a2a029e48e48a

□A⇒□□A\Box!A \fCenter \Box\Box!A

Read as: box formula A yields box box formula A

Means: box formula A yields box box formula A

1 occurrence in this chapter

Equation form expr-0d310cfebabfbeed

⇒□A↔¬◇¬A\fCenter \Box !A \liff \lnot\Diamond\lnot !A

Read as: yields box formula A if and only if not diamond not formula A

Means: yields box formula A if and only if not diamond not formula A

1 occurrence in this chapter

Equation form expr-104c163fc9acba6d

B,A⇒A∧B!B, !A \fCenter !A \land !B

Read as: formula B comma formula A yields formula A and formula B

Means: formula B comma formula A yields formula A and formula B

1 occurrence in this chapter

Equation form expr-10ae08ffb985e2e2

Γ,◇Π⇒□Δ,Λ,A\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Lambda, !A

Read as: Gamma comma diamond Pi yields box Delta comma Lambda comma formula A

Means: Gamma comma diamond Pi yields box Delta comma Lambda comma formula A

1 occurrence in this chapter

Equation form expr-13281e8b77b52b71

⇒□A,◇¬A\fCenter \Box !A, \Diamond\lnot !A

Read as: yields box formula A comma diamond not formula A

Means: yields box formula A comma diamond not formula A

1 occurrence in this chapter

Equation form expr-165a2676a255cdfb

KT⊢D\Log{KT} \Proves \Ax{D}

Read as: modal system K T derives axiom D

Means: modal system K T derives axiom D

1 occurrence in this chapter

Equation form expr-166d4ccd027fe77d

□Γ⇒◇Δ,□A\Box\Gamma \fCenter \Diamond\Delta, \Box!A

Read as: box Gamma yields diamond Delta comma box formula A

Means: box Gamma yields diamond Delta comma box formula A

1 occurrence in this chapter

Equation form expr-17e09680d193f473

¬◇¬A⇒□A\lnot\Diamond\lnot !A \fCenter \Box !A

Read as: not diamond not formula A yields box formula A

Means: not diamond not formula A yields box formula A

1 occurrence in this chapter

Equation form expr-18ec1b377df01eca

⇒◇□A→A\fCenter \Diamond\Box!A \lif !A

Read as: yields diamond box formula A implies formula A

Means: yields diamond box formula A implies formula A

1 occurrence in this chapter

Equation form expr-1b358765e557e1af

□A∧□B,□A∧□B⇒□(A∧B)\Box!A \land \Box!B, \Box!A \land \Box!B \fCenter \Box (!A \land !B)

Read as: 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

Means: 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

1 occurrence in this chapter

Equation form expr-1d53a3d55dc2a808

◇A,□Γ⇒◇Δ\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta

Read as: diamond formula A comma box Gamma yields diamond Delta

Means: diamond formula A comma box Gamma yields diamond Delta

1 occurrence in this chapter

Equation form expr-1e095d3ffc5363ea

KB5⊢4\Log{KB5} \Proves \Ax{4}

Read as: modal system K B five derives axiom four

Means: modal system K B five derives axiom four

1 occurrence in this chapter

Equation form expr-1e1eed9c7b8f0d1c

□A→□□A\Box!A \lif \Box\Box!A

Read as: box formula A implies box box formula A

Means: box formula A implies box box formula A

1 occurrence in this chapter

Equation form expr-21d031b0dacd8cc7

K\Log{K}

Read as: modal system K

Means: modal system K

5 occurrences in this chapter

Equation form expr-258241999db8397a

A,□Γ⇒◇Δ!A, \Box\Gamma \fCenter \Diamond\Delta

Read as: formula A comma box Gamma yields diamond Delta

Means: formula A comma box Gamma yields diamond Delta

1 occurrence in this chapter

Equation form expr-274b575a29c806cf

B⇒A,B!B \fCenter !A, !B

Read as: formula B yields formula A comma formula B

Means: formula B yields formula A comma formula B

1 occurrence in this chapter

Equation form expr-28fc3f45e792a3a4

A⇒A,B!A \fCenter !A, !B

Read as: formula A yields formula A comma formula B

Means: formula A yields formula A comma formula B

1 occurrence in this chapter

Equation form expr-308e7581edc27c37

⊢(□A∧□B)→□(A∧B)\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)

Read as: derives open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis

Means: derives open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-36857028496beb66

◇□A⇒A\Diamond\Box!A \fCenter !A

Read as: diamond box formula A yields formula A

Means: diamond box formula A yields formula A

1 occurrence in this chapter

Equation form expr-3b9b79000d3b0004

S5⊢5\Log{S5} \Proves \Ax{5}

Read as: modal system S five derives axiom five

Means: modal system S five derives axiom five

1 occurrence in this chapter

Equation form expr-3dd2842e80d11f12

□A,□A∧□B⇒□(A∧B)\Box!A, \Box!A \land \Box!B \fCenter \Box (!A \land !B)

Read as: box formula A comma box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis

Means: box formula A comma box formula A and box formula B yields box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-48b7b8587503e897

B=KTB\Log{B} = \Log{KTB}

Read as: modal system B equals modal system K T B

Means: modal system B equals modal system K T B

1 occurrence in this chapter

Equation form expr-4b3f8c5b9e20c0c3

□Γ⇒◇Δ,A\Box\Gamma \fCenter \Diamond\Delta, !A

Read as: box Gamma yields diamond Delta comma formula A

Means: box Gamma yields diamond Delta comma formula A

1 occurrence in this chapter

Equation form expr-4b5d6fb787124374

◇A,Γ,□Π⇒Λ,◇Δ\Diamond!A, \Gamma, \Box\Pi \fCenter \Lambda, \Diamond\Delta

Read as: diamond formula A comma Gamma comma box Pi yields Lambda comma diamond Delta

Means: diamond formula A comma Gamma comma box Pi yields Lambda comma diamond Delta

1 occurrence in this chapter

Equation form expr-4ee59b68125f5f6c

(□p∨□q)→□(p∨q)(\Box p \lor \Box q) \lif \Box(p \lor q)

Read as: open parenthesis box propositional variable p or box propositional variable q close parenthesis implies box open parenthesis propositional variable p or propositional variable q close parenthesis

Means: open parenthesis box propositional variable p or box propositional variable q close parenthesis implies box open parenthesis propositional variable p or propositional variable q close parenthesis

1 occurrence in this chapter

Equation form expr-4efb245d5d027e51

□A⇒□A\Box!A \fCenter \Box!A

Read as: box formula A yields box formula A

Means: box formula A yields box formula A

1 occurrence in this chapter

Equation form expr-5136fc4246e7d497

◇\Diamond

Read as: diamond

Means: diamond

22 occurrences in this chapter

Equation form expr-52baf5b113b97063

KDB4⊢T\Log{KDB4} \Proves \Ax{T}

Read as: modal system K D B four derives axiom T

Means: modal system K D B four derives axiom T

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

3 occurrences in this chapter

Equation form expr-57ba3e400544d418

A,Γ⇒Δ!A, \Gamma \fCenter \Delta

Read as: formula A comma Gamma yields Delta

Means: formula A comma Gamma yields Delta

1 occurrence in this chapter

Equation form expr-62a7581d7620bb78

K4\Log{K4}

Read as: modal system K four

Means: modal system K four

1 occurrence in this chapter

Equation form expr-64d0f2c008a7c881

LK\Log{LK}

Read as: modal system L K

Means: modal system L K

2 occurrences in this chapter

Equation form expr-7120f8695fd9aa83

KB4⊢5\Log{KB4} \Proves \Ax{5}

Read as: modal system K B four derives axiom five

Means: modal system K B four derives axiom five

1 occurrence in this chapter

Equation form expr-751379acac529582

◇p→◇(p∨q)\Diamond p \lif \Diamond(p \lor q)

Read as: diamond propositional variable p implies diamond open parenthesis propositional variable p or propositional variable q close parenthesis

Means: diamond propositional variable p implies diamond open parenthesis propositional variable p or propositional variable q close parenthesis

1 occurrence in this chapter

Equation form expr-76de36a7895b26b9

◇□A→A\Diamond\Box !A \lif !A

Read as: diamond box formula A implies formula A

Means: diamond box formula A implies formula A

1 occurrence in this chapter

Equation form expr-78891f179acaabfa

□Γ⇒◇Δ\Box\Gamma \fCenter \Diamond\Delta

Read as: box Gamma yields diamond Delta

Means: box Gamma yields diamond Delta

1 occurrence in this chapter

Equation form expr-790096d98bef3ec8

◇Δ\Diamond\Delta

Read as: diamond Delta

Means: diamond Delta

2 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

4 occurrences in this chapter

Equation form expr-85882d911ac7a0f4

□A∨□¬A\Box!A \lor \Box \lnot !A

Read as: box formula A or box not formula A

Means: box formula A or box not formula A

1 occurrence in this chapter

Equation form expr-88855060a722f93c

◇A→□◇A\Diamond!A \lif \Box\Diamond!A

Read as: diamond formula A implies box diamond formula A

Means: diamond formula A implies box diamond formula A

1 occurrence in this chapter

Equation form expr-8a026e0b5e09d4fc

⇒A,¬A\fCenter !A, \lnot !A

Read as: yields formula A comma not formula A

Means: yields formula A comma not formula A

1 occurrence in this chapter

Equation form expr-8c2574892063f995

RR

Read as: accessibility relation R

Means: accessibility relation R

1 occurrence in this chapter

Equation form expr-8c2ec4ac07ee1593

T=KT\Log{T} = \Log{KT}

Read as: modal system T equals modal system K T

Means: modal system T equals modal system K T

1 occurrence in this chapter

Equation form expr-8d9103e703ca6968

◇(A∨B)⇒◇A∨◇B\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B

Read as: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B

Means: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B

1 occurrence in this chapter

Equation form expr-8dffb88f67702d91

□Γ\Box\Gamma

Read as: box Gamma

Means: box Gamma

2 occurrences in this chapter

Equation form expr-9b3b8b99cfdf919b

Γ⇒Δ,A\Gamma \fCenter \Delta, !A

Read as: Gamma yields Delta comma formula A

Means: Gamma yields Delta comma formula A

1 occurrence in this chapter

Equation form expr-9dcb8f45640c5664

⇒¬A,A\fCenter \lnot !A, !A

Read as: yields not formula A comma formula A

Means: yields not formula A comma formula A

1 occurrence in this chapter

Equation form expr-a0e459db53c4dc1c

□B,□A⇒□(A∧B)\Box!B, \Box!A \fCenter \Box (!A \land !B)

Read as: box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis

Means: box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-a1cb4ecf789c089a

◇(A∨B)⇒◇A∨◇B,◇A∨◇B\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B, \Diamond !A \lor \Diamond!B

Read as: 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

Means: 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

1 occurrence in this chapter

Equation form expr-a587abe07128427f

⇒◇A→□◇A\fCenter \Diamond!A \lif \Box\Diamond!A

Read as: yields diamond formula A implies box diamond formula A

Means: yields diamond formula A implies box diamond formula A

1 occurrence in this chapter

Equation form expr-a8642ea1a9070277

K4⊢4\Log{K4} \Proves \Ax{4}

Read as: modal system K four derives axiom four

Means: modal system K four derives axiom four

1 occurrence in this chapter

Equation form expr-a926ddda992bd43f

A→¬◇¬A!A \lif \lnot\Diamond\lnot !A

Read as: formula A implies not diamond not formula A

Means: formula A implies not diamond not formula A

1 occurrence in this chapter

Equation form expr-ac586b3f2db5fbe8

¬A,A⇒\lnot !A, !A \fCenter

Read as: not formula A comma formula A yields

Means: not formula A comma formula A yields

1 occurrence in this chapter

Equation form expr-ad49c2706988b429

⇒◇¬A,□A\fCenter \Diamond\lnot !A, \Box !A

Read as: yields diamond not formula A comma box formula A

Means: yields diamond not formula A comma box formula A

1 occurrence in this chapter

Equation form expr-ae25c47fcfd76df7

◇A⇒◇A\Diamond!A \fCenter \Diamond!A

Read as: diamond formula A yields diamond formula A

Means: diamond formula A yields diamond formula A

1 occurrence in this chapter

Equation form expr-b83a85c2f64acf16

◇□A⇒□A\Diamond\Box!A \fCenter \Box!A

Read as: diamond box formula A yields box formula A

Means: diamond box formula A yields box formula A

1 occurrence in this chapter

Equation form expr-bb8224d2fb111ef9

A⇒A!A \Sequent !A

Read as: formula A yields formula A

Means: formula A yields formula A

1 occurrence in this chapter

Equation form expr-bbceea92a83f4c4b

⇒□A→□□A\fCenter \Box!A \lif \Box\Box!A

Read as: yields box formula A implies box box formula A

Means: yields box formula A implies box box formula A

1 occurrence in this chapter

Equation form expr-bc73824f74696388

S5=KT5\Log{S5} = \Log{KT5}

Read as: modal system S five equals modal system K T five

Means: modal system S five equals modal system K T five

1 occurrence in this chapter

Equation form expr-c0b0ea5e36511e7f

◇A⇒□◇A\Diamond!A \fCenter \Box\Diamond!A

Read as: diamond formula A yields box diamond formula A

Means: diamond formula A yields box diamond formula A

1 occurrence in this chapter

Equation form expr-c2120eed3877fffd

A∨B⇒A,B!A \lor !B \fCenter !A, !B

Read as: formula A or formula B yields formula A comma formula B

Means: formula A or formula B yields formula A comma formula B

1 occurrence in this chapter

Equation form expr-c2d25e2bee0f401d

□A,Γ⇒Δ\Box!A, \Gamma \fCenter \Delta

Read as: box formula A comma Gamma yields Delta

Means: box formula A comma Gamma yields Delta

1 occurrence in this chapter

Equation form expr-c4c635cbade0b8c8

□A∧□B,□A⇒□(A∧B)\Box!A \land \Box!B, \Box!A \fCenter \Box (!A \land !B)

Read as: box formula A and box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis

Means: box formula A and box formula B comma box formula A yields box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-c5540bde7aef416e

□A⇒□A\Box !A \fCenter \Box!A

Read as: box formula A yields box formula A

Means: box formula A yields box formula A

1 occurrence in this chapter

Equation form expr-c5a686aa60341113

Γ⇒Δ,A□Γ⇒◇Δ,□A box ruleA,Γ⇒Δ◇A,□Γ⇒◇Δ diamond rule\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

Read as: Two modal sequent-rule diagrams, in source order. Box rule: from Gamma yields Delta, formula A, infer box Gamma yields diamond Delta, box formula A. Diamond rule: from formula A, Gamma yields Delta, infer diamond formula A, box Gamma yields diamond Delta.

Means: Two modal sequent-rule diagrams, in source order. Box rule: from Gamma yields Delta, formula A, infer box Gamma yields diamond Delta, box formula A. Diamond rule: from formula A, Gamma yields Delta, infer diamond formula A, box Gamma yields diamond Delta.

2 occurrences in this chapter

Equation form expr-c7647f91a27ddadf

⇒□A→¬◇¬A\fCenter \Box !A \lif \lnot\Diamond\lnot !A

Read as: yields box formula A implies not diamond not formula A

Means: yields box formula A implies not diamond not formula A

1 occurrence in this chapter

Equation form expr-c7ffa9f5ef523fc4

□Γ,◇Π⇒□Δ,◇Λ,A\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Diamond\Lambda, !A

Read as: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma formula A

Means: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma formula A

1 occurrence in this chapter

Equation form expr-c800acc391f730d7

B,A⇒B!B, !A \fCenter !B

Read as: formula B comma formula A yields formula B

Means: formula B comma formula A yields formula B

1 occurrence in this chapter

Equation form expr-caab90411625abb6

B,A⇒A!B, !A \fCenter !A

Read as: formula B comma formula A yields formula A

Means: formula B comma formula A yields formula A

1 occurrence in this chapter

Equation form expr-cbede77419bcc57e

S5\Log{S5}

Read as: modal system S five

Means: modal system S five

2 occurrences in this chapter

Equation form expr-cd01c07a83684207

◇(A∨B)⇒◇A,◇A∨◇B\Diamond(!A \lor !B) \fCenter \Diamond !A, \Diamond !A \lor \Diamond!B

Read as: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula A or diamond formula B

Means: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula A or diamond formula B

1 occurrence in this chapter

Equation form expr-cf692f2a25666b75

□A⇒A\Box!A \fCenter !A

Read as: box formula A yields formula A

Means: box formula A yields formula A

1 occurrence in this chapter

Equation form expr-d2b079bbc75c2bbb

A⇒A⇒A,¬A negation right rule⇒□A,□¬A invalid starred box rule⇒□A∨□¬A disjunction right ruleA⇒A¬A,A⇒ negation left rule◇¬A,◇A⇒ invalid starred diamond rule◇A⇒¬◇¬A negation right rule⇒◇A→¬◇¬A conditional right rule\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

Read as: Two hypothetical invalid derivations, in source order. First, formula A yields formula A. Negation-right gives the empty antecedent yields formula A, not formula A. The invalid starred box rule gives the empty antecedent yields box formula A, box not formula A. A double inference line and disjunction-right give the empty antecedent yields box formula A or box not formula A. Second, formula A yields formula A. Negation-left gives not formula A, formula A yields the empty succedent. The invalid starred diamond rule gives diamond not formula A, diamond formula A yields the empty succedent. Negation-right gives diamond formula A yields not diamond not formula A. Conditional-right gives the empty antecedent yields diamond formula A implies not diamond not formula A.

Means: Two hypothetical invalid derivations, in source order. First, formula A yields formula A. Negation-right gives the empty antecedent yields formula A, not formula A. The invalid starred box rule gives the empty antecedent yields box formula A, box not formula A. A double inference line and disjunction-right give the empty antecedent yields box formula A or box not formula A. Second, formula A yields formula A. Negation-left gives not formula A, formula A yields the empty succedent. The invalid starred diamond rule gives diamond not formula A, diamond formula A yields the empty succedent. Negation-right gives diamond formula A yields not diamond not formula A. Conditional-right gives the empty antecedent yields diamond formula A implies not diamond not formula A.

1 occurrence in this chapter

Equation form expr-db9f3812dd3b2732

◇(A∨B)⇒◇A,◇B\Diamond(!A \lor !B) \fCenter \Diamond !A, \Diamond!B

Read as: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula B

Means: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A comma diamond formula B

1 occurrence in this chapter

Equation form expr-dc9457931fa18d83

A,◇Γ,Π⇒□Λ,Δ!A, \Diamond\Gamma, \Pi \fCenter \Box\Lambda, \Delta

Read as: formula A comma diamond Gamma comma Pi yields box Lambda comma Delta

Means: formula A comma diamond Gamma comma Pi yields box Lambda comma Delta

1 occurrence in this chapter

Equation form expr-de201ef5aca9865d

◇A→¬◇¬A\Diamond!A \lif \lnot\Diamond\lnot !A

Read as: diamond formula A implies not diamond not formula A

Means: diamond formula A implies not diamond not formula A

1 occurrence in this chapter

Equation form expr-de7a66d1e66f4bcd

A,◇Γ,□Π⇒◇Δ,□Λ!A, \Diamond\Gamma, \Box\Pi \fCenter \Diamond\Delta, \Box\Lambda

Read as: formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda

Means: formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda

1 occurrence in this chapter

Equation form expr-df1c6f7455cf6ff3

A→□A!A \lif \Box!A

Read as: formula A implies box formula A

Means: formula A implies box formula A

1 occurrence in this chapter

Equation form expr-df65b6be664a5081

B⇒B!B \fCenter !B

Read as: formula B yields formula B

Means: formula B yields formula B

2 occurrences in this chapter

Equation form expr-e145371f277ec07b

⊢◇(A∨B)→(◇A∨◇B)\Proves \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond!B)

Read as: derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or diamond formula B close parenthesis

Means: derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or diamond formula B close parenthesis

1 occurrence in this chapter

Equation form expr-e464429e46848268

A⇒A!A \fCenter !A

Read as: formula A yields formula A

Means: formula A yields formula A

5 occurrences in this chapter

Equation form expr-e55a08dcd21497e0

¬A∨□A\lnot!A \lor \Box !A

Read as: not formula A or box formula A

Means: not formula A or box formula A

1 occurrence in this chapter

Equation form expr-e7dfe81e9b84263f

Γ⇒Δ,◇A\Gamma \fCenter \Delta, \Diamond!A

Read as: Gamma yields Delta comma diamond formula A

Means: Gamma yields Delta comma diamond formula A

1 occurrence in this chapter

Equation form expr-e9332adcb25f62e9

◇¬A,□A⇒\Diamond\lnot !A, \Box !A \fCenter

Read as: diamond not formula A comma box formula A yields

Means: diamond not formula A comma box formula A yields

1 occurrence in this chapter

Equation form expr-e9a84bd55b08c88a

◇A,◇Γ,□Π⇒◇Δ,□Λ\Diamond!A,\Diamond\Gamma,\Box\Pi \fCenter \Diamond\Delta,\Box\Lambda

Read as: diamond formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda

Means: diamond formula A comma diamond Gamma comma box Pi yields diamond Delta comma box Lambda

1 occurrence in this chapter

Equation form expr-ea4c905f0e2eb74d

□A⇒¬◇¬A\Box !A \fCenter \lnot\Diamond\lnot !A

Read as: box formula A yields not diamond not formula A

Means: box formula A yields not diamond not formula A

1 occurrence in this chapter

Equation form expr-ead9284052b7ddcb

⇒¬◇¬A→□A\fCenter \lnot \Diamond \lnot !A \lif \Box !A

Read as: yields not diamond not formula A implies box formula A

Means: yields not diamond not formula A implies box formula A

1 occurrence in this chapter

Equation form expr-ebeda29fc3e4df8f

⇒(□A∧□B)→□(A∧B)\fCenter (\Box!A \land \Box!B) \lif \Box (!A \land !B)

Read as: yields open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis

Means: yields open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis

1 occurrence in this chapter

Equation form expr-ed1e21e1d5a1f4e6

□Γ,◇Π⇒□Δ,◇Λ,□A\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Diamond\Lambda, \Box!A

Read as: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma box formula A

Means: box Gamma comma diamond Pi yields box Delta comma diamond Lambda comma box formula A

1 occurrence in this chapter

Equation form expr-f157f71e0163a897

□\Box

Read as: box

Means: box

30 occurrences in this chapter

Equation form expr-f192680bfea27cb4

□(p∧q)→□p\Box(p \land q) \lif \Box p

Read as: box open parenthesis propositional variable p and propositional variable q close parenthesis implies box propositional variable p

Means: box open parenthesis propositional variable p and propositional variable q close parenthesis implies box propositional variable p

1 occurrence in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: Delta

3 occurrences in this chapter

Equation form expr-f427cdcccd62d1ab

□¬p→□(p→q)\Box \lnot p \lif \Box(p \lif q)

Read as: box not propositional variable p implies box open parenthesis propositional variable p implies propositional variable q close parenthesis

Means: box not propositional variable p implies box open parenthesis propositional variable p implies propositional variable q close parenthesis

1 occurrence in this chapter

Equation form expr-f6e49c596decc774

KT5⊢4\Log{KT5} \Proves \Ax{4}

Read as: modal system K T five derives axiom four

Means: modal system K T five derives axiom four

1 occurrence in this chapter

Equation form expr-f714b776f8553482

⇒◇(A∨B)→(◇A∨◇B)\fCenter \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond!B)

Read as: yields diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or diamond formula B close parenthesis

Means: yields diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or diamond formula B close parenthesis

1 occurrence in this chapter

Equation form expr-fcd07b9d1b699f6d

Γ⇒Δ\Gamma \fCenter \Delta

Read as: Gamma yields Delta

Means: Gamma yields Delta

1 occurrence in this chapter

Equation form expr-ff8bf8cabb9f2f0f

◇(A∨B)⇒◇A∨◇B,◇A\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B, \Diamond !A

Read as: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B comma diamond formula A

Means: diamond open parenthesis formula A or formula B close parenthesis yields diamond formula A or diamond formula B comma diamond formula A

1 occurrence in this chapter

Equation form expr-ffa8978a4cab6759

□Γ,Π⇒Δ,◇Λ,□A\Box\Gamma, \Pi \fCenter \Delta, \Diamond\Lambda, \Box!A

Read as: box Gamma comma Pi yields Delta comma diamond Lambda comma box formula A

Means: box Gamma comma Pi yields Delta comma diamond Lambda comma box formula A

1 occurrence in this chapter

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.

Source

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.

Source

K box-rule schema

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.

Source

K diamond-rule schema

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.

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.

Source

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.

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.

Source

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.

Source

Example: box preserves conjunction

A complete source sequent proof derives that if box A and box B, then box of A and B. Its nested proof structure preserves both premises, all structural steps, the modal rule, and the final conditional-right inference.

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.

Source

Example: diamond distributes over disjunction

A complete source sequent proof derives that diamond of A or B implies diamond A or diamond B. Its nested proof structure preserves both axiom branches, the disjunction steps, exchange, contraction, and the final conditional-right inference.

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.

Source

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.

Source

Exercises in modal sequent calculus for K

Find K sequent proofs of four listed formulas concerning boxed negation, boxed disjunction, diamond monotonicity over disjunction, and projection from a boxed conjunction. The source supplies no solutions.

Source

Outer table: more modal rules

Outer table with caption More modal rules. 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. The source caption follows the inner table and reads More modal rules.

Source

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.

Source

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.

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.

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.

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.

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.

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.

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.

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.

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.

Source

Outer table: sequent rules for modal logics

Outer table with caption Sequent rules for various modal logics. 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. The source caption follows the inner table and reads Sequent rules for various modal logics.

Source

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.

Source

Example deriving axiom four in K four

The source derives axiom four from an identity sequent by the four box rule and conditional-right. The complete three-node proof is retained in the nested proof structure.

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.

Source

Example deriving axiom five in S five

The source derives that diamond A implies box diamond A from an identity sequent by the five box rule and conditional-right. The complete three-node proof is retained in the nested proof structure.

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.

Source

S five example requiring cut

The source states that the displayed valid implication has no cut-free proof in this sequent calculus, then gives a six-node derivation using the five diamond rule, the T box rule, cut, and conditional-right. Only the active both-operators tag branch is represented.

Source

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.

Source

Exercises on additional modal rules

Give sequent derivations for six listed modal-system claims: B and four from K T five, T from K D B four, five from K B four, four from K B five, and D from K T. The source supplies no derivations.

Source

Cross-reference reference-001124

the table of additional modal sequent rules

Source occurrence

Cross-reference reference-001125

the table matching modal logics, accessibility conditions, and sequent rules

Source occurrence

Source-generated case expression tr056-source-macro-0001

∧R\RightR{\land}

Read as: conjunction right rule

Read in context source

Source-generated case expression tr056-source-macro-0002

∧L\LeftR{\land}

Read as: conjunction left rule

Read in context source

Source-generated case expression tr056-source-macro-0003

XL\LeftR{\Exchange}

Read as: exchange left rule

Read in context source

Source-generated case expression tr056-source-macro-0004

∧L\LeftR{\land}

Read as: conjunction left rule

Read in context source

Source-generated case expression tr056-source-macro-0005

CL\LeftR{\Contraction}

Read as: contraction left rule

Read in context source

Source-generated case expression tr056-source-macro-0006

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0007

∨L\LeftR{\lor}

Read as: disjunction left rule

Read in context source

Source-generated case expression tr056-source-macro-0008

∨R\RightR{\lor}

Read as: disjunction right rule

Read in context source

Source-generated case expression tr056-source-macro-0009

XR\RightR{\Exchange}

Read as: exchange right rule

Read in context source

Source-generated case expression tr056-source-macro-0010

∨R\RightR{\lor}

Read as: disjunction right rule

Read in context source

Source-generated case expression tr056-source-macro-0011

CR\RightR{\Contraction}

Read as: contraction right rule

Read in context source

Source-generated case expression tr056-source-macro-0012

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0013

¬R\RightR{\lnot}

Read as: negation right rule

Read in context source

Source-generated case expression tr056-source-macro-0014

¬R\RightR{\lnot}

Read as: negation right rule

Read in context source

Source-generated case expression tr056-source-macro-0015

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0016

¬R\RightR{\lnot}

Read as: negation right rule

Read in context source

Source-generated case expression tr056-source-macro-0017

XR\RightR{\Exchange}

Read as: exchange right rule

Read in context source

Source-generated case expression tr056-source-macro-0018

XR\RightR{\Exchange}

Read as: exchange right rule

Read in context source

Source-generated case expression tr056-source-macro-0019

¬R\RightR{\lnot}

Read as: negation right rule

Read in context source

Source-generated case expression tr056-source-macro-0020

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0021

∧R\RightR{\land}

Read as: conjunction right rule

Read in context source

Source-generated case expression tr056-source-macro-0022

TT

Read as: T

Read in context source

Source-generated case expression tr056-source-macro-0023

TT

Read as: T

Read in context source

Source-generated case expression tr056-source-macro-0024

DD

Read as: D rule

Read in context source

Source-generated case expression tr056-source-macro-0025

BB

Read as: B

Read in context source

Source-generated case expression tr056-source-macro-0026

BB

Read as: B

Read in context source

Source-generated case expression tr056-source-macro-0027

44

Read as: four

Read in context source

Source-generated case expression tr056-source-macro-0028

44

Read as: four

Read in context source

Source-generated case expression tr056-source-macro-0029

55

Read as: five

Read in context source

Source-generated case expression tr056-source-macro-0030

55

Read as: five

Read in context source

Source-generated case expression tr056-source-macro-0031

44

Read as: four

Read in context source

Source-generated case expression tr056-source-macro-0032

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0033

55

Read as: five

Read in context source

Source-generated case expression tr056-source-macro-0034

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Source-generated case expression tr056-source-macro-0035

55

Read as: five

Read in context source

Source-generated case expression tr056-source-macro-0036

TT

Read as: T

Read in context source

Source-generated case expression tr056-source-macro-0037

Cut\Cut

Read as: cut rule

Read in context source

Source-generated case expression tr056-source-macro-0038

→R\RightR{\lif}

Read as: conditional right rule

Read in context source

Ordered structures

K box-rule schema in the introduction

Structure: proof tree.

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.

Read the source-bound structure in context

K diamond-rule schema in the introduction

Structure: proof tree.

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.

Read the source-bound structure in context

K box-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

K diamond-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Hypothetical invalid starred-box derivation

Structure: proof tree.

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.

Read the source-bound structure in context

Hypothetical invalid starred-diamond derivation

Structure: proof tree.

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.

Read the source-bound structure in context

Hypothetical invalid side-formula box derivation

Structure: proof tree.

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.

Read the source-bound structure in context

Hypothetical invalid side-formula diamond derivation

Structure: proof tree.

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.

Read the source-bound structure in context

Sequent proof that box preserves conjunction

Structure: proof tree.

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.

Read the source-bound structure in context

Sequent proof that diamond distributes over disjunction

Structure: proof tree.

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.

Read the source-bound structure in context

Sequent derivation of modal duality

Structure: proof tree.

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.

Read the source-bound structure in context

Inner table: more modal rules

Structure: table.

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.

Read the source-bound structure in context

T box-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

T diamond-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

D rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

B box-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

B diamond-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Four box-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Four diamond-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Five box-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Five diamond-rule schema

Structure: proof tree.

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.

Read the source-bound structure in context

Inner table: sequent rules for modal logics

Structure: table.

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.

Read the source-bound structure in context

K four proof of axiom four

Structure: proof tree.

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.

Read the source-bound structure in context

S five proof of axiom five

Structure: proof tree.

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.

Read the source-bound structure in context

S five cut derivation of the displayed implication

Structure: proof tree.

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.

Read the source-bound structure in context