On a Question of Hamkins'

TL;DR

This work answers Hamkins' question in two parts: there is no extensional Rosser formula under broad theories, but once Extensionality is weakened to Conditional Extensionality, a $Π^0_1$-formula $ρ(x)$ can be made extensional and $Π^0_1$-flexible using a slow-provability framework. The construction relies on a uniform-provability formalism, uniform smallness, and slow provability to produce a conditional-extensional, $Π^0_1$-flexible predicate, extending ideas from Shavrukov–Visser and Kripke. The results illuminate how Gödelian phenomena interact with extensionality notions and provide a structured path to independence results under weaker extensionality, though the open problem of Consistent Extensionality remains unresolved.

Abstract

Joel Hamkins asks whether there is a $Π^0_1$-formula $ρ(x)$ such that $ρ({\ulcorner φ\urcorner})$ is independent over ${\sf PA}+φ$, if this theory is consistent, where this construction is extensional in $φ$ with respect to {\sf PA}-provable equivalence. We show that there can be no such extensional Rosser formula of any complexity. We give a positive answer to Hamkins' question for the case where we replace Extensionality by a weaker demand that we call \emph{Conditional Extensionality}. For this case, we prove an even stronger result, to wit, there is a $Π^0_1$-formula $ρ(x)$ that is extensional and $Π^0_1$-flexible. We leave one important question open: what happens when we weaken Extensionality to Consistent Extensionality, i.e., Extensionality for consistent extensions?

Theorems & Definitions (32)

• Remark 1.1
• Theorem 2.1
• proof
• Remark 2.2
• Theorem 3.1
• proof
• Theorem 3.2
• proof
• Remark 3.3
• Remark 3.4