# Is there such a thing as provability of provability?

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?

• Welcome to Philosophy SE! I have troubles understanding your concern: Gödel proved that "there are true statements that are undecidable [i.e. where neither the statement nor its negation can be proved] in a sound axiomatic system". That is, all the results about provability are theorems (i.e. proven mathematical statements). – DBK Nov 18 '13 at 0:22
• @DBK: I think the question is about proving that a certain statement can in principle be resolved, one way or another, before the actual proof becomes available, if ever. A mathematical analogy of that would be something like Implicit Function Theorem, that proves that under certain conditions a function f has inverse \$f^{-1}\$, even though finding the inverse is often impossible. – Michael Nov 18 '13 at 3:38
• @Michael: Oh, I see. If I understand the concern correctly, OP is asking then if the Entscheidungsproblem has a solution? Spoiler alert: It has not :) But the main point OP should keep in mind is that provability is relative to a given system. So the question "is S provable" does only make sense if one asks "is S provable in T". – DBK Nov 18 '13 at 6:17

## 2 Answers

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.

• I guess TeX is not activated on this site? If it were, it would be easier to express some logical notation more clearly. – JDH Dec 7 '13 at 3:28
• I wholeheartedly agree re: TeX support. Unfortunately, this request has been declined numerous times by the SE forces that be. See, e.g., this meta post – Dennis Jan 2 '14 at 0:34

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.