Equation form expr-00f18ba81ffa3b28

$\Log{K} \Proves \Box(!A \lif !B) \lif (\Diamond!A \lif \Diamond!B)$

Read as: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis

Means: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025806

Equation form expr-00fcf6f067f4a5be

$\Log{K}!A_1\dots!A_n \Proves \Dual$

Read as: modal system K formula A subscript one and so on formula A subscript n derives the duality axiom

Means: modal system K formula A subscript one and so on formula A subscript n derives the duality axiom

1 occurrence in this chapter

• Occurrence projected-formula-0025657

Equation form expr-023b85f6fb6dccc1

$\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$

Read as: modal system K T five derives box diamond box formula A implies box box formula A

Means: modal system K T five derives box diamond box formula A implies box box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025870

Equation form expr-03985b3ffef33a06

$\Gamma \Proves[\Sigma] \lnot!A \lif \lfalse$

Read as: Gamma derives in system Sigma not formula A implies falsity

Means: Gamma derives in system Sigma not formula A implies falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026057

Equation form expr-04ccf2258fa7fd73

$\lnot\Box\lnot !A$

Read as: not box not formula A

Means: not box not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025732

Equation form expr-053c54186942dd46

$\Ax{Dual}$

Read as: axiom dual

Means: axiom dual

1 occurrence in this chapter

• Occurrence projected-formula-0025528

Equation form expr-061949694fc5a2d0

$!B_n \ident !A$

Read as: formula B subscript n is syntactically identical to formula A

Means: formula B subscript n is syntactically identical to formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025554

Equation form expr-07291b17720eb742

$\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \in \Sigma,$

Read as: the result of simultaneously substituting formula D subscript one for propositional variable p subscript one comma and so on comma formula D subscript n for propositional variable p subscript n in formula A belongs to Sigma comma

Means: the result of simultaneously substituting formula D subscript one for propositional variable p subscript one comma and so on comma formula D subscript n for propositional variable p subscript n in formula A belongs to Sigma comma

1 occurrence in this chapter

• Occurrence projected-formula-0025564

Equation form expr-07f71904c4a486bd

$\Log{KTB} \Proves/ \Log{5}$

Read as: modal system K T B does not derive modal system five

Means: modal system K T B does not derive modal system five

1 occurrence in this chapter

• Occurrence projected-formula-0025970

Equation form expr-08488b55c227bb59

$<k$

Read as: is less than k

Means: is less than k

1 occurrence in this chapter

• Occurrence projected-formula-0025937

Equation form expr-092317f4ffe738ba

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

Read as: modal system K T five derives axiom B

Means: modal system K T five derives axiom B

2 occurrences in this chapter

• Occurrence projected-formula-0025848
• Occurrence projected-formula-0025854

Equation form expr-09af01ee56582782

$\Box!A \lif \Box(!B \lif (!A \land !B))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025689

Equation form expr-0a5f32fe2818b758

$\Log{KD} \Proves !B$

Read as: modal system K D derives formula B

Means: modal system K D derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025954

Equation form expr-0b5da97f1d4da2bf

$\mClass{C} \subseteq \mClass{C}_i$

Read as: class C of models is a subset of class C of models subscript i

Means: class C of models is a subset of class C of models subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0025924

Equation form expr-0bde4816bf6d76c3

$\Log K$

Read as: modal system K

Means: modal system K

1 occurrence in this chapter

• Occurrence projected-formula-0025529

Equation form expr-0c19163583ee4bfc

$\Box((!A \land !B) \lif !A) \lif (\Box(!A \land !B) \lif \Box!A)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025671

Equation form expr-0c4ca6278f066c60

$\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$

Read as: modal system K T five derives box formula A implies box diamond box formula A

Means: modal system K T five derives box formula A implies box diamond box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025867

Equation form expr-0e6552391680df3d

