Finitism, imperative programs and primitive recursion

Following the Crisis of Foundations Hilbert proposed to consider a finitistic form of arithmetic as mathematics’ safe core. This approach to finitism has often admitted primitive recursive function definitions as obviously finitistic, but some have advocated the inclusion of additional variants of recurrence, while others argued that, to the contrary, primitive recursion exceeds finitism. In a landmark essay, William Tait contested the finitistic nature of these extensions, due to their impredicativity, and advocated identifying finitism with primitive recursive arithmetic, a stance often referred to as Tait’s Thesis. However, a problem with Tait’s argument is that the recurrence schema has itself impredicative and non-finitistic facets, starting with an explicit reference to the functions being defined, which are after all infinite objects. It is therefore desirable to buttress Tait’s Thesis on grounds that avoid altogether any trace of concrete infinities or impredicativity. We propose here to do just that, building on the generic framework of [ 13]. We provide further evidence for Tait’s Thesis by outlining a proof of a purely finitistic version of Parsons’ theorem, whose intuitive gist is that finitistic reasoning is equivalent to finitistic computing.

VON NEUMANN’S CONSISTENCY PROOF

We consider the consistency proof for a weak fragment of arithmetic published by von Neumann in 1927. This proof is rather neglected in the literature on the history of consistency proofs in the Hilbert school. We explain von Neumann’s proof and argue that it fills a gap between Hilbert’s consistency proofs for the so-called elementary calculus of free variables with a successor and a predecessor function and Ackermann’s consistency proof for second-order primitive recursive arithmetic. In particular, von Neumann’s proof is the first rigorous proof of the consistency of an axiomatization of the first-order theory of a successor function.

UNFOLDING FINITIST ARITHMETIC

The concept of the (full) unfolding $\user1{{\cal U}}(S)$ of a schematic system $S$ is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted $S$? The program to determine $\user1{{\cal U}}(S)$ for various systems $S$ of foundational significance was previously carried out for a system of nonfinitist arithmetic, $NFA$; it was shown that $\user1{{\cal U}}(NFA)$ is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic system of finitist arithmetic, $FA$, and for an extension of that by a form $BR$ of the so-called Bar Rule. It is shown that $\user1{{\cal U}}(FA)$ and $\user1{{\cal U}}(FA + BR)$ are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, $PRA$, and to Peano Arithmetic, $PA$.

On mathematical instrumentalism

In this paper we devise some technical tools for dealing with problems connected with the philosophical view usually called mathematical instrumentalism. These tools are interesting in their own right, independently of their philosophical consequences. For example, we show that even though the fragment of Peanos Arithmetic known as IΣ1 is a conservative extension of the equational theory of Primitive Recursive Arithmetic (PRA). IΣ1 has a super-exponential speed-up over PRA. On the other hand, theories studied in the Program of Reverse Mathematics that formalize powerful mathematical principles have only polynomial speed-up over IΣ1.

An application of graphical enumeration to PA

For α less than ε0 let Nα be the number of occurrences of ω in the Cantor normal form of α. Further let ∣n∣ denote the binary length of a natural number n, let ∣n∣h denote the h-times iterated binary length of n and let inv(n) be the least h such that ∣n∣h ≤ 2. We show that for any natural number h first order Peano arithmetic, PA, does not prove the following sentence: For all K there exists an M which bounds the lengths n of all strictly descending sequences 〈α0, …, αn〉 of ordinals less than ε0 which satisfy the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · ∣i∣i.As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence 〈α0, …, αn〉 of ordinals less than ε0 which satisfies the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · inv(i). The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations.Using results from Otter and from Matoušek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856.…

Special issue on ‘Logical frameworks and metalanguages’

