Provability interpretations of modal logic

Abstract

We consider interpretations of modal logic in Peano arithmetic (P) determined by an assignment of a sentence v * of P to each propositional variable v. We put (⊥)*="0 = 1", (χ → ψ)* = "χ* → ψ*" and let (□ψ)* be a formalization of "ψ)* is a theorem of P". We say that a modal formula, χ, is valid if ψ* is a theorem of P in each such interpretation. We provide an axiomitization of the class of valid formulae and prove that this class is recursive. © 1976 Hebrew University.