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

• Autorzy: Oliva P. , Streicher T.
• Języki publikacji: EN

Abstrakty

EN

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 l-terms and avoids the use of new continuation constants in the interpretation of classical logic.

Słowa kluczowe

EN

classical second-order arithmetic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 84, nr 2
• Strony: 207--220
• Opis fizyczny: bibliogr. 10 poz.

Twórcy

autor

Oliva P.

autor

Streicher T.

• TU Darmstadt, Schlossgartenstrasse 7, D-64289 Darmstadt, Germany,

Bibliografia

• [1] J. Avigad. A variant of the double-negation translation. Technical Report 179, Carnegie Mellon Technical Report CMU-PHIL, 2006.
• [2] S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. The Journal of Symbolic Logic, 63(2):600-622, 1998.
• [3] U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. Lecture Notes in Logic, 20:89-107, 2005.
• [4] H. Friedman. Classically and intuitionistically provably recursive functions. In D. Scott and G. Müller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21-28. Springer, Berlin, 1978.
• [5] K. G¨odel. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, 4:34-38, 1933.
• [6] J. Krivine. A general storage theorem for integers in call-by-name lambda-calculus. Th. Comp. Sc., 129:79-94, 1994.
• [7] J. Krivine. Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Archive for Mathematical Logic,40(3):189-205, 2001.
• [8] J. Krivine. Dependent choice, "quote" and the clock. Th. Comp. Sc., 308:259-276, 2003.
• [9] A. Miquel. A strongly normalising Curry-Howard correspondence for IZF set theory. In Computer Science and Logic (CSL'03), pages 441-454, 2003.
• [10] T. Streicher and U Kohlenbach. Shoenfield is G¨odel after Krivine. Mathematical Logic Quarterly, vol. 53, pages 176-179.