There is both a great unity and a great diversity in presentations of logic. The diversity is staggering indeed – propositional logic, first-order logic, higher-order logic belong to one classification; linear logic, intuitionistic logic, classical logic, modal and temporal logics belong to another one. Logical deduction may be presented as a Hilbert style of combinators, as a natural deduction system, as sequent calculus, as proof nets of one variety or other, etc. Logic, originally a field of philosophy, turned into algebra with Boole, and more generally into meta-mathematics with Frege and Heyting. Professional logicians such as Gödel and later Tarski studied mathematical models, consistency and completeness, computability and complexity issues, set theory and foundations, etc. Logic became a very technical area of mathematical research in the last half century, with fine-grained analysis of expressiveness of subtheories of arithmetic or set theory, detailed analysis of well-foundedness through ordinal notations, logical complexity, etc. Meanwhile, computer modelling developed a need for concrete uses of logic, first for the design of computer circuits, then more widely for increasing the reliability of sofware through the use of formal specifications and proofs of correctness of computer programs. This gave rise to more exotic logics, such as dynamic logic, Hoare-style logic of axiomatic semantics, logics of partial values (such as Scott's denotational semantics and Plotkin's domain theory) or of partial terms (such as Feferman's free logic), etc. The first actual attempts at mechanisation of logical reasoning through the resolution principle (automated theorem proving) had been disappointing, but their shortcomings gave rise to a considerable body of research, developing detailed knowledge about equational reasoning through canonical simplification (rewriting theory) and proofs by induction (following Boyer and Moore successful integration of primitive recursive arithmetic within the LISP programming language). The special case of Horn clauses gave rise to a new paradigm of non-deterministic programming, called Logic Programming, developing later into Constraint Programming, blurring further the scope of logic. In order to study knowledge acquisition, researchers in artificial intelligence and computational linguistics studied exotic versions of modal logics such as Montague intentional logic, epistemic logic, dynamic logic or hybrid logic. Some others tried to capture common sense, and modeled the revision of beliefs with so-called non-monotonic logics. For the careful crafstmen of mathematical logic, this was the final outrage, and Girard gave his anathema to such “montres à moutardes”.

Intuitionistic Choice and Restricted Classical Logic

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic<br />in all finite types together with various forms of the axiom of choice and<br />a numerical omniscience schema (NOS) which implies classical logic for arithmetical<br />formulas. Feferman subsequently observed that the proof theoretic<br />strength of such systems can be determined by functional interpretation based<br />on a non-constructive mu-operator and his well-known results on the strength<br />of this operator from the 70's.<br />In this note we consider a weaker form LNOS (lesser numerical omniscience<br />schema) of NOS which suffices to derive the strong form of binary K¨onig's<br />lemma studied by Coquand/Palmgren and gives rise to a new and mathematically<br />strong semi-classical system which, nevertheless, can proof theoretically<br />be reduced to primitive recursive arithmetic PRA. The proof of this fact relies<br />on functional interpretation and a majorization technique developed in a<br />previous paper.

Foundational and Mathematical Uses of Higher Types

In this paper we develop mathematically strong systems of analysis in<br />higher types which, nevertheless, are proof-theoretically weak, i.e. conservative<br />over elementary resp. primitive recursive arithmetic. These systems<br />are based on non-collapsing hierarchies (Phi_n-WKL+, Psi_n-WKL+) of principles<br />which generalize (and for n = 0 coincide with) the so-called `weak' K¨onig's<br />lemma WKL (which has been studied extensively in the context of second order<br />arithmetic) to logically more complex tree predicates. Whereas the second<br />order context used in the program of reverse mathematics requires an encoding<br />of higher analytical concepts like continuous functions F : X -> Y between<br />Polish spaces X, Y , the more flexible language of our systems allows to treat<br />such objects directly. This is of relevance as the encoding of F used in reverse<br />mathematics tacitly yields a constructively enriched notion of continuous functions<br />which e.g. for F : N^N -> N can be seen (in our higher order context) to be equivalent<br /> to the existence of a continuous modulus of pointwise continuity.<br />For the direct representation of F the existence of such a modulus is<br />independent even of full arithmetic in all finite types E-PA^omega plus quantifier-free<br />choice, as we show using a priority construction due to L. Harrington.<br />The usual WKL-based proofs of properties of F given in reverse mathematics<br />make use of the enrichment provided by codes of F, and WKL does not seem<br />to be sufficient to obtain similar results for the direct representation of F in<br />our setting. However, it turns out that Psi_1-WKL+ is sufficient.<br />Our conservation results for (Phi_n-WKL+, Psi_n-WKL+) are proved via a new<br />elimination result for a strong non-standard principle of uniform Sigma^0_1-<br />boundedness<br />which we introduced in 1996 and which implies the WKL-extensions studied<br />in this paper.