9 found
Alexander P. Kreuzer [8]Alexander Kreuzer [1]
  1.  10
    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 (4 more)  
    Export citation  
    My bibliography   4 citations  
  2. On Idempotent Ultrafilters in Higher-Order Reverse Mathematics.Alexander P. Kreuzer - 2015 - Journal of Symbolic Logic 80 (1):179-193.
  3.  12
    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 (6 more)  
    Export citation  
    My bibliography   3 citations  
  4.  12
    Non-Principal Ultrafilters, Program Extraction and Higher-Order Reverse Mathematics.Alexander P. Kreuzer - 2012 - Journal of Mathematical Logic 12 (01):1250002-.
  5.  10
    Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
    This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In the (...)
    Direct download (5 more)  
    Export citation  
    My bibliography   3 citations  
  6.  9
    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  
    My bibliography   1 citation  
  7.  7
    On Principles Between Σ1- and Σ2-Induction, and Monotone Enumerations.Alexander P. Kreuzer & Keita Yokoyama - forthcoming - Journal of Mathematical Logic.
  8.  9
    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  
    My bibliography  
  9. From Bolzano-Weierstraß to Arzelà-Ascoli.Alexander P. Kreuzer - 2014 - Mathematical Logic Quarterly 60 (3):177-183.
    No categories
      Direct download (2 more)  
    Export citation  
    My bibliography