Unprovability of circuit upper bounds in Cook's theory PV

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.

Bibliographic Details
Main Authors: Jan Krajicek, Igor C. Oliveira
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2017-02-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/3119/pdf