In this paper we introduce a novel way of building arithmetics whose background logic is R. The purpose of doing this is to point in the direction of a novel family of systems that could be candidates for being the infamous R#1/2 that Meyer suggested we look for.

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...) developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)

Gentzen’s approach by transfinite induction and that of intuitionist Heyting arithmetic to completeness and the self-foundation of mathematics are compared and opposed to the Gödel incompleteness results as to Peano arithmetic. Quantum mechanics involves infinity by Hilbert space, but it is finitist as any experimental science. The absence of hidden variables in it interpretable as its completeness should resurrect Hilbert’s finitism at the cost of relevant modification of the latter already hinted by intuitionism and Gentzen’s approaches for completeness. This paper (...) investigates both conditions and philosophical background necessary for that modification. The main conclusion is that the concept of infinity as underlying contemporary mathematics cannot be reduced to a single Peano arithmetic, but to at least two ones independent of each other. Intuitionism, quantum mechanics, and Gentzen’s approaches to completeness an even Hilbert’s finitism can be unified from that viewpoint. Mathematics may found itself by a way of finitism complemented by choice. The concept of information as the quantity of choices underlies that viewpoint. Quantum mechanics interpretable in terms of information and quantum information is inseparable from mathematics and its foundation. (shrink)

A practical viewpoint links reality, representation, and language to calculation by the concept of Turing (1936) machine being the mathematical model of our computers. After the Gödel incompleteness theorems (1931) or the insolvability of the so-called halting problem (Turing 1936; Church 1936) as to a classical machine of Turing, one of the simplest hypotheses is completeness to be suggested for two ones. That is consistent with the provability of completeness by means of two independent Peano arithmetics discussed in Section I. (...) Many modifications of Turing machines cum quantum ones are researched in Section II for the Halting problem and completeness, and the model of two independent Turing machines seems to generalize them. Then, that pair can be postulated as the formal definition of reality therefore being complete unlike any of them standalone, remaining incomplete without its complementary counterpart. Representation is formal defined as a one-to-one mapping between the two Turing machines, and the set of all those mappings can be considered as “language” therefore including metaphors as mappings different than representation. Section III investigates that formal relation of “reality”, “representation”, and “language” modeled by (at least two) Turing machines. The independence of (two) Turing machines is interpreted by means of game theory and especially of the Nash equilibrium in Section IV. Choice and information as the quantity of choices are involved. That approach seems to be equivalent to that based on set theory and the concept of actual infinity in mathematics and allowing of practical implementations. (shrink)

A set theory model of reality, representation and language based on the relation of completeness and incompleteness is explored. The problem of completeness of mathematics is linked to its counterpart in quantum mechanics. That model includes two Peano arithmetics or Turing machines independent of each other. The complex Hilbert space underlying quantum mechanics as the base of its mathematical formalism is interpreted as a generalization of Peano arithmetic: It is a doubled infinite set of doubled Peano arithmetics having a remarkable (...) symmetry to the axiom of choice. The quantity of information is interpreted as the number of elementary choices (bits). Quantum information is seen as the generalization of information to infinite sets or series. The equivalence of that model to a quantum computer is demonstrated. The condition for the Turing machines to be independent of each other is reduced to the state of Nash equilibrium between them. Two relative models of language as game in the sense of game theory and as ontology of metaphors (all mappings, which are not one-to-one, i.e. not representations of reality in a formal sense) are deduced. (shrink)

In his remarkable paper Formalism 64, Robinson defends his eponymous position concerning the foundations of mathematics, as follows:Any mention of infinite totalities is literally meaningless.We should act as if infinite totalities really existed. Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that ‘some infinite totalities are more meaningful than others’, the textbook example being that of infinitesimals. For instance, Bishop and Connes have made such claims regarding infinitesimals, (...) and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate ‘meaning’ and ‘computational content’, though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects in Nonstandard Analysis yields the absence of meaning. We will debunk the Bishop–Connes critique by establishing the contrary, namely that the presence of ideal objects in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content, similar to the ‘reversals’ from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation. (shrink)

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

