# 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

There are certainly true statements which cannot be proven true. For example, there are some algorithms which never terminate, but cannot be proven not to terminate. This is a consequence of the undecidability of the halting problem.

-
@AlexBexker This seems to involve a quantifier shift fallacy. The undecidability of he halting problem shows that that for any rich enough formal theory T there will be an algorithm which doesn't terminate such that T can't prove the true sentence which says it doesn't halt. It doesn't follow that there is some terminating algorithm such that no theory proves its non-termination. – Peter Smith Sep 26 '12 at 21:36
@PeterSmith I'm working in a fixed (but arbitrary, up to certain restrictions) theory. – Alex Becker Sep 26 '12 at 21:50
But then I doubt that addresses the OP's intended question, which seems to be wondering whether there are propositions we can show to be undecidable tout court (not just undecidable in this or that theory). – Peter Smith Sep 26 '12 at 22:02

In general, the big question is how do you define proof? If proof P1 proves, that Q is not provable, then P1 is only valid in a formal system S, on which P1 rests. Every proof of non-decidability contains in it the notion of proof. Outside formal systems (assuming this is really a valid concept), you have for example phenomena such as Heisenberg's uncertainty principle and Schrödinger's cat. Do we know for certain that these physical laws in the form of uncertainty principles are true? Note that a lot of modern physics and science in general is about modeling uncertainty through probability distributions or other means. I believe that it is possible that there might be new modes of computing which might render old conjectures and proofs about undecidability meaningless. I.e. one could imagine, that there is a new formal system or system of computation, such that old conjectures are no longer valid. I think the jury is still out on some of these questions with quantum computation for example.

-