Abstract This paper provides a case study for the extraction of computational content of proofs in geometry using Herbrand’s theorem. More specifically, we show how a valid Herbrand disjunction for the outer Pasch theorem can be extracted in a modular way from its proof by Schwabhäuser, Szmielew and Tarski.

Abstract We investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector’s consistency proof of ACA0 and from the negative translation of RCA0, as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.

Abstract In this paper we study with proof-theoretic methods the function(al)s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functional provably recursive from are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that is -conservative over PRA. Recent work of the first author showed that is equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs. For Ramsey's theorem for pairs and two colors we obtain the upper bounded that the type 2 functional provable recursive relative to are inT1. This is the fragment of Gödel's systemTcontaining only type 1 recursion—roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction ofT1-bounds from proofs that use . Moreover, this yields a new proof of the fact that is -conservative over . The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using -comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for ).

Abstract 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 FIPP1. That turned out to not be the proper formulation and so we proposed an alternative version FIPP2. Tao himself formulated yet another version FIPP3 in a revised version of his essay. We give a counterexample to FIPP1 and discuss for both of the versions FIPP2 and FIPP3 the faithfulness of their respective finitization of IPP by studying the equivalences IPP ↔ FIPP2 and IPP ↔ FIPP3 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.

The topic of this paper is relative constructivism. We are concerned with classifying nonconstructive principles from the constructive viewpoint. We compare, up to provability in intuitionistic arithmetic, subclassical principles like Markov's principle, (a function-free version of) weak Konig's lemma, Post's theorem, excluded middle for simply existential and simply universal statements, and many others. Our motivations are rooted in the experience of one of the authors with an extended program extraction and of another author with bound extraction from classical proofs.

Abstract In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theoremA(Aprenex) of first-order Peano arithmeticPAone can find ordinal recursive functionals of order type < ε0which realize the Herbrand normal formAHofA. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as alocalproof interpretation and don't respect the modus ponens on the level of the nocounterexample interpretation of formulasAandA → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and—at least not constructively—(γ) which are part of the definition of an ‘interpretation of a formal system’ as formulated in [15].

In a previous paper [13] we introduced a hierarchy (GnAω)n∈ℕ of subsystems of classical arithmetic in all finite types where the growth of definable functions of GnAω corresponds to the well-known Grzegorczyk hierarchy. Let AC-qf denote the schema of quantifier-free choice. [11], [13], [8] and [7] study various analytical principles Γ in the context of the theories GnAω + AC-qf (mainly for n = 2) and use proof-theoretic tools like, e.g., monotone functional interpretation (which was introduced in [12]) to determine their impact on the growth of uniform bounds Φ such that which are extractable from given proofs (based on these principles Γ) of sentences Here A0(u, k, v, w) is quantifier-free and contains only u, k, v, w as free variables; t is a closed term and ≤p is defined pointwise. The term ‘uniform bound’ refers to the fact that Φ does not depend on v ≤ptuk (see [12] for the relevance of such uniform bounds in numerical analysis and for concrete applications to approximation theory).

Abstract We show how to extract effective bounds Φ for ⋀ u 1 ⋀ v ≤ y tu ⋁ w η G 0 -sentences which depend on u only (i.e. ⋀ u ⋀ v ≤ y , tu ⋁ w ≤ η Φ u G 0 ) from arithmetical proofs which use analytical assumptions of the form ( ϒ, δ, ρ , and τ are arbitrary finite types, η ≤ 2, G 0 and F 0 are quantifier-free, and s and t are closed terms). If τ ≤ 2, (*) can be weakened to This is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.