3 papers
math.LO2025
Tarskian Theories of Krivine's Classical Realisability
Daichi Hayashi, Graham E. Leigh
This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic (). To formulate the theory as an extension of…
math.LO2025
A Friedman--Sheard-style Theory for Classical Realisability
Daichi Hayashi, Graham E. Leigh
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 reali…
cs.LO2016
On the Herbrand content of LK
Bahareh Afshari, Stefan Hetzl, Graham E. Leigh
We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-determinis…