Largeness notions and polytime translation for $\forall Σ^0_3$-consequences of $\mathsf{RT}^2_2$
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917293145980928 |
|---|---|
| author | Houérou, Quentin Le Patey, Ludovic |
| author_facet | Houérou, Quentin Le Patey, Ludovic |
| contents | Le Houérou, Patey and Yokoyama defined a parameterized version of $α$-largeness to prove that $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ is a $\forall Σ^0_3$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$, where $\forall Σ^0_3$ is the universal set-closure of the class of $Σ^0_3$-formulas. We introduce a variant of this notion of largeness and obtain polynomial bounds, using a tree partition theorem based on Milliken's tree theorem. Thanks to the framework of forcing interpretation, this yields that any proof of a $\forall Σ^0_3$-sentence in the theory $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ can be translated into a proof in $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$ at the cost of a polynomial increase in size. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_11906 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Largeness notions and polytime translation for $\forall Σ^0_3$-consequences of $\mathsf{RT}^2_2$ Houérou, Quentin Le Patey, Ludovic Logic 03F20, 03F35, 03B30 (Primary) 03F25, 05D10 (Secondary) Le Houérou, Patey and Yokoyama defined a parameterized version of $α$-largeness to prove that $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ is a $\forall Σ^0_3$-conservative extension of $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$, where $\forall Σ^0_3$ is the universal set-closure of the class of $Σ^0_3$-formulas. We introduce a variant of this notion of largeness and obtain polynomial bounds, using a tree partition theorem based on Milliken's tree theorem. Thanks to the framework of forcing interpretation, this yields that any proof of a $\forall Σ^0_3$-sentence in the theory $\mathsf{WKL}_0 + \mathsf{RT}^2_2$ can be translated into a proof in $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$ at the cost of a polynomial increase in size. |
| title | Largeness notions and polytime translation for $\forall Σ^0_3$-consequences of $\mathsf{RT}^2_2$ |
| topic | Logic 03F20, 03F35, 03B30 (Primary) 03F25, 05D10 (Secondary) |
| url | https://arxiv.org/abs/2602.11906 |