The Absorption Law, or How to Kreisel a Hilbert-Bernays-L\"ob

TL;DR

This paper presents a method to construct a $\Sigma^0_1$-predicate satisfying both L"ob and Kreisel conditions for any consistent theory, even if unsound, allowing the theory to internally verify the Kreisel condition.

Contribution

It introduces a novel construction of a $\Sigma^0_1$-predicate that meets both L"ob and Kreisel conditions within any consistent theory, including unsound ones.

Findings

Constructs a $\Sigma^0_1$-predicate satisfying L"ob and Kreisel conditions.

Enables a theory to verify the Kreisel condition internally.

Works even for unsound theories.

Abstract

In this paper, we show how to construct for a given consistent theory $U$ a $\Sigma^0_1$-predicate that both satisfies the L\"ob Conditions and the Kreisel Condition ---even if $U$ is unsound. We do this in such a way that $U$ itself can verify satisfaction of an internal version of the Kreisel Condition.