It is folklore that if a continuous function on a complete metric space has approximate roots and in a uniform manner at most one root, then it actually has a root, which of course is uniquely determined. Also in Bishop's constructive mathematics with countable choice, the general setting of the present note, there is a simple method to validate this heuristic principle. The unique solution even becomes a continuous function in the parameters by a mild modification of the uniqueness hypothesis. (...) Moreover, Brouwer's fan theorem for decidable bars turns out to be equivalent to the statement that, for uniformly continuous functions on a compact metric space, the crucial uniform “at most one” condition follows from its non-uniform counterpart. This classification in the spirit of the constructive reverse mathematics, as propagated by Ishihara and others, sharpens an earlier result obtained jointly with Berger and Bridges. (shrink)

The period in the foundations of mathematics that started in 1879 with the publication of Frege's Begriffsschrift and ended in 1931 with Gödel's Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I can reasonably be called the classical period. It saw the development of three major foundational programmes: the logicism of Frege, Russell and Whitehead, the intuitionism of Brouwer, and Hilbert's formalist and proof-theoretic programme. In this period, there were also lively exchanges between the various schools culminating in (...) the famous Hilbert-Brouwer controversy in the 1920s. -/- The purpose of this anthology is to review the programmes in the foundations of mathematics from the classical period and to assess their possible relevance for contemporary philosophy of mathematics. What can we say, in retrospect, about the various foundational programmes of the classical period and the disputes that took place between them? To what extent do the classical programmes of logicism, intuitionism and formalism represent options that are still alive today? These questions are addressed in this volume by leading mathematical logicians and philosophers of mathematics. (shrink)

In this paper, I develop a view on set-theoretic ontology I call Universe-Indeterminism, according to which there is a unique but indeterminate universe of sets. I argue that Solomon Feferman’s work on semi-constructive set theories can be adapted to this project, and develop a philosophical motivation for a semi-constructive set theory closely based on Feferman’s but tailored to the Universe-Indeterminist’s viewpoint. I also compare the emergent Universe-Indeterminist view to some more familiar views on set-theoretic ontology.

We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] . This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied to fixed (...) sequences in Πi ∈ℕ[–ki, ki]. (shrink)

Jean van Heijenoort was best known for his editorial work in the history of mathematical logic. I survey his contributions to model-theoretic proof theory, and in particular to the falsifiability tree method. This work of van Heijenoort’s is not widely known, and much of it remains unpublished. A complete list of van Heijenoort’s unpublished writings on tableaux methods and related work in proof theory is appended.

We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher-order arithmetic. Let [Formula: see text] be the statement that a non-principal ultrafilter on ℕ exists and let [Formula: see text] be the higher-order extension of ACA0. We show that [Formula: see text] is [Formula: see text]-conservative over [Formula: see text] and thus that [Formula: see text] is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly (...) [Formula: see text] statement ∀ f ∃ g A qf in [Formula: see text] a realizing term in Gödel's system T can be extracted. This means that one can extract a term t ∈ T, such that ∀ f A qf). (shrink)

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".

The aim of this article is to give an introduction to functional interpretations of set theory given by the authorin Burr (2000a). The first part starts with some general remarks on Gödel's functional interpretation with a focus on aspects related to problems that arise in the context of set theory. The second part gives an insight in the techniques needed to perform a functional interpretation of systems of set theory. However, the first part of this article is not intended to (...) be a complete survey of functional interpretations and here we recommend, for example, Avigad and Feferman (1998),Troelstra (1990) and Troelstra (1973). (shrink)

We sketch the historical and conceptual context of Turing's analysis of algorithmic or mechanical computation. We then discuss two responses to that analysis, by Gödel and by Gandy, both of which raise, though in very different ways. The possibility of computation procedures that cannot be reduced to the basic procedures into which Turing decomposed computation. Along the way, we touch on some of Cleland's views.

Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for α < ε₀ and primitive recursion over (...) finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg’s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Tᵢ then terms built from BR^ℕ,σ for this particular Y are definable in the fragment T_i+max{1,level(σ)}+2. (shrink)

