RE is recursively enumerable

DescriptiveComplexity.RE_subset_rePred: a problem in the logically defined class DescriptiveComplexity.RE denotes, through the encoding of FirstOrder.Language.FinStruct, an REPred in the sense of Mathlib's computability layer. It is what makes the name of the class a theorem rather than a convention, and it needs no machine model at all.

The argument

∃SO[new]-definability says

P A ↔ ∃ m : ℕ, ∃ ρ : B.Assignment (A ⊕ Fin m), φ holds in the extended structure

with φ a fixed first-order sentence. Both existentials are absorbed into a single unbounded search over a Primcodable witness: the number m of invented values, and a list of Boolean tables standing for the assignment ρ. Given the witness, the extended structure is built as data (DescriptiveComplexity.extStruct) and φ is evaluated on it by the primitive recursive evaluator of DescriptiveComplexity.Computability.Eval. Unbounded search over a decidable test is exactly REPred.

Two facts carry the proof:

• every list of Booleans denotes an assignment and every assignment is denoted by one (DescriptiveComplexity.exists_tab), because the extended universe is finite – this is where the certificate being a finite object is used;
• the structure built from the witness is isomorphic to the extended structure of the logic (DescriptiveComplexity.extIso), so the fixed sentence says the same thing about both.

The converse

That every REPred is in RE is proved one layer up, in DescriptiveComplexity.Computability.CodeHaltComplete (DescriptiveComplexity.mem_RE_iff_rePred). It needs a target whose programs already exist, so that the reduction can draw a semi-decision procedure inside the instance rather than build one.

Unbounded search over a coded witness

theorem DescriptiveComplexity.rePred_of_exists {α β : Type} [Primcodable α] [Primcodable β] {p : α → Prop} {f : α → β → Bool} (hf : Primrec₂ f) (h : ∀ (a : α), p a ↔ ∃ (b : β), f a b = true) : REPred p

A predicate found by unbounded search over a coded witness is recursively enumerable. The witness type is any Primcodable type; the search is Mathlib's Nat.rfind over its codes.

The vocabularies of the second-order machinery

def DescriptiveComplexity.oldVocab : FirstOrder.Language.oldMark.FinVocab

The one-symbol vocabulary marking the original elements, presented.

Equations

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

noncomputable def DescriptiveComplexity.blockNum (B : SOBlock) : ℕ

The number of relation variables of a block.

Equations

• DescriptiveComplexity.blockNum B = ⋯.choose

noncomputable def DescriptiveComplexity.blockEq (B : SOBlock) : Fin (blockNum B) ≃ B.ι

A numbering of the relation variables of a block.

Equations

• DescriptiveComplexity.blockEq B = ⋯.some.symm

noncomputable def DescriptiveComplexity.blockVocab (B : SOBlock) : B.lang.FinVocab

The vocabulary of a second-order quantifier block, presented: one symbol per relation variable.

Equations

• DescriptiveComplexity.blockVocab B = FirstOrder.Language.FinVocab.ofEquivSigma (DescriptiveComplexity.blockNum B) ((DescriptiveComplexity.blockEq B).trans (Equiv.sigmaFiberEquiv B.arity).symm)

theorem DescriptiveComplexity.index_blockVocab (B : SOBlock) {n : ℕ} (r : B.lang.Relations n) : (blockVocab B).index r = (blockEq B).symm ↑r

noncomputable def DescriptiveComplexity.soVocab {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) : ((newLang L).sum B.lang).FinVocab

The vocabulary an ∃SO[new] kernel is read over: the instance's, the mark of the original elements, and the block's.

Equations

• DescriptiveComplexity.soVocab V B = (V.sum DescriptiveComplexity.oldVocab).sum (DescriptiveComplexity.blockVocab B)

The extended structure, as data

def DescriptiveComplexity.extEquivFin {L : FirstOrder.Language} {V : L.FinVocab} (s : FirstOrder.Language.FinStruct V) (m : ℕ) : s.Univ ⊕ Fin m ≃ Fin (s.univSize + m + 1)

The numbering of the extended universe: the instance first, the invented values after it.

Equations

• DescriptiveComplexity.extEquivFin s m = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem DescriptiveComplexity.val_extEquivFin_inl {L : FirstOrder.Language} {V : L.FinVocab} (s : FirstOrder.Language.FinStruct V) (m : ℕ) (a : s.Univ) : ↑((extEquivFin s m) (Sum.inl a)) = ↑a

@[simp]

theorem DescriptiveComplexity.val_extEquivFin_inr {L : FirstOrder.Language} {V : L.FinVocab} (s : FirstOrder.Language.FinStruct V) (m : ℕ) (j : Fin m) : ↑((extEquivFin s m) (Sum.inr j)) = s.card + ↑j

theorem DescriptiveComplexity.val_extEquivFin_lt {L : FirstOrder.Language} {V : L.FinVocab} (s : FirstOrder.Language.FinStruct V) (m : ℕ) (y : s.Univ ⊕ Fin m) : ↑((extEquivFin s m) y) < s.card ↔ ∃ (a : s.Univ), y = Sum.inl a

noncomputable def DescriptiveComplexity.extRel {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) {n : ℕ} : ((newLang L).sum B.lang).Relations n → (Fin n → Fin (s.univSize + m + 1)) → Bool

The relations of the extended structure, read off the instance and the guessed table: an original symbol holds of a tuple of original elements exactly where it holds in the instance, the mark holds of the original elements, and a relation variable reads its guessed table.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.extRel V B s m tab (Sum.inl (Sum.inr FirstOrder.Language.oldRel.old)) x_3 = decide (↑(x_3 0) < s.card)

@[simp]

