Post's correspondence problem is RE-complete

The two halves meet: DescriptiveComplexity.HALT is RE-hard (DescriptiveComplexity.halt_RE_hard, the machine bridge) and reduces to DescriptiveComplexity.PCP by the computation-history dominoes (DescriptiveComplexity.halt_ordered_fo_reduction_pcp), so PCP is RE-hard; with membership (DescriptiveComplexity.pcp_mem_RE) it is RE-complete.

Undecidability of Post's problem (DescriptiveComplexity.pcp_not_computable) follows with no computability work of its own: RE-hardness makes the concrete instances a target of the code model's halting problem, and first-order reductions are computable.

theorem DescriptiveComplexity.pcp_RE_hard : RE.Hard PCP

PCP is RE-hard: the halting problem is, and its computation-history dominoes carry hardness forward.

theorem DescriptiveComplexity.pcp_RE_complete : RE.Complete PCP

PCP is RE-complete.

theorem DescriptiveComplexity.pcp_not_computable (V : FirstOrder.Language.pcp.FinVocab) : ¬ComputablePred (PCP.toPred V)

Post's correspondence problem is undecidable: no numbering of its instances has a computable characteristic function.