Provable(P) ⇒ provable(provable(P))? Why if provable(P) then provable(provable(P))?
I was reading Godel's incompleteness theorem explained in words of one syllable and came across this assertion (near the end of the first paragraph):

In fact, if a claim can be proved, then it can be proved that the claim can be proved.

Can you give a proof (or a counterexample if it's false)?
 A: (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 proved1, then it can be proved1 that the claim can be proved2.
The instances of "can be proved1" refer to proving a formal sentence in a fixed theory, whereas "can be proved2" is itself a formal sentence within that theory. In the notation Andrej uses in his post, "can be proved2" 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.)
A: In order to talk about provability, we need to say what provability is.  There are basically two options:


*

*Define an explicit provability predicate: encode some proof calculus in the natural numbers, then define "is a valid proof of $\phi$" as a predicate on natural number codes for proofs, then define "$\phi$ is provable" as "there exists a proof $\phi$".  This was a major component of G\"odel's famous incompleteness proof.

*Select a set of axioms for the provability predicate, such that formulae involving "is provable" (but not "is a valid proof") follow from the axioms just in case they are true for a "sensible" proof system.  If we take "sensible" to mean predicate calculus under the axioms of Peano Arithmetic, then the axioms of modal logic K4 plus the axiom $\Box(\Box A\Rightarrow A)\Rightarrow \Box A$ have this property; this seminal result is due to Solovay.
From perspective #2, the requirement "if $\phi$ is provable, it is provable that $\phi$ is provable" is taken to be part of the basic definition of provability.  This is essentially an axiom excluding the possibility that we might be dealing with more than one notion of provability or entailment.

(or a counterexample if it's false)?

One often-overlooked case is when dealing with two different provability predicates.  For example, take:


*

*$\Box\phi$ to mean "$\neg\phi$ is inconsistent with ZFC" -- a fancy way of saying that if $M\vDash ZFC$, then $M\vDash \phi$

*$\Box_\omega\phi$ to mean "$\neg\phi$ is $\omega$-inconsistent with ZFC" -- a fancy way of saying that if $M\vDash ZFC$ and $M$'s $\omega$ ordinal is well-founded, then $M\vDash \phi$.
In this scenario we do not have $\Box_\omega A \Rightarrow \Box_\omega \Box A$. 
Such methods can be used to investigate how much first-order notions of provability ($\Box$) can tell us about infinitary ($\Box_\omega$) notions of provability and vice versa.
A: Here's the way that I would think about the proof of the result which Wang asks about. First show that Robinson's Q proves every Sigma^0_1 sentence which is true on the standard model. (One way to establish this is to realize that the standard models embeds into every model of Robinson's Q). Second show that this first fact can be established in a subsystem of PA like ISigma^0_1, so that within ISigma^0_1 a schema is provable which asserts, for each Sigma^0_1 sentence, that if it is true then it is provable from Robinson's Q. (You need to go up to an intermediary system like ISigma^0_1 because you will need a little bit of induction to prove the first fact). Third note that formalized versions of provability statements have complexity Sigma^0_1.
A: We work with Peano arithmetic PA. Following Goedel, in PA we can define a primitive recursive relation $\mathrm{Prf}(m,n)$ such that Peano arithmetic proves $\mathrm{Prf}(m,n)$ if, and only if, $n$ is the Goedel code of a proof of the statement whose Goedel code is $m$. This much you have to take on trust, or look it up in a book.
Now suppose a statement $\phi$ is provable. Then it has a proof $p$. From $\phi$ and $p$ we can compute their Goedel codes $m$ and $n$, respectively. Because $p$ is a proof of $\phi$, it follows that $\mathrm{Prf}(n,m)$ is provable in PA.
More generally, we can ask your question in the language of Provability logic, namely is it the case that $\square \phi \Rightarrow \square \square \phi$ (the modal operator $\square$ means "it is provable that"). The answer is positive, as this is known as the K4 axiom of modal logic, and it is part of Provability logic.
