A proof complexity conjecture and the Incompleteness theorem
share
Given 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 ⊈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 NP sets.
READ FULL TEXT