RE is exactly recursive enumerability

The three readings of the one construction of DescriptiveComplexity.Problems.CodeHalt.Hardness, the ordered first-order reduction of any semi-decidable problem to DescriptiveComplexity.CODEHALT.

• DescriptiveComplexity.codehalt_RE_complete – CODEHALT is RE-complete: membership is DescriptiveComplexity.codehalt_mem_RE, and hardness is the reduction instantiated at DescriptiveComplexity.FINSAT, which is RE-hard already, and transported forward.
• DescriptiveComplexity.mem_RE_iff_rePred – a decision problem is in the logically defined class DescriptiveComplexity.RE exactly when its concrete instances form a recursively enumerable set. This is the RE analogue of the machine side of Fagin's theorem, with no machine model on either side: the forward half evaluates the ∃SO[new] kernel on a searched-for witness (DescriptiveComplexity.RE_subset_rePred), the converse draws the semi-decision procedure inside the instance.
• DescriptiveComplexity.RE_ne_coRE – RE and co-RE differ, which the library used to disclaim twice. Were CODEHALTᶜ recursively enumerable, the equivalence above would make CODEHALT.toPred and its complement both REPred, hence computable by Post's theorem, against DescriptiveComplexity.not_computablePred_codehalt.

theorem DescriptiveComplexity.codehalt_RE_hard : RE.Hard CODEHALT

CODEHALT is RE-hard. Finite satisfiability is RE-hard and recursively enumerable, so it reduces to CODEHALT by the construction of DescriptiveComplexity.orderedReduction_codehalt, and hardness travels forward.

theorem DescriptiveComplexity.codehalt_RE_complete : RE.Complete CODEHALT

CODEHALT is RE-complete.

theorem DescriptiveComplexity.mem_RE_iff_rePred {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) (P : DecisionProblem L) : RE.Mem P ↔ REPred (P.toPred V)

RE is exactly the recursively enumerable properties of finite structures. A problem is ∃SO[new]-definable exactly when the set of its concrete instances is semi-decidable in Mathlib's sense.

theorem DescriptiveComplexity.RE_ne_coRE : RE ≠ coRE

RE is not closed under complement. With the equivalence above, this is Post's theorem applied to the undecidability of CODEHALT: a problem and its complement both recursively enumerable would be decidable.