theorem DescriptiveComplexity.extRel_inl_inl {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) {n : ℕ} (r : L.Relations n) (x : Fin n → Fin (s.univSize + m + 1)) : extRel V B s m tab (Sum.inl (Sum.inl r)) x = (FirstOrder.Language.andAll (List.ofFn fun (j : Fin n) => decide (↑(x j) < s.card)) && (s.table.getD ↑(V.index r) []).getD (FirstOrder.Language.tupleIdx s.card (List.ofFn fun (j : Fin n) => ↑(x j))) false)

theorem DescriptiveComplexity.oldArity {n : ℕ} : ∀ (a : FirstOrder.Language.oldMark.Relations n), n = 1

The only symbol of the marking vocabulary has arity one.

@[simp]

theorem DescriptiveComplexity.extRel_old {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) (x : Fin 1 → Fin (s.univSize + m + 1)) : extRel V B s m tab (Sum.inl (Sum.inr FirstOrder.Language.oldSym)) x = decide (↑(x 0) < s.card)

@[simp]

theorem DescriptiveComplexity.extRel_inr {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) {n : ℕ} (br : B.lang.Relations n) (x : Fin n → Fin (s.univSize + m + 1)) : extRel V B s m tab (Sum.inr br) x = (tab.getD ↑((blockVocab B).index br) []).getD (FirstOrder.Language.tupleIdx (s.univSize + m + 1) (List.ofFn fun (j : Fin n) => ↑(x j))) false

theorem DescriptiveComplexity.extRel_old_eq {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) {n : ℕ} (o : FirstOrder.Language.oldMark.Relations n) (x : Fin n → Fin (s.univSize + m + 1)) : extRel V B s m tab (Sum.inl (Sum.inr o)) x = decide (↑(x (Fin.cast ⋯ 0)) < s.card)

noncomputable def DescriptiveComplexity.extStruct {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) : FirstOrder.Language.FinStruct (soVocab V B)

The extended structure as data: the instance, m invented values, and the guessed relations, encoded as one concrete finite structure over the vocabulary the ∃SO[new] kernel is read in.

Equations

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

@[simp]

theorem DescriptiveComplexity.relMapBool_extStruct {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) {n : ℕ} (R : ((newLang L).sum B.lang).Relations n) (x : Fin n → (extStruct V B s m tab).Univ) : (extStruct V B s m tab).relMapBool R x = extRel V B s m tab R x

def DescriptiveComplexity.tabAssign {L : FirstOrder.Language} {V : L.FinVocab} (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) : B.Assignment (s.Univ ⊕ Fin m)

The assignment of the relation variables a guessed table denotes.

Equations

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

The data is the extended structure of the logic

theorem DescriptiveComplexity.ofFn_extEquivFin {L : FirstOrder.Language} {V : L.FinVocab} {n : ℕ} (s : FirstOrder.Language.FinStruct V) (m : ℕ) {x : Fin n → s.Univ ⊕ Fin m} {y : Fin n → s.Univ} (hy : ∀ (j : Fin n), x j = Sum.inl (y j)) : (List.ofFn fun (j : Fin n) => ↑((extEquivFin s m) (x j))) = List.ofFn fun (j : Fin n) => ↑(y j)

The tuple of values of an original tuple.

theorem DescriptiveComplexity.extRel_inl_inl_iff {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) (r : L.Relations n) (x : Fin n → s.Univ ⊕ Fin m) : (extRel V B s m tab (Sum.inl (Sum.inl r)) fun (j : Fin n) => (extEquivFin s m) (x j)) = true ↔ ∃ (y : Fin n → s.Univ), (∀ (j : Fin n), x j = Sum.inl (y j)) ∧ FirstOrder.Language.Structure.RelMap r y

The original symbols of the extended structure read the instance, on original elements only.

noncomputable def DescriptiveComplexity.extIso {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (tab : List (List Bool)) : ((newLang L).sum B.lang).Equiv (s.Univ ⊕ Fin m) (extStruct V B s m tab).Univ

The extended structure as data is the extended structure of the logic: the numbering of DescriptiveComplexity.extEquivFin is an isomorphism, for the assignment the guessed table denotes.

Equations

• DescriptiveComplexity.extIso V B s m tab = { toEquiv := DescriptiveComplexity.extEquivFin s m, map_fun' := ⋯, map_rel' := ⋯ }

Every assignment is denoted by a table

The extended universe is finite, so an assignment of the relation variables is a finite object: it is the reading of some list of Boolean tables. This is the step that turns the second-order existential of ∃SO[new] into a search over a Primcodable witness.

theorem DescriptiveComplexity.exists_tab {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) (s : FirstOrder.Language.FinStruct V) (m : ℕ) (ρ : B.Assignment (s.Univ ⊕ Fin m)) : ∃ (tab : List (List Bool)), tabAssign B s m tab = ρ

The witness is read primitive recursively

theorem DescriptiveComplexity.primrec_extStruct {L : FirstOrder.Language} (V : L.FinVocab) (B : SOBlock) : Primrec fun (p : FirstOrder.Language.FinStruct V × ℕ × List (List Bool)) => extStruct V B p.1 p.2.1 p.2.2

The theorem

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

A recursively enumerable problem denotes a recursively enumerable set of concrete instances. The class DescriptiveComplexity.RE is defined by a logic – definability in ∃SO[new] – and this is the statement that the name is honest: through the encoding of FirstOrder.Language.FinStruct, its problems are exactly semi-decidable in Mathlib's sense.

No machine model is involved. The ∃SO[new] witness – a number of invented values and an assignment of the relation variables – is a finite object, so it is searched for; the first-order kernel is checked on it by the primitive recursive evaluator of DescriptiveComplexity.Computability.Eval.