5 problems

Let $\mathcal S$ be the base arithmetic theory under consideration, and let $Con_{\mathcal S}(n)$ denote its bounded consistency statement at length $n$. Write…

Polynomial-length consistency conjecture. There are no such sequences of proofs whose lengths are polynomial in $n$.

Polynomial consistency-speedup conjecture. For every sound $\Delta^b_1(S^1_2)$ theory $S$ and every $l\in\omega$, there exists a sound $\Delta^b_1(S^1_2)$ theory $T$ such that

Classification conjecture for monotone proof-theoretic operators. Suppose $\mathfrak{g}$ is monotone, non-constant, and recursive, with $\mathfrak{g}(\varphi)\in\Pi_1$ for every se…

Let $\operatorname{Con}^\diamond(\mathbf{PA}+\varphi)$ denote slow consistency based on the fast-growing function $F_{\varepsilon_0}$, and let finite iterations of slow consistency…