# 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