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.

• Type: Journal
• Year: 2008
• Where: FUIN
• Authors: Paulo Oliva, Thomas Streicher
• Keywords: FUIN 2008, Realizability Interpretation, Standard Realizability Interpretation, Two-step Interpretation