Frame definability, canonicity and cut elimination in common sense modal predicate logics

The paper presents semantically complete Hilbert-style systems for some variants of common sense modal predicate logic proposed by van Benthem and further developed by Seligman. The paper also investigates frame definability in the logics and shows what axiom schema is canonical in the logics. In addition to these semantic investigations on the logics, the paper provides the sequent calculi for some of the logics which enjoy cut elimination theorem.

Decidable fragments of first-order modal logics

The paper considers the setof first-order polymodal formulas the modal operators in which can be applied to subformulas of at most one free variable. Using a mosaic technique, we prove a general satisfiability criterion for formulas in, which reduces the modal satisfiability to the classical one. The criterion is then used to single out a number of new, in a sense optimal, decidable fragments of various modal predicate logics.

On the degrees of unsolvability of modal predicate logics of provability

The modal predicate logic of provability identifies the “□” of modal logic with the “Bew” of proof theory, so that, where “Bew” is a formula representing, in the usual way, provability in a consistent, recursively axiomatized theory Γ extending Peano arithmetic (PA), an interpretation of a language for the modal predicate calculus is a map * which associates with each modal formula an arithmetical formula with the same free variables which commutes with the Boolean connectives and the quantifiers and which sets (□ϕ)* equal to Bew(⌈ϕ*⌉). Where Δ is an extension of PA (all the theories we discuss will be extensions of PA), MPL(Δ) will be the set of modal formulas ϕ such that, for every interpretation *, ϕ* is a theorem of Δ. Most of what is currently known about the modal predicate logic of provability consists in demonstrations that MPL(Δ) must be computationally highly complex. Thus Vardanyan [11] shows that, provided that Δ is 1-consistent and recursively axiomatizable, MPL(Δ) will be complete , and Boolos and McGee [5] show that MPL({true arithmetical sentences}) is complete in {true arithmetical sentences}. All of these results take as their starting point Artemov's demonstration in [1] that {true arithmetical sentences} is 1-reducible to MPL({true arithmetical sentences}).The aim here is to consolidate these results by providing a general theorem which yields all the other results as special cases. These results provide a striking contrast with the situation in modal sentential logic (MSL); according to fundamental results of Solovay [8], provided Γ does not entail any falsehoods, MSL({true arithmetical sentences}) and MSL(PA) (which is the same as MSL(Γ)) are both decidable.

Finite Kripke models and predicate logics of provability

The paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic:If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR.This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.