CODEHALT is in RE

The syntax half of DescriptiveComplexity.CodeHalt.codehalt_iff_cert: the certificate of a halting computation is written as an ∃SO[new] sentence, the logic defining RE.

• the invented values are the numeral segment – no other sort is needed, so every quantifier of the kernel is guarded either by ¬old (a numeral) or by old (a node of the instance);
• the five components of DescriptiveComplexity.CodeHalt.Cert are the relation variables of a single existential second-order block (DescriptiveComplexity.CodeHalt.evBlock);
• the six conditions of DescriptiveComplexity.CodeHalt.CertOK are the conjuncts of the first-order kernel.

The deep conjunct is the justification of an evaluation fact (DescriptiveComplexity.CodeHalt.evOkS): eleven guarded quantifiers, which is why the variables are named by their distance from their binder, exactly as in DescriptiveComplexity.Problems.Machine.HaltMem.

The corollary the file exists for is DescriptiveComplexity.codehalt_le_finsat, and with it DescriptiveComplexity.finsat_not_computable: Trakhtenbrot's theorem, now with nothing left to assume.

The second-order block

inductive DescriptiveComplexity.CodeHalt.EvIx : Type

The relation variables of the ∃SO[new] definition of CODEHALT: the order of the numeral segment, addition and pairing on it, the code each node draws, and the value each code takes on each argument.

• le : EvIx

  The order of the numeral segment.

• add : EvIx

  Addition on the segment.

• pr : EvIx

  Cantor's pairing on the segment.

• dec : EvIx

  The number of the code a node draws.

• ev : EvIx

  The value a code takes on an argument.

@[instance_reducible]

instance DescriptiveComplexity.CodeHalt.instDecidableEqEvIx : DecidableEq EvIx

Equations

• DescriptiveComplexity.CodeHalt.instDecidableEqEvIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.CodeHalt.instFintypeEvIx : Fintype EvIx

Equations

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

def DescriptiveComplexity.CodeHalt.evBlock : SOBlock

The single existential block of the definition.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.certLang : FirstOrder.Language

The vocabulary the kernel is written in.

Equations

• DescriptiveComplexity.CodeHalt.certLang = DescriptiveComplexity.soLang (DescriptiveComplexity.newLang FirstOrder.Language.code) [DescriptiveComplexity.CodeHalt.evBlock]

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.instSym {n : ℕ} (R : FirstOrder.Language.code.Relations n) : certLang.Relations n

A relation symbol of the instance, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.CodeHalt.instSym R = Sum.inl (Sum.inl R)

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.oldSym : certLang.Relations 1

The symbol marking the original elements.

Equations

• DescriptiveComplexity.CodeHalt.oldSym = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.leSym : certLang.Relations 2

The order symbol.

Equations

• DescriptiveComplexity.CodeHalt.leSym = Sum.inr ⟨DescriptiveComplexity.CodeHalt.EvIx.le, DescriptiveComplexity.CodeHalt.leSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.addSym : certLang.Relations 3

The addition symbol.

Equations

• DescriptiveComplexity.CodeHalt.addSym = Sum.inr ⟨DescriptiveComplexity.CodeHalt.EvIx.add, DescriptiveComplexity.CodeHalt.addSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.prSym : certLang.Relations 3

The pairing symbol.

Equations

• DescriptiveComplexity.CodeHalt.prSym = Sum.inr ⟨DescriptiveComplexity.CodeHalt.EvIx.pr, DescriptiveComplexity.CodeHalt.prSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.decSym : certLang.Relations 2

The decoding symbol.

Equations

• DescriptiveComplexity.CodeHalt.decSym = Sum.inr ⟨DescriptiveComplexity.CodeHalt.EvIx.dec, DescriptiveComplexity.CodeHalt.decSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.evSym : certLang.Relations 3

The evaluation symbol.

Equations

• DescriptiveComplexity.CodeHalt.evSym = Sum.inr ⟨DescriptiveComplexity.CodeHalt.EvIx.ev, DescriptiveComplexity.CodeHalt.evSym._proof_1⟩

The extended universe

@[instance_reducible]

noncomputable def DescriptiveComplexity.CodeHalt.extCode {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} : FirstOrder.Language.code.Structure (A ⊕ Fin m)

The vocabulary of the instance, read on the extended universe.

Equations

• DescriptiveComplexity.CodeHalt.extCode = DescriptiveComplexity.extBase FirstOrder.Language.code A m

