On the strength of the finite intersection principle

We study the logical content of several maximality principles related to the finite intersection principle (FIP) in set theory. Classically, these are all equivalent to the axiom of choice, but in the context of reverse mathematics their strengths vary: some are equivalent to ACA₀ over RCA₀, while others are strictly weaker and incomparable with WKL₀. We show that there is a computable instance of FIP every solution of which has hyperimmune degree, and that every computable instance has a solution in every nonzero c.e. degree. In particular, FIP implies the omitting partial types principle (OPT) over RCA₀. We also show that, modulo Σ ₂ ⁰ induction, FIP lies strictly below the atomic model theorem (AMT).     

The maximal linear extension theorem in second order arithmetic

We show that the maximal linear extension theorem for well partial orders is equivalent over RCA ₀ to ATR ₀. Analogously, the maximal chain theorem for well partial orders is equivalent to ATR ₀ over RCA ₀.     

Derived sequences and reverse mathematics

One of the earliest applications of transfinite numbers is in the construction of derived sequences by Cantor [2]. In [6], the existence of derived sequences for countable closed sets is proved in ATR₀. This existence theorem is an intermediate step in a proof that a statement concerning topological comparability is equivalent to ATR₀. In actuality, the full strength of ATR₀ is used in proving the existence theorem. To show this, we will derive a statement known to be equivalent to ATR₀, using only RCA₀ and the assertion that every countable closed set has a derived sequence. We will use three of the subsystems of second order arithmetic defined by H. Friedman ([3], [4]), which can be roughly characterized by the strength of their set comprehension axioms. RCA₀ includes comprehension for Δ definable sets, ACA₀ includes comprehension for arithmetical sets, and ATR₀ appends to ACA₀ a comprehension scheme for sets defined by transfinite recursion on arithmetical formulas. MSC: 03F35, 54B99.     

The strong soundness theorem for real closed fields and Hilbert’s Nullstellensatz in second order arithmetic

By RCA₀, we denote a subsystem of second order arithmetic based on ⁰₁ comprehension and ⁰₁ induction. We show within this system that the real number system R satisfies all the theorems (possibly with non-standard length) of the theory of real closed fields under an appropriate truth definition. This enables us to develop linear algebra and polynomial ring theory over real and complex numbers, so that we particularly obtain Hilberts Nullstellensatz in RCA₀.Mathematics Subject Classification (2000): Primary 03F35; Secondary 03B30, 12D10     

A new conservation result of WKL0 over RCA0

In this paper we give a partial answer to a conjecture of Tanaka. We prove that: if WKL₀ proves a sentence of the form (∀X)(∃!Y)ψ(X, Y) for a Σ⁰ ₃-formula ψ, then so does RCA₀. Received: 12 April 1999 / Published online: 3 October 2001     

On the Π11‐separation principle

We study the proof‐theoretic strength of the Π₁¹‐separation axiom scheme, and we show that Π₁¹‐separation lies strictly in between the Δ₁¹‐comprehension and Σ₁¹‐choice axiom schemes over RCA₀. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Some More Conservation Results on the Baire Category Theorem

In this paper, we generalize a result of Brown and Simpson [1] to prove that RCA₀+Π⁰_∞‐BCT is conservative over RCA₀ with respect to the set of formulae in the form ∃!Xφ(X), where φ is arithmetical. We also consider the conservation of Π⁰_0∞‐BCT over Σ^b₁‐NIA+∇^b₁‐CA.     

Infinite games in the Cantor space and subsystems of second order arithmetic

In this paper we study the determinacy strength of infinite games in the Cantor space and compare them with their counterparts in the Baire space. We show the following theorems: 1. RCA₀ ? ‐Det* ? ‐Det* ? WKL₀. 2. RCA₀ ? ( )2‐Det* ? ACA₀. 3. RCA₀ ? ‐Det* ? ‐Det* ? ‐Det ? ‐Det ? ATR₀. 4. For 1 < k < ω, RCA₀ ? ( )_k ‐Det* ? ( )_{k –1}‐Det. 5. RCA₀ ? ‐Det* ? ‐Det. Here, Det* (respectively Det) stands for the determinacy of infinite games in the Cantor space (respectively the Baire space), and ( )_k is the collection of formulas built from formulas by applying the difference operator k – 1 times. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Effectiveness for infinite variable words and the Dual Ramsey Theorem

We examine the Dual Ramsey Theorem and two related combinatorial principles VW(k,l) and OVW(k,l) from the perspectives of reverse mathematics and effective mathematics. We give a statement of the Dual Ramsey Theorem for open colorings in second order arithmetic and formalize work of Carlson and Simpson [1] to show that this statement implies ACA₀ over RCA₀. We show that neither VW(2,2) nor OVW(2,2) is provable in WKL₀. These results give partial answers to questions posed by Friedman and Simpson [3].The first authors research is partially supported by an NSF VIGRE Grant at Indiana University. The second authors research is partially supported by an NSF Postdoctoral Fellowship.     

Reverse mathematics and initial intervals

