This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the (...) paper, we will point out some open problems and directions for future research, including some initial results on saturation principles. (shrink)

We adapt a continuous logic axiomatization of tracial von Neumann algebras due to Farah, Hart and Sherman in order to prove a metatheorem for this class of structures in the style of proof mining, a research programme that aims to obtain the hidden computational content of ordinary mathematical proofs using tools from proof theory.

This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of counterexamples for A which became witnesses for ¬A when defining (...) the formula interpretation and, second, the inductive information about the witnesses of A which is considered in the proof of soundness. Sufficient conditions on the parameters are also given which ensure the soundness of the resulting functional interpretation. The relation between the parametrized interpretation and the recent bounded functional interpretation is also discussed. (shrink)

In this note we show that proof-theoretic uniform boundedness or bounded collection principles which allow one to formalize certain instances of countable Heine–Borel compactness in proofs using abstract metric structures must be carefully distinguished from an unrestricted use of countable Heine–Borel compactness.

This article systematically investigates so-called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q-modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q-variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q-variants (...) of the Diller-Nahm interpretation, the bounded modified realizability and the bounded functional interpretation. (shrink)

In 2007. Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP₁. That turned out to not be the proper formulation and so we proposed an alternative version FIPP₂. Tao himself formulated yet another version FIPP₃ in a revised version of his essay. We give (...) a counterexample to FIPP₁ and discuss for both of the versions FIPP₂ and FIPP₃ the faithfulness of their respective finitization of IPP by studying the equivalences IPP ↔ FIPP₂ and IPP ↔ FIPP₃ in the context of reverse mathematics ([9]). In the process of doing this we also introduce a continuous uniform boundedness principle CUB as a formalization of Tao's notion of a correspondence principle and study the strength of this principle and various restrictions thereof in terms of reverse mathematics, i.e., in terms of the "big five" subsystems of second order arithmetic. (shrink)

We adapt Streicher and Kohlenbach's proof of the factorization S = KD of the Shoenfield translation S in terms of Krivine's negative translation K and the Gödel functional interpretation D, obtaining a proof of the factorization U = KB of Ferreira's Shoenfield-like bounded functional interpretation U in terms of K and Ferreira and Oliva's bounded functional interpretation B.

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.

In finite type arithmetic, the real numbers are represented by rapidly converging Cauchy sequences of rational numbers. Ulrich Kohlenbach introduced abstract types for certain structures such as metric spaces, normed spaces, Hilbert spaces, etc. With these types, the elements of the spaces are given directly, not through the mediation of a representation. However, these abstract spaces presuppose the real numbers. In this paper, we show how to set up an abstract type for the real numbers. The appropriateness of our construction (...) works in tandem with the bounded functional interpretation. (shrink)

We present a functional interpretation of Peano arithmetic that uses Gödel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles are interpreted while maintaining unmoved the -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.

We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with our interpretation in the case when least elements exist . The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well-founded.

In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively.

It is well-known that an element of a commutative ring with identity is nilpotent if, and only if, it lies in every prime ideal of the ring. A modification of this fact is amenable to a very simple proof mining analysis. We formulate a quantitative version of this modification and obtain an explicit bound. We present an application. This proof mining analysis is the leitmotif for some comments and observations on the methodology of computational extraction. In particular, we emphasize that (...) the formulation of quantitative versions of ordinary mathematical theorems is of independent interest from proof mining metatheorems. (shrink)

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.

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...) calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)

Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the settheoretic universe is as an indefinite (or “potential”) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a definite (or “completed”) totality, for which classical logic is appropriate; so on that view, set theory should be axiomatized on some correspondingly mixed basis. Similarly, in the (...) case of predicative analysis, the natural numbers are considered to form a definite totality, while the universe of sets (or functions) of natural numbers are viewed as an indefinite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. Various such semiconstructive systems of analysis and set theory are formulated here and their proof-theoretic strength is characterized. Interestingly, though the logic is weakened, one can in compensation strengthen certain principles in a way that could be advantageous for mathematical applications. (shrink)

We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functionals 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.

We show how to interpret weak Kőnig's lemma in some recently defined theories of nonstandard arithmetic in all finite types. Two types of interpretations are described, with very different verifications. The celebrated conservation result of Friedman's about weak Kőnig's lemma can be proved using these interpretations. We also address some issues concerning the collecting of witnesses in herbrandized functional interpretations.

Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.