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

Issue title: Logic for Pragmatics

Article type: Research Article

Authors: Oliva, Paulo | Streicher, Thomas

Affiliations: Department of Computer Science, Queen Mary, University of London London, E1 4NS, UK. E-mail: pbo@dcs.qmul.ac.uk | TU Darmstadt, Schlossgartenstrasse 7, D-64289 Darmstadt, Germany. E-mail: streicher@mathematik.tu-darmstadt.de

Note: [] Address for correspondence: TU Darmstadt, Schlossgartenstrasse 7, D-64289 Darmstadt, Germany

Abstract: 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 twostep 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.

Journal: Fundamenta Informaticae, vol. 84, no. 2, pp. 207-220, 2008