Kripke models built from models of arithmetic

Citations of this article
Mendeley users who have this article in their library.
Get full text


We introduce three relations between models of Peano Arithmetic (PA), each of which is characterized as an arithmetical accessibility relation. A relation R is said to be an arithmetical accessibility relation if for any model M of PA, M ⊧ Pr π (φ) iff M′ ⊧ φ for all M′ with M R M′, where Pr π (x) is an intensionally correct provability predicate of PA. The existence of arithmetical accessibility relations yields a new perspective on the arithmetical completeness of GL. We show that any finite Kripke model for the provability logic GL is bisimilar to some “arithmetical” Kripke model whose domain consists of models of PA and whose accessibility relation is an arithmetical accessibility relation. This yields a new interpretation of the modal operators in the context of PA: an arithmetical assertion φ is consistent (possible, ◊φ) if it holds in some arithmetically accessible model, and provable (necessary, □φ) if it holds in all arithmetically accessible models.




Henk, P. (2015). Kripke models built from models of arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8984, pp. 157–174). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free