# Unprovable Post correspondence problem instance

Since there is no algorithm for the post correspondence problem, there exists an instance of this problem such that we can neither prove that the instance is positive nor prove that the instance is negative, i.e. an unprovable instance of this problem. Otherwise, for each instance, a proof that the instance is positive or a proof that the instance is negative exists and we could just use an algorithm which enumerates all the possible proofs until it finds such a proof, it always terminates and it correctly answers yes/no according to the proof found.

For finding such an instance, I pick a random instance, I try with a semi-decision procedure and, after some time, if this doesn't work, I try to prove that the instance is negative. Since this heuristic has always finished, I have not find such an instance until now, but it should be possible.

This is not specific to the Post correspondence problem, an unprovable instance should exist for all undecidable problems.

• Why do you think that we can find such an instance? How have you tried? – babou Mar 27 '15 at 17:57
• What notion of proof are you using here? – Klaus Draeger Mar 30 '15 at 10:47
• But first order logic is undecidable. – Pål GD Mar 30 '15 at 11:01
• Also check out this nice question from the Philosophy department: How can first order logic be complete but not decidable? – Pål GD Mar 30 '15 at 11:08
• "Since there is no algorithm for the post correspondence problem, there exists [...] an unprovable instance of this problem" -- core fallacy; I'm sure we have a duplicate dealing with the same "argument" for the halting problem. – Raphael Mar 31 '15 at 7:31

## 2 Answers

The argument you outline doesn't actually work. In fact, for any specific PCP instance, there is an algorithm which produces the right answer; it is either "output 'yes'" or "output 'no'". It is only when you require the algorithm to work for all the infinitely many instances that undecidability enters the picture (since an algorithm needs to be finite, you cannot just cobble together all the individual solutions).

Now it is true that given any particular PCP instance, you could just enumerate the potential solutions. The problem with this is that while for solvable instances, you will eventually find the solution, for (non-trivial) unsolvable ones, you will never get an answer. That is, what you have here is a semi-decision procedure.

I find an answer here :

https://math.stackexchange.com/questions/1214823/have-we-found-a-turing-machine-for-which-halting-non-halting-is-unprovable

Since we can encode turing machine in PCP, we can construct an instance such that we can neither prove that the instance is positive nor prove that the instance is negative.