# Some kind of incompleteness over proofs

There are some mathematical questions which one wants to knows if are demonstrable or refutable, for instance the Goldbach conjecture, Collatz conjecture and so on.

But what happens if that can't be answered, i.e.

Is there some proposition $Q$ so that is not possible to show that $Q$ is probable or $Q$ is refutable?

What I want to know is if there exist a $Q$ as in the dialog:

Asker: Can we show $Q$? Can we refute it?

Answerer: It's impossible to know that. Proof:...

-
I think this question is a duplicate. –  Quinn Culver Sep 27 '12 at 2:17
@QuinnCulver so I, but I can't find the post so far. –  leo Sep 27 '12 at 2:25

Yes. For every suitable theory (powerful enough to handle basic arithmetic) there is a statement $G$ in the language of that theory such that one can proof that no proof of $G$ exists. Moreover, $G$ is true, hence a proof of $\neg G$ should not exist either. However, one is not absolutely sure of the latter because one cannot prove satisfactorily that the theory is sound.

Look for Gödel and incompleteness theorem.

Actually, this is possibly not exactly what you talk about later in the dialog. The $G$ mentioned above is provably not provable and it is (assuming soundness of arithmetic) provably not refutable. Hence it is not possible to show that $G$ is provable and it is not possible to sow that $G$ is refutable (because it is impossible to show wrong things). But if the Asker asks: "Can we show $G$? Can we refute it?", the Answerer might reply "We know that we can'T" and not "It is impossible to know that". Do you really want this extra level of uncertainty or was that just a bad formulation?

In that case: Loosely speaking, $G$ is obtained by formalising "$x$ is a proof of $y$" and introducing Gödel numberings to make provabilty a question about arithmetic properties. Then comes diagonalization and one has

• a map $\Gamma$ from the set of formulas to $\mathbb N$
• a represented proof predicate $$P(a,b)=\Gamma^{-1}(a)\mathrm{\ is\ a\ proof\ of\ }\Gamma^{-1}(b)$$
• thus a represented theorem predicate $T(b)=\exists a\colon P(a,b)$
• a represented diagonalization $$D(a,b,n)=\Gamma^{-1}(a)\mathrm{\ is\ }\Gamma^{-1}(b)\mathrm{\ with\ all\ occurences\ of\ }x\mathrm{\ replaced\ by\ }\underbrace{ S\cdots S}_n0$$
• finally a represented predicate $$G_0(n)=\exists b\colon D(n,b,n)\land T(b)$$ The last step is to consider $n:=\Gamma(\neg G_0(x))$ and the statement $G:=G_0(n)$. With all reinterpretations, if $G$ is true, then $\neg G_0(n)$ is provable - contradiction. Hence $G$ is false and $\neg G=\neg G_0(n)$ is true but not provable.

Now replace $T$ ("provable") above with "decideable": $$T'(a)=T(a)\lor T(\Gamma(\neg\Gamma^{-1}(a))).$$ Does that help?

-
Yes, I want that extra level of uncertainly. It seems that you've understood correctly my question. It's quite complicated to formulate correctly what I want to know. The dialog was an attempt to do so. –  leo Sep 27 '12 at 0:44
We can even ask if there is a statement $G$ so that the question formulated in the post can be proved to be unanswerable, and so on, each time one level up. I wonder if is someone have been already worried about this kind of procces. –  leo Sep 27 '12 at 0:49
Let me think about it. –  leo Sep 27 '12 at 17:11