The halting problem is in RE

The membership half of the RE machine line: acceptance of a Turing machine with no step bound and no space bound is definable in ∃SO[new] (DescriptiveComplexity.halt_sigmaSONewDefinable), the logic defining RE.

The mathematical content is DescriptiveComplexity.halt_iff_runRel: the machine accepts exactly when the invented values carry a run – two sorts with their orders, an input page, and the state, the head and the tape contents at each time point. This file is that statement written out in syntax:

• the invented values are the extension A ⊕ Fin m, m unbounded – the only difference from a Σ₁ definition, and what puts the problem beyond NP;
• the nine components of DescriptiveComplexity.TMData.RunRel are the relation variables of a single existential second-order block (DescriptiveComplexity.Halt.runBlock);
• every condition is a conjunct of the first-order kernel, with each quantifier guarded by its sort: time points and pages by ¬old, states, symbols and positions of the machine by old.

The corollary the file exists for is DescriptiveComplexity.halt_le_finsat: the halting problem first-order-reduces to finite satisfiability, which is Trakhtenbrot's theorem in the form it is usually stated. It needs no new hardness work – FINSAT is already RE-hard.

The second-order block

inductive DescriptiveComplexity.Halt.RunIx : Type

The relation variables of the ∃SO[new] definition of HALT: the two sorts of invented values with their orders, the input page, and the state, the head and the tape contents at each time point.

• time : RunIx

  The time points.

• tle : RunIx

  The order of time.

• page : RunIx

  The pages.

• ple : RunIx

  The order of the pages.

• zero : RunIx

  The input page.

• st : RunIx

  st t q: the state at the time point t.

• hdP : RunIx

  hdP t z: the page the head is on.

• hdC : RunIx

  hdC t p: the position within that page.

• sym : RunIx

  sym t z p a: the cell (z, p) holds a at the time point t.

@[instance_reducible]

instance DescriptiveComplexity.Halt.instDecidableEqRunIx : DecidableEq RunIx

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.Halt.instFintypeRunIx : Fintype RunIx

Equations

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

def DescriptiveComplexity.Halt.runBlock : 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.Halt.runLang : FirstOrder.Language

The vocabulary of the kernel: that of the instance, the marker old of the original elements, and the nine relation variables.

Equations

• DescriptiveComplexity.Halt.runLang = DescriptiveComplexity.soLang (DescriptiveComplexity.newLang FirstOrder.Language.turing) [DescriptiveComplexity.Halt.runBlock]

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.instSym {n : ℕ} (R : FirstOrder.Language.turing.Relations n) : runLang.Relations n

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

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.oldSym : runLang.Relations 1

The marker of the original elements, in the kernel's vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.timeSym : runLang.Relations 1

The relation variable of the time points.

Equations

• DescriptiveComplexity.Halt.timeSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.time, DescriptiveComplexity.Halt.timeSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.tleSym : runLang.Relations 2

The relation variable of the order of time.

Equations

• DescriptiveComplexity.Halt.tleSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.tle, DescriptiveComplexity.Halt.tleSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.pageSym : runLang.Relations 1

The relation variable of the pages.

Equations

• DescriptiveComplexity.Halt.pageSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.page, DescriptiveComplexity.Halt.pageSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.pleSym : runLang.Relations 2

The relation variable of the order of the pages.

Equations

• DescriptiveComplexity.Halt.pleSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.ple, DescriptiveComplexity.Halt.pleSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.zeroSym : runLang.Relations 1

The relation variable of the input page.

Equations

• DescriptiveComplexity.Halt.zeroSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.zero, DescriptiveComplexity.Halt.zeroSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.stSym : runLang.Relations 2

The relation variable of the state.

Equations

• DescriptiveComplexity.Halt.stSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.st, DescriptiveComplexity.Halt.stSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.hdPSym : runLang.Relations 2

The relation variable of the page of the head.

Equations

