Sciweavers

Share
FUIN
2008

On Krivine's Realizability Interpretation of Classical Second-Order Arithmetic

11 years 5 months ago
On Krivine's Realizability Interpretation of Classical Second-Order Arithmetic
This article investigates Krivine's realizability interpretation of classical second-order arithmetic and its recent extension handling countable choice. We will start by presenting a two-step interpretation which first eliminates classical logic via a negative translation and then applies standard realizability interpretation. We then argue that a slight variant of Krivine's interpretation corresponds to this two-step interpretation. This variant can be viewed as the continuation passing style variant of Krivine's original interpretation, and as such uses standard -terms and avoids the use of new continuation constants in the interpretation of classical logic.
Paulo Oliva, Thomas Streicher
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FUIN
Authors Paulo Oliva, Thomas Streicher
Comments (0)
books