In this paper we study the reverse mathematics of two theorems by Bonnet about partial orders. These results concern the structure and cardinality of the collection of initial intervals. The first theorem states that a partial order has no infinite antichains if and only if its initial intervals are finite unions of ideals. The second one asserts that a countable partial order is scattered and does not contain infinite antichains if and only if it has countably many initial intervals. We show that the left to right directions of these theorems are equivalent to _ACA0${\mathsf{ACA}}_0$ and _ATR0${\mathsf{ATR}}_0$, respectively. On the other hand, the opposite directions are both provable in _WKL0${\mathsf{WKL}}_0$, but not in _RCA0${\mathsf{RCA}}_0$. We also prove the equivalence with _ACA0${\mathsf{ACA}}_0$ of the following result of Erdös and Tarski: a partial order with no infinite strong antichains has no arbitrarily large finite strong antichains.     

Determinacy of Wadge classes and subsystems of second order arithmetic

In this paper we study the logical strength of the determinacy of infinite binary games in terms of second order arithmetic. We define new determinacy schemata inspired by the Wadge classes of Polish spaces and show the following equivalences over the system RCA₀*, which consists of the axioms of discrete ordered semi‐rings with exponentiation, Δ₁⁰ comprehension and Π₀⁰ induction, and which is known as a weaker system than the popularbase theory RCA₀: 1. Bisep(Δ₁⁰, Σ₁⁰)‐Det* ? WKL₀, (1) 2. Bisep(Δ₁⁰, Σ₂⁰)‐Det* ? ATR₀ + Σ₁¹ induction, (2) 3. Bisep(Σ₁⁰, Σ₂⁰)‐Det* ? Sep(Σ₁⁰, Σ₂⁰)‐Det* ? Π₁¹‐CA₀, (3) 4. Bisep(Δ₂⁰, Σ₂⁰)‐Det* ? Π₁¹‐TR₀, (4) where Det* stands for the determinacy of infinite games in the Cantor space (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Reverse mathematics,well-quasi-orders,and Noetherian spaces

A quasi-order Q induces two natural quasi-orders on \({\mathcal{P}(Q)}\), but if Q is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq (Proceedings of the 22nd Annual IEEE Symposium 4 on Logic in Computer Science (LICS’07), pp. 453–462, 2007) showed that moving from a well-quasi-order Q to the quasi-orders on \({\mathcal{P}(Q)}\) preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the induced quasi-orders on \({\mathcal{P}(Q)}\) are Noetherian, which means that they contain no infinite strictly descending sequences of closed sets. We analyze various theorems of the form “if Q is a well-quasi-order then a certain topology on (a subset of) \({\mathcal{P}(Q)}\) is Noetherian” in the style of reverse mathematics, proving that these theorems are equivalent to ACA₀ over RCA₀. To state these theorems in RCA₀ we introduce a new framework for dealing with second-countable topological spaces.     

Harrington’s conservation theorem redone

Leo Harrington showed that the second-order theory of arithmetic WKL ₀ is -conservative over the theory RCA ₀. 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.      

Graph Coloring and Reverse Mathematics

Improving a theorem of Gasarch and Hirst, we prove that if 2 ≤ k ≤ m < ω, then the following is equivalent to WKL₀ over RCA₀ Every locally k‐colorable graph is m‐colorable.     

Orders on computable rings

The Artin-Schreier theorem says that every formally real field has orders. Friedman, Simpson and Smith showed in [6] that the Artin-Schreier theorem is equivalent to ${\mathsf{WKL}}_0$ over ${\mathsf{RCA}}_0$. We first prove that the generalization of the Artin-Schreier theorem to noncommutative rings is equivalent to ${\mathsf{WKL}}_0$ over ${\mathsf{RCA}}_0$. In the theory of orderings on rings, following an idea of Serre, we often show the existence of orders on formally real rings by extending pre-orders to orders, where Zorn's lemma is used. We then prove that “pre-orders on rings not necessarily commutative extend to orders” is equivalent to ${\mathsf{WKL}}_0$.     

Embeddings into the Medvedev and Muchnik lattices of Π<Superscript>0</Superscript><Subscript>1</Subscript> classes

Let _w and _M be the countable distributive lattices of Muchnik and Medvedev degrees of non-empty ₁⁰ subsets of 2, under Muchnik and Medvedev reducibility, respectively. We show that all countable distributive lattices are lattice-embeddable below any non-zero element of _w. We show that many countable distributive lattices are lattice-embeddable below any non-zero element of _M.Simpsons research was partially supported by NSF Grant DMS-0070718. We thank the anonymous referee for a careful reading of this paper and helpful comments.     

Herbrand consistency of some finite fragments of bounded arithmetical theories

We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of IΔ₀ whose Herbrand Consistency is not provable in IΔ₀. We also show the existence of an IΔ₀-derivable Π ₁-sentence such that IΔ₀ cannot prove its Herbrand Consistency.     

Rank-one convex hulls in \mathbb{R}^{2\times2}

We study the rank-one convex hull of compact sets . We show that if K contains no two matrices whose difference has rank one, and if K contains no four matrices forming a T ₄ configuration, then the rank-one convex hull K ^rc is equal to K. Furthermore, we give a simple numerical criterion for testing for T ₄ configurations. Received: 20 August 2003, Accepted: 3 March 2004, Published online: 12 May 2004 Mathematics Subject Classification (2000): 49J45, 52A30 An erratum to this article can be found at