Is there such a thing as provability of provability?

Question

Gödel says that there are true statements that can't be proved, given a sound axiomatic system. Does anyone say anything about the provability of the provability of statements?

Is it still an open question that every logic statement that is provable can be proved to be provable? Or equivalently that every unprovable statement can be proved to be unprovable?

Or more specifically, is it still an open question if a subset of the provable statements (for example the true ones) can always be proved to be provable/unprovable so that one day we might come to the conclusion that all the true provable theorems can be proved to be provable?

---

UPDATE

I think my question may be a little outside of the box. I'll try to be more clear.

Gödel didn't specify the class of statements which are undecidable. What if, for example, all true theorems that can't be proved have some property P.

P being the property ‘useless for all practical purposes’.

Then we’d know that even though there are true theorems which cannot be proved, they are useless theorems. Wait a minute...is there such a thing as a useless theorem?

Answer 1

It is a central feature of all the main formal systems that when a statement is provable, then it is provably provable. Indeed, this feature is one of the derivability conditions that is commonly used in the proof of the incompleteness theorem, and it is central to Goedel's proof of the second incompleteness theorem.

But also, I might add, this principle is clearly something that we want to have in our formal systems. If you can prove a statement, it means that you have a finite proof, a sequence of statements each of which is either an axiom or follows from the previous statements by one of the deduction rules, and which ends in the statement being proved. To check that a proof really is a proof is meant to be a routine task. Thus, whenever a statement is provable, then we should expect that we can prove that it is provable, since this amounts just to proving that the proof really is a proof, which is something about which there will be little disagreement.

So yes, indeed, in any of the usual formal systems, whenever a statement is provable, then we can also prove that it is provable.

One may introduce the provability modality, writing Box φ to mean that φ is provable (in some fixed formal system under discussion). In this modal terminology, the principle that every provable statement is provably provable is the axiom:

• □ φ → □ □ φ

and this axiom is known as axiom 4 in the modal theory S4.

Answer 2

There exists a proof that a certain class of geometric statements is resolvable by a Turing machine in finite time.

This result was a spin-off of Hilbert's 10th problem, where he asked a question whether all arithmetic equations are solvable by an algorithm, which was answered in negative in 1970.

An analogous question came up about the possibility of an algorithm that would prove any true statement in elementary geometry and refute any false statement. It turns out such algorithm indeed exists, although it is useless for practical purposes because it's so inefficient that it would take more time than the existence of the Universe to resolve a problem using such algorithm.

However, because the above algorithm exists in principle, you can take its existence as the proof that all true geometric statements are provable.