I'm trying to remember who is responsible for the following well-known weak version of the first incompleteness theorem:
Suppose $T$ is a c.e. consistent $\Pi_2$ extension of Robinson's $\mathsf{Q}$ (or any c.e. consistent theory which interprets such). Then $T$ is incomplete.
Proof: we can computably enumerate the indices of $T$-provably-total computable functions, and then diagonalize against these; by $\Pi_2$-soundness of $T$, the result is a total computable function which is clearly not $T$-provably total. $\quad\Box$
Essentially the same idea gives a version of the second incompleteness theorem for $1$-consistency in place of consistency. Harvey Friedman writes about this here (page 14), and says that its original provenance is a bit murky:
"The origins of G2/1-con = G2 for 1-consistency are rather unclear. Lev Beklemishev has a paper in the 1980's about this, but it probably was first proved much earlier, perhaps when the notion of provably recursive functions of a theory first came into common use. That is probably in the 1950s with G. Kreisel. Some of the early proof theorists of that period are good candidates for having known about the directly straightforward proof of G2/1-con that we sketch now. (I don't know if Kreisel had this)."