$(\lnot \Box \lnot\lnot p \lif \Diamond \lnot p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025706

Equation form expr-102884d364453489

$\Log{K} \Proves \Subst{!C}{!A}{q} \liff \Subst{!C}{!B}{q}$

Read as: modal system K derives the result of substituting formula A for propositional variable q in formula C if and only if the result of substituting formula B for propositional variable q in formula C

Means: modal system K derives the result of substituting formula A for propositional variable q in formula C if and only if the result of substituting formula B for propositional variable q in formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025759

Equation form expr-103542f371fe8edd

$\Gamma \cup \{ !A\} \Proves[\Sigma] !B$

Read as: Gamma union open set formula A close set derives in system Sigma formula B

Means: Gamma union open set formula A close set derives in system Sigma formula B

1 occurrence in this chapter

• Occurrence projected-formula-0026024

Equation form expr-1078b1cad3f129a0

$\Box\lnot !A$

Read as: box not formula A

Means: box not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025789

Equation form expr-12318729933c8a39

$\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$

Read as: modal system K D B four derives box box formula A implies diamond box formula A

Means: modal system K D B four derives box box formula A implies diamond box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025875

Equation form expr-13f237de7b4b344c

$(!A \land !B) \lif !B$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025673

Equation form expr-148de9c5a7a44d19

$p$

Read as: propositional variable p

Means: propositional variable p

9 occurrences in this chapter

• Occurrence projected-formula-0025775
• Occurrence projected-formula-0025777
• Occurrence projected-formula-0025787
• Occurrence projected-formula-0025840
• Occurrence projected-formula-0025862
• Occurrence projected-formula-0025866
• Occurrence projected-formula-0025878
• Occurrence projected-formula-0025885
• Occurrence projected-formula-0025893

Equation form expr-15428c53a6d72152

$\Box(!A \lif (!B \lif (!A \land !B))) \lif (\Box!A \lif \Box(!B \lif (!A \land !B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025688

Equation form expr-165a2676a255cdfb

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

Read as: modal system K T derives axiom D

Means: modal system K T derives axiom D

2 occurrences in this chapter

• Occurrence projected-formula-0025853
• Occurrence projected-formula-0025898

Equation form expr-16b95c611a54e3bb

$!A = \lnot p$

Read as: formula A equals not propositional variable p

Means: formula A equals not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025974

Equation form expr-18866b84545a9559

$\Sigma'$

Read as: Sigma prime

Means: Sigma prime

1 occurrence in this chapter

• Occurrence projected-formula-0025948

Equation form expr-189f40034be7a199

$j$

Read as: j

Means: j

1 occurrence in this chapter

• Occurrence projected-formula-0025550

Equation form expr-19581e27de7ced00

$9$

Read as: nine

Means: nine

2 occurrences in this chapter

• Occurrence projected-formula-0025683
• Occurrence projected-formula-0025701

Equation form expr-19840bcd955ee83f

$\Log{KB4} \Proves \Diamond\Diamond !A \lif \Diamond !A$

Read as: modal system K B four derives diamond diamond formula A implies diamond formula A

Means: modal system K B four derives diamond diamond formula A implies diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025886

Equation form expr-1a063c50d61363dc

$\Log{K} \Proves \Diamond(!A\lor!B) \lif (\Diamond!B \lor \Diamond!A)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025834

Equation form expr-1a8025b822ea3ae8

$(\Box(!A \land !B) \lif \Box!A) \lif{}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025677

Equation form expr-1b16b1df538ba12d

$n$

Read as: n

Means: n

4 occurrences in this chapter

• Occurrence projected-formula-0025576
• Occurrence projected-formula-0025579
• Occurrence projected-formula-0025745
• Occurrence projected-formula-0025749

Equation form expr-1b6b21b5976caa8c

$\Log{K} \Proves \Box(!A \lor !B) \lif (\Diamond !A \lor \Box !B)$

Read as: modal system K derives box open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or box formula B close parenthesis

Means: modal system K derives box open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula A or box formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025836

Equation form expr-1c7c647db363a3d5

$\Log{K} \Proves \lnot(!A \lor !B) \lif \lnot!A$

Read as: modal system K derives not open parenthesis formula A or formula B close parenthesis implies not formula A

Means: modal system K derives not open parenthesis formula A or formula B close parenthesis implies not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025817

Equation form expr-1e095d3ffc5363ea

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

Read as: modal system K B five derives axiom four

Means: modal system K B five derives axiom four

2 occurrences in this chapter

• Occurrence projected-formula-0025852
• Occurrence projected-formula-0025890

Equation form expr-1edbbd842397f724

$\Ax{T_\Diamond}$

Read as: axiom T subscript diamond

Means: axiom T subscript diamond

3 occurrences in this chapter

• Occurrence projected-formula-0025857
• Occurrence projected-formula-0025864
• Occurrence projected-formula-0025901

Equation form expr-1f2c1ee94265bef0

$\Log{K}!A_1\dots !A_n \Proves !B$

Read as: modal system K formula A subscript one and so on formula A subscript n derives formula B

Means: modal system K formula A subscript one and so on formula A subscript n derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025912

Equation form expr-2089967f10a9b8f2

$\Box(!B \lif (!A \land !B)) \lif (\Box!B \lif \Box(!A \land !B))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025690

Equation form expr-216c5d7f3e59d6c0

$\Log{K} \Proves !A \lif (!B \lif (!A \land !B))$

Read as: modal system K derives formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis

Means: modal system K derives formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025751

Equation form expr-21d031b0dacd8cc7

$\Log{K}$

Read as: modal system K

Means: modal system K

2 occurrences in this chapter

• Occurrence projected-formula-0025597
• Occurrence projected-formula-0025721

Equation form expr-2265d2c05f6ad387

$\lnot \Box p \lif \lnot\Box\lnot\lnot p$

Read as: not box propositional variable p implies not box not not propositional variable p

Means: not box propositional variable p implies not box not not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025713

Equation form expr-22a89cafaee2591f

$(\Box(!A \land !B) \lif (\Box !A \land \Box!B))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025681

Equation form expr-231e35a00ca52652

$\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$

Read as: model M does not satisfy box propositional variable p implies box box propositional variable p at world w subscript one

Means: model M does not satisfy box propositional variable p implies box box propositional variable p at world w subscript one

2 occurrences in this chapter

• Occurrence projected-formula-0025963
• Occurrence projected-formula-0025985

Equation form expr-240381337f804e9f

$!A \lif !B$

Read as: formula A implies formula B

Means: formula A implies formula B

3 occurrences in this chapter

• Occurrence projected-formula-0025531
• Occurrence projected-formula-0025725
• Occurrence projected-formula-0025727

Equation form expr-24cd4e56416f5e50

$\mSat/{{}}{\Diamond\lnot p}$

Read as: the displayed model does not satisfy diamond not propositional variable p at every world

Means: the displayed model does not satisfy diamond not propositional variable p at every world

1 occurrence in this chapter

• Occurrence projected-formula-0025978

Equation form expr-257be58da2eade38

$\Box!A \lif \Diamond!A$

Read as: box formula A implies diamond formula A

Means: box formula A implies diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025845

Equation form expr-25b3e180818b5473

$\Gamma \cup \Delta \Proves[\Sigma] !B$

Read as: Gamma union Delta derives in system Sigma formula B

Means: Gamma union Delta derives in system Sigma formula B

1 occurrence in this chapter

• Occurrence projected-formula-0026013

Equation form expr-270dc0fdb619ba89

$\Log{KDB4} \Proves \Diamond\Box!A \lif !A$

Read as: modal system K D B four derives diamond box formula A implies formula A

Means: modal system K D B four derives diamond box formula A implies formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025873

Equation form expr-28a789f9715e1be9

$> 1$

Read as: is greater than one

Means: is greater than one

1 occurrence in this chapter

• Occurrence projected-formula-0025624

Equation form expr-2c624232cdd22177

$8$

Read as: eight

Means: eight

1 occurrence in this chapter

• Occurrence projected-formula-0025718

Equation form expr-2d1270bb640714d1

$(\lnot \Box \lnot\lnot p \lif \Diamond \lnot p) \lif (\lnot \Box p \lif \Diamond\lnot p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025716

Equation form expr-2d7530d3a21435c8

$k>1$

Read as: k is greater than one

Means: k is greater than one

1 occurrence in this chapter

• Occurrence projected-formula-0025928

Equation form expr-2d7f97cd2a0481c5

$\Gamma, !A \Proves[\Sigma] !B$

Read as: Gamma comma formula A derives in system Sigma formula B

Means: Gamma comma formula A derives in system Sigma formula B

1 occurrence in this chapter

• Occurrence projected-formula-0026023

Equation form expr-2e18ad1f908942dc

$\Log{KD} \Proves/ \Box p \lif p$

Read as: modal system K D does not derive box propositional variable p implies propositional variable p

Means: modal system K D does not derive box propositional variable p implies propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025958

Equation form expr-2ed749931ec462f5

$\lnot\Diamond !A$

Read as: not diamond formula A

Means: not diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025788

Equation form expr-2f70130c7ab5739f

$K \in \Sigma$

Read as: K belongs to Sigma

Means: K belongs to Sigma

1 occurrence in this chapter

• Occurrence projected-formula-0025656

Equation form expr-2fc04c33adb96f01

$\Log{K} \Proves \Box\lnot !A \lif (\lnot \Box \lnot (!A \lor!B) \lif \lnot\Box\lnot !B)$

Read as: modal system K derives box not formula A implies open parenthesis not box not open parenthesis formula A or formula B close parenthesis implies not box not formula B close parenthesis

Means: modal system K derives box not formula A implies open parenthesis not box not open parenthesis formula A or formula B close parenthesis implies not box not formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025828

Equation form expr-2fc31acef0d322e4

$\Log{KTB4} = \Log{KT5} = \Log{KDB4} = \Log{KDB5}$

Read as: modal system K T B four equals modal system K T five equals modal system K D B four equals modal system K D B five

Means: modal system K T B four equals modal system K T five equals modal system K D B four equals modal system K D B five

1 occurrence in this chapter

• Occurrence projected-formula-0025903

Equation form expr-3106fac3e3c8f992

$w_2$

Read as: w subscript two

Means: w subscript two

4 occurrences in this chapter

• Occurrence projected-formula-0025968
• Occurrence projected-formula-0025975
• Occurrence projected-formula-0025982
• Occurrence projected-formula-0025986

Equation form expr-319b49b17c38d247

$!B_n \in \Gamma$

Read as: formula B subscript n belongs to Gamma

Means: formula B subscript n belongs to Gamma

1 occurrence in this chapter

• Occurrence projected-formula-0026002

Equation form expr-31d6a90607a6bc01

$(\Box!A \lif (\Box !B \lif \Box(!A \land !B))))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025693

Equation form expr-31ee67f41c5384b5

$!B \in \Log{K}!A_1 \dots !A_n$

Read as: formula B belongs to modal system K formula A subscript one and so on formula A subscript n

Means: formula B belongs to modal system K formula A subscript one and so on formula A subscript n

2 occurrences in this chapter

• Occurrence projected-formula-0025622
• Occurrence projected-formula-0025631

Equation form expr-32f11b9dc837c819

$!B_k$

Read as: formula B subscript k

Means: formula B subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0025549

Equation form expr-3313ce876fcd6074

$\Log{K} \Proves \Box!A \lif \Box (!B\lif !A)$

Read as: modal system K derives box formula A implies box open parenthesis formula B implies formula A close parenthesis

Means: modal system K derives box formula A implies box open parenthesis formula B implies formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025663

Equation form expr-331bbe87972d0b2f

$\Box(\lnot\lnot p \lif p) \lif (\Box \lnot\lnot p \lif \Box p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025710

Equation form expr-33a13c40e931da5f

$!B \equiv \Box !C$

Read as: formula B is equivalent to box formula C

Means: formula B is equivalent to box formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025632

Equation form expr-341d96cde465b372

$!B_2$

Read as: formula B subscript two

Means: formula B subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0025544

Equation form expr-343d2a2c1ab275b2

$\Log{K} \Proves \lnot\Diamond !A \liff \Box\lnot !A$

Read as: modal system K derives not diamond formula A if and only if box not formula A

Means: modal system K derives not diamond formula A if and only if box not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025790

Equation form expr-3719bd0e81217b5a

$\Log{K} \Proves (\Diamond !A \lif \Box !B) \lif \Box(!A \lif !B)$

Read as: modal system K derives open parenthesis diamond formula A implies box formula B close parenthesis implies box open parenthesis formula A implies formula B close parenthesis

Means: modal system K derives open parenthesis diamond formula A implies box formula B close parenthesis implies box open parenthesis formula A implies formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025837

Equation form expr-379b609d18ceb5b3

$\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$

Read as: modal system K derives not formula A implies open parenthesis not formula B implies not open parenthesis formula A or formula B close parenthesis close parenthesis

Means: modal system K derives not formula A implies open parenthesis not formula B implies not open parenthesis formula A or formula B close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025826

Equation form expr-3994f5bb8fc49c9b

$\Log{K} \Proves \Diamond \lnot p \liff \lnot\Box\lnot\lnot p$

Read as: modal system K derives diamond not propositional variable p if and only if not box not not propositional variable p

Means: modal system K derives diamond not propositional variable p if and only if not box not not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025772

Equation form expr-3aca066f86c9298a

$\Log{K}!A_1\dots!A_n \Proves !C \lif !B$

Read as: modal system K formula A subscript one and so on formula A subscript n derives formula C implies formula B

Means: modal system K formula A subscript one and so on formula A subscript n derives formula C implies formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025645

Equation form expr-3b60a51ca60feb0d

$\Log{K} \Proves \Box!A \lif (\Diamond(!A \lif !B) \lif \Diamond !B)$

Read as: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis

Means: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025813

Equation form expr-3bc29fc095523486

$\Diamond \lnot p \liff \lnot\Box\lnot\lnot p$

Read as: diamond not propositional variable p if and only if not box not not propositional variable p

Means: diamond not propositional variable p if and only if not box not not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025704

Equation form expr-3c5592ed3a6cb02b

$\Gamma \Proves[\Sigma] \lfalse$

Read as: Gamma derives in system Sigma falsity

Means: Gamma derives in system Sigma falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026059

Equation form expr-3d1e5ad3c4923511

$\Log{K} \Proves (!A \lif !B) \lif (\lnot !B \lif \lnot !A)$

Read as: modal system K derives open parenthesis formula A implies formula B close parenthesis implies open parenthesis not formula B implies not formula A close parenthesis

Means: modal system K derives open parenthesis formula A implies formula B close parenthesis implies open parenthesis not formula B implies not formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025802

Equation form expr-3e01c74c53729a40

$\Log{K} \Proves \Box!A \lif (\Box !B \lif \Box(!A \land !B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025752

Equation form expr-3f96bc573087aa57

$!A \in \Sigma$

Read as: formula A belongs to Sigma

Means: formula A belongs to Sigma

2 occurrences in this chapter

• Occurrence projected-formula-0025561
• Occurrence projected-formula-0025572

Equation form expr-438757f12dd8c3fc

$w_1$

Read as: w subscript one

Means: w subscript one

4 occurrences in this chapter

• Occurrence projected-formula-0025966
• Occurrence projected-formula-0025972
• Occurrence projected-formula-0025979
• Occurrence projected-formula-0025988

Equation form expr-43a9c3c2e61f7961

$(\Box \lnot\lnot p \lif \Box p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025711

Equation form expr-43fa93d0be1e4969

$!C \lif !B \in \Log{K}!A_1 \dots !A_n$

Read as: formula C implies formula B belongs to modal system K formula A subscript one and so on formula A subscript n

Means: formula C implies formula B belongs to modal system K formula A subscript one and so on formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025630

Equation form expr-4446fcf0cd4d6fb1

$\Box!A \lif \Box (!B\lif !A)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025667

Equation form expr-44a0cd8d367911cf

$\Log{KB4} \Proves \Diamond!A \lif \Box\Diamond!A$

Read as: modal system K B four derives diamond formula A implies box diamond formula A

Means: modal system K B four derives diamond formula A implies box diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025889

Equation form expr-453110e031e4f41a

$\lnot\lnot p \lif p$

Read as: not not propositional variable p implies propositional variable p

Means: not not propositional variable p implies propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025708

Equation form expr-4794277b410dfc51

$\lnot p$

Read as: not propositional variable p

Means: not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025839

Equation form expr-47bd1b3452eab684

$\lnot\Box\lnot$

Read as: not box not

Means: not box not

5 occurrences in this chapter

• Occurrence projected-formula-0025808
• Occurrence projected-formula-0025815
• Occurrence projected-formula-0025822
• Occurrence projected-formula-0025833
• Occurrence projected-formula-0025841

Equation form expr-47c6793cea7c1123

$!C_k = !B$

Read as: formula C subscript k equals formula B

Means: formula C subscript k equals formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025605

Equation form expr-49fbfbae7391d15b

$\Ax{K}$

Read as: axiom K

Means: axiom K

2 occurrences in this chapter

• Occurrence projected-formula-0025527
• Occurrence projected-formula-0025607

Equation form expr-4a44dc15364204a8

$10$

Read as: ten

Means: ten

1 occurrence in this chapter

• Occurrence projected-formula-0025719

Equation form expr-4a8223ac7b0e9518

$\Log{KB} \neq \Log{K4}$

Read as: modal system K B is not equal to modal system K four

Means: modal system K B is not equal to modal system K four

1 occurrence in this chapter

• Occurrence projected-formula-0025959

Equation form expr-4b32f069e8444936

$(\Box!A \lif (\Box !B \lif \Box(!A \land !B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025695

Equation form expr-4bd801cb1572ecb0

$(!A \lif \lfalse) \lif ((\lnot!A \lif \lfalse) \lif \lfalse)$

Read as: open parenthesis formula A implies falsity close parenthesis implies open parenthesis open parenthesis not formula A implies falsity close parenthesis implies falsity close parenthesis

Means: open parenthesis formula A implies falsity close parenthesis implies open parenthesis open parenthesis not formula A implies falsity close parenthesis implies falsity close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0026058

Equation form expr-4dd70e1f2e572d71

$\mClass{C} = \mClass{C}_1 \cap \dots \cap \mClass{C}_n$

Read as: class C of models equals class C of models subscript one intersected with and so on intersected with class C of models subscript n

Means: class C of models equals class C of models subscript one intersected with and so on intersected with class C of models subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025915

Equation form expr-4e07408562bedb8b

$3$

Read as: three

Means: three

1 occurrence in this chapter

• Occurrence projected-formula-0025991

Equation form expr-4ee59b68125f5f6c

$(\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

• Occurrence projected-formula-0025723

Equation form expr-4ef706eb029cf11a

$\Log{K} \Proves \Box (!A \lif !B) \lif (\Diamond !A \lif \Diamond !B)$

Read as: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis

Means: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025801

Equation form expr-500c11a94df59a45

$\Log{K} !A_1 \dots !A_n$

Read as: modal system K formula A subscript one and so on formula A subscript n

Means: modal system K formula A subscript one and so on formula A subscript n

4 occurrences in this chapter

• Occurrence projected-formula-0025596
• Occurrence projected-formula-0025598
• Occurrence projected-formula-0025601
• Occurrence projected-formula-0025640

Equation form expr-506924f8b577f722

$\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$

Read as: modal system K derives not box propositional variable p implies diamond not propositional variable p

Means: modal system K derives not box propositional variable p implies diamond not propositional variable p

5 occurrences in this chapter

• Occurrence projected-formula-0025703
• Occurrence projected-formula-0025771
• Occurrence projected-formula-0025774
• Occurrence projected-formula-0025781
• Occurrence projected-formula-0025793

Equation form expr-50f74f36c7758da0

$\Box((!A \land !B) \lif !B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025674

Equation form expr-50f8049a09f05d01

$!B_j$

Read as: B subscript j

Means: B subscript j

2 occurrences in this chapter

• Occurrence projected-formula-0025548
• Occurrence projected-formula-0025552

Equation form expr-5136fc4246e7d497

$\Diamond$

Read as: diamond

Means: diamond

7 occurrences in this chapter

• Occurrence projected-formula-0025559
• Occurrence projected-formula-0025760
• Occurrence projected-formula-0025807
• Occurrence projected-formula-0025814
• Occurrence projected-formula-0025821
• Occurrence projected-formula-0025832
• Occurrence projected-formula-0025842

Equation form expr-51aeea8ffa05d262

$n-1$

Read as: n minus one

Means: n minus one

1 occurrence in this chapter

• Occurrence projected-formula-0025578

Equation form expr-51e7856994a926ec

$\Gamma \Proves[\Sigma] !A \lor !B$

Read as: Gamma derives in system Sigma formula A or formula B

Means: Gamma derives in system Sigma formula A or formula B

1 occurrence in this chapter

• Occurrence projected-formula-0026020

Equation form expr-52baf5b113b97063

$\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

2 occurrences in this chapter

• Occurrence projected-formula-0025850
• Occurrence projected-formula-0025872

Equation form expr-52bb5adcf016a8a2

$\Gamma \Proves/[\Sigma] \lfalse$

Read as: Gamma does not derive in system Sigma falsity

Means: Gamma does not derive in system Sigma falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026033

Equation form expr-53c8b8afb540c2ea

$\Log{K} \Proves \Diamond!A \lif \Diamond(!A \lor !B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025820

Equation form expr-5414c01467975560

$\mSat/{{}}{\Box\Diamond\lnot p}$

Read as: the displayed model does not satisfy box diamond not propositional variable p at every world

Means: the displayed model does not satisfy box diamond not propositional variable p at every world

1 occurrence in this chapter

• Occurrence projected-formula-0025981

Equation form expr-546773d1ccbf5c7a

$\Log{K}\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$

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

Means: modal system K 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

• Occurrence projected-formula-0025685

Equation form expr-559582ac022e201a

$\Box((!A \land !B) \lif !B) \lif (\Box(!A \land !B) \lif \Box!B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025675

Equation form expr-55c17123174d849d

$\Sigma' \Proves !A$

Read as: Sigma prime derives formula A

Means: Sigma prime derives formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025950

Equation form expr-560ac2b1f4286405

$(\Box!A \lif (\Box !B \lif \Box(!A \land !B)))) \lif {}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025697

Equation form expr-56eaa7e521d8b68a

$!C \ident !A \lif !B$

Read as: formula C is syntactically identical to formula A implies formula B

Means: formula C is syntactically identical to formula A implies formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025536

Equation form expr-573dcf0de5d66fd4

$!A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots)$

Read as: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis

Means: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025574

Equation form expr-57885e4c75965b23

$\Gamma$

Read as: Gamma

Means: Gamma

8 occurrences in this chapter

• Occurrence projected-formula-0025996
• Occurrence projected-formula-0025999
• Occurrence projected-formula-0026005
• Occurrence projected-formula-0026025
• Occurrence projected-formula-0026030
• Occurrence projected-formula-0026036
• Occurrence projected-formula-0026037
• Occurrence projected-formula-0026044

Equation form expr-580dbff7b7bba68a

$\Gamma \Proves[\Sigma] !A_1$

Read as: Gamma derives in system Sigma formula A subscript one

Means: Gamma derives in system Sigma formula A subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0026016

Equation form expr-581916bfec222f93

$& (p \lif q) \lif (\lnot q \lif \lnot p) \\ & (p \lif q) \lif ((q \lif r) \lif (p \lif r)).$

Read as: Two tautological schemata. First: if p implies q, then if not q, then not p. Second: if p implies q, then if q implies r, then p implies r.

Means: Two tautological schemata. First: if p implies q, then if not q, then not p. Second: if p implies q, then if q implies r, then p implies r.

1 occurrence in this chapter

• Occurrence projected-formula-0025720

Equation form expr-59ffeaf5963458db

$(\Diamond \lnot p \liff \lnot\Box\lnot\lnot p) \lif {}$

Read as: open parenthesis diamond not propositional variable p if and only if not box not not propositional variable p close parenthesis implies open set close set

Means: open parenthesis diamond not propositional variable p if and only if not box not not propositional variable p close parenthesis implies open set close set

1 occurrence in this chapter

• Occurrence projected-formula-0025705

Equation form expr-5a6035a3fb0dfbd8

$!C_k$

Read as: formula C subscript k

Means: formula C subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0025604

Equation form expr-5a8201e9de54d471

$\Box(!A \land !B) \lif \Box!A$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025672

Equation form expr-5c830159f595bce4

$\Log{K} \Proves !A_1$

Read as: modal system K derives formula A subscript one

Means: modal system K derives formula A subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0025735

Equation form expr-5cd68f262fd86ad0

$(\Box(!B \lif (!A \land !B)) \lif (\Box!B \lif \Box(!A \land !B))) \lif {}$

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

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

2 occurrences in this chapter

• Occurrence projected-formula-0025692
• Occurrence projected-formula-0025694

Equation form expr-5d8d083cbb26120c

$\Log{KT} \Proves \Log{D}$

Read as: modal system K T derives modal system D

Means: modal system K T derives modal system D

1 occurrence in this chapter

• Occurrence projected-formula-0025956

Equation form expr-5d8f6af316e3245f

$\Log{K} \Proves \Diamond!B \lif \Diamond(!A \lor !B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025823

Equation form expr-5e22763a65c3f0a3

$\Log{KDB4} \Proves \Box!A \lif !A$

Read as: modal system K D B four derives box formula A implies formula A

Means: modal system K D B four derives box formula A implies formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025881

Equation form expr-5e585fb8dfd9f7c9

$\Gamma \subseteq \Delta$

Read as: Gamma is a subset of Delta

Means: Gamma is a subset of Delta

1 occurrence in this chapter

• Occurrence projected-formula-0026007

Equation form expr-6061a5591edaa80a

$\Ax{5_\Diamond}$

Read as: axiom five subscript diamond

Means: axiom five subscript diamond

2 occurrences in this chapter

• Occurrence projected-formula-0025869
• Occurrence projected-formula-0025895

Equation form expr-60a4de1bd67e026d

$\Log{K} \Proves \lnot\lnot p \liff p$

Read as: modal system K derives not not propositional variable p if and only if propositional variable p

Means: modal system K derives not not propositional variable p if and only if propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025780

Equation form expr-60add8f35a287afd

$\Log{KD5} \neq \Log{KT4} = \Log{S4}$

Read as: modal system K D five is not equal to modal system K T four equals modal system S four

Means: modal system K D five is not equal to modal system K T four equals modal system S four

1 occurrence in this chapter

• Occurrence projected-formula-0025984

Equation form expr-619c6509406bf4f8

$\mSat/{{}}{\Box p}$

Read as: the displayed model does not satisfy box propositional variable p at every world

Means: the displayed model does not satisfy box propositional variable p at every world

1 occurrence in this chapter

• Occurrence projected-formula-0025967

Equation form expr-61f3515f0e2771bd

$\Gamma \Proves[\Sigma] \lnot !A$

Read as: Gamma derives in system Sigma not formula A

Means: Gamma derives in system Sigma not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0026021

Equation form expr-63806ef7f6aa0dee

$\Log{KT5} \Proves !A \lif \Box\Diamond!A$

Read as: modal system K T five derives formula A implies box diamond formula A

Means: modal system K T five derives formula A implies box diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025858

Equation form expr-67bb42c13a45506c

$\Proves !C(!B)$

Read as: derives formula C open parenthesis formula B close parenthesis

Means: derives formula C open parenthesis formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025770

Equation form expr-6875e4221251441e

$\lnot \Box q \lif \Diamond \lnot p$

Read as: not box propositional variable q implies diamond not propositional variable p

Means: not box propositional variable q implies diamond not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025785

Equation form expr-68af1b29d5f49fb3

$\Sigma \Proves !A$

Read as: Sigma derives formula A

Means: Sigma derives formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025557

Equation form expr-691a0b96f32b9f7e

$\Log{KB4} \Proves \Diamond!A \lif \Box \Diamond\Diamond!A$

Read as: modal system K B four derives diamond formula A implies box diamond diamond formula A

Means: modal system K B four derives diamond formula A implies box diamond diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025883

Equation form expr-6b86b273ff34fce1

$1$

Read as: one

Means: one

2 occurrences in this chapter

• Occurrence projected-formula-0025617
• Occurrence projected-formula-0025917

Equation form expr-6d34fa36d139b1d0

$\Gamma \Proves[\Sigma] !A \to \lfalse$

Read as: Gamma derives in system Sigma formula A implies falsity

Means: Gamma derives in system Sigma formula A implies falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026056

Equation form expr-6e248011b2a8b9e1

$\Gamma \Proves[\Sigma] !B \lif !A$

Read as: Gamma derives in system Sigma formula B implies formula A

Means: Gamma derives in system Sigma formula B implies formula A

1 occurrence in this chapter

• Occurrence projected-formula-0026015

Equation form expr-6e9c39a8bb74cb83

$\Proves !A \liff !B$

Read as: derives formula A if and only if formula B

Means: derives formula A if and only if formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025769

Equation form expr-6fb4d8e138798b3d

$\Dual$

Read as: the duality axiom

Means: the duality axiom

2 occurrences in this chapter

• Occurrence projected-formula-0025608
• Occurrence projected-formula-0025618

Equation form expr-7120f8695fd9aa83

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

Read as: modal system K B four derives axiom five

Means: modal system K B four derives axiom five

2 occurrences in this chapter

• Occurrence projected-formula-0025851
• Occurrence projected-formula-0025882

Equation form expr-72039af57d5ec07d

$\Log{K} \Proves \Diamond \lnot \lfalse \lif (\Box !A \lif \Diamond !A)$

Read as: modal system K derives diamond not falsity implies open parenthesis box formula A implies diamond formula A close parenthesis

Means: modal system K derives diamond not falsity implies open parenthesis box formula A implies diamond formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025835

Equation form expr-72fb6b0ff9a2ed1c

$\Log{K} \Proves (\Diamond!A \lor\Diamond!B) \lif \Diamond(!A \lor !B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025824

Equation form expr-74fbe4a1906c905e

$\lnot\lnot !A$

Read as: not not formula A

Means: not not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025733

Equation form expr-751379acac529582

$\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

• Occurrence projected-formula-0025724

Equation form expr-773bd9f41893c402

$!B \in \Log{K}!A_1\dots!A_n$

Read as: formula B belongs to modal system K formula A subscript one and so on formula A subscript n

Means: formula B belongs to modal system K formula A subscript one and so on formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025636

Equation form expr-776e6199da44defe

$\tag{\Ax{T_\Diamond}} p & \lif \Diamond p\\ \tag{\Ax{B_\Diamond}} \Diamond\Box p & \lif p\\ \tag{\Ax{4_\Diamond}} \Diamond\Diamond p & \lif \Diamond p\\ \tag{\Ax{5_\Diamond}} \Diamond\Box p & \lif \Box p$

Read as: The four dual schemata, in order. T diamond: if p then possibly p. B diamond: if possibly necessarily p then p. Four diamond: if possibly possibly p then possibly p. Five diamond: if possibly necessarily p then necessarily p.

Means: The four dual schemata, in order. T diamond: if p then possibly p. B diamond: if possibly necessarily p then p. Four diamond: if possibly possibly p then possibly p. Five diamond: if possibly necessarily p then necessarily p.

1 occurrence in this chapter

• Occurrence projected-formula-0025838

Equation form expr-78e80e6c22a9a4b7

$\Log{K} !A_1 \dots !A_n \Proves !B$

Read as: modal system K formula A subscript one and so on formula A subscript n derives formula B

Means: modal system K formula A subscript one and so on formula A subscript n derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025602

Equation form expr-790f441d2dc498bc

$(\Box(!A \land !B) \lif \Box!B) \lif{}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025680

Equation form expr-7b8dff15e7d0e9be

$!D_n$

Read as: formula D subscript n

Means: formula D subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025563

Equation form expr-7b981162fa144a02

$\Log{KB5} \Proves \Box!A \lif \Box\Diamond\Box !A$

Read as: modal system K B five derives box formula A implies box diamond box formula A

Means: modal system K B five derives box formula A implies box diamond box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025891

Equation form expr-7c92cb41f5dc5782

$\lnot\Diamond\lnot$

Read as: not diamond not

Means: not diamond not

1 occurrence in this chapter

• Occurrence projected-formula-0025843

Equation form expr-7d2ec9b68b9609db

$\Log{KD} \subsetneq \Log{KT}$

Read as: modal system K D is a proper subset of modal system K T

Means: modal system K D is a proper subset of modal system K T

1 occurrence in this chapter

• Occurrence projected-formula-0025952

Equation form expr-7d44f5dae51c5481

$((\Box(!A \land !B) \lif \Box!B) \lif{}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025678

Equation form expr-7ffee107cfb27a7b

$\Log{KT} \Proves \Box !A \lif \Diamond !A$

Read as: modal system K T derives box formula A implies diamond formula A

Means: modal system K T derives box formula A implies diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025902

Equation form expr-8009e7649758501d

$\Gamma, !A \Proves[\Sigma] \lfalse$

Read as: Gamma comma formula A derives in system Sigma falsity

Means: Gamma comma formula A derives in system Sigma falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026054

Equation form expr-804eecd0d613d453

$\Log{K} \Proves \Box(!A \lif !B) \lif (\Box\lnot!B \lif \Box\lnot!A)$

Read as: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis box not formula B implies box not formula A close parenthesis

Means: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis box not formula B implies box not formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025803

Equation form expr-8063806edfa91aa3

$\Log{KD} \subseteq \Log{KT}$

Read as: modal system K D is a subset of modal system K T

Means: modal system K D is a subset of modal system K T

1 occurrence in this chapter

• Occurrence projected-formula-0025953

Equation form expr-8238c028f61fc0f7

$!A$

Read as: formula A

Means: formula A

18 occurrences in this chapter

• Occurrence projected-formula-0025530
• Occurrence projected-formula-0025534
• Occurrence projected-formula-0025537
• Occurrence projected-formula-0025540
• Occurrence projected-formula-0025555
• Occurrence projected-formula-0025565
• Occurrence projected-formula-0025568
• Occurrence projected-formula-0025734
• Occurrence projected-formula-0025762
• Occurrence projected-formula-0025766
• Occurrence projected-formula-0025783
• Occurrence projected-formula-0025795
• Occurrence projected-formula-0025796
• Occurrence projected-formula-0025846
• Occurrence projected-formula-0025949
• Occurrence projected-formula-0025997
• Occurrence projected-formula-0026039
• Occurrence projected-formula-0026046

Equation form expr-8251e8502b2ca005

$\Dual \in \Sigma$

Read as: the duality axiom belongs to Sigma

Means: the duality axiom belongs to Sigma

1 occurrence in this chapter

• Occurrence projected-formula-0025658

Equation form expr-85c3ce29e3a4dc40

$\mClass{C}$

Read as: class C of models

Means: class C of models

5 occurrences in this chapter

• Occurrence projected-formula-0025921
• Occurrence projected-formula-0025926
• Occurrence projected-formula-0025938
• Occurrence projected-formula-0025940
• Occurrence projected-formula-0025945

Equation form expr-861c59f6c65c88e0

$\Log{K} \Proves \Subst{!C}{B}{q}$

Read as: modal system K derives the result of substituting formula B for propositional variable q in formula C

Means: modal system K derives the result of substituting formula B for propositional variable q in formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025756

Equation form expr-874748ebc3ce81d4

$((\Box!A \land \Box!B) \lif \Box(!A \land !B))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025698

Equation form expr-88ede056472d4ec7

$\Proves !C(!A)$

Read as: derives formula C open parenthesis formula A close parenthesis

Means: derives formula C open parenthesis formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025768

Equation form expr-89d4d22866321b82

$\tag{\Ax{K}} & \Box(p \lif q) \lif (\Box p \lif \Box q), \\ \tag{\Dual} & \Diamond p \liff \lnot\Box\lnot p$

Read as: tagged axiom K next alignment column box open parenthesis propositional variable p implies propositional variable q close parenthesis implies open parenthesis box propositional variable p implies box propositional variable q close parenthesis comma next line tagged the duality axiom next alignment column diamond propositional variable p if and only if not box not propositional variable p

Means: tagged axiom K next alignment column box open parenthesis propositional variable p implies propositional variable q close parenthesis implies open parenthesis box propositional variable p implies box propositional variable q close parenthesis comma next line tagged the duality axiom next alignment column diamond propositional variable p if and only if not box not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025571

Equation form expr-89d67874d1f6d123

$\Log{K} \Proves \Box\lnot !A \lif (\Box\lnot!B \lif \Box \lnot (!A \lor !B))$

Read as: modal system K derives box not formula A implies open parenthesis box not formula B implies box not open parenthesis formula A or formula B close parenthesis close parenthesis

Means: modal system K derives box not formula A implies open parenthesis box not formula B implies box not open parenthesis formula A or formula B close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025827

Equation form expr-8bd2005830815bd2

$\Box!A$

Read as: box formula A

Means: box formula A

4 occurrences in this chapter

• Occurrence projected-formula-0025861
• Occurrence projected-formula-0025865
• Occurrence projected-formula-0025877
• Occurrence projected-formula-0025892

Equation form expr-8c02bb37c0e400a6

$\mSat{{}}{\Diamond\lnot p}$

Read as: the displayed model satisfies diamond not propositional variable p at every world

Means: the displayed model satisfies diamond not propositional variable p at every world

1 occurrence in this chapter

• Occurrence projected-formula-0025980

Equation form expr-8d06eb5be2ab477b

$\mSat/{M}{\Box p \to \Box \Box p}[w_1]$

Read as: model M does not satisfy box propositional variable p implies box box propositional variable p at world w subscript one

Means: model M does not satisfy box propositional variable p implies box box propositional variable p at world w subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0025971

Equation form expr-8e37e5feabde8d38

$\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$

Read as: modal system K D B four derives box formula A implies box box formula A

Means: modal system K D B four derives box formula A implies box box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025880

Equation form expr-8eb83b2ad42d11d3

$\Log{K} \Proves \Box!A \lif (\lnot \Box\lnot (!A\lif !B) \lif \lnot \Box\lnot!B)$

Read as: modal system K derives box formula A implies open parenthesis not box not open parenthesis formula A implies formula B close parenthesis implies not box not formula B close parenthesis

Means: modal system K derives box formula A implies open parenthesis not box not open parenthesis formula A implies formula B close parenthesis implies not box not formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025812

Equation form expr-8f4c747df4608f85

$\Log{K}!A_1\dots!A_n \Proves \Ax{K}$

Read as: modal system K formula A subscript one and so on formula A subscript n derives axiom K

Means: modal system K formula A subscript one and so on formula A subscript n derives axiom K

1 occurrence in this chapter

• Occurrence projected-formula-0025655

Equation form expr-8f707e40fb6af3d1

$(\Box \lnot\lnot p \lif \Box p) \lif (\lnot \Box p \lif \lnot\Box\lnot\lnot p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025712

Equation form expr-8f983d6fea027c03

$\mClass{C}_1 \cap \dots \cap \mClass{C}_n$

Read as: class C of models subscript one intersected with and so on intersected with class C of models subscript n

Means: class C of models subscript one intersected with and so on intersected with class C of models subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025914

Equation form expr-8fded0ecc6c367dd

$\Log{KDB4} \Proves \Box\Box!A \lif !A$

Read as: modal system K D B four derives box box formula A implies formula A

Means: modal system K D B four derives box box formula A implies formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025879

Equation form expr-903d52c30476fc27

$\Gamma \Proves/[\Sigma] !A$

Read as: Gamma does not derive in system Sigma formula A

Means: Gamma does not derive in system Sigma formula A

1 occurrence in this chapter

• Occurrence projected-formula-0026040

Equation form expr-928d3dcddf5279f8

$!B \in \Sigma$

Read as: formula B belongs to Sigma

Means: formula B belongs to Sigma

2 occurrences in this chapter

• Occurrence projected-formula-0025567
• Occurrence projected-formula-0025611

Equation form expr-92b59bb8de3808b7

$!B_i$

Read as: formula B subscript i

Means: formula B subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0025546

Equation form expr-93aa632d054e9ffb

$!A \lif (!B \lif !A)$

Read as: formula A implies open parenthesis formula B implies formula A close parenthesis

Means: formula A implies open parenthesis formula B implies formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025664

Equation form expr-954d59819434a41a

$!A \lif (!B \lif (!A \land !B))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025686

Equation form expr-966b2d3dcfa7cc20

$\mSat{{}}{\Box p}, \mSat/{{}}{\Box\Box p}$

Read as: the displayed model satisfies box propositional variable p at every world comma the displayed model does not satisfy box box propositional variable p at every world

Means: the displayed model satisfies box propositional variable p at every world comma the displayed model does not satisfy box box propositional variable p at every world

1 occurrence in this chapter

• Occurrence projected-formula-0025987

Equation form expr-973219f61c684db2

$\mSat/{{}}{\Box\Box p}$

Read as: the displayed model does not satisfy box box propositional variable p at every world

Means: the displayed model does not satisfy box box propositional variable p at every world

2 occurrences in this chapter

• Occurrence projected-formula-0025965
• Occurrence projected-formula-0025977

Equation form expr-9763a163e7ff6591

$w_3$

Read as: w subscript three

Means: w subscript three

2 occurrences in this chapter

• Occurrence projected-formula-0025983
• Occurrence projected-formula-0025989

Equation form expr-9861ca19be665e0a

$\Ax{D}$

Read as: axiom D

Means: axiom D

1 occurrence in this chapter

• Occurrence projected-formula-0025876

Equation form expr-98b3da780aeffee8

$\Log{KB4} \Proves \Box\Diamond\Diamond !A \lif \Box \Diamond!A$

Read as: modal system K B four derives box diamond diamond formula A implies box diamond formula A

Means: modal system K B four derives box diamond diamond formula A implies box diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025888

Equation form expr-992accb9917efeb5

$!C$

Read as: formula C

Means: formula C

10 occurrences in this chapter

• Occurrence projected-formula-0025535
• Occurrence projected-formula-0025627
• Occurrence projected-formula-0025629
• Occurrence projected-formula-0025633
• Occurrence projected-formula-0025647
• Occurrence projected-formula-0025757
• Occurrence projected-formula-0025934
• Occurrence projected-formula-0025936
• Occurrence projected-formula-0025942
• Occurrence projected-formula-0025944

Equation form expr-9947646a3ceed43b

$\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$

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

Means: modal system K 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

• Occurrence projected-formula-0025750

Equation form expr-9a44b9bb01db1eac

$\Delta \Proves[\Sigma] !A$

Read as: Delta derives in system Sigma formula A

Means: Delta derives in system Sigma formula A

1 occurrence in this chapter

• Occurrence projected-formula-0026008

Equation form expr-9b550f2bb9885b69

$\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$

Read as: modal system K T five derives box formula A implies diamond box formula A

Means: modal system K T five derives box formula A implies diamond box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025863

Equation form expr-9b91d4c4c00d00f8

$\Log{K}!A = \Log{K}!A_{\Diamond}$

Read as: modal system K formula A equals modal system K formula A subscript diamond

Means: modal system K formula A equals modal system K formula A subscript diamond

1 occurrence in this chapter

• Occurrence projected-formula-0025847

Equation form expr-9c46576ff4aee158

$\Log{KT5} \Proves !A \lif \Diamond!A$

Read as: modal system K T five derives formula A implies diamond formula A

Means: modal system K T five derives formula A implies diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025856

Equation form expr-9cdeed6ed221f857

$\Log{K} \Proves (\Diamond!A \lor \Diamond!B) \lif \Diamond(!A \lor !B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025816

Equation form expr-9da3705cc5efefce

$\Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B} \subseteq \Log{K} !A_1 \dots !A_n$

Read as: the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B is a subset of modal system K formula A subscript one and so on formula A subscript n

Means: the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B is a subset of modal system K formula A subscript one and so on formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025615

Equation form expr-9e4668e35b07aeed

$\Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1} \lif \Box!A_n)\cdots).$

Read as: box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis period

Means: box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis period

1 occurrence in this chapter

• Occurrence projected-formula-0025575

Equation form expr-9f3adbad42513293

$\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$

Read as: modal system K T five derives diamond box formula A implies box formula A

Means: modal system K T five derives diamond box formula A implies box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025868

Equation form expr-a0ad19b3662c695f

$\Gamma \Proves[\Sigma] !B$

Read as: Gamma derives in system Sigma formula B

Means: Gamma derives in system Sigma formula B

2 occurrences in this chapter

• Occurrence projected-formula-0026019
• Occurrence projected-formula-0026022

Equation form expr-a0be2a80eca4a7c9

$& !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots) \in \Sigma \intertext{By the induction hypothesis, we have} & \Box!A_1 \lif (\Box!A_2 \lif \cdots \Box(!A_{n-1} \lif !A_n)\cdots) \in \Sigma \intertext{Since $\Sigma$ is a normal modal logic, it contains all instances of~$\Ax{K}$, in particular} & \Box(!A_{n-1} \lif !A_n) \lif (\Box!A_{n-1} \lif \Box!A_n) \in \Sigma \intertext{Using modus ponens and suitable tautological instances we get} & \Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1} \lif \Box!A_n)\cdots) \in \Sigma.$

Read as: Induction display for rule R K. First assume the nested conditional from A one through A n belongs to Sigma. By the induction hypothesis, the corresponding nested conditional has boxes on A one through A n minus one, and a box around the final conditional. Since Sigma is normal, it contains the K instance taking that boxed final conditional to the conditional from box A n minus one to box A n. Modus ponens and propositional tautologies give the fully boxed nested conditional.

Means: Induction display for rule R K. First assume the nested conditional from A one through A n belongs to Sigma. By the induction hypothesis, the corresponding nested conditional has boxes on A one through A n minus one, and a box around the final conditional. Since Sigma is normal, it contains the K instance taking that boxed final conditional to the conditional from box A n minus one to box A n. Modus ponens and propositional tautologies give the fully boxed nested conditional.

1 occurrence in this chapter

• Occurrence projected-formula-0025580

Equation form expr-a10d1e8bd329c89a

$\Gamma \cup \{ \lnot!A \}$

Read as: Gamma union open set not formula A close set

Means: Gamma union open set not formula A close set

3 occurrences in this chapter

• Occurrence projected-formula-0026042
• Occurrence projected-formula-0026049
• Occurrence projected-formula-0026052

Equation form expr-a13c4538b2c8a517

$\Log{K} \Proves \Box !A_1 \lif (\Box !A_2 \lif \cdots (\Box !A_{n-1} \lif \Box !A_n)\dots)$

Read as: modal system K derives box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis

Means: modal system K derives box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025748

Equation form expr-a158c8ba25884247

$\Log{K} \Proves !A$

Read as: modal system K derives formula A

Means: modal system K derives formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025799

Equation form expr-a27dc218af2e26e3

$\Log{K} \Proves \Box(!A \lif !B) \lif (\lnot \Box\lnot!A \lif \lnot\Box\lnot!B)$

Read as: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis

Means: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025805

Equation form expr-a32559d88fbf8b15

$!A \lif !C$

Read as: formula A implies formula C

Means: formula A implies formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025729

Equation form expr-a3550a26e80e1d24

$((\lnot \Box \lnot\lnot p \lif \Diamond \lnot p) \lif (\lnot \Box p \lif \Diamond\lnot p))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025715

Equation form expr-a41c104b89d839cd

$(\Box!A \lif \Box(!B \lif (!A \land !B))) \lif {}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025691

Equation form expr-a4448888755f3ded

$\lnot\Box p \lif \Diamond \lnot p$

Read as: not box propositional variable p implies diamond not propositional variable p

Means: not box propositional variable p implies diamond not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025717

Equation form expr-a69f0090227bdc1b

$\mSat/{M}{\Diamond \lnot p \lif \Box \Diamond \lnot p}[w_2]$

Read as: model M does not satisfy diamond not propositional variable p implies box diamond not propositional variable p at world w subscript two

Means: model M does not satisfy diamond not propositional variable p implies box diamond not propositional variable p at world w subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0025973

Equation form expr-a81c5dff5a355f30

$!A_1 \lif (!A_2 \lif \cdots (!A_n \lif !B)\dots)$

Read as: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n implies formula B close parenthesis and so on close parenthesis

Means: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n implies formula B close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025744

Equation form expr-a90fd7c7139176dc

$\Log{K} \Proves \lnot \Box \lnot(!A\lor!B) \lif (\lnot \lnot\Box\lnot!B \lif \lnot\Box\lnot!A)$

Read as: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis not not box not formula B implies not box not formula A close parenthesis

Means: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis not not box not formula B implies not box not formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025830

Equation form expr-aa1d4eafd3d3b4e2

$\lnot \Box \lnot\lnot p \lif \Diamond \lnot p$

Read as: not box not not propositional variable p implies diamond not propositional variable p

Means: not box not not propositional variable p implies diamond not propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025707

Equation form expr-aa413926f024cbf8

$\Nec$

Read as: necessitation

Means: necessitation

1 occurrence in this chapter

• Occurrence projected-formula-0025635

Equation form expr-ab342c2b31de328b

$\Gamma, \lnot !A \Proves[\Sigma] \lfalse$

Read as: Gamma comma not formula A derives in system Sigma falsity

Means: Gamma comma not formula A derives in system Sigma falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026055

Equation form expr-ab65862f3a9a5605

$(\Box(!A \land !B) \lif (\Box !A \land \Box!B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025679

Equation form expr-ab768e094a624812

$\Log{K} \Proves \lnot \Box \lnot(!A \lor !B) \lif (\Box \lnot !A \lif \lnot\Box\lnot !B)$

Read as: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis box not formula A implies not box not formula B close parenthesis

Means: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis box not formula A implies not box not formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025829

Equation form expr-ace37362f4ba506b

$\Log{K}!A_1\dots!A_n \Proves !B$

Read as: modal system K formula A subscript one and so on formula A subscript n derives formula B

Means: modal system K formula A subscript one and so on formula A subscript n derives formula B

2 occurrences in this chapter

• Occurrence projected-formula-0025642
• Occurrence projected-formula-0025646

Equation form expr-ae6f502e1eafd390

$!B_n$

Read as: formula B subscript n

Means: formula B subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025545

Equation form expr-aedc11f05c691d13

$\Box(!A \land !B) \lif \Box!B$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025676

Equation form expr-b09ff6a930a933f1

$(\lnot \Box p \lif \lnot\Box\lnot\lnot p) \lif {}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025714

Equation form expr-b166fed420776931

$\Log{K} \Proves !A_n$

Read as: modal system K derives formula A subscript n

Means: modal system K derives formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025736

Equation form expr-b20e9d692ac74bcc

$\Box !A \lif \Box !B$

Read as: box formula A implies box formula B

Means: box formula A implies box formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025726

Equation form expr-b2766662c1b2b4b3

$\Gamma \cup \{!B\} \Proves[\Sigma] !A$

Read as: Gamma union open set formula B close set derives in system Sigma formula A

Means: Gamma union open set formula B close set derives in system Sigma formula A

1 occurrence in this chapter

• Occurrence projected-formula-0026014

Equation form expr-b2e4530d11f452e0

$\Log{K} \Proves !A \liff !B$

Read as: modal system K derives formula A if and only if formula B

Means: modal system K derives formula A if and only if formula B

2 occurrences in this chapter

• Occurrence projected-formula-0025754
• Occurrence projected-formula-0025758

Equation form expr-b37271a74c8e10eb

$(\Box!A \land \Box!B) \lif \Box(!A \land !B)$

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

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

• Occurrence projected-formula-0025699

Equation form expr-b3fe98e1db720b4d

$!B = \Box!C$

Read as: formula B equals box formula C

Means: formula B equals box formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025943

Equation form expr-b5c1f4a7b21c9554

$\Box(!A \lif (!B \lif (!A \land !B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025687

Equation form expr-b691f35f3ec733f5

$\Log{KT5} \Proves \Box!A \lif \Box\Box!A$

Read as: modal system K T five derives box formula A implies box box formula A

Means: modal system K T five derives box formula A implies box box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025871

Equation form expr-b6bb0344fc788375

$\{ \Diamond p, \Box\Diamond p \lif q, \lnot q \}$

Read as: open set diamond propositional variable p comma box diamond propositional variable p implies propositional variable q comma not propositional variable q close set

Means: open set diamond propositional variable p comma box diamond propositional variable p implies propositional variable q comma not propositional variable q close set

1 occurrence in this chapter

• Occurrence projected-formula-0026035

Equation form expr-b77169ba82bdbcc1

$\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box(!A \land !B)$

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

Means: modal system K 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

• Occurrence projected-formula-0025753

Equation form expr-b86d664e9d04a1d1

$\Log{KT5} \Proves \Diamond\Box!A \lif \Box\Diamond\Box!A$

Read as: modal system K T five derives diamond box formula A implies box diamond box formula A

Means: modal system K T five derives diamond box formula A implies box diamond box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025860

Equation form expr-ba33b91da534d9ab

$!C \lif !B$

Read as: formula C implies formula B

Means: formula C implies formula B

4 occurrences in this chapter

• Occurrence projected-formula-0025628
• Occurrence projected-formula-0025648
• Occurrence projected-formula-0025933
• Occurrence projected-formula-0025935

Equation form expr-ba72b23ae60a855e

$(!A \land !B) \lif !A$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025669

Equation form expr-baacfd9d189243cd

$\Diamond !A$

Read as: diamond formula A

Means: diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025731

Equation form expr-bafca01030687e8f

$\Log{K} \Proves \Box\lnot(!A \lor !B) \lif \Box\lnot!A$

Read as: modal system K derives box not open parenthesis formula A or formula B close parenthesis implies box not formula A

Means: modal system K derives box not open parenthesis formula A or formula B close parenthesis implies box not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025818

Equation form expr-bc8b4a672f6adfd1

$\Log{KTB} \Proves/ \Log{4}$

Read as: modal system K T B does not derive modal system four

Means: modal system K T B does not derive modal system four

1 occurrence in this chapter

• Occurrence projected-formula-0025969

Equation form expr-bc9367794d2761fe

$!A \in \Gamma$

Read as: formula A belongs to Gamma

Means: formula A belongs to Gamma

2 occurrences in this chapter

• Occurrence projected-formula-0026009
• Occurrence projected-formula-0026028

Equation form expr-bf4368e84c5c5200

$\lnot\Diamond\lfalse$

Read as: not diamond falsity

Means: not diamond falsity

1 occurrence in this chapter

• Occurrence projected-formula-0025582

Equation form expr-c0ca760c88f1b93d

$\Box(!A \lif (!B \lif !A))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025665

Equation form expr-c22cf48a730d0251

$\Log{K4} \nsubseteq \Log{KB}$

Read as: modal system K four is not a subset of modal system K B

Means: modal system K four is not a subset of modal system K B

1 occurrence in this chapter

• Occurrence projected-formula-0025960

Equation form expr-c2f654654c2304a2

$\Box(!A \lif (!B \lif !A)) \lif (\Box!A \lif \Box(!B \lif !A))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025666

Equation form expr-c35dad4edbf69089

$\Sigma \Proves !B_1 \lif (!B_2 \lif \cdots (!B_n \lif !A) \cdots)$

Read as: Sigma derives formula B subscript one implies open parenthesis formula B subscript two implies and so on open parenthesis formula B subscript n implies formula A close parenthesis and so on close parenthesis

Means: Sigma derives formula B subscript one implies open parenthesis formula B subscript two implies and so on open parenthesis formula B subscript n implies formula A close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0026003

Equation form expr-c36eaa7131fe1ea6

$\Box!A \lif (\Box !B \lif \Box(!A \land !B)))$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025696

Equation form expr-c418210dcd66e4ac

$\Log{K} \Proves \Box(!A \land !B) \lif (\Box !A \land \Box!B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025668

Equation form expr-c457dbcdd3b49987

$w_4$

Read as: w subscript four

Means: w subscript four

1 occurrence in this chapter

• Occurrence projected-formula-0025990

Equation form expr-c4a0ac6cdda65caa

$\Box\lnot$

Read as: box not

Means: box not

1 occurrence in this chapter

• Occurrence projected-formula-0025791

Equation form expr-c530c268d23c02c8

$\Log{K} \Proves !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\dots)$

Read as: modal system K derives formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis

Means: modal system K derives formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025747

Equation form expr-c75e0b4cdbd40d65

$\mClass{C}_i$

Read as: class C of models subscript i

Means: class C of models subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0025923

Equation form expr-c79bef26205fead8

$\lnot\Diamond$

Read as: not diamond

Means: not diamond

1 occurrence in this chapter

• Occurrence projected-formula-0025792

Equation form expr-c92de1399f3089f9

$!C \in \Log{K}!A_1 \dots !A_n$

Read as: formula C belongs to modal system K formula A subscript one and so on formula A subscript n

Means: formula C belongs to modal system K formula A subscript one and so on formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025634

Equation form expr-c9712394b59a992a

$\Log{KB5} \Proves \Box\Diamond\Box!A \lif \Box\Box !A$

Read as: modal system K B five derives box diamond box formula A implies box box formula A

Means: modal system K B five derives box diamond box formula A implies box box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025896

Equation form expr-c99941201027b5be

$\Gamma \Proves[\Sigma] !A$

Read as: Gamma derives in system Sigma formula A

Means: Gamma derives in system Sigma formula A

6 occurrences in this chapter

• Occurrence projected-formula-0026000
• Occurrence projected-formula-0026006
• Occurrence projected-formula-0026010
• Occurrence projected-formula-0026011
• Occurrence projected-formula-0026027
• Occurrence projected-formula-0026041

Equation form expr-c9dde05108389629

$\Box(!A \land !B) \lif (\Box !A \land \Box!B)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025682

Equation form expr-cc9ce2bc1818217a

$\Log{KT} \Proves \Box !A \lif !A$

Read as: modal system K T derives box formula A implies formula A

Means: modal system K T derives box formula A implies formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025899

Equation form expr-cdc2ed7d3b3d72c2

$\lfalse$

Read as: falsity

Means: falsity

1 occurrence in this chapter

• Occurrence projected-formula-0026029

Equation form expr-cdc98f5ac803e93b

$\Log{KT} \Proves !A \lif \Diamond!A$

Read as: modal system K T derives formula A implies diamond formula A

Means: modal system K T derives formula A implies diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025900

Equation form expr-cefa278d24370919

$\Log{K} \Proves \Box!A \lif (\Box\lnot!B \lif \Box\lnot (!A\lif !B))$

Read as: modal system K derives box formula A implies open parenthesis box not formula B implies box not open parenthesis formula A implies formula B close parenthesis close parenthesis

Means: modal system K derives box formula A implies open parenthesis box not formula B implies box not open parenthesis formula A implies formula B close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025811

Equation form expr-d055ee4dbcdd0c8b

$!B$

Read as: formula B

Means: formula B

33 occurrences in this chapter

• Occurrence projected-formula-0025532
• Occurrence projected-formula-0025533
• Occurrence projected-formula-0025539
• Occurrence projected-formula-0025599
• Occurrence projected-formula-0025600
• Occurrence projected-formula-0025613
• Occurrence projected-formula-0025616
• Occurrence projected-formula-0025623
• Occurrence projected-formula-0025625
• Occurrence projected-formula-0025626
• Occurrence projected-formula-0025641
• Occurrence projected-formula-0025649
• Occurrence projected-formula-0025651
• Occurrence projected-formula-0025652
• Occurrence projected-formula-0025737
• Occurrence projected-formula-0025741
• Occurrence projected-formula-0025746
• Occurrence projected-formula-0025763
• Occurrence projected-formula-0025767
• Occurrence projected-formula-0025784
• Occurrence projected-formula-0025797
• Occurrence projected-formula-0025800
• Occurrence projected-formula-0025913
• Occurrence projected-formula-0025916
• Occurrence projected-formula-0025920
• Occurrence projected-formula-0025922
• Occurrence projected-formula-0025925
• Occurrence projected-formula-0025927
• Occurrence projected-formula-0025929
• Occurrence projected-formula-0025932
• Occurrence projected-formula-0025939
• Occurrence projected-formula-0025941
• Occurrence projected-formula-0025946

Equation form expr-d07113a87d2fa4fa

$\lnot\lnot p$

Read as: not not propositional variable p

Means: not not propositional variable p

3 occurrences in this chapter

• Occurrence projected-formula-0025776
• Occurrence projected-formula-0025778
• Occurrence projected-formula-0025786

Equation form expr-d0a2b90b3d18abd7

$\mModel{M}$

Read as: model M

Means: model M

2 occurrences in this chapter

• Occurrence projected-formula-0025961
• Occurrence projected-formula-0025962

Equation form expr-d252332300cf8bee

$\Gamma \cup \{ !A \}$

Read as: Gamma union open set formula A close set

Means: Gamma union open set formula A close set

2 occurrences in this chapter

• Occurrence projected-formula-0026047
• Occurrence projected-formula-0026051

Equation form expr-d2cb79dbc568c1a6

$\Log{K} \Proves \Subst{!C}{!A}{q}$

Read as: modal system K derives the result of substituting formula A for propositional variable q in formula C

Means: modal system K derives the result of substituting formula A for propositional variable q in formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025755

Equation form expr-d43b451130ac883a

$\Log{KT} \Proves !B$

Read as: modal system K T derives formula B

Means: modal system K T derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025955

Equation form expr-d4c0a0fee0146d61

$\{ \Box(p \lif q), \Box p, \lnot\Box q \}$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0026034

Equation form expr-d54fc95b3832ec0d

$\Log{K} !A_1 \dots !A_n = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B}$

Read as: modal system K formula A subscript one and so on formula A subscript n equals the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B

Means: modal system K formula A subscript one and so on formula A subscript n equals the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025614

Equation form expr-d61252d38c5eba2f

$!B \lif !C$

Read as: formula B implies formula C

Means: formula B implies formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025728

Equation form expr-d65d75b1e6562713

$\Sigma$

Read as: Sigma

Means: Sigma

30 occurrences in this chapter

• Occurrence projected-formula-0025542
• Occurrence projected-formula-0025547
• Occurrence projected-formula-0025556
• Occurrence projected-formula-0025560
• Occurrence projected-formula-0025570
• Occurrence projected-formula-0025581
• Occurrence projected-formula-0025585
• Occurrence projected-formula-0025590
• Occurrence projected-formula-0025612
• Occurrence projected-formula-0025643
• Occurrence projected-formula-0025650
• Occurrence projected-formula-0025653
• Occurrence projected-formula-0025654
• Occurrence projected-formula-0025661
• Occurrence projected-formula-0025662
• Occurrence projected-formula-0025947
• Occurrence projected-formula-0025951
• Occurrence projected-formula-0025994
• Occurrence projected-formula-0025995
• Occurrence projected-formula-0025998
• Occurrence projected-formula-0026004
• Occurrence projected-formula-0026026
• Occurrence projected-formula-0026031
• Occurrence projected-formula-0026032
• Occurrence projected-formula-0026038
• Occurrence projected-formula-0026043
• Occurrence projected-formula-0026045
• Occurrence projected-formula-0026048
• Occurrence projected-formula-0026050
• Occurrence projected-formula-0026053

Equation form expr-da24afe828450851

$\Log{KT4} \Proves/ \Ax{B}$

Read as: modal system K T four does not derive axiom B

Means: modal system K T four does not derive axiom B

1 occurrence in this chapter

• Occurrence projected-formula-0025992

Equation form expr-dac2379a7b03b342

$\Log{K}!A_1\dots!A_n \Proves !C$

Read as: modal system K formula A subscript one and so on formula A subscript n derives formula C

Means: modal system K formula A subscript one and so on formula A subscript n derives formula C

2 occurrences in this chapter

• Occurrence projected-formula-0025644
• Occurrence projected-formula-0025659

Equation form expr-db3432d1486ff645

$!A \lif !B \in \Sigma$

Read as: formula A implies formula B belongs to Sigma

Means: formula A implies formula B belongs to Sigma

1 occurrence in this chapter

• Occurrence projected-formula-0025566

Equation form expr-db52a305090ae209

$\Log{K}\Proves \Box!A \lif (\Diamond(!A \lif !B) \lif \Diamond !B)$

Read as: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis

Means: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025809

Equation form expr-dc7b67a450c5c4ac

$k < i$

Read as: k is less than i

Means: k is less than i

1 occurrence in this chapter

• Occurrence projected-formula-0025551

Equation form expr-dcc90525101f03b4

$\Log{K} \Proves \Diamond(!A \lor !B) \lif (\lnot \Diamond!B \lif \Diamond!A)$

Read as: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis not diamond formula B implies diamond formula A close parenthesis

Means: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis not diamond formula B implies diamond formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025831

Equation form expr-dce1bf6f74513bd5

$\Log{K} \Proves \lnot\Box\lnot !A \lif \lnot\Box\lnot(!A \lor!B)$

Read as: modal system K derives not box not formula A implies not box not open parenthesis formula A or formula B close parenthesis

Means: modal system K derives not box not formula A implies not box not open parenthesis formula A or formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025819

Equation form expr-dd03d8e24cbef5e2

$\Log{K} \Proves !B$

Read as: modal system K derives formula B

Means: modal system K derives formula B

2 occurrences in this chapter

• Occurrence projected-formula-0025740
• Occurrence projected-formula-0025798

Equation form expr-dd1b44f4a83297ba

$!C_i$

Read as: formula C subscript i

Means: formula C subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0025606

Equation form expr-dd85ccf5c34e5656

$\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$

Read as: modal system K T five derives diamond formula A implies box diamond formula A

Means: modal system K T five derives diamond formula A implies box diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025855

Equation form expr-de64372991421159

$!A_n$

Read as: formula A subscript n

Means: formula A subscript n

15 occurrences in this chapter

• Occurrence projected-formula-0025584
• Occurrence projected-formula-0025587
• Occurrence projected-formula-0025589
• Occurrence projected-formula-0025592
• Occurrence projected-formula-0025595
• Occurrence projected-formula-0025610
• Occurrence projected-formula-0025620
• Occurrence projected-formula-0025639
• Occurrence projected-formula-0025739
• Occurrence projected-formula-0025743
• Occurrence projected-formula-0025905
• Occurrence projected-formula-0025907
• Occurrence projected-formula-0025909
• Occurrence projected-formula-0025919
• Occurrence projected-formula-0025931

Equation form expr-de8d2d541234b4f3

$\Box !C$

Read as: box formula C

Means: box formula C

1 occurrence in this chapter

• Occurrence projected-formula-0025660

Equation form expr-dea7a7a12c10f4e9

$\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$

Read as: modal system K derives not box not not propositional variable p implies diamond not propositional variable p

Means: modal system K derives not box not not propositional variable p implies diamond not propositional variable p

2 occurrences in this chapter

• Occurrence projected-formula-0025773
• Occurrence projected-formula-0025779

Equation form expr-dffa227108b65500

$!A_1$

Read as: formula A subscript one

Means: formula A subscript one

15 occurrences in this chapter

• Occurrence projected-formula-0025583
• Occurrence projected-formula-0025586
• Occurrence projected-formula-0025588
• Occurrence projected-formula-0025591
• Occurrence projected-formula-0025594
• Occurrence projected-formula-0025609
• Occurrence projected-formula-0025619
• Occurrence projected-formula-0025638
• Occurrence projected-formula-0025738
• Occurrence projected-formula-0025742
• Occurrence projected-formula-0025904
• Occurrence projected-formula-0025906
• Occurrence projected-formula-0025908
• Occurrence projected-formula-0025918
• Occurrence projected-formula-0025930

Equation form expr-e1380a9ed7fd015c

$\Log{KB5} \Proves \Box!A \lif \Box\Box!A$

Read as: modal system K B five derives box formula A implies box box formula A

Means: modal system K B five derives box formula A implies box box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025897

Equation form expr-e22c886a1252930f

$\mClass{C}_1$

Read as: class C of models subscript one

Means: class C of models subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0025910

Equation form expr-e35bf51cc6365a92

$\Log{K} \Proves \Diamond(!A \lor!B) \lif (\Diamond!A \lor \Diamond!B)$

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

Means: modal system K 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

• Occurrence projected-formula-0025825

Equation form expr-e465c769515a9c81

$\Delta \cup \{!A\} \Proves[\Sigma] !B$

Read as: Delta union open set formula A close set derives in system Sigma formula B

Means: Delta union open set formula A close set derives in system Sigma formula B

1 occurrence in this chapter

• Occurrence projected-formula-0026012

Equation form expr-e4d3411c938d353e

$\Log{K} \Proves \lnot\Box !A \lif \Diamond \lnot !A$

Read as: modal system K derives not box formula A implies diamond not formula A

Means: modal system K derives not box formula A implies diamond not formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025794

Equation form expr-e50e42a2d390fcff

$!C_1$

Read as: C subscript one

Means: C subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0025603

Equation form expr-e73d34b956cd2003

$\Box((!A \land !B) \lif !A)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025670

Equation form expr-e779e6010066a063

$!C(!B)$

Read as: C open parenthesis formula B close parenthesis

Means: C open parenthesis formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025764

Equation form expr-e7f6c011776e8db7

$6$

Read as: six

Means: six

1 occurrence in this chapter

• Occurrence projected-formula-0025700

Equation form expr-e9d180c86baae894

$!B \ident \Box !A$

Read as: formula B is syntactically identical to box formula A

Means: formula B is syntactically identical to box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025541

Equation form expr-eb1cfd0db4a6efc1

$(p \lif q) & \lif ((q \lif r) \lif (p \lif r)) \\ (p \lif (q \lif r)) & \lif ((p \land q) \lif r)$

Read as: Two tautological schemata. First: if p implies q, then if q implies r, then p implies r. Second: if p implies, if q implies r, then if p and q, then r.

Means: Two tautological schemata. First: if p implies q, then if q implies r, then p implies r. Second: if p implies, if q implies r, then if p and q, then r.

1 occurrence in this chapter

• Occurrence projected-formula-0025702

Equation form expr-eb70ca682872db12

$\Diamond!A$

Read as: diamond formula A

Means: diamond formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025884

Equation form expr-ecea92bf5007b042

$!C(!A)$

Read as: formula C open parenthesis formula A close parenthesis

Means: formula C open parenthesis formula A close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025765

Equation form expr-edb7b0e0e2b5ce3c

$(p \lif q) \lif ((p \lif r) \lif (p \lif (q \land r))).$

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

Means: open parenthesis propositional variable p implies propositional variable q close parenthesis implies open parenthesis open parenthesis propositional variable p implies propositional variable r close parenthesis implies open parenthesis propositional variable p implies open parenthesis propositional variable q and propositional variable r close parenthesis close parenthesis close parenthesis period

1 occurrence in this chapter

• Occurrence projected-formula-0025684

Equation form expr-ee8034d960d5569c

$j < i$

Read as: j is less than i

Means: j is less than i

1 occurrence in this chapter

• Occurrence projected-formula-0025553

Equation form expr-f125bec727d9081e

$\Log{KB5} \Proves \Diamond\Box!A \lif \Box !A$

Read as: modal system K B five derives diamond box formula A implies box formula A

Means: modal system K B five derives diamond box formula A implies box formula A

1 occurrence in this chapter

• Occurrence projected-formula-0025894

Equation form expr-f157f71e0163a897

$\Box$

Read as: box

Means: box

3 occurrences in this chapter

• Occurrence projected-formula-0025558
• Occurrence projected-formula-0025761
• Occurrence projected-formula-0025844

Equation form expr-f28479ca0ee4db1f

$\mSat{{}}{\Box p}$

Read as: the displayed model satisfies box propositional variable p at every world

Means: the displayed model satisfies box propositional variable p at every world

2 occurrences in this chapter

• Occurrence projected-formula-0025964
• Occurrence projected-formula-0025976

Equation form expr-f2e77153d6d9c7f0

$\Ax{B_\Diamond}$

Read as: axiom B subscript diamond

Means: axiom B subscript diamond

1 occurrence in this chapter

• Occurrence projected-formula-0025874

Equation form expr-f427cdcccd62d1ab

$\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

• Occurrence projected-formula-0025722

Equation form expr-f53e6ebf8be57b90

$\Log{K} \Proves !A \lif (\lnot!B \lif \lnot (!A \lif !B))$

Read as: modal system K derives formula A implies open parenthesis not formula B implies not open parenthesis formula A implies formula B close parenthesis close parenthesis

Means: modal system K derives formula A implies open parenthesis not formula B implies not open parenthesis formula A implies formula B close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025810

Equation form expr-f545575b944a213f

$\Box(\lnot\lnot p \lif p)$

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

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

1 occurrence in this chapter

• Occurrence projected-formula-0025709

Equation form expr-f5737f6aeb4c1e78

$\Ax{4_\Diamond}$

Read as: axiom four subscript diamond

Means: axiom four subscript diamond

1 occurrence in this chapter

• Occurrence projected-formula-0025887

Equation form expr-f5fcab0ce115697e

$!A_1 \to (!A_2 \lif \cdots (!A_n \lif !B)\cdots)$

Read as: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n implies formula B close parenthesis and so on close parenthesis

Means: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n implies formula B close parenthesis and so on close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0026018

Equation form expr-f65f435afa981240

$\Frm[L]$

Read as: the set of formulas of language L

Means: the set of formulas of language L

1 occurrence in this chapter

• Occurrence projected-formula-0025593

Equation form expr-f6e49c596decc774

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

Read as: modal system K T five derives axiom four

Means: modal system K T five derives axiom four

2 occurrences in this chapter

• Occurrence projected-formula-0025849
• Occurrence projected-formula-0025859

Equation form expr-f7cbeb6021713f1e

$!C(q)$

Read as: formula C open parenthesis propositional variable q close parenthesis

Means: formula C open parenthesis propositional variable q close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025782

Equation form expr-f80eece1214c4a79

$!D_1$

Read as: formula D subscript one

Means: formula D subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0025562

Equation form expr-f87a549f62a7a792

$\Box !A$

Read as: box formula A

Means: box formula A

2 occurrences in this chapter

• Occurrence projected-formula-0025538
• Occurrence projected-formula-0025569

Equation form expr-f95e691abec3021e

$(!A \lif !B) \lif ((!B \lif !C) \lif (!A \lif !C))$

Read as: open parenthesis formula A implies formula B close parenthesis implies open parenthesis open parenthesis formula B implies formula C close parenthesis implies open parenthesis formula A implies formula C close parenthesis close parenthesis

Means: open parenthesis formula A implies formula B close parenthesis implies open parenthesis open parenthesis formula B implies formula C close parenthesis implies open parenthesis formula A implies formula C close parenthesis close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025730

Equation form expr-f96630922dfc449a

$n = 1$

Read as: n equals one

Means: n equals one

1 occurrence in this chapter

• Occurrence projected-formula-0025577

Equation form expr-f9ab85ba8196f530

$\mClass{C}_n$

Read as: class C of models subscript n

Means: class C of models subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025911

Equation form expr-f9e469296b427af3

$\Box p \lif p$

Read as: box propositional variable p implies propositional variable p

Means: box propositional variable p implies propositional variable p

1 occurrence in this chapter

• Occurrence projected-formula-0025957

Equation form expr-fbcd364a88df16e8

$\Log{K}!A_1\dots!A_n$

Read as: modal system K formula A subscript one and so on formula A subscript n

Means: modal system K formula A subscript one and so on formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0025621

Equation form expr-fc43eeb4239b357e

$\Sigma = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B }$

Read as: Sigma equals the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B

Means: Sigma equals the set of formula B such that modal system K formula A subscript one and so on formula A subscript n derives formula B

1 occurrence in this chapter

• Occurrence projected-formula-0025637

Equation form expr-fd091be747da93e5

$\Log{KT4} \Proves/ \Ax{5}$

Read as: modal system K T four does not derive axiom five

Means: modal system K T four does not derive axiom five

1 occurrence in this chapter

• Occurrence projected-formula-0025993

Equation form expr-feae71007c657c2c

$\Box !A \in \Sigma$

Read as: box formula A belongs to Sigma

Means: box formula A belongs to Sigma

1 occurrence in this chapter

• Occurrence projected-formula-0025573

Equation form expr-fef36b264ce11f72

$\Gamma \Proves[\Sigma] !A_n$

Read as: Gamma derives in system Sigma formula A subscript n

Means: Gamma derives in system Sigma formula A subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0026017

Equation form expr-ff0ef5c23edbf7bf

$!B_1$

Read as: B subscript one

Means: B subscript one

2 occurrences in this chapter

• Occurrence projected-formula-0025543
• Occurrence projected-formula-0026001

Equation form expr-ff76b01fde436596

$\Log{K} \Proves (\Box\lnot!B \lif \Box\lnot!A) \lif (\lnot \Box\lnot!A \lif \lnot\Box\lnot!B)$

Read as: modal system K derives open parenthesis box not formula B implies box not formula A close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis

Means: modal system K derives open parenthesis box not formula B implies box not formula A close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis

1 occurrence in this chapter

• Occurrence projected-formula-0025804

Definition of modus ponens

From A and the conditional from A to B, infer B. The following-from clause identifies the second premise with that conditional; the embedded proof tree records the two ordered premises and conclusion.

Source

Modus ponens inference schema

Source premise node one: formula A. Source premise node two: formula A implies formula B. The next inference is labeled modus ponens. From nodes one, then two, infer node three: formula B. The root conclusion is node three. End proof tree.

Source

Definition of necessitation

From A infer necessarily A. The following-from clause says B follows from A by necessitation exactly when B is syntactically identical to necessarily A.

Source

Necessitation inference schema

Source premise node one: formula A. The next inference is labeled necessitation. From node one, infer node two: box formula A. The root conclusion is node two. End proof tree.

Source

Definition of an axiomatic derivation

A derivation from Sigma is a finite sequence ending in A. Every line is a tautological instance, an instance of an axiom in Sigma, a modus-ponens consequence of two earlier lines, or a necessitation consequence of an earlier line.

Source

Definition of a modal logic

A modal logic contains all tautologies and is closed under uniform substitution and modus ponens. The simultaneous-substitution display preserves the indexed replacement order.

Source

Definition of a normal modal logic

A normal modal logic is a modal logic containing the K schema and the duality schema and closed under necessitation.

Source

K and duality schemata

The first line is K: necessarily, if p then q, implies that necessarily p implies necessarily q. The second is duality: possibly p if and only if not necessarily not p.

Source

Normal modal logics are closed under rule R K

The proposition states an n-ary boxed conditional rule. The proof proceeds by induction, using necessitation for n equals one and K plus propositional reasoning in the step.

Source

Rule R K inference schema

Source premise node one: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis. The next inference is labeled rule R K. From node one, infer node two: box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis period. The root conclusion is node two. End proof tree.

Source

Inductive chain proving rule R K

Four displayed stages retain the nested conditional, the induction-hypothesis boxing, the relevant K instance, and the final fully boxed conditional.

Source

Normal modal logics exclude possible falsity

Every normal modal logic contains not possibly falsity.

Source

Exercise on possible falsity

Prove the preceding proposition that every normal modal logic contains not possibly falsity. The exercise is unsolved.

Source

Existence of the smallest generated modal logic

For any finite list of formulas, there is a smallest normal modal logic containing all their substitution instances, obtained by intersecting all such normal modal logics.

Source

Definition of a modal system

The smallest normal modal logic containing the given formulas is denoted K followed by those formulas. K alone denotes the smallest normal modal logic.

Source

Definition of derivability in a modal system

A formula B is derivable in K extended by A one through A n when a finite sequence ends in B and every line is an allowed axiom instance or follows from earlier lines by modus ponens or necessitation.

Source

Modal-system membership equals derivability

The system K extended by A one through A n is exactly the set of formulas derivable in that system. The proof establishes both inclusions and closure under every defining operation.

Source

Boxed weakening theorem

K derives: if necessarily A, then necessarily, if B then A. The following four-line derivation gives the source proof.

Source

Four-line K proof of boxed weakening

Derivation. Line one: formula A implies open parenthesis formula B implies formula A close parenthesis. Justification: tautological instance. Line two: box open parenthesis formula A implies open parenthesis formula B implies formula A close parenthesis close parenthesis. Justification: necessitation. Line three: box open parenthesis formula A implies open parenthesis formula B implies formula A close parenthesis close parenthesis implies open parenthesis box formula A implies box open parenthesis formula B implies formula A close parenthesis close parenthesis. Justification: axiom K. Line four: box formula A implies box open parenthesis formula B implies formula A close parenthesis. Justification: modus ponens. End derivation.

Source

Box distributes to both conjuncts

K derives that necessity of A and B implies both necessarily A and necessarily B. The following eleven-line derivation proves the two projections and combines them propositionally.

Source

Eleven-line K proof distributing box over conjunction

Derivation. Line one: open parenthesis formula A and formula B close parenthesis implies formula A. Justification: tautological instance. Line two: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula A close parenthesis. Justification: necessitation. Line three: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula A close parenthesis implies open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula A close parenthesis. Justification: axiom K. Line four: box open parenthesis formula A and formula B close parenthesis implies box formula A. Justification: modus ponens. Line five: open parenthesis formula A and formula B close parenthesis implies formula B. Justification: tautological instance. Line six: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula B close parenthesis. Justification: necessitation. Line seven: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula B close parenthesis implies open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis. Justification: axiom K. Line eight: box open parenthesis formula A and formula B close parenthesis implies box formula B. Justification: modus ponens. Line nine: open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula A close parenthesis implies open set close set. Justification: tautological instance. Source justification formulas, in order: open parenthesis open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis implies open set close set; then open parenthesis box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis close parenthesis close parenthesis. Line ten: open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis implies open set close set. Justification: modus ponens. Source justification formula, in order: open parenthesis box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis close parenthesis. Line eleven: box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis. Justification: modus ponens. End derivation.

Source

Two necessary conjuncts imply their necessary conjunction

K derives that necessarily A and necessarily B together imply necessarily A and B. The following ten-line derivation uses K twice and propositional composition.

Source

Ten-line K proof combining two boxed conjuncts

Derivation. Line one: formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: box open parenthesis formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: necessitation. Line three: box open parenthesis formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open parenthesis box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: axiom K. Line four: box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: modus ponens. Line five: box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: axiom K. Line six: open parenthesis box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set. Justification: tautological instance. Source justification formulas, in order: open parenthesis box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set; then open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis close parenthesis. Line seven: open parenthesis box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set. Justification: modus ponens. Source justification formula, in order: open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Line eight: box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: modus ponens. Line nine: open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis close parenthesis. Line ten: open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis. Justification: modus ponens. End derivation.

Source

Two propositional tautologies used in the conjunction proof

The first composes two conditionals; the second turns a nested conditional into a conditional from a conjunction.

Source

Box and diamond under negation

For the complete language with both modalities primitive, K derives that not necessarily p implies possibly not p. The source also prints alternative profile branches, but this canonical projection retains the both-primitive proof.

Source

Twelve-line K proof relating box and diamond under negation

Derivation. Line one: diamond not propositional variable p if and only if not box not not propositional variable p. Justification: duality axiom. Line two: open parenthesis diamond not propositional variable p if and only if not box not not propositional variable p close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis. Line three: not box not not propositional variable p implies diamond not propositional variable p. Justification: modus ponens. Line four: not not propositional variable p implies propositional variable p. Justification: tautological instance. Line five: box open parenthesis not not propositional variable p implies propositional variable p close parenthesis. Justification: necessitation. Line six: box open parenthesis not not propositional variable p implies propositional variable p close parenthesis implies open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis. Justification: axiom K. Line seven: open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis. Justification: modus ponens. Line eight: open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies not box not not propositional variable p close parenthesis. Justification: tautological instance. Line nine: not box propositional variable p implies not box not not propositional variable p. Justification: modus ponens. Line ten: open parenthesis not box propositional variable p implies not box not not propositional variable p close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies diamond not propositional variable p close parenthesis close parenthesis. Line eleven: open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies diamond not propositional variable p close parenthesis. Justification: modus ponens. Line twelve: not box propositional variable p implies diamond not propositional variable p. Justification: modus ponens. End derivation.

Source

Contraposition and transitivity tautologies

The first schema is contraposition. The second composes conditionals. They justify the indicated lines of the preceding modal derivation.

Source

Exercises in K

Find K derivations of three listed modal formulas concerning boxed negation, boxed disjunction, and monotonicity of possibility. No derivations are supplied.

Source

Propositional consequence may be used inside K

If K derives A one through A n and B follows propositionally from them, K derives B. The proof uses the corresponding nested tautological conditional and n applications of modus ponens.

Source

Derived n-ary rule R K

A derivable nested conditional remains derivable after boxing every component. The proof is the same induction as the earlier closure proposition.

Source

Short proof of boxed conjunction

The proposition repeats the result that two boxed conjuncts imply their boxed conjunction, now using the derived rules.

Source

Three-line derived proof combining boxed conjuncts

Derivation. Line one: modal system K derives formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis. Justification: propositional logic. End derivation.

Source

Rewriting proposition

Provable equivalence permits replacement of A by B inside a formula context C. The printed conclusion writes B without the source formula marker used elsewhere; that notation is preserved and disclosed.

Source

Exercise proving the rewriting proposition

Prove rewriting by structural induction on C, first establishing equivalence of the two substitution instances. The proof remains unsupplied.

Source

Three-line rewriting-rule abbreviation

Derivation. Unnumbered source line one: derives formula C open parenthesis formula A close parenthesis. Justification: no separate justification is printed. Unnumbered source line two: derives formula A if and only if formula B. Justification: no separate justification is printed. Unnumbered source line three: derives formula C open parenthesis formula B close parenthesis. Justification: the cited rewriting proposition. Source reference: the rewriting proposition. End derivation.

Source

Not-box implies possible negation

K derives that not necessarily p implies possibly not p. The canonical branch uses duality and a final replacement of double negation by p.

Source

Three-line proof of not-box implying possible negation

Derivation. Line one: modal system K derives diamond not propositional variable p if and only if not box not not propositional variable p. Justification: duality axiom. Line two: modal system K derives not box not not propositional variable p implies diamond not propositional variable p. Justification: propositional logic. Line three: modal system K derives not box propositional variable p implies diamond not propositional variable p. Justification: the source-listed replacement. Source justification formulas, in order: propositional variable p; then not not propositional variable p. End derivation.

Source

Expanded final rewriting step

Derivation. Unnumbered source line one: modal system K derives not box not not propositional variable p implies diamond not propositional variable p. Justification: no separate justification is printed. Unnumbered source line two: modal system K derives not not propositional variable p if and only if propositional variable p. Justification: tautological instance. Unnumbered source line three: modal system K derives not box propositional variable p implies diamond not propositional variable p. Justification: the cited rewriting proposition. Source reference: the rewriting proposition. End derivation.

Source

Uniform substitution preserves derivability

Every substitution instance of a K theorem is again a K theorem. The proof checks axiom instances and both inference rules by induction on derivation length.

Source

Boxed implication preserves possibility

K derives that necessity of A implies B entails that possibility of A implies possibility of B.

Source

Five-line proof that box preserves diamond implication

Derivation. Line one: modal system K derives open parenthesis formula A implies formula B close parenthesis implies open parenthesis not formula B implies not formula A close parenthesis. Justification: propositional logic. Line two: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis box not formula B implies box not formula A close parenthesis. Justification: rule R K. Line three: modal system K derives open parenthesis box not formula B implies box not formula A close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis. Justification: tautological instance. Line four: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis. Justification: propositional logic. Line five: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. End derivation.

Source

A boxed antecedent and possible conditional yield a possible consequent

K derives: if necessarily A, then if A implies B is possible, B is possible.

Source

Four-line mixed box-and-diamond implication proof

Derivation. Line one: modal system K derives formula A implies open parenthesis not formula B implies not open parenthesis formula A implies formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box formula A implies open parenthesis box not formula B implies box not open parenthesis formula A implies formula B close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives box formula A implies open parenthesis not box not open parenthesis formula A implies formula B close parenthesis implies not box not formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. End derivation.

Source

Either possible disjunct makes the disjunction possible

K derives that possibly A or possibly B implies possibly A or B.

Source

Six-line proof that possibility is monotone over disjunction

Derivation. Line one: modal system K derives not open parenthesis formula A or formula B close parenthesis implies not formula A. Justification: tautological instance. Line two: modal system K derives box not open parenthesis formula A or formula B close parenthesis implies box not formula A. Justification: rule R K. Line three: modal system K derives not box not formula A implies not box not open parenthesis formula A or formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives diamond formula A implies diamond open parenthesis formula A or formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. Line five: modal system K derives diamond formula B implies diamond open parenthesis formula A or formula B close parenthesis. Justification: the analogous preceding argument. Line six: modal system K derives open parenthesis diamond formula A or diamond formula B close parenthesis implies diamond open parenthesis formula A or formula B close parenthesis. Justification: propositional logic. End derivation.

Source

Possibility distributes over disjunction

K derives that possibility of A or B implies possibly A or possibly B. The source proof ends in the reversed disjunct order, which is propositionally equivalent to the stated result.

Source

Seven-line proof that possibility distributes over disjunction

Derivation. Line one: modal system K derives not formula A implies open parenthesis not formula B implies not open parenthesis formula A or formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box not formula A implies open parenthesis box not formula B implies box not open parenthesis formula A or formula B close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives box not formula A implies open parenthesis not box not open parenthesis formula A or formula B close parenthesis implies not box not formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis box not formula A implies not box not formula B close parenthesis. Justification: propositional logic. Line five: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis not not box not formula B implies not box not formula A close parenthesis. Justification: propositional logic. Line six: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis not diamond formula B implies diamond formula A close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. Line seven: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula B or diamond formula A close parenthesis. Justification: propositional logic. End derivation.

Source

Exercises on derived K proofs

Show three listed claims about possibility of truth, a boxed disjunction, and converting a possible-to-necessary premise into a boxed implication. The exercises remain unsolved.

Source

Definition of the dual modal schemata

The display gives T diamond, B diamond, four diamond, and five diamond in that order, then explains how contraposition and dual replacement obtain them from their box counterparts.

Source

Four dual schemata

T diamond is p implies possibly p. B diamond is possibly necessarily p implies p. Four diamond contracts two possibilities to one. Five diamond takes possibly necessarily p to necessarily p.

Source

A modal schema and its dual generate the same system

For each listed schema A, K extended by A equals K extended by its diamond dual.

Source

Exercise on dual modal systems

Prove that adjoining each modal schema or its dual produces the same modal system. No proof is supplied.

Source

Six derivability facts among modal systems

The proposition lists derivations of B and four in K T five, T in K D B four, five in K B four, four in K B five, and D in K T.

Source

Three-line K T five proof of axiom B

Derivation. Line one: modal system K T five derives diamond formula A implies box diamond formula A. Justification: axiom five. Line two: modal system K T five derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T five derives formula A implies box diamond formula A. Justification: propositional logic. End derivation.

Source

Six-line K T five proof of axiom four

Derivation. Line one: modal system K T five derives diamond box formula A implies box diamond box formula A. Justification: axiom five; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K T five derives box formula A implies diamond box formula A. Justification: axiom T subscript diamond; the source-listed replacement. Source justification formulas, in order: axiom T subscript diamond; then box formula A; then propositional variable p. Line three: modal system K T five derives box formula A implies box diamond box formula A. Justification: propositional logic. Line four: modal system K T five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line five: modal system K T five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line six: modal system K T five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

Source

Five-line K D B four proof of axiom T

Derivation. Line one: modal system K D B four derives diamond box formula A implies formula A. Justification: axiom B subscript diamond. Source justification formula, in order: axiom B subscript diamond. Line two: modal system K D B four derives box box formula A implies diamond box formula A. Justification: axiom D; the source-listed replacement. Source justification formulas, in order: axiom D; then box formula A; then propositional variable p. Line three: modal system K D B four derives box box formula A implies formula A. Justification: propositional logic. Line four: modal system K D B four derives box formula A implies box box formula A. Justification: axiom four. Line five: modal system K D B four derives box formula A implies formula A. Justification: propositional logic. End derivation.

Source

Four-line K B four proof of axiom five

Derivation. Line one: modal system K B four derives diamond formula A implies box diamond diamond formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: diamond formula A; then propositional variable p. Line two: modal system K B four derives diamond diamond formula A implies diamond formula A. Justification: axiom four subscript diamond. Source justification formula, in order: axiom four subscript diamond. Line three: modal system K B four derives box diamond diamond formula A implies box diamond formula A. Justification: rule R K. Line four: modal system K B four derives diamond formula A implies box diamond formula A. Justification: propositional logic. End derivation.

Source

Four-line K B five proof of axiom four

Derivation. Line one: modal system K B five derives box formula A implies box diamond box formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K B five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line three: modal system K B five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line four: modal system K B five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

Source

Three-line K T proof of axiom D

Derivation. Line one: modal system K T derives box formula A implies formula A. Justification: axiom T. Line two: modal system K T derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T derives box formula A implies diamond formula A. Justification: propositional logic. End derivation.

Source

Definitions of S four and S five

S four is defined as K T four, and S five as K T B four.

Source

Equivalent axiomatizations of S five

The systems K T B four, K T five, K D B four, and K D B five are equal.

Source

Exercise proving the S-five equivalences

Prove the preceding equality of four axiomatizations of S five. The proof remains the source word Exercise.

Source

Soundness theorem for modal systems

If each added axiom family is valid in its corresponding class of models, every theorem of the combined modal system is valid in the intersection of those classes. The proof is by induction on proof length.

Source

K D is a proper subsystem of K T

The inclusion follows because K T derives D. Properness follows from a serial countermodel to T and soundness. The source writes modal system D where the cited result is axiom D; that notation is preserved and disclosed.

Source

K B differs from K four

A two-world symmetric model falsifies axiom four, showing K four is not a subset of K B.

Source

Figure: symmetric countermodel to axiom four

The figure contains the complete two-world directed graph and its printed valuation and modal-truth annotations. The nested graph structure supplies every node and arrow.

Source

Two-world symmetric countermodel to axiom four

Model graph. World w subscript one has valuation propositional variable p is printed false at this world. Its printed claims are the displayed model satisfies box propositional variable p at every world and the displayed model does not satisfy box box propositional variable p at every world. World w subscript two has valuation propositional variable p is printed true at this world. Its printed claim is the displayed model does not satisfy box propositional variable p at every world. There is one directed arrow from w one to w two and one from w two to w one; no loops or other arrows are printed. End model graph.

Source

K T B derives neither four nor five

A single reflexive symmetric model contains failures of an instance of axiom four and an instance of axiom five. The theorem prints modal-system symbols four and five in the non-derivability displays; that source notation is retained.

Source

Figure: reflexive symmetric countermodel to four and five

The figure contains three worlds, a reflexive loop at each, four cross-world arrows, valuations, and all printed modal claims.

Source

Three-world reflexive symmetric countermodel to axioms four and five

Model graph. World w subscript one has valuation propositional variable p is printed true at this world. Its printed claims, in order, are the displayed model satisfies box propositional variable p at every world, the displayed model does not satisfy box box propositional variable p at every world, and the displayed model does not satisfy diamond not propositional variable p at every world. World w subscript two has valuation propositional variable p is printed true at this world. Its claims are the displayed model satisfies diamond not propositional variable p at every world and the displayed model does not satisfy box diamond not propositional variable p at every world. World w subscript three has valuation propositional variable p is printed false at this world. Each world has a reflexive loop. The remaining arrows are w one to w two, w two to w three, w three to w two, and w two to w one. End model graph.

Source

K D five differs from S four

A serial Euclidean four-world model falsifies axiom four, so K D five is not K T four, which is S four.

Source

Figure: serial Euclidean countermodel to axiom four

The figure contains four worlds, three reflexive loops, eight directed cross-world arrows, valuations, and the printed box and double-box claims at w one.

Source

Four-world serial Euclidean countermodel to axiom four

Model graph. World w subscript two has valuation propositional variable p is printed true at this world. World w subscript one has valuation propositional variable p is printed false at this world and carries the two printed claims the displayed model satisfies box propositional variable p at every world comma the displayed model does not satisfy box box propositional variable p at every world. World w subscript three has valuation propositional variable p is printed true at this world. World w subscript four has valuation propositional variable p is printed false at this world. Worlds w two, w three, and w four each have a reflexive loop and arrows in both directions between every distinct pair among them. World w one has arrows to w two and w three only. No other arrows are printed. End model graph.

Source

Exercise seeking a three-world countermodel

Give an alternative proof that K D five differs from S four using a model with three worlds. No model is supplied.

Source

Exercise seeking one S-four countermodel to B and five

Provide one reflexive transitive model showing that K T four derives neither axiom B nor axiom five. No model is supplied.

Source

Definition of derivability from a set

Gamma derives A in modal system Sigma exactly when finitely many formulas B one through B n from Gamma form a nested conditional to A that Sigma derives.

Source

Five properties of derivability from a set

The proposition states monotonicity, reflexivity, cut, the deduction theorem, and propositional rule T for derivability relative to a modal system.

Source

Definition of deductive closure

Gamma is deductively closed relative to Sigma when every formula derivable from Gamma in Sigma already belongs to Gamma.

Source

Definition of relative consistency

Gamma is Sigma-consistent exactly when falsity is not derivable from Gamma in Sigma.

Source

Three consistency facts

Consistency is equivalent to failure to derive some formula; derivability of A is equivalent to inconsistency after adjoining not A; and every consistent set has at least one consistent extension by A or not A.

Source

Cross-reference reference-000973

the proposition that no normal modal logic permits possibly falsity

Source occurrence

Cross-reference reference-000974

the table of valid and invalid modal schemata

Source occurrence

Cross-reference reference-000975

the proposition that every normal modal logic is closed under rule R K

Source occurrence

Cross-reference reference-000976

the rewriting proposition

Source occurrence

Cross-reference reference-000977

the rewriting proposition

Source occurrence

Cross-reference reference-000978

the rewriting proposition

Source occurrence

Cross-reference reference-000979

the rewriting proposition

Source occurrence

Cross-reference reference-000980

the rewriting proposition

Source occurrence

Cross-reference reference-000981

the rewriting proposition

Source occurrence

Cross-reference reference-000982

the section on derived rules

Source occurrence

Cross-reference reference-000983

the definition of the dual modal schemata

Source occurrence

Cross-reference reference-000984

the proposition that adjoining a schema or its dual gives the same modal system

Source occurrence

Cross-reference reference-000985

the proposition characterizing equivalence relations

Source occurrence

Cross-reference reference-000986

the proposition giving equivalent axiomatizations of S five

Source occurrence

Cross-reference reference-000987

the proposition that tautological instances are valid

Source occurrence

Cross-reference reference-000988

the proposition that axiom K is valid

Source occurrence

Cross-reference reference-000989

the proposition that the duality schema is valid

Source occurrence

Cross-reference reference-000990

the proposition preserving validity under subclasses of models

Source occurrence

Cross-reference reference-000991

the soundness of modus ponens

Source occurrence

Cross-reference reference-000992

the validity-preservation rule for necessitation

Source occurrence

Cross-reference reference-000993

the section on proofs in modal systems

Source occurrence

Cross-reference reference-000994

the soundness theorem for modal systems

Source occurrence

Cross-reference reference-000995

the proposition listing modal-system derivability facts

Source occurrence

Cross-reference reference-000996

the item stating that K T derives axiom D

Source occurrence

Cross-reference reference-000997

the soundness theorem for modal systems

Source occurrence

Cross-reference reference-000998

the symmetric countermodel to axiom four

Source occurrence

Cross-reference reference-000999

the proposition that axiom K is valid

Source occurrence

Cross-reference reference-001000

the theorem connecting modal schemata with accessibility conditions

Source occurrence

Cross-reference reference-001001

the theorem connecting modal schemata with accessibility conditions

Source occurrence

Cross-reference reference-001002

the reflexive symmetric countermodel to axioms four and five

Source occurrence

Cross-reference reference-001003

the theorem that K T B derives neither axiom four nor axiom five

Source occurrence

Cross-reference reference-001004

the theorem connecting modal schemata with accessibility conditions

Source occurrence

Cross-reference reference-001005

the serial Euclidean countermodel to axiom four

Source occurrence

Cross-reference reference-001006

the theorem distinguishing K D five from S four

Source occurrence

Cross-reference reference-001007

the theorem distinguishing K D five from S four

Source occurrence

Cross-reference reference-001008

the section on proofs in modal systems

Source occurrence

Cross-reference reference-001009

the rule-T item among the derivability properties

Source occurrence

Cross-reference reference-001010

the proposition listing derivability properties

Source occurrence

Cross-reference reference-001011

the consistency-extension item

Source occurrence

Cross-reference reference-001012

the consistency characterization by adjoining a negation

Source occurrence

Cross-reference reference-001013

the proposition listing derivability properties

Source occurrence

Cross-reference reference-001014

the rule-T item among the derivability properties

Source occurrence

Source disclosures

• TR052-SAR-001: Source notation note. The conclusion's replacement argument is printed as capital B without the formula marker that accompanies B in the premise. It is read as formula B, and the exact source remains preserved. source
• TR052-SAR-002: Source notation note. This sentence prints modal system D as the object derived by K T, while the cited earlier item states derivability of axiom D. The printed notation is retained and identified. source
• TR052-SAR-003: Source notation note. The theorem prints modal-system symbols four and five after non-derivability, while its proof discusses axiom four and axiom five. Both printed displays are preserved and spoken literally as source notation. source

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

$\MP$

Read as: modus ponens

Read in context source

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

$\Nec$

Read as: necessitation

Read in context source

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

$\RK$

Read as: rule R K

Read in context source

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

$\mFalse{p}$

Read as: propositional variable p is printed false at this world

Read in context source

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

$\mTrue{p}$

Read as: propositional variable p is printed true at this world

Read in context source

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

$\mTrue{p}$

Read as: propositional variable p is printed true at this world

Read in context source

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

$\mTrue{p}$

Read as: propositional variable p is printed true at this world

Read in context source

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

$\mFalse{p}$

Read as: propositional variable p is printed false at this world

Read in context source

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

$\mTrue{p}$

Read as: propositional variable p is printed true at this world

Read in context source

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

$\mFalse{p}$

Read as: propositional variable p is printed false at this world

Read in context source

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

$\mTrue{p}$

Read as: propositional variable p is printed true at this world

Read in context source

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

$\mFalse{p}$

Read as: propositional variable p is printed false at this world

Read in context source

Ordered structures

Modus ponens inference schema

Structure: proof tree.

Source premise node one: formula A. Source premise node two: formula A implies formula B. The next inference is labeled modus ponens. From nodes one, then two, infer node three: formula B. The root conclusion is node three. End proof tree.

Read the source-bound structure in context

Necessitation inference schema

Structure: proof tree.

Source premise node one: formula A. The next inference is labeled necessitation. From node one, infer node two: box formula A. The root conclusion is node two. End proof tree.

Read the source-bound structure in context

Rule R K inference schema

Structure: proof tree.

Source premise node one: formula A subscript one implies open parenthesis formula A subscript two implies and so on open parenthesis formula A subscript n - one implies formula A subscript n close parenthesis and so on close parenthesis. The next inference is labeled rule R K. From node one, infer node two: box formula A subscript one implies open parenthesis box formula A subscript two implies and so on open parenthesis box formula A subscript n - one implies box formula A subscript n close parenthesis and so on close parenthesis period. The root conclusion is node two. End proof tree.

Read the source-bound structure in context

Four-line K proof of boxed weakening

Structure: derivation.

Derivation. Line one: formula A implies open parenthesis formula B implies formula A close parenthesis. Justification: tautological instance. Line two: box open parenthesis formula A implies open parenthesis formula B implies formula A close parenthesis close parenthesis. Justification: necessitation. Line three: box open parenthesis formula A implies open parenthesis formula B implies formula A close parenthesis close parenthesis implies open parenthesis box formula A implies box open parenthesis formula B implies formula A close parenthesis close parenthesis. Justification: axiom K. Line four: box formula A implies box open parenthesis formula B implies formula A close parenthesis. Justification: modus ponens. End derivation.

Read the source-bound structure in context

Eleven-line K proof distributing box over conjunction

Structure: derivation.

Derivation. Line one: open parenthesis formula A and formula B close parenthesis implies formula A. Justification: tautological instance. Line two: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula A close parenthesis. Justification: necessitation. Line three: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula A close parenthesis implies open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula A close parenthesis. Justification: axiom K. Line four: box open parenthesis formula A and formula B close parenthesis implies box formula A. Justification: modus ponens. Line five: open parenthesis formula A and formula B close parenthesis implies formula B. Justification: tautological instance. Line six: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula B close parenthesis. Justification: necessitation. Line seven: box open parenthesis open parenthesis formula A and formula B close parenthesis implies formula B close parenthesis implies open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis. Justification: axiom K. Line eight: box open parenthesis formula A and formula B close parenthesis implies box formula B. Justification: modus ponens. Line nine: open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula A close parenthesis implies open set close set. Justification: tautological instance. Source justification formulas, in order: open parenthesis open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis implies open set close set; then open parenthesis box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis close parenthesis close parenthesis. Line ten: open parenthesis box open parenthesis formula A and formula B close parenthesis implies box formula B close parenthesis implies open set close set. Justification: modus ponens. Source justification formula, in order: open parenthesis box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis close parenthesis. Line eleven: box open parenthesis formula A and formula B close parenthesis implies open parenthesis box formula A and box formula B close parenthesis. Justification: modus ponens. End derivation.

Read the source-bound structure in context

Ten-line K proof combining two boxed conjuncts

Structure: derivation.

Derivation. Line one: formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: box open parenthesis formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: necessitation. Line three: box open parenthesis formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open parenthesis box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: axiom K. Line four: box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: modus ponens. Line five: box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: axiom K. Line six: open parenthesis box formula A implies box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set. Justification: tautological instance. Source justification formulas, in order: open parenthesis box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set; then open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis close parenthesis. Line seven: open parenthesis box open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis implies open set close set. Justification: modus ponens. Source justification formula, in order: open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Line eight: box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: modus ponens. Line nine: open parenthesis box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis close parenthesis. Line ten: open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis. Justification: modus ponens. End derivation.

Read the source-bound structure in context

Twelve-line K proof relating box and diamond under negation

Structure: derivation.

Derivation. Line one: diamond not propositional variable p if and only if not box not not propositional variable p. Justification: duality axiom. Line two: open parenthesis diamond not propositional variable p if and only if not box not not propositional variable p close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis. Line three: not box not not propositional variable p implies diamond not propositional variable p. Justification: modus ponens. Line four: not not propositional variable p implies propositional variable p. Justification: tautological instance. Line five: box open parenthesis not not propositional variable p implies propositional variable p close parenthesis. Justification: necessitation. Line six: box open parenthesis not not propositional variable p implies propositional variable p close parenthesis implies open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis. Justification: axiom K. Line seven: open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis. Justification: modus ponens. Line eight: open parenthesis box not not propositional variable p implies box propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies not box not not propositional variable p close parenthesis. Justification: tautological instance. Line nine: not box propositional variable p implies not box not not propositional variable p. Justification: modus ponens. Line ten: open parenthesis not box propositional variable p implies not box not not propositional variable p close parenthesis implies open set close set. Justification: tautological instance. Source justification formula, in order: open parenthesis open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies diamond not propositional variable p close parenthesis close parenthesis. Line eleven: open parenthesis not box not not propositional variable p implies diamond not propositional variable p close parenthesis implies open parenthesis not box propositional variable p implies diamond not propositional variable p close parenthesis. Justification: modus ponens. Line twelve: not box propositional variable p implies diamond not propositional variable p. Justification: modus ponens. End derivation.

Read the source-bound structure in context

Three-line derived proof combining boxed conjuncts

Structure: derivation.

Derivation. Line one: modal system K derives formula A implies open parenthesis formula B implies open parenthesis formula A and formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box formula A implies open parenthesis box formula B implies box open parenthesis formula A and formula B close parenthesis close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives open parenthesis box formula A and box formula B close parenthesis implies box open parenthesis formula A and formula B close parenthesis. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Three-line rewriting-rule abbreviation

Structure: derivation.

Derivation. Unnumbered source line one: derives formula C open parenthesis formula A close parenthesis. Justification: no separate justification is printed. Unnumbered source line two: derives formula A if and only if formula B. Justification: no separate justification is printed. Unnumbered source line three: derives formula C open parenthesis formula B close parenthesis. Justification: the cited rewriting proposition. Source reference: the rewriting proposition. End derivation.

Read the source-bound structure in context

Three-line proof of not-box implying possible negation

Structure: derivation.

Derivation. Line one: modal system K derives diamond not propositional variable p if and only if not box not not propositional variable p. Justification: duality axiom. Line two: modal system K derives not box not not propositional variable p implies diamond not propositional variable p. Justification: propositional logic. Line three: modal system K derives not box propositional variable p implies diamond not propositional variable p. Justification: the source-listed replacement. Source justification formulas, in order: propositional variable p; then not not propositional variable p. End derivation.

Read the source-bound structure in context

Expanded final rewriting step

Structure: derivation.

Derivation. Unnumbered source line one: modal system K derives not box not not propositional variable p implies diamond not propositional variable p. Justification: no separate justification is printed. Unnumbered source line two: modal system K derives not not propositional variable p if and only if propositional variable p. Justification: tautological instance. Unnumbered source line three: modal system K derives not box propositional variable p implies diamond not propositional variable p. Justification: the cited rewriting proposition. Source reference: the rewriting proposition. End derivation.

Read the source-bound structure in context

Five-line proof that box preserves diamond implication

Structure: derivation.

Derivation. Line one: modal system K derives open parenthesis formula A implies formula B close parenthesis implies open parenthesis not formula B implies not formula A close parenthesis. Justification: propositional logic. Line two: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis box not formula B implies box not formula A close parenthesis. Justification: rule R K. Line three: modal system K derives open parenthesis box not formula B implies box not formula A close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis. Justification: tautological instance. Line four: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis not box not formula A implies not box not formula B close parenthesis. Justification: propositional logic. Line five: modal system K derives box open parenthesis formula A implies formula B close parenthesis implies open parenthesis diamond formula A implies diamond formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. End derivation.

Read the source-bound structure in context

Four-line mixed box-and-diamond implication proof

Structure: derivation.

Derivation. Line one: modal system K derives formula A implies open parenthesis not formula B implies not open parenthesis formula A implies formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box formula A implies open parenthesis box not formula B implies box not open parenthesis formula A implies formula B close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives box formula A implies open parenthesis not box not open parenthesis formula A implies formula B close parenthesis implies not box not formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives box formula A implies open parenthesis diamond open parenthesis formula A implies formula B close parenthesis implies diamond formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. End derivation.

Read the source-bound structure in context

Six-line proof that possibility is monotone over disjunction

Structure: derivation.

Derivation. Line one: modal system K derives not open parenthesis formula A or formula B close parenthesis implies not formula A. Justification: tautological instance. Line two: modal system K derives box not open parenthesis formula A or formula B close parenthesis implies box not formula A. Justification: rule R K. Line three: modal system K derives not box not formula A implies not box not open parenthesis formula A or formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives diamond formula A implies diamond open parenthesis formula A or formula B close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. Line five: modal system K derives diamond formula B implies diamond open parenthesis formula A or formula B close parenthesis. Justification: the analogous preceding argument. Line six: modal system K derives open parenthesis diamond formula A or diamond formula B close parenthesis implies diamond open parenthesis formula A or formula B close parenthesis. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Seven-line proof that possibility distributes over disjunction

Structure: derivation.

Derivation. Line one: modal system K derives not formula A implies open parenthesis not formula B implies not open parenthesis formula A or formula B close parenthesis close parenthesis. Justification: tautological instance. Line two: modal system K derives box not formula A implies open parenthesis box not formula B implies box not open parenthesis formula A or formula B close parenthesis close parenthesis. Justification: rule R K. Line three: modal system K derives box not formula A implies open parenthesis not box not open parenthesis formula A or formula B close parenthesis implies not box not formula B close parenthesis. Justification: propositional logic. Line four: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis box not formula A implies not box not formula B close parenthesis. Justification: propositional logic. Line five: modal system K derives not box not open parenthesis formula A or formula B close parenthesis implies open parenthesis not not box not formula B implies not box not formula A close parenthesis. Justification: propositional logic. Line six: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis not diamond formula B implies diamond formula A close parenthesis. Justification: the source-listed replacement. Source justification formulas, in order: diamond; then not box not. Line seven: modal system K derives diamond open parenthesis formula A or formula B close parenthesis implies open parenthesis diamond formula B or diamond formula A close parenthesis. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Three-line K T five proof of axiom B

Structure: derivation.

Derivation. Line one: modal system K T five derives diamond formula A implies box diamond formula A. Justification: axiom five. Line two: modal system K T five derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T five derives formula A implies box diamond formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Six-line K T five proof of axiom four

Structure: derivation.

Derivation. Line one: modal system K T five derives diamond box formula A implies box diamond box formula A. Justification: axiom five; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K T five derives box formula A implies diamond box formula A. Justification: axiom T subscript diamond; the source-listed replacement. Source justification formulas, in order: axiom T subscript diamond; then box formula A; then propositional variable p. Line three: modal system K T five derives box formula A implies box diamond box formula A. Justification: propositional logic. Line four: modal system K T five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line five: modal system K T five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line six: modal system K T five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Five-line K D B four proof of axiom T

Structure: derivation.

Derivation. Line one: modal system K D B four derives diamond box formula A implies formula A. Justification: axiom B subscript diamond. Source justification formula, in order: axiom B subscript diamond. Line two: modal system K D B four derives box box formula A implies diamond box formula A. Justification: axiom D; the source-listed replacement. Source justification formulas, in order: axiom D; then box formula A; then propositional variable p. Line three: modal system K D B four derives box box formula A implies formula A. Justification: propositional logic. Line four: modal system K D B four derives box formula A implies box box formula A. Justification: axiom four. Line five: modal system K D B four derives box formula A implies formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Four-line K B four proof of axiom five

Structure: derivation.

Derivation. Line one: modal system K B four derives diamond formula A implies box diamond diamond formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: diamond formula A; then propositional variable p. Line two: modal system K B four derives diamond diamond formula A implies diamond formula A. Justification: axiom four subscript diamond. Source justification formula, in order: axiom four subscript diamond. Line three: modal system K B four derives box diamond diamond formula A implies box diamond formula A. Justification: rule R K. Line four: modal system K B four derives diamond formula A implies box diamond formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Four-line K B five proof of axiom four

Structure: derivation.

Derivation. Line one: modal system K B five derives box formula A implies box diamond box formula A. Justification: axiom B; the source-listed replacement. Source justification formulas, in order: box formula A; then propositional variable p. Line two: modal system K B five derives diamond box formula A implies box formula A. Justification: axiom five subscript diamond. Source justification formula, in order: axiom five subscript diamond. Line three: modal system K B five derives box diamond box formula A implies box box formula A. Justification: rule R K. Line four: modal system K B five derives box formula A implies box box formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Three-line K T proof of axiom D

Structure: derivation.

Derivation. Line one: modal system K T derives box formula A implies formula A. Justification: axiom T. Line two: modal system K T derives formula A implies diamond formula A. Justification: axiom T subscript diamond. Source justification formula, in order: axiom T subscript diamond. Line three: modal system K T derives box formula A implies diamond formula A. Justification: propositional logic. End derivation.

Read the source-bound structure in context

Two-world symmetric countermodel to axiom four

Structure: diagram tikz.

Model graph. World w subscript one has valuation propositional variable p is printed false at this world. Its printed claims are the displayed model satisfies box propositional variable p at every world and the displayed model does not satisfy box box propositional variable p at every world. World w subscript two has valuation propositional variable p is printed true at this world. Its printed claim is the displayed model does not satisfy box propositional variable p at every world. There is one directed arrow from w one to w two and one from w two to w one; no loops or other arrows are printed. End model graph.

Read the source-bound structure in context

Three-world reflexive symmetric countermodel to axioms four and five

Structure: diagram tikz.

Model graph. World w subscript one has valuation propositional variable p is printed true at this world. Its printed claims, in order, are the displayed model satisfies box propositional variable p at every world, the displayed model does not satisfy box box propositional variable p at every world, and the displayed model does not satisfy diamond not propositional variable p at every world. World w subscript two has valuation propositional variable p is printed true at this world. Its claims are the displayed model satisfies diamond not propositional variable p at every world and the displayed model does not satisfy box diamond not propositional variable p at every world. World w subscript three has valuation propositional variable p is printed false at this world. Each world has a reflexive loop. The remaining arrows are w one to w two, w two to w three, w three to w two, and w two to w one. End model graph.

Read the source-bound structure in context

Four-world serial Euclidean countermodel to axiom four

Structure: diagram tikz.

Model graph. World w subscript two has valuation propositional variable p is printed true at this world. World w subscript one has valuation propositional variable p is printed false at this world and carries the two printed claims the displayed model satisfies box propositional variable p at every world comma the displayed model does not satisfy box box propositional variable p at every world. World w subscript three has valuation propositional variable p is printed true at this world. World w subscript four has valuation propositional variable p is printed false at this world. Worlds w two, w three, and w four each have a reflexive loop and arrows in both directions between every distinct pair among them. World w one has arrows to w two and w three only. No other arrows are printed. End model graph.

Read the source-bound structure in context