论文标题
拉姆西的对，收集和证明大小的定理
Ramsey's theorem for pairs, collection, and proof size
论文作者
论文摘要
我们证明，理论中的任何证明$ \forallσ^0_2 $句子$ \ mathrm {wkl} _0 + \ mathrm {rt}^2_2 $都可以在$ \ mathrm {rca} _0 _0中的证明，以多样性的增长成本增加。实际上，可以通过多项式算法找到$ \ mathrm {rca} _0 $的证明。另一方面，$ \ mathrm {rt}^2_2 $在弱基理论$ \ mathrm {rca}^*_ 0 $方面具有非质量加速，用于$σ_1$句子的证明。 我们还表明，对于$ n \ ge 0 $，$π_{n+2} $句子的证明$ \ mathrm {b}σ_{n+1}+\ exp $可以在$ \ mathrm {i}σ_{n} n}+\ exp $下以polynomial成本转换为$ \ mathrm {i} n} n}+\ exp $。此外，$π_{n + 2} $ - $ \ mathrm {b}σ_{n + 1} + \ exp $ a $ \ mathrm {i}σ_{n} + \ exp $的保守性可以以$ \ \ \ \ m vartimition compotition compotitiantime compotition compotition compotition contrimitiant a fority a forityed a andited arith，可以在$ \ mathrm {pv} $中预测。对于$ n \ ge 1 $，这回答了Clote，Hájek和Paris的问题。
We prove that any proof of a $\forall Σ^0_2$ sentence in the theory $\mathrm{WKL}_0 + \mathrm{RT}^2_2$ can be translated into a proof in $\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $\mathrm{RCA}^*_0$ for proofs of $Σ_1$ sentences. We also show that for $n \ge 0$, proofs of $Π_{n+2}$ sentences in $\mathrm{B}Σ_{n+1}+\exp$ can be translated into proofs in $\mathrm{I}Σ_{n} + \exp$ at polynomial cost. Moreover, the $Π_{n+2}$-conservativity of $\mathrm{B}Σ_{n+1} + \exp$ over $\mathrm{I}Σ_{n} + \exp$ can be proved in $\mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n \ge 1$, this answers a question of Clote, Hájek, and Paris.