@[instance_reducible]

noncomputable def DescriptiveComplexity.CodeHalt.certStr {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) : certLang.Structure (A ⊕ Fin m)

The structure the kernel is read in: the extended structure together with an assignment of the relation variables.

Equations

• DescriptiveComplexity.CodeHalt.certStr ρ = (DescriptiveComplexity.newLang FirstOrder.Language.code).sumStructure DescriptiveComplexity.CodeHalt.evBlock.lang (A ⊕ Fin m)

theorem DescriptiveComplexity.CodeHalt.relMap_inl {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m k : ℕ} (R : FirstOrder.Language.code.Relations k) (y : Fin k → A) : (FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => Sum.inl (y i)) ↔ FirstOrder.Language.Structure.RelMap R y

@[simp]

theorem DescriptiveComplexity.CodeHalt.relMap_inl₁ {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.code.Relations 1) (a : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a] ↔ FirstOrder.Language.Structure.RelMap R ![a]

@[simp]

theorem DescriptiveComplexity.CodeHalt.relMap_inl₂ {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.code.Relations 2) (a b : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a, Sum.inl b] ↔ FirstOrder.Language.Structure.RelMap R ![a, b]

The certificate an assignment carries

def DescriptiveComplexity.CodeHalt.certOf {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) : Cert A (Fin m)

The certificate an assignment carries: the relation variables read at the sorts they are meant for.

Equations

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

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_le {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) (x y : Fin m) : (certOf ρ).Le x y ↔ ρ EvIx.le ![Sum.inr x, Sum.inr y]

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_add {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) (x y z : Fin m) : (certOf ρ).Add x y z ↔ ρ EvIx.add ![Sum.inr x, Sum.inr y, Sum.inr z]

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_pr {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) (a b p : Fin m) : (certOf ρ).Pr a b p ↔ ρ EvIx.pr ![Sum.inr a, Sum.inr b, Sum.inr p]

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_dec {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) (n : A) (e : Fin m) : (certOf ρ).Dec n e ↔ ρ EvIx.dec ![Sum.inl n, Sum.inr e]

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_ev {A : Type} {m : ℕ} (ρ : evBlock.Assignment (A ⊕ Fin m)) (e x v : Fin m) : (certOf ρ).Ev e x v ↔ ρ EvIx.ev ![Sum.inr e, Sum.inr x, Sum.inr v]

Atomic formulas

noncomputable def DescriptiveComplexity.CodeHalt.instF₁ {γ : Type} (R : FirstOrder.Language.code.Relations 1) (x : γ) : certLang.Formula γ

An atom of a unary relation of the instance.

Equations

• DescriptiveComplexity.CodeHalt.instF₁ R x = (DescriptiveComplexity.CodeHalt.instSym R).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.CodeHalt.instF₂ {γ : Type} (R : FirstOrder.Language.code.Relations 2) (x y : γ) : certLang.Formula γ

An atom of a binary relation of the instance.

Equations

• DescriptiveComplexity.CodeHalt.instF₂ R x y = (DescriptiveComplexity.CodeHalt.instSym R).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.CodeHalt.oldF {γ : Type} (x : γ) : certLang.Formula γ

x is an original element.

Equations

• DescriptiveComplexity.CodeHalt.oldF x = DescriptiveComplexity.CodeHalt.oldSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.CodeHalt.eqF {γ : Type} (x y : γ) : certLang.Formula γ

Equality of two variables.

Equations

• DescriptiveComplexity.CodeHalt.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.CodeHalt.leF {γ : Type} (x y : γ) : certLang.Formula γ

The numeral x is at most the numeral y.

Equations

• DescriptiveComplexity.CodeHalt.leF x y = DescriptiveComplexity.CodeHalt.leSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.CodeHalt.addF {γ : Type} (x y z : γ) : certLang.Formula γ

x + y = z.

Equations

• DescriptiveComplexity.CodeHalt.addF x y z = DescriptiveComplexity.CodeHalt.addSym.formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.CodeHalt.prF {γ : Type} (a b p : γ) : certLang.Formula γ

⟨a, b⟩ = p.

Equations

• DescriptiveComplexity.CodeHalt.prF a b p = DescriptiveComplexity.CodeHalt.prSym.formula ![FirstOrder.Language.var a, FirstOrder.Language.var b, FirstOrder.Language.var p]

