The catalog's vocabularies, presented

The vocabularies of the two problems the machine bridge is about, exhibited as FirstOrder.Language.FinVocabs, and the concrete reading of DescriptiveComplexity.RE_subset_rePred at them:

• DescriptiveComplexity.halt_rePred – the halting problem, as a set of concrete machine instances, is recursively enumerable in Mathlib's sense;
• DescriptiveComplexity.finsat_rePred – likewise for finite satisfiability.

Both are instances of one theorem and neither needs anything problem-specific beyond listing the symbols of the vocabulary: this is the point of encoding structures once for the catalog rather than once per problem.

Neither statement says undecidable. That reading is supplied one file over, by DescriptiveComplexity.Computability.CodeHalt: a known-undecidable set – Mathlib's halting problem – maps computably into concrete instances of DescriptiveComplexity.CODEHALT, whence DescriptiveComplexity.finsat_not_computable, Trakhtenbrot's theorem outright. The hypothetical form kept here, DescriptiveComplexity.finsat_not_computable_of_halt, routes the same conclusion through the machine model instead; its hypothesis is supplied by DescriptiveComplexity.halt_not_computable.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSigmaNatRelationsTuring : DecidableEq ((n : ℕ) × FirstOrder.Language.turing.Relations n)

Equations

• DescriptiveComplexity.instDecidableEqSigmaNatRelationsTuring = DescriptiveComplexity.instDecidableEqSigmaNatRelationsTuring._aux_1

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSigmaNatRelationsFinsat : DecidableEq ((n : ℕ) × FirstOrder.Language.finsat.Relations n)

Equations

• DescriptiveComplexity.instDecidableEqSigmaNatRelationsFinsat = DescriptiveComplexity.instDecidableEqSigmaNatRelationsFinsat._aux_1

def DescriptiveComplexity.turingVocab : FirstOrder.Language.turing.FinVocab

The vocabulary of machine instances, presented: twelve symbols, six unary and six binary.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.finsatVocab : FirstOrder.Language.finsat.FinVocab

The vocabulary of first-order sentences as instances, presented: fourteen symbols of arity at most three.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.halt_rePred : REPred (HALT.toPred turingVocab)

The halting problem is recursively enumerable in Mathlib's sense, on the concrete machine instances of FirstOrder.Language.FinStruct.

This is DescriptiveComplexity.halt_mem_RE – a purely logical statement, an ∃SO[new] definition of acceptance – read through the encoding, with no machine model on either side.

theorem DescriptiveComplexity.finsat_rePred : REPred (FINSAT.toPred finsatVocab)

Finite satisfiability is recursively enumerable in Mathlib's sense: the easy half of Trakhtenbrot's theorem, on concrete instances.

theorem DescriptiveComplexity.finsat_not_computable_of_halt (h : ¬ComputablePred (HALT.toPred turingVocab)) : ¬ComputablePred (FINSAT.toPred finsatVocab)

Trakhtenbrot's theorem, through the halting link: if the halting problem is undecidable as a set of concrete machine instances, then finite satisfiability is undecidable too.

The reduction is DescriptiveComplexity.halt_le_finsat, which exists because FINSAT is RE-hard and HALT is in RE; that it is a computable many-one reduction of the induced sets is DescriptiveComplexity.not_computablePred_of_relOrderedReduction. The hypothesis is discharged by DescriptiveComplexity.halt_not_computable; the conditional form is kept because it is Trakhtenbrot's theorem in the shape it is usually stated – undecidability imported from the halting problem by a reduction.