Cut-free tableau calculi for some propositional normal modal logics

✍ Scribed by Martin Amerbauer

• Publisher: Springer Netherlands
• Year: 1996
• Tongue: English
• Weight: 700 KB
• Volume: 57
• Category: Article
• ISSN: 0039-3215
• DOI: 10.1007/bf00370840

✦ Synopsis

We give sound and complete tableau and sequent calculi for the propositional normal modal logics $4.04, K4B and G O (these logics axe the smallest normal modal logics containing K and the schemata [:]A -+ ODA, DA --+ A and D<)DA --+ (A --+ DA) ; DA -+ D[]A and A -+ D<>A ; DA --+ D[qA and D(D(A --+ DA) -+ A) -+ DA resp.) with the following properties: the calculi for S4.04 and G O are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, the so-called analytical cut-rule.

In addition we show that G 0 is not compact (and therefore not canonical), and we proof with the tableau-method that G O is chaxacterised by the class of all finite, (transitive) trees of degenerate or simple clusters of worlds; therefore G O is decidable and also chaxacterised by the class of all frames for G 0.