Switch to: References

Citations of:

On the no-counterexample interpretation

Ulrich Kohlenbach

Journal of Symbolic Logic 64 (4):1491-1511 (1999)

Add citations

You must login to add citations.

(1 other version)On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness.Ulrich Kohlenbach - 1998 - Annals of Pure and Applied Logic 95 (1-3):257-285.details In this paper the numerical strength of fragments of arithmetical comprehension, choice and general uniform boundedness is studied systematically. These principles are investigated relative to base systems Tnω in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive functions of low growth. We reduce the use of instances of these principles in Tnω-proofs of a large class of formulas to the use of instances of certain arithmetical principles thereby determining faithfully the arithmetical (...) Download Export citation Bookmark 3 citations
A direct proof of schwichtenberg’s bar recursion closure theorem.Paulo Oliva & Silvia Steila - 2018 - Journal of Symbolic Logic 83 (1):70-83.details 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 (...) Download Export citation Bookmark 3 citations
Gödel functional interpretation and weak compactness.Ulrich Kohlenbach - 2012 - Annals of Pure and Applied Logic 163 (11):1560-1579.details In recent years, proof theoretic transformations that are based on extensions of monotone forms of Gödel’s famous functional interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and (...) Download Export citation Bookmark
Gödel's functional interpretation and its use in current mathematics.Ulrich Kohlenbach - 2008 - Dialectica 62 (2):223–267.details Download Export citation Bookmark 1 citation
Non-principal ultrafilters, program extraction and higher-order reverse mathematics.Alexander P. Kreuzer - 2012 - Journal of Mathematical Logic 12 (1):1250002-.details 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 (...) Download Export citation Bookmark 4 citations
On the computational content of the Bolzano-Weierstraß Principle.Pavol Safarik & Ulrich Kohlenbach - 2010 - Mathematical Logic Quarterly 56 (5):508-532.details 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 (...) Download Export citation Bookmark 6 citations
(1 other version)Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The no-counterexample interpretation.W. W. Tait - 2005 - Bulletin of Symbolic Logic 11 (2):225-238.details The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s ﬁrst version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), ﬁll in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs. Download Export citation Bookmark 10 citations
On Spector's bar recursion.Paulo Oliva & Thomas Powell - 2012 - Mathematical Logic Quarterly 58 (4-5):356-265.details We show that Spector's “restricted” form of bar recursion is sufficient (over system T) to define Spector's search functional. This new result is then used to show that Spector's restricted form of bar recursion is in fact as general as the supposedly more general form of bar recursion. Given that these two forms of bar recursion correspond to the (explicitly controlled) iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is T‐equivalent to the (...) Download Export citation Bookmark 4 citations

1