一句话：无条件证明每个 k 都存在 P 语言 L，使 PV 不能证明 L 不属于 Size(n^k)。
该论文研究 Cook 的有界算术理论 PV 能否证明多项式时间语言的电路上界。作者无条件地证明：对任意整数 k≥1，都存在一个属于 P 的语言 L，使得在 PV 中“L 不属于 Size(n^k)”这一命题与 PV 一致；换言之，PV 无法证明 L 可由规模 n^k 的电路计算。证明是非构造性的，没有给出 L 的显式描述，因此结果不直接给出具体的 P 问题，而是建立了电路复杂性下界在弱算术理论中的不可证明性现象，连接了证明复杂度、有界算术与电路复杂性。
We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in \mbox{P}$ such that it is consistent with Cook's theory PV that $L \notin Size(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language.
@article{paperbot206,
title = {Unprovability of circuit upper bounds in Cook's theory PV},
author = {Jan Krajicek and Igor C. Oliveira},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:4)2017}
}