Alessandra Carbone, Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo; Computability in Europe 2010, Journal of Logic and Computation, Volume 25, Issue 4,

Abstract We define a functional interpretation of KP ω using Howard’s primitive recursive tree functionals of finite type and associated terms. We prove that the Σ-ordinal of KP ω is the least ordinal not given by a closed term of the ground type of the trees (the Bachmann-Howard ordinal). We also extend KP ω to a second-order theory with Δ 1-comprehension and strict- ${\rm{\Pi }}_1^1$ reflection and show that the Σ-ordinal of this theory is still the Bachmann-Howard ordinal. It is also argued that the second-order theory is Σ1-conservative over KPω.

Abstract It has been known for six years that the restriction of Girard's polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to η-conversions.

F. FerreiraDepartamento de Matematica, Faculdade de Ciencias, Universidade de Lisboa, Campo Grande,1749-016 Lisboa, Portugale-mail: [email protected]. Lowe ( )Institute for Logic, Language and Computation, Universiteit van Amsterdam, Postbus 94242,1090 GE Amsterdam, The Netherlandse-mail: [email protected]. LoweDepartment Mathematik, Universitat Hamburg, Bundesstrasse 55, 20146 Hamburg, GermanyE. MayordomoDepartamento de Informatica e Ingenieria de Sistemas, Instituto de Investigacion en Ingenieria deAragon (I3A), Universidad de Zaragoza, 50015 Zaragoza, Spaine-mail: [email protected]

Abstract We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functional of finite type. As an application, we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.

Abstract We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.

Abstract This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q.

Abstract We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.