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 ${\mbox {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:

1. 1. There is no p-optimal propositional proof system (this is equivalent to the non-existence of a time-optimal propositional proof search algorithm).

2. 2. $E \not \subseteq P/poly$.

3. 3. 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 ${\text {NP}}$ sets.

A cornerstone of modern mathematical logic is the diagonal lemma of Gödel and Carnap. It is used in, for example, the classical proofs of the theorems of Gödel, Rosser, and Tarski. From its first explication in 1934, just essentially one proof has appeared for the diagonal lemma in the literature; a proof that is so tricky and hard to relate that many authors have tried to avoid the lemma altogether. As a result, some so-called diagonal-free proofs have been given for the above-mentioned fundamental theorems of logic. In this paper, we provide new proofs for the semantic formulation of the diagonal lemma, and for a weak version of the syntactic formulation of it.