noncomputable def DescriptiveComplexity.CodeHalt.decF {γ : Type} (n e : γ) : certLang.Formula γ

The node n draws the code numbered e.

Equations

• DescriptiveComplexity.CodeHalt.decF n e = DescriptiveComplexity.CodeHalt.decSym.formula₂ (FirstOrder.Language.var n) (FirstOrder.Language.var e)

noncomputable def DescriptiveComplexity.CodeHalt.evF {γ : Type} (e x v : γ) : certLang.Formula γ

The code numbered e returns v on x.

Equations

• DescriptiveComplexity.CodeHalt.evF e x v = DescriptiveComplexity.CodeHalt.evSym.formula ![FirstOrder.Language.var e, FirstOrder.Language.var x, FirstOrder.Language.var v]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_instF₁ {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.code.Relations 1) (x : γ) (v : γ → A ⊕ Fin m) : (instF₁ R x).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_instF₂ {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.code.Relations 2) (x y : γ) (v : γ → A ⊕ Fin m) : (instF₂ R x y).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x, v y]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_oldF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (oldF x).Realize v ↔ IsOld (v x)

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_eqF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_leF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (leF x y).Realize v ↔ ρ EvIx.le ![v x, v y]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_addF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y z : γ) (v : γ → A ⊕ Fin m) : (addF x y z).Realize v ↔ ρ EvIx.add ![v x, v y, v z]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_prF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (a b p : γ) (v : γ → A ⊕ Fin m) : (prF a b p).Realize v ↔ ρ EvIx.pr ![v a, v b, v p]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_decF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (n e : γ) (v : γ → A ⊕ Fin m) : (decF n e).Realize v ↔ ρ EvIx.dec ![v n, v e]

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_evF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (e x v' : γ) (v : γ → A ⊕ Fin m) : (evF e x v').Realize v ↔ ρ EvIx.ev ![v e, v x, v v']

Naming the symbols of the instance

noncomputable def DescriptiveComplexity.CodeHalt.crootF {γ : Type} (x : γ) : certLang.Formula γ

Being the root.

Equations

• DescriptiveComplexity.CodeHalt.crootF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cRoot x

noncomputable def DescriptiveComplexity.CodeHalt.czeroF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor zero.

Equations

• DescriptiveComplexity.CodeHalt.czeroF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cZero x

noncomputable def DescriptiveComplexity.CodeHalt.csuccF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor succ.

Equations

• DescriptiveComplexity.CodeHalt.csuccF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cSucc x

noncomputable def DescriptiveComplexity.CodeHalt.cleftF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor left.

Equations

• DescriptiveComplexity.CodeHalt.cleftF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cLeft x

noncomputable def DescriptiveComplexity.CodeHalt.crightF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor right.

Equations

• DescriptiveComplexity.CodeHalt.crightF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cRight x

noncomputable def DescriptiveComplexity.CodeHalt.cpairF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor pair.

Equations

• DescriptiveComplexity.CodeHalt.cpairF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cPair x

noncomputable def DescriptiveComplexity.CodeHalt.ccompF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor comp.

Equations

• DescriptiveComplexity.CodeHalt.ccompF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cComp x

noncomputable def DescriptiveComplexity.CodeHalt.cprecF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor prec.

Equations

• DescriptiveComplexity.CodeHalt.cprecF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cPrec x

noncomputable def DescriptiveComplexity.CodeHalt.crfindF {γ : Type} (x : γ) : certLang.Formula γ

Drawing the constructor rfind'.

Equations

• DescriptiveComplexity.CodeHalt.crfindF x = DescriptiveComplexity.CodeHalt.instF₁ FirstOrder.Language.cRfind x

noncomputable def DescriptiveComplexity.CodeHalt.carg1F {γ : Type} (x y : γ) : certLang.Formula γ

Being the first child.

Equations

• DescriptiveComplexity.CodeHalt.carg1F x y = DescriptiveComplexity.CodeHalt.instF₂ FirstOrder.Language.cArg1 x y

noncomputable def DescriptiveComplexity.CodeHalt.carg2F {γ : Type} (x y : γ) : certLang.Formula γ

Being the second child.

Equations

• DescriptiveComplexity.CodeHalt.carg2F x y = DescriptiveComplexity.CodeHalt.instF₂ FirstOrder.Language.cArg2 x y

Guarded quantifiers

Every quantifier of the kernel ranges over one of the two sorts of the extended universe – the nodes of the instance, marked by old, and the numerals – and is guarded accordingly. A variable is named by its distance from its binder.

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.up {γ : Type} (x : γ) : γ ⊕ Unit

A variable of the enclosing scope, seen from inside one guarded quantifier.

Equations

• DescriptiveComplexity.CodeHalt.up x = Sum.inl x

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr0 {γ : Type} : γ ⊕ Unit

The variable bound by the innermost guarded quantifier.

Equations

• DescriptiveComplexity.CodeHalt.vr0 = Sum.inr ()

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr1 {γ : Type} : (γ ⊕ Unit) ⊕ Unit

The variable bound one guarded quantifier further out.

Equations

• DescriptiveComplexity.CodeHalt.vr1 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr0

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr2 {γ : Type} : ((γ ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound two guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr2 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr1

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr3 {γ : Type} : (((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound three guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr3 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr2

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr4 {γ : Type} : ((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound four guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr4 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr3

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr5 {γ : Type} : (((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound five guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr5 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr4

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr6 {γ : Type} : ((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound six guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr6 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr5

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr7 {γ : Type} : (((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound seven guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr7 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr6

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr8 {γ : Type} : ((((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound eight guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr8 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr7

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr9 {γ : Type} : (((((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound nine guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr9 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr8

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr10 {γ : Type} : ((((((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound ten guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr10 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr9

@[reducible, inline]

abbrev DescriptiveComplexity.CodeHalt.vr11 {γ : Type} : (((((((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound eleven guarded quantifiers further out.

Equations

• DescriptiveComplexity.CodeHalt.vr11 = DescriptiveComplexity.CodeHalt.up DescriptiveComplexity.CodeHalt.vr10

noncomputable def DescriptiveComplexity.CodeHalt.exOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ x, old x ∧ φ: a quantifier over the nodes of the instance.

Equations

• DescriptiveComplexity.CodeHalt.exOldF φ = FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.CodeHalt.oldF DescriptiveComplexity.CodeHalt.vr0 ⊓ φ)

noncomputable def DescriptiveComplexity.CodeHalt.allOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ x, old x → φ: a quantifier over the nodes of the instance.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.exNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ d, ¬old d ∧ φ: a quantifier over the numerals.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.allNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ d, ¬old d → φ: a quantifier over the numerals.

Equations

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

theorem DescriptiveComplexity.CodeHalt.exists_inr_of_not_isOld {A : Type} {m : ℕ} {x : A ⊕ Fin m} (h : ¬IsOld x) : ∃ (j : Fin m), x = Sum.inr j

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_exOldF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exOldF φ).Realize v ↔ ∃ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_allOldF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allOldF φ).Realize v ↔ ∀ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_exNewF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exNewF φ).Realize v ↔ ∃ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

@[simp]

theorem DescriptiveComplexity.CodeHalt.realize_allNewF {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allNewF φ).Realize v ↔ ∀ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

The shapes that repeat

The order-theoretic shapes (IsZ, IsS, strictly below) and the arithmetic of a code's number, each a builder used many times below.

noncomputable def DescriptiveComplexity.CodeHalt.ltF {γ : Type} (x y : γ) : certLang.Formula γ

The numeral x is strictly below y.

Equations

• DescriptiveComplexity.CodeHalt.ltF x y = DescriptiveComplexity.CodeHalt.leF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.CodeHalt.eqF x y)

noncomputable def DescriptiveComplexity.CodeHalt.isZF {γ : Type} (x : γ) : certLang.Formula γ

x is the least numeral.

Equations

• DescriptiveComplexity.CodeHalt.isZF x = DescriptiveComplexity.CodeHalt.allNewF (DescriptiveComplexity.CodeHalt.leF (DescriptiveComplexity.CodeHalt.up x) DescriptiveComplexity.CodeHalt.vr0)

noncomputable def DescriptiveComplexity.CodeHalt.isSF {γ : Type} (x y : γ) : certLang.Formula γ

y is the numeral just above x.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.quadF {γ : Type} (p q : γ) : certLang.Formula γ

q is four times p.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.plus4F {γ : Type} (q e : γ) : certLang.Formula γ

e is q + 4.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.plus5F {γ : Type} (q e : γ) : certLang.Formula γ

e is q + 5.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.plus6F {γ : Type} (q e : γ) : certLang.Formula γ

e is q + 6.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.plus7F {γ : Type} (q e : γ) : certLang.Formula γ

e is q + 7.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isOneF {γ : Type} (e : γ) : certLang.Formula γ

e is the numeral 1.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isTwoF {γ : Type} (e : γ) : certLang.Formula γ

e is the numeral 2.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isThreeF {γ : Type} (e : γ) : certLang.Formula γ

e is the numeral 3.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isPairEF {γ : Type} (e e₁ e₂ : γ) : certLang.Formula γ

e numbers the code pair e₁ e₂.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isPrecEF {γ : Type} (e e₁ e₂ : γ) : certLang.Formula γ

e numbers the code prec e₁ e₂.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isCompEF {γ : Type} (e e₁ e₂ : γ) : certLang.Formula γ

e numbers the code comp e₁ e₂.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.isRfindEF {γ : Type} (e e₁ : γ) : certLang.Formula γ

e numbers the code rfind' e₁.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.nextPRF {γ : Type} (a' b' a b : γ) : certLang.Formula γ

(a, b) is the pair enumerated just after (a', b').

Equations

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

The order of the numeral segment

noncomputable def DescriptiveComplexity.CodeHalt.leReflS : certLang.Sentence

The order is reflexive.

Equations

• DescriptiveComplexity.CodeHalt.leReflS = DescriptiveComplexity.CodeHalt.allNewF (DescriptiveComplexity.CodeHalt.leF DescriptiveComplexity.CodeHalt.vr0 DescriptiveComplexity.CodeHalt.vr0)

noncomputable def DescriptiveComplexity.CodeHalt.leTransS : certLang.Sentence

The order is transitive.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.leAntisymmS : certLang.Sentence

The order is antisymmetric.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.leTotalS : certLang.Sentence

The order is total.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.linS : certLang.Sentence

The numeral segment is linearly ordered.

Equations

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

The justification rules

noncomputable def DescriptiveComplexity.CodeHalt.addOkS : certLang.Sentence

Every addition fact is justified by the recurrence.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.prOkS : certLang.Sentence

Every pairing fact is justified by the successor rule.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.decOkS : certLang.Sentence

Every decoding fact is justified by the node's mark and its children.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.evOkS : certLang.Sentence

Every evaluation fact is justified by the rules of its code.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.rootS : certLang.Sentence

The root draws a code that returns something on 0.

Equations

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

noncomputable def DescriptiveComplexity.CodeHalt.kernelS : certLang.Sentence

The kernel: the invented values carry a halting computation.

Equations

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

What the kernel says

theorem DescriptiveComplexity.CodeHalt.realize_kernelS {A : Type} [FirstOrder.Language.code.Structure A] [Nonempty A] {m : ℕ} {ρ : evBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ kernelS ↔ CertOK (certOf ρ)

The assignment a certificate induces

Read back by DescriptiveComplexity.CodeHalt.certOf, this is the identity definitionally, which is what makes the round trip a rfl.

def DescriptiveComplexity.CodeHalt.certAssign {A : Type} {m : ℕ} (c : Cert A (Fin m)) : evBlock.Assignment (A ⊕ Fin m)

The assignment a certificate induces.

Equations

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

@[simp]

theorem DescriptiveComplexity.CodeHalt.certOf_certAssign {A : Type} {m : ℕ} (c : Cert A (Fin m)) : certOf (certAssign c) = c

The theorems

theorem DescriptiveComplexity.codehalt_sigmaSONewDefinable : SigmaSONewDefinable CODEHALT

CODEHALT is definable in ∃SO[new]: the invented values are the numeral segment of a halting computation of the code the root draws, and the kernel says that they carry one.

theorem DescriptiveComplexity.codehalt_mem_RE : RE.Mem CODEHALT

CODEHALT is in RE. The certificate is the whole computation of the drawn code – its numbers, its pairings and its intermediate values – which is a finite object, but no function of the instance bounds it: that is exactly the difference between Σ₁ and ∃SO[new], and between NP and RE.

theorem DescriptiveComplexity.codehalt_le_finsat : Nonempty (RelOrderedFOReduction CODEHALT FINSAT)

CODEHALT first-order-reduces to finite satisfiability. No new hardness work is needed: DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable is proved for an arbitrary source vocabulary, so putting a problem in RE reduces it to DescriptiveComplexity.FINSAT at once.