• DescriptiveComplexity.Halt.hdPSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.hdP, DescriptiveComplexity.Halt.hdPSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.hdCSym : runLang.Relations 2

The relation variable of the position of the head.

Equations

• DescriptiveComplexity.Halt.hdCSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.hdC, DescriptiveComplexity.Halt.hdCSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.symSym : runLang.Relations 4

The relation variable of the tape contents.

Equations

• DescriptiveComplexity.Halt.symSym = Sum.inr ⟨DescriptiveComplexity.Halt.RunIx.sym, DescriptiveComplexity.Halt.symSym._proof_1⟩

The extended universe

@[instance_reducible]

noncomputable def DescriptiveComplexity.Halt.extTuring {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} : FirstOrder.Language.turing.Structure (A ⊕ Fin m)

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

Equations

• DescriptiveComplexity.Halt.extTuring = DescriptiveComplexity.extBase FirstOrder.Language.turing A m

@[instance_reducible]

noncomputable def DescriptiveComplexity.Halt.certStr {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) : runLang.Structure (A ⊕ Fin m)

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

Equations

• DescriptiveComplexity.Halt.certStr ρ = (DescriptiveComplexity.newLang FirstOrder.Language.turing).sumStructure DescriptiveComplexity.Halt.runBlock.lang (A ⊕ Fin m)

The instance, read on the extended universe