At the most general level, the concept of finitism is typically characterized by saying that finitistic mathematics is that part of mathematics which does not appeal to completed infinite totalities and is endowed with some epistemological property that makes it secure or privileged. This paper argues that this characterization can in fact be sharpened in various ways, giving rise to different conceptions of finitism. The paper investigates these conceptions and shows that they sanction different portions of mathematics as finitistic.

In the present paper we give a functional interpretation of Aczel's constructive set theories CZF − and CZF in systems T ∈ and T ∈ + of constructive set functionals of finite types. This interpretation is obtained by a translation × , a refinement of the ∧ -translation introduced by Diller and Nahm 49–66) which again is an extension of Gödel's Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF − and CZF in terms of (...) constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the translation × . We further show that the simplest non-trivial axiom of extensionality is not interpretable by functionals of T ∈ and T ∈ + . We obtain this result by adapting Howard's notion of hereditarily majorizable functionals to set functionals. Subject of the last section is the translation ∨ that is defined in Burr for an interpretation of Kripke-Platek set theory with infinity. (shrink)

Abstract.Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in the extended language, (...) the terms are ordinary PL-terms. In contrast to approaches to Herbrand’s theorem based on cut elimination orɛ-elimination this extraction technique is, except for the normalization step, of low polynomial complexity, fully modular and furthermore allows an analysis of the structure of the Herbrand terms, in the spirit of Kreisel ([13]), already prior to the normalization step. It is expected that the implementation of functional interpretation in Schwichtenberg’s MINLOG system can be adapted to yield an efficient Herbrand-term extraction tool. (shrink)

Hilbert developed his famous finitist point of view in several essays in the 1920s. In this paper, we discuss various extensions of it, with particular emphasis on those suggested by Hilbert and Bernays in Grundlagen der Mathematik (vol. I 1934, vol. II 1939). The paper is in three sections. The first deals with Hilbert's introduction of a restricted ? -rule in his 1931 paper ?Die Grundlegung der elementaren Zahlenlehre?. The main question we discuss here is whether the finitist (meta-)mathematician would (...) be entitled to accept this rule as a finitary rule of inference. In the second section, we assess the strength of finitist metamathematics in Hilbert and Bernays 1934. The third and final section is devoted to the second volume of Grundlagen der Mathematik. For preparatory reasons, we first discuss Gentzen's proposal of expanding the range of what can be admitted as finitary in his esssay ?Die Widerspruchsfreiheit der reinen Zahlentheorie? (1936). As to Hilbert and Bernays 1939, we end on a ?critical? note: however considerable the impact of this work may have been on subsequent developments in metamathematics, there can be no doubt that in it the ideals of Hilbert's original finitism have fallen victim to sheer proof-theoretic pragmatism. (shrink)

The papers of Kurt Gödel were donated to the Institute for Advanced Study by his widow Adele shortly after his death in 1978. They were catalogued by the review.

The logic of identity contains riches not seen through the coarse lens of predicate logic. This is one of several lessons to draw from the subtle treatment of identity in Martin‐Löf type theory, to which the reader will be introduced in this article. After a brief general introduction we shall mainly be concerned with the distinction between identity propositions and identity judgements. These differ from each other both in logical form and in logical strength. Along the way, connections to philosophical (...) debates concerning identity are noted. Some use of logical symbolism is inevitable in any serious discussion of type theory, but the emphasis here is on basic ideas rather than technicalities. (shrink)

Tarski’s conceptual analysis of the notion of logical consequence is one of the pinnacles of the process of defining the metamathematical foundations of mathematics in the tradition of his predecessors Euclid, Frege, Russell and Hilbert, and his contemporaries Carnap, Gödel, Gentzen and Turing. However, he also notes that in defining the concept of consequence “efforts were made to adhere to the common usage of the language of every day life.” This paper addresses the issue of what relationship Tarski’s analysis, and (...) Béziau’s further generalization of it in universal logic, have to reasoning in the everyday lives of ordinary people from the cognitive processes of children through to those of specialists in the empirical and deductive sciences. It surveys a selection of relevant research in a range of disciplines providing theoretical and empirical studies of human reasoning, discusses the value of adopting a universal logic perspective, answers the questions posed in the call for this special issue, and suggests some specific research challenges. (shrink)

