A proof complexity conjecture and the Incompleteness theorem

Jan Krajicek

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…