theorem DescriptiveComplexity.Halt.relMap_inl {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m k : ℕ} (R : FirstOrder.Language.turing.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.Halt.relMap_inl₁ {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.turing.Relations 1) (a : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a] ↔ FirstOrder.Language.Structure.RelMap R ![a]

@[simp]

theorem DescriptiveComplexity.Halt.relMap_inl₂ {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.turing.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

The nine relation variables, read at the sorts they are meant for: the two sorts and their orders among the invented values, the state, the head and the tape contents across the two sorts.

def DescriptiveComplexity.Halt.certRun {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) : TMData.RunRel A (Fin m)

The run an assignment carries.

Equations

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

@[simp]

theorem DescriptiveComplexity.Halt.certRun_time {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t : Fin m) : (certRun ρ).Time t ↔ ρ RunIx.time ![Sum.inr t]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_tle {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t t' : Fin m) : (certRun ρ).TLe t t' ↔ ρ RunIx.tle ![Sum.inr t, Sum.inr t']

@[simp]

theorem DescriptiveComplexity.Halt.certRun_page {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (z : Fin m) : (certRun ρ).Page z ↔ ρ RunIx.page ![Sum.inr z]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_ple {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (z z' : Fin m) : (certRun ρ).PLe z z' ↔ ρ RunIx.ple ![Sum.inr z, Sum.inr z']

@[simp]

theorem DescriptiveComplexity.Halt.certRun_zero {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (z : Fin m) : (certRun ρ).Zero z ↔ ρ RunIx.zero ![Sum.inr z]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_st {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t : Fin m) (q : A) : (certRun ρ).St t q ↔ ρ RunIx.st ![Sum.inr t, Sum.inl q]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_hdP {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t z : Fin m) : (certRun ρ).HdP t z ↔ ρ RunIx.hdP ![Sum.inr t, Sum.inr z]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_hdC {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t : Fin m) (p : A) : (certRun ρ).HdC t p ↔ ρ RunIx.hdC ![Sum.inr t, Sum.inl p]

@[simp]

theorem DescriptiveComplexity.Halt.certRun_sym {A : Type} {m : ℕ} (ρ : runBlock.Assignment (A ⊕ Fin m)) (t z : Fin m) (p a : A) : (certRun ρ).Sym t z p a ↔ ρ RunIx.sym ![Sum.inr t, Sum.inr z, Sum.inl p, Sum.inl a]

Atomic formulas

noncomputable def DescriptiveComplexity.Halt.instF₁ {γ : Type} (R : FirstOrder.Language.turing.Relations 1) (x : γ) : runLang.Formula γ

An atom of a unary relation of the instance.

Equations

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

noncomputable def DescriptiveComplexity.Halt.instF₂ {γ : Type} (R : FirstOrder.Language.turing.Relations 2) (x y : γ) : runLang.Formula γ

An atom of a binary relation of the instance.

Equations

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

noncomputable def DescriptiveComplexity.Halt.oldF {γ : Type} (x : γ) : runLang.Formula γ

x is an original element.

Equations

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

noncomputable def DescriptiveComplexity.Halt.eqF {γ : Type} (x y : γ) : runLang.Formula γ

Equality of two variables.

Equations

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

noncomputable def DescriptiveComplexity.Halt.timeF {γ : Type} (x : γ) : runLang.Formula γ

x is a time point.

Equations

• DescriptiveComplexity.Halt.timeF x = DescriptiveComplexity.Halt.timeSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Halt.tleF {γ : Type} (x y : γ) : runLang.Formula γ

The time point x precedes y.

Equations

• DescriptiveComplexity.Halt.tleF x y = DescriptiveComplexity.Halt.tleSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Halt.pageF {γ : Type} (x : γ) : runLang.Formula γ

x is a page.

Equations

• DescriptiveComplexity.Halt.pageF x = DescriptiveComplexity.Halt.pageSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Halt.pleF {γ : Type} (x y : γ) : runLang.Formula γ

The page x precedes y.

Equations

• DescriptiveComplexity.Halt.pleF x y = DescriptiveComplexity.Halt.pleSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Halt.zeroF {γ : Type} (x : γ) : runLang.Formula γ

x is the input page.

Equations

• DescriptiveComplexity.Halt.zeroF x = DescriptiveComplexity.Halt.zeroSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Halt.stF {γ : Type} (t q : γ) : runLang.Formula γ

The state at the time point t is q.

Equations

• DescriptiveComplexity.Halt.stF t q = DescriptiveComplexity.Halt.stSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var q)

noncomputable def DescriptiveComplexity.Halt.hdPF {γ : Type} (t z : γ) : runLang.Formula γ

The head is on the page z at the time point t.

Equations

• DescriptiveComplexity.Halt.hdPF t z = DescriptiveComplexity.Halt.hdPSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var z)

noncomputable def DescriptiveComplexity.Halt.hdCF {γ : Type} (t p : γ) : runLang.Formula γ

The head is at the position p at the time point t.

Equations

• DescriptiveComplexity.Halt.hdCF t p = DescriptiveComplexity.Halt.hdCSym.formula₂ (FirstOrder.Language.var t) (FirstOrder.Language.var p)

noncomputable def DescriptiveComplexity.Halt.symF {γ : Type} (t z p a : γ) : runLang.Formula γ

The cell (z, p) holds a at the time point t.

Equations

• DescriptiveComplexity.Halt.symF t z p a = DescriptiveComplexity.Halt.symSym.formula ![FirstOrder.Language.var t, FirstOrder.Language.var z, FirstOrder.Language.var p, FirstOrder.Language.var a]

@[simp]

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

@[simp]

theorem DescriptiveComplexity.Halt.realize_instF₂ {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.turing.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.Halt.realize_oldF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (oldF x).Realize v ↔ IsOld (v x)

@[simp]

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

@[simp]

theorem DescriptiveComplexity.Halt.realize_timeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (timeF x).Realize v ↔ ρ RunIx.time ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_tleF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (tleF x y).Realize v ↔ ρ RunIx.tle ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_pageF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (pageF x).Realize v ↔ ρ RunIx.page ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_pleF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (pleF x y).Realize v ↔ ρ RunIx.ple ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_zeroF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (zeroF x).Realize v ↔ ρ RunIx.zero ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_stF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (t q : γ) (v : γ → A ⊕ Fin m) : (stF t q).Realize v ↔ ρ RunIx.st ![v t, v q]

@[simp]

theorem DescriptiveComplexity.Halt.realize_hdPF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (t z : γ) (v : γ → A ⊕ Fin m) : (hdPF t z).Realize v ↔ ρ RunIx.hdP ![v t, v z]

@[simp]

theorem DescriptiveComplexity.Halt.realize_hdCF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (t p : γ) (v : γ → A ⊕ Fin m) : (hdCF t p).Realize v ↔ ρ RunIx.hdC ![v t, v p]

@[simp]

theorem DescriptiveComplexity.Halt.realize_symF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (t z p a : γ) (v : γ → A ⊕ Fin m) : (symF t z p a).Realize v ↔ ρ RunIx.sym ![v t, v z, v p, v a]

Naming the symbols of the instance

noncomputable def DescriptiveComplexity.Halt.posnF {γ : Type} (x : γ) : runLang.Formula γ

Being a position.

Equations

• DescriptiveComplexity.Halt.posnF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmPosn x

noncomputable def DescriptiveComplexity.Halt.leF {γ : Type} (x y : γ) : runLang.Formula γ

The order on positions.

Equations

• DescriptiveComplexity.Halt.leF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmLe x y

noncomputable def DescriptiveComplexity.Halt.trF {γ : Type} (x : γ) : runLang.Formula γ

Being a transition.

Equations

• DescriptiveComplexity.Halt.trF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmTr x

noncomputable def DescriptiveComplexity.Halt.startF {γ : Type} (x : γ) : runLang.Formula γ

Being a start state.

Equations

• DescriptiveComplexity.Halt.startF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmStart x

noncomputable def DescriptiveComplexity.Halt.accF {γ : Type} (x : γ) : runLang.Formula γ

Being an accepting state.

Equations

• DescriptiveComplexity.Halt.accF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmAcc x

noncomputable def DescriptiveComplexity.Halt.blankF {γ : Type} (x : γ) : runLang.Formula γ

Being the blank symbol.

Equations

• DescriptiveComplexity.Halt.blankF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmBlank x

noncomputable def DescriptiveComplexity.Halt.rightF {γ : Type} (x : γ) : runLang.Formula γ

Moving the head right.

Equations

• DescriptiveComplexity.Halt.rightF x = DescriptiveComplexity.Halt.instF₁ FirstOrder.Language.tmRight x

noncomputable def DescriptiveComplexity.Halt.srcF {γ : Type} (x y : γ) : runLang.Formula γ

The state a transition applies in.

Equations

• DescriptiveComplexity.Halt.srcF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmSrc x y

noncomputable def DescriptiveComplexity.Halt.readF {γ : Type} (x y : γ) : runLang.Formula γ

The symbol a transition reads.

Equations

• DescriptiveComplexity.Halt.readF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmRead x y

noncomputable def DescriptiveComplexity.Halt.dstF {γ : Type} (x y : γ) : runLang.Formula γ

The state a transition moves to.

Equations

• DescriptiveComplexity.Halt.dstF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmDst x y

noncomputable def DescriptiveComplexity.Halt.writeF {γ : Type} (x y : γ) : runLang.Formula γ

The symbol a transition writes.

Equations

• DescriptiveComplexity.Halt.writeF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmWrite x y

noncomputable def DescriptiveComplexity.Halt.inpF {γ : Type} (x y : γ) : runLang.Formula γ

The initial contents of a cell.

Equations

• DescriptiveComplexity.Halt.inpF x y = DescriptiveComplexity.Halt.instF₂ FirstOrder.Language.tmInp x y

Guarded quantifiers

Every quantifier of the kernel ranges over one of the two sorts of the extended universe – the original elements, marked by old, and the invented values – and is guarded accordingly. A variable is named by its distance from its binder: vr0 is bound by the innermost guarded quantifier, vr1 by the one just outside it, and so on.

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The variable bound by the innermost guarded quantifier.

Equations

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

@[reducible, inline]

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

The variable bound one guarded quantifier further out.

Equations

• DescriptiveComplexity.Halt.vr1 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr0

@[reducible, inline]

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

The variable bound two guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr2 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr1

@[reducible, inline]

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

The variable bound three guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr3 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr2

@[reducible, inline]

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

The variable bound four guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr4 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr3

@[reducible, inline]

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

The variable bound five guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr5 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr4

@[reducible, inline]

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

The variable bound six guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr6 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr5

@[reducible, inline]

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

The variable bound seven guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr7 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr6

@[reducible, inline]

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

The variable bound eight guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr8 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr7

@[reducible, inline]

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

The variable bound nine guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr9 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr8

@[reducible, inline]

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

The variable bound ten guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr10 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr9

@[reducible, inline]

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

The variable bound eleven guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr11 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr10

@[reducible, inline]

abbrev DescriptiveComplexity.Halt.vr12 {γ : Type} : ((((((((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound twelve guarded quantifiers further out.

Equations

• DescriptiveComplexity.Halt.vr12 = DescriptiveComplexity.Halt.up DescriptiveComplexity.Halt.vr11

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

∃ x, old x ∧ φ: a quantifier over the original elements.

Equations

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

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

∀ x, old x → φ: a quantifier over the original elements.

Equations

• DescriptiveComplexity.Halt.allOldF φ = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.imp (DescriptiveComplexity.Halt.oldF DescriptiveComplexity.Halt.vr0) φ)

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

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

Equations

• DescriptiveComplexity.Halt.exNewF φ = FirstOrder.Language.Formula.iExs Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.Halt.oldF DescriptiveComplexity.Halt.vr0) ⊓ φ)

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

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

Equations

• DescriptiveComplexity.Halt.allNewF φ = FirstOrder.Language.Formula.iAlls Unit ((FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.Halt.oldF DescriptiveComplexity.Halt.vr0)).imp φ)

theorem DescriptiveComplexity.Halt.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.Halt.realize_exOldF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : runLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exOldF φ).Realize v ↔ ∃ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

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

@[simp]

theorem DescriptiveComplexity.Halt.realize_exNewF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : runLang.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.Halt.realize_allNewF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : runLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allNewF φ).Realize v ↔ ∀ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

Realization of the named symbols

@[simp]

theorem DescriptiveComplexity.Halt.realize_posnF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (posnF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_leF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (leF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_trF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (trF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmTr ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_startF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (startF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmStart ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_accF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (accF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmAcc ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_blankF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (blankF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmBlank ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_rightF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (rightF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmRight ![v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_srcF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (srcF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmSrc ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_readF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (readF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmRead ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_dstF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (dstF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmDst ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_writeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (writeF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmWrite ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Halt.realize_inpF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (inpF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmInp ![v x, v y]

Well-formedness

The kernel has to check well-formedness, since junk instances are no-instances: each conjunct of DescriptiveComplexity.TMData.WellFormed is one sentence, every quantifier ranging over the original elements.

noncomputable def DescriptiveComplexity.Halt.leReflS : runLang.Sentence

The order on positions is reflexive.

Equations

• DescriptiveComplexity.Halt.leReflS = DescriptiveComplexity.Halt.allOldF (DescriptiveComplexity.Halt.leF DescriptiveComplexity.Halt.vr0 DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.leTransS : runLang.Sentence

The order on positions is transitive.

Equations

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

noncomputable def DescriptiveComplexity.Halt.leAntisymmS : runLang.Sentence

The order on positions is antisymmetric.

Equations

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

noncomputable def DescriptiveComplexity.Halt.leTotalS : runLang.Sentence

The order on positions is total.

Equations

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

noncomputable def DescriptiveComplexity.Halt.posnExS : runLang.Sentence

There is a position.

Equations

• DescriptiveComplexity.Halt.posnExS = DescriptiveComplexity.Halt.exOldF (DescriptiveComplexity.Halt.posnF DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.inpFunS : runLang.Sentence

The input is functional.

Equations

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

noncomputable def DescriptiveComplexity.Halt.blankExS : runLang.Sentence

There is a blank symbol.

Equations

• DescriptiveComplexity.Halt.blankExS = DescriptiveComplexity.Halt.exOldF (DescriptiveComplexity.Halt.blankF DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.blankUniqS : runLang.Sentence

There is at most one blank symbol.

Equations

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

noncomputable def DescriptiveComplexity.Halt.wfS : runLang.Sentence

The machine is well-formed: the conjuncts of DescriptiveComplexity.TMData.WellFormed.

Equations

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

theorem DescriptiveComplexity.Halt.realize_wfS {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ wfS ↔ (tmData A).WellFormed

The shapes that repeat

MinPos, MaxPos and SuccPos occur over the positions of the machine and over each of the two guessed sorts; InitTape and DescriptiveComplexity.TMData.SuccCellRel occur inside the initial and the step clause. Each is a builder with one realization lemma, so that the conjuncts below stay readable and their proofs stay one simp only.

noncomputable def DescriptiveComplexity.Halt.minPosOldF {γ : Type} (x : γ) : runLang.Formula γ

A lowest position of the machine.

Equations

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

noncomputable def DescriptiveComplexity.Halt.maxPosOldF {γ : Type} (x : γ) : runLang.Formula γ

A highest position of the machine.

Equations

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

noncomputable def DescriptiveComplexity.Halt.succPosOldF {γ : Type} (x y : γ) : runLang.Formula γ

The next position of the machine.

Equations

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

noncomputable def DescriptiveComplexity.Halt.minTimeF {γ : Type} (x : γ) : runLang.Formula γ

A lowest time point.

Equations

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

noncomputable def DescriptiveComplexity.Halt.maxTimeF {γ : Type} (x : γ) : runLang.Formula γ

A highest time point.

Equations

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

noncomputable def DescriptiveComplexity.Halt.succTimeF {γ : Type} (x y : γ) : runLang.Formula γ

The next time point.

Equations

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

noncomputable def DescriptiveComplexity.Halt.succPageF {γ : Type} (x y : γ) : runLang.Formula γ

The next page.

Equations

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

noncomputable def DescriptiveComplexity.Halt.initTapeF {γ : Type} (p a : γ) : runLang.Formula γ

The cell p initially holds a.

Equations

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

noncomputable def DescriptiveComplexity.Halt.succCellF {γ : Type} (z p z' p' : γ) : runLang.Formula γ

The cell (z', p') is the next one after (z, p).

Equations

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

@[simp]

theorem DescriptiveComplexity.Halt.realize_minPosOldF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (minPosOldF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![v x] ∧ ∀ (a : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![Sum.inl a] → FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![v x, Sum.inl a]

@[simp]

theorem DescriptiveComplexity.Halt.realize_maxPosOldF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (maxPosOldF x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![v x] ∧ ∀ (a : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![Sum.inl a] → FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![Sum.inl a, v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_succPosOldF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (succPosOldF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![v x] ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![v y] ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![v x, v y] ∧ v x ≠ v y ∧ ∀ (a : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![Sum.inl a] → FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![v x, Sum.inl a] → FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![Sum.inl a, v y] → Sum.inl a = v x ∨ Sum.inl a = v y

@[simp]

theorem DescriptiveComplexity.Halt.realize_minTimeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (minTimeF x).Realize v ↔ ρ RunIx.time ![v x] ∧ ∀ (j : Fin m), ρ RunIx.time ![Sum.inr j] → ρ RunIx.tle ![v x, Sum.inr j]

@[simp]

theorem DescriptiveComplexity.Halt.realize_maxTimeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (maxTimeF x).Realize v ↔ ρ RunIx.time ![v x] ∧ ∀ (j : Fin m), ρ RunIx.time ![Sum.inr j] → ρ RunIx.tle ![Sum.inr j, v x]

@[simp]

theorem DescriptiveComplexity.Halt.realize_succTimeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (succTimeF x y).Realize v ↔ ρ RunIx.time ![v x] ∧ ρ RunIx.time ![v y] ∧ ρ RunIx.tle ![v x, v y] ∧ v x ≠ v y ∧ ∀ (j : Fin m), ρ RunIx.time ![Sum.inr j] → ρ RunIx.tle ![v x, Sum.inr j] → ρ RunIx.tle ![Sum.inr j, v y] → Sum.inr j = v x ∨ Sum.inr j = v y

@[simp]

theorem DescriptiveComplexity.Halt.realize_succPageF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (succPageF x y).Realize v ↔ ρ RunIx.page ![v x] ∧ ρ RunIx.page ![v y] ∧ ρ RunIx.ple ![v x, v y] ∧ v x ≠ v y ∧ ∀ (j : Fin m), ρ RunIx.page ![Sum.inr j] → ρ RunIx.ple ![v x, Sum.inr j] → ρ RunIx.ple ![Sum.inr j, v y] → Sum.inr j = v x ∨ Sum.inr j = v y

@[simp]

theorem DescriptiveComplexity.Halt.realize_initTapeF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (p a : γ) (v : γ → A ⊕ Fin m) : (initTapeF p a).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmInp ![v p, v a] ∨ (∀ (b : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmInp ![v p, Sum.inl b]) ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmBlank ![v a]

@[simp]

theorem DescriptiveComplexity.Halt.realize_succCellF {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} {γ : Type} (z p z' p' : γ) (v : γ → A ⊕ Fin m) : (succCellF z p z' p').Realize v ↔ v z' = v z ∧ (succPosOldF p p').Realize v ∨ (succPageF z z').Realize v ∧ (maxPosOldF p).Realize v ∧ (minPosOldF p').Realize v

The certificate: the shape conditions

One sentence per field of DescriptiveComplexity.TMData.RunRelOK, every quantifier guarded by its sort, and one realization lemma each so that the assembly below is a conjunction and nothing more.

noncomputable def DescriptiveComplexity.Halt.timeExS : runLang.Sentence

There is a time point.

Equations

• DescriptiveComplexity.Halt.timeExS = DescriptiveComplexity.Halt.exNewF (DescriptiveComplexity.Halt.timeF DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.tleLinS : runLang.Sentence

Time is linearly ordered.

Equations

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

noncomputable def DescriptiveComplexity.Halt.pageExS : runLang.Sentence

There is a page.

Equations

• DescriptiveComplexity.Halt.pageExS = DescriptiveComplexity.Halt.exNewF (DescriptiveComplexity.Halt.pageF DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.pleLinS : runLang.Sentence

The pages are linearly ordered.

Equations

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

noncomputable def DescriptiveComplexity.Halt.zeroExS : runLang.Sentence

There is an input page.

Equations

• DescriptiveComplexity.Halt.zeroExS = DescriptiveComplexity.Halt.exNewF (DescriptiveComplexity.Halt.zeroF DescriptiveComplexity.Halt.vr0)

noncomputable def DescriptiveComplexity.Halt.zeroPageS : runLang.Sentence

The input page is a page.

Equations

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

noncomputable def DescriptiveComplexity.Halt.zeroUniqS : runLang.Sentence

There is at most one input page.

Equations

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

noncomputable def DescriptiveComplexity.Halt.stTotS : runLang.Sentence

Every time point has a state.

Equations

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

noncomputable def DescriptiveComplexity.Halt.stFunS : runLang.Sentence

A time point has at most one state.

Equations

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

noncomputable def DescriptiveComplexity.Halt.hdPTotS : runLang.Sentence

At every time point the head is on a page.

Equations

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

noncomputable def DescriptiveComplexity.Halt.hdPFunS : runLang.Sentence

The head is on at most one page.

Equations

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

noncomputable def DescriptiveComplexity.Halt.hdCTotS : runLang.Sentence

At every time point the head is at a position.

Equations

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

noncomputable def DescriptiveComplexity.Halt.hdCFunS : runLang.Sentence

The head is at most at one position.

Equations

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

noncomputable def DescriptiveComplexity.Halt.symTotS : runLang.Sentence

Every cell holds a symbol at every time point.

Equations

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

noncomputable def DescriptiveComplexity.Halt.symFunS : runLang.Sentence

A cell holds at most one symbol.

Equations

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

The certificate: initial, step, accepting

The three conditions that say the data is a run. The step clause is the deep one: eight guarded quantifiers for the two time points and the configuration they relate, one more for the transition, and four more inside the frame condition – thirteen in all, which is why the variables are named by their distance from their binder.

noncomputable def DescriptiveComplexity.Halt.initS : runLang.Sentence

At the lowest time point the configuration is initial.

Equations

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

noncomputable def DescriptiveComplexity.Halt.stepS : runLang.Sentence

Along every step of the time order, one transition applies.

Equations

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

noncomputable def DescriptiveComplexity.Halt.accS : runLang.Sentence

At the highest time point the state is accepting.

Equations

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

The kernel

noncomputable def DescriptiveComplexity.Halt.certS : runLang.Sentence

The certificate: the eighteen conditions of DescriptiveComplexity.TMData.RunRelOK, conjoined.

Equations

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

noncomputable def DescriptiveComplexity.Halt.kernelS : runLang.Sentence

The kernel: the machine is well-formed and the invented values carry a run of it.

Equations

• DescriptiveComplexity.Halt.kernelS = DescriptiveComplexity.Halt.wfS ⊓ DescriptiveComplexity.Halt.certS

theorem DescriptiveComplexity.Halt.realize_certS {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ certS ↔ (tmData A).RunRelOK (certRun ρ)

theorem DescriptiveComplexity.Halt.realize_kernelS {A : Type} [FirstOrder.Language.turing.Structure A] [Nonempty A] {m : ℕ} {ρ : runBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ kernelS ↔ (tmData A).WellFormed ∧ (tmData A).RunRelOK (certRun ρ)

The assignment a run induces

The converse reading: a DescriptiveComplexity.TMData.RunRel becomes an assignment of the block by dispatching on the sort of each argument, so that reading it back is the identity definitionally – which is what makes DescriptiveComplexity.Halt.certRun_runAssign a rfl.

def DescriptiveComplexity.Halt.runAssign {A : Type} {m : ℕ} (c : TMData.RunRel A (Fin m)) : runBlock.Assignment (A ⊕ Fin m)

The assignment a run induces.

Equations

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

@[simp]

theorem DescriptiveComplexity.Halt.certRun_runAssign {A : Type} {m : ℕ} (c : TMData.RunRel A (Fin m)) : certRun (runAssign c) = c

The theorems

theorem DescriptiveComplexity.halt_sigmaSONewDefinable : SigmaSONewDefinable HALT

The halting problem is definable in ∃SO[new]: the invented values are the time points and the pages of an accepting run, and the kernel says that the machine is well-formed and that they carry one.

theorem DescriptiveComplexity.halt_mem_RE : RE.Mem HALT

The halting problem is in RE. A run is a finite object, but no function of the instance bounds it, which is exactly the difference between Σ₁ and ∃SO[new] – and between NP and RE.

theorem DescriptiveComplexity.halt_le_finsat : Nonempty (RelOrderedFOReduction HALT FINSAT)

The halting problem first-order-reduces to finite satisfiability: Trakhtenbrot's theorem in the form it is usually stated. It needs no new hardness work – DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable is already proved for an arbitrary source vocabulary, so putting a problem in RE reduces it to DescriptiveComplexity.FINSAT at once.