  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 \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 NP sets.
