Provability Logic: models within models in Peano Arithmetic

TL;DR

This paper explores the relationship between provability logic and models within models in Peano Arithmetic, demonstrating independence results for the existence of certain models without relying on the arithmetized completeness theorem.

Contribution

It introduces a new interpretation of provability logic in PA using $oldsymbol{ ext{Σ}}^0_2$-models, advancing model-theoretic methods in provability logic.

Findings

The existence of a $oldsymbol{ ext{Σ}}^0_2$-model of PA is independent of PA.

A new interpretation of provability logic using truth in all $oldsymbol{ ext{Σ}}^0_2$-models.

Avoids passing through the arithmetized completeness theorem.

Abstract

In 1994 Jech gave a model theoretic proof of G\"odel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano Arithmetic with the role of models being taken by complete consistent extensions. In this note we take another step in the direction of replacing proof-theoretic by model-theoretic arguments. We show, without passing through the arithmetized completeness theorem, that the existence of a model of PA of complexity $\Sigma^0_2$ is independent of PA, where a model is identified with the set of formulas with parameters which hold in the model. Our approach is based on a new interpretation of the provability logic of Peano Arithmetic with the modal operator interpreted as truth in every $\Sigma^0_2$-model.