After briefly discussing the relevance of the notions computation and implementation for cognitive science, I summarize some of the problems that have been found in their most common interpretations. In particular, I argue that standard notions of computation together with a state-to-state correspondence view of implementation cannot overcome difficulties posed by Putnam's Realization Theorem and that, therefore, a different approach to implementation is required. The notion realization of a function, developed out of physical theories, is then introduced as a replacement (...) for the notional pair computation-implementation. After gradual refinement, taking practical constraints into account, this notion gives rise to the notion digital system which singles out physical systems that could be actually used, and possibly even built. (shrink)

Recently, the second author, Briseid, and Safarik introduced nonstandard Dialectica, a functional interpretation capable of eliminating instances of familiar principles of nonstandard arithmetic—including overspill, underspill, and generalizations to higher types—from proofs. We show that the properties of this interpretation are mirrored by first-order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren, and draw some new connections between nonstandard principles and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of (...) the Diller–Nahm interpretation with two different kinds of quantifiers, similar to Hernest’s light Dialectica interpretation, and show that one can obtain nonstandard Dialectica by weakening the computational content of the existential quantifiers—a process called herbrandization. We also define a constructive sheaf model mirroring this new functional interpretation, and show that the process of herbrandization has a clear meaning in terms of these sheaf models. (shrink)

This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible — and hence most natural — sense, disjunction and conjunction as deterministic-choice combinations of problems , and “absurd” as a computational problem of universal strength.

This essay consists of two parts. In the first part, I focus my attention on the remarks that Frege makes on consistency when he sets about criticizing the method of creating new numbers through definition or abstraction. This gives me the opportunity to comment also a little on H. Hankel, J. Thomae—Frege’s main targets when he comes to criticize “formal theories of arithmetic” in Die Grundlagen der Arithmetik (1884) and the second volume of Grundgesetze der Arithmetik (1903)—G. Cantor, L. E. (...) J. Brouwer and D. Hilbert (1899). Part 2 is mainly devoted to Hilbert’s proof theory of the 1920s (1922–1931). I begin with an account of his early attempt to prove directly, and thus not by reduction or by constructing a model, the consistency of (a fragment of) arithmetic. In subsequent sections, I give a kind of overview of Hilbert’s metamathematics of the 1920s and try to shed light on a number of difficulties to which it gives rise. One serious difficulty that I discuss is the fact, widely ignored in the pertinent literature on Hilbert’s programme, that his language of finitist metamathematics fails to supply the conceptual resources for formulating a consistency statement qua unbounded quantification. Along the way, I shall comment on W. W. Tait’s objection to an interpretation of Hilbert’s finitism by Niebergall and Schirn, on G. Gentzen’s allegedly finitist consistency proof for Peano Arithmetic as well as his ideas on the provability and unprovability of initial cases of transfinite induction in pure number theory. Another topic I deal with is what has come to be known as partial realizations of Hilbert’s programme, chiefly advocated by S. G. Simpson. Towards the end of this essay, I take a critical look at Wittgenstein’s views about (in)consistency and consistency proofs in the period 1929–1933. I argue that both his insouciant attitude towards the emergence of a contradiction in a calculus and his outright repudiation of metamathematical consistency proofs are unwarranted. In particular, I argue that Wittgenstein falls short of making a convincing case against Hilbert’s programme. I conclude with some philosophical remarks on consistency proofs and soundness and raise a question concerning the consistency of analysis. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

This article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy (...) of ordinal recursive functionals of arbitrary type that can be reduced by substitution to natural number functions. (shrink)

Hamkins and Löwe proved that the modal logic of forcing is S4.2 . In this paper, we consider its modal companion, the intermediate logic KC and relate it to the fatal Heyting algebra H ZFC of forcing persistent sentences. This Heyting algebra is equationally generic for the class of fatal Heyting algebras. Motivated by these results, we further analyse the class of fatal Heyting algebras.