Partial impredicativity in reverse mathematics

Journal of Symbolic Logic 78 (2):459-488 (2013)
  Copy   BIBTEX


In reverse mathematics, it is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on how to weaken the assumption while preserving the conclusion (other than reducing all the way to the tautology of assuming the conclusion). A main cause of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$. Using methods based on the functional interpretation, we introduce a family of weakenings of $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$ and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs



    Upload a copy of this work     Papers currently archived: 93,098

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

19 (#825,863)

6 months
2 (#1,259,876)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Proof-theoretic investigations on Kruskal's theorem.Michael Rathjen & Andreas Weiermann - 1993 - Annals of Pure and Applied Logic 60 (1):49-88.
Ordinal numbers and the Hilbert basis theorem.Stephen G. Simpson - 1988 - Journal of Symbolic Logic 53 (3):961-974.
An effective proof that open sets are Ramsey.Jeremy Avigad - 1998 - Archive for Mathematical Logic 37 (4):235-240.
Functional interpretation and inductive definitions.Jeremy Avigad & Henry Towsner - 2009 - Journal of Symbolic Logic 74 (4):1100-1120.
A recursion theoretic analysis of the clopen Ramsey theorem.Peter Clote - 1984 - Journal of Symbolic Logic 49 (2):376-400.

View all 6 references / Add more references