ABSTRACT
We have seen that any attempt to capture mathematics in Hilbert’s prooftheoretical framework is doomed.
What is worse, we now notice, is that provability — in PA and a wide range of theories related to PA — is necessarily unpredictable. That is, we cannot computably decide whether a given sentence is going to be provable or not. And this is a big problem when we have limited time to wait for our theory to deliver a decision on a given ϕ, and the theory is incomplete — and so does not guarantee to tell us anything about ϕ !
