We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RTkndenote Ramsey's theorem fork–colorings ofn–element sets, and let RT<∞ndenote (∀k)RTkn. Our main result on computability is: For anyn≥ 2 and any computable (recursive)k–coloring of then–element sets of natural numbers, there is an infinite homogeneous setXwithX″ ≤T0(n). LetIΣnandBΣndenote the Σninduction and bounding schemes, respectively. Adapting the casen= 2 of the above result (whereXis low2) to models of arithmetic enables us to show that RCA0+IΣ2+ (...) RT22is conservative over RCA0+IΣ2for Π11statements and that RCA0+IΣ3+ RT<∞2is Π11-conservative over RCA0+IΣ3. It follows that RCA0+ RT22does not implyBΣ3. In contrast, J. Hirst showed that RCA0+ RT<∞2does implyBΣ3, and we include a proof of a slightly strengthened version of this result. It follows that RT<∞2is strictly stronger than RT22overRCA0. (shrink)

A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...) of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)

We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.

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.

In this paper, we introduce the systems ns-ACA₀ and ns-WKL₀ of non-standard second-order arithmetic in which we can formalize non-standard arguments in ACA₀ and WKL₀, respectively. Then, we give direct transformations from non-standard proofs in ns-ACA₀ or ns-WKL₀ into proofs in ACA₀ or WKL₀.

By , we denote the system of second-order arithmetic based on recursive comprehension axioms and Σ10 induction. is defined to be plus weak König's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. In this paper, we first show that for any countable model M of , there exists a countable model M′ of whose first-order part is the same as that of M, and whose second-order part consists of the M-recursive sets and sets not (...) in the second-order part of M. By combining this fact with a certain forcing argument over universal trees, we obtain the following result : if proves X!Y with arithmetical, so does . We also discuss several improvements of this results. (shrink)

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 Peano's Arithmetic known as IΣ₁ is a conservative extension of the equational theory of Primitive Recursive Arithmetic (PRA). IΣ₁ 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Σ₁. (shrink)

We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...) and the axiom of choice both for arbitrary formulae; and $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO ; but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

We prove two conservation results involving a generalization of the principle of strict ${\Pi^1_1}$ -reflection, in the context of bounded arithmetic. In this context a separation between the concepts of bounded set and binary sequence seems to emerge as fundamental.

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.

In this paper we give a partial answer to a conjecture of Tanaka. We prove that: if WKL0 proves a sentence of the form (∀X)(∃!Y)ψ(X, Y) for a Σ03-formula ψ, then so does RCA0.

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 Peano's Arithmetic known as IΣ₁ is a conservative extension of the equational theory of Primitive Recursive Arithmetic, IΣ₁ 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Σ₁. (shrink)

Reverse mathematics studies which subsystems of second order arithmetic are equivalent to key theorems of ordinary, non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of different foundations for mathematics in a formally precise manner. This paper gives a detailed account of the motivations and methodology of foundational analysis, which have heretofore been largely left implicit in the practice. It then shows how this account can be fruitfully applied in the (...) evaluation of major foundational approaches by a careful examination of two case studies: a partial realization of Hilbert’s program due to Simpson [1988], and predicativism in the extended form due to Feferman and Schütte. -/- Shore [2010, 2013] proposes that equivalences in reverse mathematics be proved in the same way as inequivalences, namely by considering only omega-models of the systems in question. Shore refers to this approach as computational reverse mathematics. This paper shows that despite some attractive features, computational reverse mathematics is inappropriate for foundational analysis, for two major reasons. Firstly, the computable entailment relation employed in computational reverse mathematics does not preserve justification for the foundational programs above. Secondly, computable entailment is a Pi-1-1 complete relation, and hence employing it commits one to theoretical resources which outstrip those available within any foundational approach that is proof-theoretically weaker than Pi-1-1-CA0. (shrink)

A general method of interpreting weak higher-type theories of nonstandard arithmetic in their standard counterparts is presented. In particular, this provides natural nonstandard conservative extensions of primitive recursive arithmetic, elementary recursive arithmetic, and polynomial-time computable arithmetic. A means of formalizing basic real analysis in such theories is sketched.

From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.

These are some minor notes and observations related to a paper by Cholak, Jockusch, and Slaman [3].