A Friedman--Sheard-style Theory for Classical Realisability
Daichi Hayashi, Graham E. Leigh
TL;DR
This work extends Krivine's classical realisability by formulating a Friedman--Sheard-style, type-free realisability theory $\mathsf{FSR}$ that supports self-referential reasoning. It introduces the generalised compositional realisability $\mathsf{GCR}$ and the Friedman--Sheard realisability system $\mathsf{FSR}$, along with a revision model to handle evolving interpretations and a proof-theoretic analysis showing $\mathsf{FSR}$ is conservative over $\mathsf{PA}$ and closely tied to the truth-theoretic framework $\mathsf{FS}$ viaInterpretations such as $\mathsf{FSR}^{\emptyset}$ and $\mathrm{TI}(<\varphi 20)$. The paper proves self-realisability for $\mathsf{FSR}$ and derives two key applications: a relative truth definability result for $\mathsf{FS}$ and a McGee-style analysis yielding an almost-$\omega$-inconsistency phenomenon, including a dedicated sentence $\gamma$ that exhibits this behavior. Overall, the results illuminate how self-referential realisability can emulate Friedman--Sheard truth constructs while preserving important proof-theoretic properties, suggesting avenues for deeper model-theoretic and ordinal analyses in self-referential arithmetic systems.
Abstract
In Hayashi and Leigh (2024), the authors formulate classical number realisability for first-order arithmetic and a corresponding axiomatic system based on Krivine's classical realisability interpretation. This paper presents a self-referential generalisation of previous results in the spirit of Friedman and Sheard (1987).