Decidable and enumerable predicate logics of provability (Q750418)

The predicate modal logic with \(\square\) interpreted as provability in some extension T of arithmetic is not recursively axiomatizable, and the set of true formulas is not arithmetic. The author finds enumerable fragments. A proof of decidability and completeness for formulas in one individual variable x is presented, where \(\forall x\) is interpreted as an S5-modality with additional axiom \(\square \forall A\to \forall \square A\). For provably \(\Pi_ 1\)-complete theories T the predicate version of K is complete for the predicate modal formulas of depth 1, and the predicate version of K4 is complete for the formulas \(\square^ n\perp \to A\) with arbitrary A. \(\Pi_ 1\)-completeness is used to describe inside T the construction of a model.