A new perspective on the arithmetical completeness of GL
Paula Henk
Abstract:
Solovay’s proof of the arithmetical completeness of the provability
logic GL proceeds by simulating a finite Kripke model inside the
theory of Peano Arithmetic (PA). In this article, a new perspective on
the proof of GL’s arithmetical completeness will be given. Instead of
simulating a Kripke structure inside the theory of PA, it will be
embedded into an arithmetically defined Kripke structure. We will
examine the relation of strong interpretability, which will turn out
to have exactly the suitable properties for assuming the role of the
accessibility relation in a Kripke structure whose domain consists of
models of PA.
Given any finite Kripke model for GL, we can then find a bisimilar
model whose nodes are certain nonstandard models of PA. The arith-
metical completeness of GL is an immediate consequence of this result.
In order to define the bisimulation, however, and to prove its
existence, the most crucial and ingenious ingredients of Solovay’s
original proof are needed. The main result of the current work is thus
not so much a new proof as a new perspective on an already known
proof.