9 found
Order:
  1.  18
    On Principles Between ∑1- and ∑2-Induction, and Monotone Enumerations.Alexander P. Kreuzer & Keita Yokoyama - 2016 - Journal of Mathematical Logic 16 (1):1650004.
    We show that many principles of first-order arithmetic, previously only known to lie strictly between [Formula: see text]-induction and [Formula: see text]-induction, are equivalent to the well-foundedness of [Formula: see text]. Among these principles are the iteration of partial functions of Hájek and Paris, the bounded monotone enumerations principle by Chong, Slaman, and Yang, the relativized Paris–Harrington principle for pairs, and the totality of the relativized Ackermann–Péter function. With this we show that the well-foundedness of [Formula: see text] is a (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  28
    Primitive Recursion and the Chain Antichain Principle.Alexander P. Kreuzer - 2012 - Notre Dame Journal of Formal Logic 53 (2):245-265.
    Let the chain antichain principle (CAC) be the statement that each partial order on $\mathbb{N}$ possesses an infinite chain or an infinite antichain. Chong, Slaman, and Yang recently proved using forcing over nonstandard models of arithmetic that CAC is $\Pi^1_1$-conservative over $\text{RCA}_0+\Pi^0_1\text{-CP}$ and so in particular that CAC does not imply $\Sigma^0_2$-induction. We provide here a different purely syntactical and constructive proof of the statement that CAC (even together with WKL) does not imply $\Sigma^0_2$-induction. In detail we show using a (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  3.  4
    On the Uniform Computational Content of the Baire Category Theorem.Vasco Brattka, Matthew Hendtlass & Alexander P. Kreuzer - 2018 - Notre Dame Journal of Formal Logic 59 (4):605-636.
    We study the uniform computational content of different versions of the Baire category theorem in the Weihrauch lattice. The Baire category theorem can be seen as a pigeonhole principle that states that a complete metric space cannot be decomposed into countably many nowhere dense pieces. The Baire category theorem is an illuminating example of a theorem that can be used to demonstrate that one classical theorem can have several different computational interpretations. For one, we distinguish two different logical versions of (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  25
    Non-Principal Ultrafilters, Program Extraction and Higher-Order Reverse Mathematics.Alexander P. Kreuzer - 2012 - Journal of Mathematical Logic 12 (1):1250002-.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  25
    The Cohesive Principle and the Bolzano‐Weierstraß Principle.Alexander P. Kreuzer - 2011 - Mathematical Logic Quarterly 57 (3):292-298.
    The aim of this paper is to determine the logical and computational strength of instances of the Bolzano-Weierstraß principle and a weak variant of it.We show that BW is instance-wise equivalent to the weak König’s lemma for Σ01-trees . This means that from every bounded sequence of reals one can compute an infinite Σ01-0/1-tree, such that each infinite branch of it yields an accumulation point and vice versa. Especially, this shows that the degrees d ≫ 0′ are exactly those containing (...)
    No categories
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  6.  20
    Term Extraction and Ramsey's Theorem for Pairs.Alexander P. Kreuzer & Ulrich Kohlenbach - 2012 - Journal of Symbolic Logic 77 (3):853-895.
    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 $RCA_0 + COH + \Pi _1^0 - CP$ 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 $WKL_0 + \Pi _1^0 - (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  7.  14
    On Idempotent Ultrafilters in Higher-Order Reverse Mathematics.Alexander P. Kreuzer - 2015 - Journal of Symbolic Logic 80 (1):179-193.
  8.  9
    From Bolzano-Weierstraß to Arzelà-Ascoli.Alexander P. Kreuzer - 2014 - Mathematical Logic Quarterly 60 (3):177-183.
    No categories
    Direct download (6 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  9.  18
    Program Extraction for 2-Random Reals.Alexander P. Kreuzer - 2013 - Archive for Mathematical Logic 52 (5-6):659-666.
    Let ${2-\textsf{RAN}}$ be the statement that for each real X a real 2-random relative to X exists. We apply program extraction techniques we developed in Kreuzer and Kohlenbach (J. Symb. Log. 77(3):853–895, 2012. doi:10.2178/jsl/1344862165), Kreuzer (Notre Dame J. Formal Log. 53(2):245–265, 2012. doi:10.1215/00294527-1715716) to this principle. Let ${{\textsf{WKL}_0^\omega}}$ be the finite type extension of ${\textsf{WKL}_0}$ . We obtain that one can extract primitive recursive realizers from proofs in ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN}}$ , i.e., if ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN} (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark