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:...
 A: 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?
A: 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.
A: 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.
