All finitely axiomatizable subframe logics containing the provability logic CSM\(_0\) are decidable (Q1128179)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: All finitely axiomatizable subframe logics containing the provability logic CSM\(_0\) are decidable |
scientific article; zbMATH DE number 1187520
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | All finitely axiomatizable subframe logics containing the provability logic CSM\(_0\) are decidable |
scientific article; zbMATH DE number 1187520 |
Statements
All finitely axiomatizable subframe logics containing the provability logic CSM\(_0\) are decidable (English)
0 references
25 October 1998
0 references
The propositional logics considered here have two modalities \(\square_1\), \(\square_2\) interpreted usually as provability in two systems \(S_1\), \(S_2\). Decidability is based on a completeness theorem for an axiomatization by characteristic formulas of finite Kripke-type frames, which in the unimodal case is traceable to a construction in the decidability proof for extensions of K4 due to K. Fine.
0 references
provability logic
0 references
bimodal logic
0 references
completeness
0 references
axiomatization
0 references
Kripke-type frames
0 references
decidability
0 references
0.7921647429466248
0 references
0.7912465333938599
0 references
0.7762816548347473
0 references
0.7688612341880798
0 references
