Fernando Ferreira

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.

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.

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 Frege’s logicism, numbers are logical objects in the sense that they are extensions of certain concepts. Frege’s logical system is inconsistent, but Richard Heck showed that its restriction to predicative quantification is consistent. This predicative fragment is, nevertheless, too weak to develop arithmetic. In this paper, I will consider an extension of Heck’s system with impredicative quantifiers. In this extended system, both predicative and impredicative quantifiers co-exist but it is only permissible to take extensions of concepts formulated in the predicative fragment of the language. This system is consistent. Moreover, it proves the principle of reducibility applied to concepts true of only finitely many objects. With the aid of this form of reducibility, it is possible to develop arithmetic in a thoroughly Fregean way.

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.

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.

Frege’s Grundgesetze der Arithmetik is formally inconsistent. This system is, except for minor differences, second-order logic together with an abstraction operator governed by Frege’s Axiom V. A few years ago, Richard Heck showed that the ramified predicative second-order fragment of the Grundgesetze is consistent. In this paper, we show that the above fragment augmented with the axiom of reducibility for concepts true of only finitely many individuals is still consistent, and that elementary Peano arithmetic (and more) is interpretable in this extended system.

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

Recently, Feferman and Hellman (and Aczel) showed how to establish the existence and categoricity of a natural number system by predicative means given the primitive notion of a finite set of individuals and given also a suitable pairing function operating on individuals. This short paper shows that this existence and categoricity result does not rely (even indirectly) on finite-set induction, thereby sustaining Feferman and Hellman's point in favor of the view that natural number induction can be derived from a very weak fragment of finite-set theory, so weak that finite-set induction is not assumed. Many basic features of finiteness fail to hold in these weak fragments, conspicuously the principle that finite sets are in one-one correspondence with a proper initial segments of a (any) natural number structure. In the last part of the paper, we propose two prima facie evident principles for finite sets that, when added to these fragments, entail this principle

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so interpreted. We explain some of these results and rely on them to discuss Nelson's position.