The halting problem is RE-complete

DescriptiveComplexity.orderedReduction_halt: every decision problem whose concrete instances form a recursively enumerable set reduces to DescriptiveComplexity.HALT by an ordered first-order reduction – the machine bridge for RE, at the machine model. The reduction draws the fixed simulating machine of DescriptiveComplexity.HaltHard.simTM – whose states, symbols and transitions are tags, free at every instance size – together with the instance's own relation tables as the chain of one-bit comp frames on the initial tape (DescriptiveComplexity.HaltHard.inputChain).

With membership (DescriptiveComplexity.halt_mem_RE), this makes HALT RE-complete (DescriptiveComplexity.halt_RE_complete): the machine model now states “RE is the class of semi-decidable problems” alongside the code model (DescriptiveComplexity.codehalt_RE_complete).

theorem DescriptiveComplexity.orderedReduction_halt {L : FirstOrder.Language} [L.IsRelational] {V : L.FinVocab} (P : DecisionProblem L) (h : REPred (P.toPred V)) : Nonempty (OrderedFOReduction P HALT)

A semi-decidable problem reduces to HALT. The reduction draws the fixed simulating machine – Turing.ToPartrec.Code.exists_code supplies its fold and semi-decision codes – and spells the instance's bit table as the input chain on the initial tape.

theorem DescriptiveComplexity.halt_RE_hard : RE.Hard HALT

HALT is RE-hard. Finite satisfiability is RE-hard and recursively enumerable, so it reduces to HALT, and hardness travels forward.

theorem DescriptiveComplexity.halt_RE_complete : RE.Complete HALT

HALT is RE-complete.

theorem DescriptiveComplexity.halt_not_computable (V' : FirstOrder.Language.turing.FinVocab) : ¬ComputablePred (HALT.toPred V')

The halting problem is undecidable, in the concrete sense: no numbering of its instances has a computable characteristic function.