ECCC-Report TR23-030https://eccc.weizmann.ac.il/report/2023/030Comments and Revisions published for TR23-030en-usTue, 21 Mar 2023 12:10:27 +0200
Paper TR23-030
| A proof complexity conjecture and the Incompleteness theorem |
Jan Krajicek
https://eccc.weizmann.ac.il/report/2023/030Given a sound first-order p-time theory $T$ capable of formalizing syntax of
first-order logic we define a p-time function $g_T$ that stretches all inputs by one
bit and we use its properties to show that $T$ must be incomplete. We leave it as an
open problem whether for some $T$ the range of $g_T$ intersects all infinite NP sets
(i.e. whether it is a proof complexity generator hard for all proof systems).
A propositional version of the construction shows that at least one of the following
three statements is true:
- there is no p-optimal propositional proof system (this is equivalent to the
non-existence of a time-optimal propositional proof search algorithm),
- $E \not\subseteq P/poly$,
- there exists function $h$ that stretches all inputs by one bit,
is computable in sub-exponential time and its range $Rng(h)$ intersects all infinite
N sets.Tue, 21 Mar 2023 12:10:27 +0200https://eccc.weizmann.ac.il/report/2023/030