一句话：证明循环算术 CΣ_n 与 IΣ_{n+1} 的 Π_{n+1} 定理相同，并给出证明规模与一致性强度新界。
本文研究 Simpson（2017）循环算术 CA 的逻辑复杂度，以量词交替为标尺，其中 CΣ_n 是仅含 Σ_n 公式的循环证明的逻辑后承。主结果为：对所有 n≥0，IΣ_{n+1} 与 CΣ_n 证明相同的 Π_{n+1} 定理；方法的均匀性还表明 CA 与 PA 证明同一定理的规模仅差指数级。包含 IΣ_{n+1}⊆CΣ_n 用 PA 证明的正规形式与结构操作证明，改进 IΣ_n⊆CΣ_n；反向包含 CΣ_n⊆IΣ_{n+1} 则用 KMPS'16 关于 Büchi 定理反数学的结果校准 Simpson 方法。由此可刻画 CA 片段：CΣ_n 的一致性在 IΣ_{n+2} 可证但不在 IΣ_{n+1} 可证；并推出 McNaughton 定理某些版本在 RCA_0 不可证，部分解决 KMPS'16 公开问题。
We study the logical complexity of proofs in cyclic arithmetic ($\mathsf{CA}$), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing $C\Sigma_n$ for (the logical consequences of) cyclic proofs containing only $\Sigma_n$ formulae, our main result is that $I\Sigma_{n+1}$ and $C\Sigma_n$ prove the same $\Pi_{n+1}$ theorems, for all $n\geq 0$. Furthermore, due to the 'uniformity' of our method, we also show that $\mathsf{CA}$ and Peano Arithmetic ($\mathsf{PA}$) proofs of the same theorem differ only exponentially in size. The inclusion $I\Sigma_{n+1} \subseteq C\Sigma_n$ is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of $\mathsf{PA}$ proofs. It improves upon the natural result that $I\Sigma_n$ is contained in $C\Sigma_n$. The converse inclusion, $C\Sigma_n \subseteq I\Sigma_{n+1}$, is obtained by calibrating the approach of Simpson '17 with recent results on the reverse mathematics of B\"uchi's theorem in Ko{\l}odziejczyk, Michalewski, Pradic & Skrzypczak '16 (KMPS'16), and specialising to the case of cyclic proofs. These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson '17 and also an alternative approach due to Berardi & Tatsuta '17. The uniformity of our method also allows us to recover a metamathematical account of fragments of $\mathsf{CA}$; in particular we show that, for $n\geq 0$, the consistency of $C\Sigma_n$ is provable in $I\Sigma_{n+2}$ but not $I\Sigma_{n+1}$. As a result, we show that certain versions of McNaughton's theorem (the determinisation of $\omega$-word automata) are not provable in $\mathsf{RCA}_0$, partially resolving an open problem from KMPS '16.