In this paper we investigate those extensions of the bimodal provability logic C⃗ SM0 (alias P⃗ RL1 or F⃗ −) which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing C⃗ SM0 are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with respect to Kripke semantics.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:31888 |
| Date | 12 October 2018 |
| Creators | Wolter, Frank |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, doc-type:article, info:eu-repo/semantics/article, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | 0933-5846, 1432-0665 |
Page generated in 0.0013 seconds