(This is really just a comment, but apparently I don't have enough reputation to leave comments yet.)

I think there's some room for more care in the notation. $\Box \phi \implies \Box \Box \phi$ looks suspiciously like a formal sentence within a particular theory, and while undoubtedly true I feel it sweeps some things under the rug.

In the quote, the word "proved" formally has two meanings:

In fact, if a claim can be proved_{1}, then it can be proved_{1} that the claim can be proved_{2}.

The instances of "can be proved_{1}" refer to proving a formal sentence in a fixed theory, whereas "can be proved_{2}" is *itself* a formal sentence within that theory. In the notation Andrej uses in his post, "can be proved_{2}" is the predicate $\mathrm{Prf}$. The quote can be formalised like this, for Peano arithmetic at least: "If $\mathrm{PA} \vdash \phi$ then $\mathrm{PA} \vdash \exists n . \mathrm{Prf}(m, n)$, where $m$ is the Gödel code of the sentence $\phi$ and $n$ is the code of any valid proof of $\phi$ (from the axioms of PA).

(For what it's worth, when I first started looking at logic I was confused about the difference between $\vdash$ and $\implies$. This is of a similar nature, I think.)

secondincompleteness theorem, and one of them is that your theory be able to prove Prov(x) => Prov(Prov(x)). $\endgroup$ – Timothy Chow Dec 20 '10 at 16:34firstHilbert—Bernays condition, that for every true sentence P, we have Prov(#P)... but the title of the question is thesecondHilbert—Bernays condition, which is rather more interesting, because it says for any sentence P whatsoever (even false ones!), Prov(#P) => Prov(#Prov(#P)). $\endgroup$ – Zhen Lin Dec 20 '10 at 16:51