Machine acceptance is existential second-order definable

The membership half of the machine bridge: NTMAccept is Σ₁-definable, hence in NP. This is Fagin's tableau argument, and – unlike the certificate of a weighted problem – it needs no arithmetic at all: one existential block guesses the run, and a first-order kernel checks it clause by clause.

What is guessed

Three relation variables, indexed by the positions, which are simultaneously the tape cells and the time steps:

• Q t q – at time t the machine is in state q;
• H t p – at time t the head is on the cell p;
• T t p a – at time t the cell p holds the symbol a.

That the guess is a run is exactly DescriptiveComplexity.TMData.RelWalk, and DescriptiveComplexity.TMData.exists_relWalk_iff_exists_walk together with DescriptiveComplexity.TMData.accepts_iff_exists_walk is what connects it back to acceptance. So this file is a transcription: every clause below mirrors one field of RelWalk or one conjunct of DescriptiveComplexity.TMData.WellFormed, and each has its own realization lemma. Nothing here does mathematics; the mathematics is in DescriptiveComplexity.Problems.Machine.Walk.

The clauses

Seventeen of them, conjoined into DescriptiveComplexity.tqKernel: four saying the order is linear, four more for the remaining promises of WellFormed, six for the functionality of the guess, then the initial clause, the step clause and the accepting clause. The step clause is the largest formula in the library – an existential over a transition element with seven conjuncts, against a stutter alternative – and is kept manageable by parameterizing its body (DescriptiveComplexity.tqStepBodyF) over the three variables it reads, so that no Sum nesting goes deeper than two levels.

The order predicates

MinPos, MaxPos and SuccPos are relativized to the positions, so they are not the ordered-structure guards of DescriptiveComplexity.OrderWalk but formulas over the instance's own le and posn symbols, defined here as DescriptiveComplexity.tqMinPosF and friends.

The block

inductive DescriptiveComplexity.TMIdx : Type

The relation variables of the certificate: the state, the head and the tape of the configuration at each time.

• state : TMIdx

  The state at a time.

• head : TMIdx

  The head cell at a time.

• tape : TMIdx

  The tape contents at a time.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqTMIdx : DecidableEq TMIdx

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeTMIdx : Fintype TMIdx

Equations

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

def DescriptiveComplexity.tmGuessBlock : SOBlock

The single existential block: the run, guessed as a state, a head position and a tape contents for each time.

Equations

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

def DescriptiveComplexity.tqStateRel : tmGuessBlock.lang.Relations 2

The symbol of the state relation variable.

Equations

• DescriptiveComplexity.tqStateRel = ⟨DescriptiveComplexity.TMIdx.state, DescriptiveComplexity.tqStateRel._proof_1⟩

def DescriptiveComplexity.tqHeadRel : tmGuessBlock.lang.Relations 2

The symbol of the head relation variable.

Equations

• DescriptiveComplexity.tqHeadRel = ⟨DescriptiveComplexity.TMIdx.head, DescriptiveComplexity.tqHeadRel._proof_1⟩

def DescriptiveComplexity.tqTapeRel : tmGuessBlock.lang.Relations 3

The symbol of the tape relation variable.

Equations

• DescriptiveComplexity.tqTapeRel = ⟨DescriptiveComplexity.TMIdx.tape, DescriptiveComplexity.tqTapeRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.tqSOLang : FirstOrder.Language

The vocabulary of the kernel: machine instances together with the guessed run.

Equations

• DescriptiveComplexity.tqSOLang = FirstOrder.Language.turing.sum DescriptiveComplexity.tmGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.tqPosnSym : tqSOLang.Relations 1

The position symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqPosnSym = Sum.inl FirstOrder.Language.tmPosn

@[reducible, inline]

abbrev DescriptiveComplexity.tqTrSym : tqSOLang.Relations 1

The transition symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqTrSym = Sum.inl FirstOrder.Language.tmTr

@[reducible, inline]

abbrev DescriptiveComplexity.tqStartSym : tqSOLang.Relations 1

The start-state symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqStartSym = Sum.inl FirstOrder.Language.tmStart

@[reducible, inline]

abbrev DescriptiveComplexity.tqAccSym : tqSOLang.Relations 1

The accepting-state symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqAccSym = Sum.inl FirstOrder.Language.tmAcc

@[reducible, inline]

abbrev DescriptiveComplexity.tqBlankSym : tqSOLang.Relations 1

The blank symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqBlankSym = Sum.inl FirstOrder.Language.tmBlank

@[reducible, inline]

abbrev DescriptiveComplexity.tqRightSym : tqSOLang.Relations 1

The move-right symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqRightSym = Sum.inl FirstOrder.Language.tmRight

@[reducible, inline]

abbrev DescriptiveComplexity.tqLeSym : tqSOLang.Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqLeSym = Sum.inl FirstOrder.Language.tmLe

@[reducible, inline]

abbrev DescriptiveComplexity.tqSrcSym : tqSOLang.Relations 2

The transition-source symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqSrcSym = Sum.inl FirstOrder.Language.tmSrc

@[reducible, inline]

abbrev DescriptiveComplexity.tqReadSym : tqSOLang.Relations 2

The transition-read symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqReadSym = Sum.inl FirstOrder.Language.tmRead

@[reducible, inline]

abbrev DescriptiveComplexity.tqDstSym : tqSOLang.Relations 2

The transition-destination symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqDstSym = Sum.inl FirstOrder.Language.tmDst

@[reducible, inline]

abbrev DescriptiveComplexity.tqWriteSym : tqSOLang.Relations 2

The transition-write symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqWriteSym = Sum.inl FirstOrder.Language.tmWrite

@[reducible, inline]

abbrev DescriptiveComplexity.tqInpSym : tqSOLang.Relations 2

The input symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqInpSym = Sum.inl FirstOrder.Language.tmInp

@[reducible, inline]

abbrev DescriptiveComplexity.tqStateSym : tqSOLang.Relations 2

The guessed-state symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqStateSym = Sum.inr DescriptiveComplexity.tqStateRel

@[reducible, inline]

abbrev DescriptiveComplexity.tqHeadSym : tqSOLang.Relations 2

The guessed-head symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqHeadSym = Sum.inr DescriptiveComplexity.tqHeadRel

@[reducible, inline]

abbrev DescriptiveComplexity.tqTapeSym : tqSOLang.Relations 3

The guessed-tape symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.tqTapeSym = Sum.inr DescriptiveComplexity.tqTapeRel

Formula builders

def DescriptiveComplexity.tqPosnF {α : Type} (x : α) : tqSOLang.Formula α

x is a position, as a formula.

Equations

• DescriptiveComplexity.tqPosnF x = DescriptiveComplexity.tqPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqTrF {α : Type} (x : α) : tqSOLang.Formula α

x is a transition, as a formula.

Equations

• DescriptiveComplexity.tqTrF x = DescriptiveComplexity.tqTrSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqStartF {α : Type} (x : α) : tqSOLang.Formula α

x is a start state, as a formula.

Equations

• DescriptiveComplexity.tqStartF x = DescriptiveComplexity.tqStartSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqAccF {α : Type} (x : α) : tqSOLang.Formula α

x is an accepting state, as a formula.

Equations

• DescriptiveComplexity.tqAccF x = DescriptiveComplexity.tqAccSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqBlankF {α : Type} (x : α) : tqSOLang.Formula α

x is the blank symbol, as a formula.

Equations

• DescriptiveComplexity.tqBlankF x = DescriptiveComplexity.tqBlankSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqRightF {α : Type} (x : α) : tqSOLang.Formula α

x moves the head right, as a formula.

Equations

• DescriptiveComplexity.tqRightF x = DescriptiveComplexity.tqRightSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.tqLeF {α : Type} (x y : α) : tqSOLang.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.tqLeF x y = DescriptiveComplexity.tqLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqEqF {α : Type} (x y : α) : tqSOLang.Formula α

x = y, as a formula.

Equations

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

def DescriptiveComplexity.tqSrcF {α : Type} (x y : α) : tqSOLang.Formula α

The transition x applies in the state y, as a formula.

Equations

• DescriptiveComplexity.tqSrcF x y = DescriptiveComplexity.tqSrcSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqReadF {α : Type} (x y : α) : tqSOLang.Formula α

The transition x reads the symbol y, as a formula.

Equations

• DescriptiveComplexity.tqReadF x y = DescriptiveComplexity.tqReadSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqDstF {α : Type} (x y : α) : tqSOLang.Formula α

The transition x moves to the state y, as a formula.

Equations

• DescriptiveComplexity.tqDstF x y = DescriptiveComplexity.tqDstSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqWriteF {α : Type} (x y : α) : tqSOLang.Formula α

The transition x writes the symbol y, as a formula.

Equations

• DescriptiveComplexity.tqWriteF x y = DescriptiveComplexity.tqWriteSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqInpF {α : Type} (x y : α) : tqSOLang.Formula α

The cell x initially holds y, as a formula.

Equations

• DescriptiveComplexity.tqInpF x y = DescriptiveComplexity.tqInpSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqStateF {α : Type} (x y : α) : tqSOLang.Formula α

The state at time x is y, as a formula.

Equations

• DescriptiveComplexity.tqStateF x y = DescriptiveComplexity.tqStateSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqHeadF {α : Type} (x y : α) : tqSOLang.Formula α

The head at time x is on y, as a formula.

Equations

• DescriptiveComplexity.tqHeadF x y = DescriptiveComplexity.tqHeadSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.tqTapeF {α : Type} (x y z : α) : tqSOLang.Formula α

At time x the cell y holds z, as a formula.

Equations

• DescriptiveComplexity.tqTapeF x y z = DescriptiveComplexity.tqTapeSym.formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.tqMinPosF {α : Type} (x : α) : tqSOLang.Formula α

x is the lowest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.tqMaxPosF {α : Type} (x : α) : tqSOLang.Formula α

x is the highest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.tqSuccPosF {α : Type} (x y : α) : tqSOLang.Formula α

y is the position immediately above x, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.tqMoveF {α : Type} (t t' : α) (dir : Bool) : tqSOLang.Formula α

The head moves from its cell at t to its cell at t', in the direction dir.

Equations

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

noncomputable def DescriptiveComplexity.tqStepBodyF {α : Type} (t t' τ : α) : tqSOLang.Formula α

The step body: the transition τ takes the configuration at t to the one at t'. Its seven conjuncts are those of DescriptiveComplexity.TMData.RelStep.

Equations

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

noncomputable def DescriptiveComplexity.tqStutterBodyF {α : Type} (t t' : α) : tqSOLang.Formula α

The stutter body: an accepting configuration repeated.

Equations

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

noncomputable def DescriptiveComplexity.tqInitTapeF {α : Type} (x y : α) : tqSOLang.Formula α

The cell x may initially hold y: the input where it is defined, the blank elsewhere.

Equations

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

Realization of the builders

@[simp]

theorem DescriptiveComplexity.realize_tqPosnF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqPosnF x).Realize v ↔ TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqTrF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqTrF x).Realize v ↔ TMTr (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqStartF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqStartF x).Realize v ↔ TMStart (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqAccF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqAccF x).Realize v ↔ TMAcc (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqBlankF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqBlankF x).Realize v ↔ TMBlank (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqRightF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqRightF x).Realize v ↔ TMRight (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqLeF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqLeF x y).Realize v ↔ TMLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqEqF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqEqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.realize_tqSrcF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqSrcF x y).Realize v ↔ TMSrc (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqReadF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqReadF x y).Realize v ↔ TMRead (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqDstF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqDstF x y).Realize v ↔ TMDst (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqWriteF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqWriteF x y).Realize v ↔ TMWrite (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqInpF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqInpF x y).Realize v ↔ TMInp (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqStateF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqStateF x y).Realize v ↔ ρ TMIdx.state ![v x, v y]

@[simp]

theorem DescriptiveComplexity.realize_tqHeadF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqHeadF x y).Realize v ↔ ρ TMIdx.head ![v x, v y]

@[simp]

theorem DescriptiveComplexity.realize_tqTapeF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y z : α) : (tqTapeF x y z).Realize v ↔ ρ TMIdx.tape ![v x, v y, v z]

@[simp]

theorem DescriptiveComplexity.realize_tqMinPosF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqMinPosF x).Realize v ↔ MinPos TMLe TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqMaxPosF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (tqMaxPosF x).Realize v ↔ MaxPos TMLe TMPosn (v x)

@[simp]

theorem DescriptiveComplexity.realize_tqSuccPosF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqSuccPosF x y).Realize v ↔ SuccPos TMLe TMPosn (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqInitTapeF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (tqInitTapeF x y).Realize v ↔ TMInp (v x) (v y) ∨ (∀ (b : A), ¬TMInp (v x) b) ∧ TMBlank (v y)

@[simp]

theorem DescriptiveComplexity.realize_tqMoveF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (t t' : α) (dir : Bool) : (tqMoveF t t' dir).Realize v ↔ ∀ (p p' : A), ρ TMIdx.head ![v t, p] → ρ TMIdx.head ![v t', p'] → if dir = true then SuccPos TMLe TMPosn p p' else SuccPos TMLe TMPosn p' p

theorem DescriptiveComplexity.realize_tqStepBodyF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (t t' τ : α) : (tqStepBodyF t t' τ).Realize v ↔ TMTr (v τ) ∧ (∀ (q : A), ρ TMIdx.state ![v t, q] → TMSrc (v τ) q) ∧ (∀ (p a : A), ρ TMIdx.head ![v t, p] → ρ TMIdx.tape ![v t, p, a] → TMRead (v τ) a) ∧ (∀ (q : A), ρ TMIdx.state ![v t', q] → TMDst (v τ) q) ∧ (∀ (p a : A), ρ TMIdx.head ![v t, p] → ρ TMIdx.tape ![v t', p, a] → TMWrite (v τ) a) ∧ (∀ (p a : A), ¬ρ TMIdx.head ![v t, p] → (ρ TMIdx.tape ![v t, p, a] ↔ ρ TMIdx.tape ![v t', p, a])) ∧ ((TMRight (v τ) ∧ ∀ (p p' : A), ρ TMIdx.head ![v t, p] → ρ TMIdx.head ![v t', p'] → SuccPos TMLe TMPosn p p') ∨ ¬TMRight (v τ) ∧ ∀ (p p' : A), ρ TMIdx.head ![v t, p] → ρ TMIdx.head ![v t', p'] → SuccPos TMLe TMPosn p' p)

theorem DescriptiveComplexity.realize_tqStutterBodyF {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) {α : Type} (v : α → A) (t t' : α) : (tqStutterBodyF t t').Realize v ↔ (∀ (q : A), ρ TMIdx.state ![v t, q] → TMAcc q) ∧ (∀ (q : A), ρ TMIdx.state ![v t', q] ↔ ρ TMIdx.state ![v t, q]) ∧ (∀ (p : A), ρ TMIdx.head ![v t', p] ↔ ρ TMIdx.head ![v t, p]) ∧ ∀ (p a : A), ρ TMIdx.tape ![v t', p, a] ↔ ρ TMIdx.tape ![v t, p, a]

The clauses of the kernel

Each mirrors one field of DescriptiveComplexity.TMData.RelWalk.

noncomputable def DescriptiveComplexity.tqStateExClause : tqSOLang.Sentence

There is a state at each time.

Equations

• DescriptiveComplexity.tqStateExClause = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.tqStateF (Sum.inl (Sum.inr 0)) (Sum.inr 0)))

noncomputable def DescriptiveComplexity.tqStateUniqClause : tqSOLang.Sentence

There is only one state at each time.

Equations

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

noncomputable def DescriptiveComplexity.tqHeadExClause : tqSOLang.Sentence

The head is somewhere at each time.

Equations

• DescriptiveComplexity.tqHeadExClause = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.tqHeadF (Sum.inl (Sum.inr 0)) (Sum.inr 0)))

noncomputable def DescriptiveComplexity.tqHeadUniqClause : tqSOLang.Sentence

The head is in only one place at each time.

Equations

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

noncomputable def DescriptiveComplexity.tqTapeExClause : tqSOLang.Sentence

Every cell holds a symbol at each time.

Equations

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

noncomputable def DescriptiveComplexity.tqTapeUniqClause : tqSOLang.Sentence

Every cell holds only one symbol at each time.

Equations

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

noncomputable def DescriptiveComplexity.tqStepClause : tqSOLang.Sentence

Consecutive times are related by a step or by an accepting stutter.

Equations

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

noncomputable def DescriptiveComplexity.tqInitClause : tqSOLang.Sentence

At the lowest time the configuration is initial.

Equations

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

noncomputable def DescriptiveComplexity.tqReflClause : tqSOLang.Sentence

The order is reflexive.

Equations

• DescriptiveComplexity.tqReflClause = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.tqLeF (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.tqTransClause : tqSOLang.Sentence

The order is transitive.

Equations

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

noncomputable def DescriptiveComplexity.tqAntisymClause : tqSOLang.Sentence

The order is antisymmetric.

Equations

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

noncomputable def DescriptiveComplexity.tqTotalClause : tqSOLang.Sentence

The order is total.

Equations

• DescriptiveComplexity.tqTotalClause = FirstOrder.Language.Formula.iAlls (Fin 2) (DescriptiveComplexity.tqLeF (Sum.inr 0) (Sum.inr 1) ⊔ DescriptiveComplexity.tqLeF (Sum.inr 1) (Sum.inr 0))

noncomputable def DescriptiveComplexity.tqPosnExClause : tqSOLang.Sentence

There is a position.

Equations

• DescriptiveComplexity.tqPosnExClause = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.tqPosnF (Sum.inr 0))

noncomputable def DescriptiveComplexity.tqInpFunClause : tqSOLang.Sentence

The input is functional.

Equations

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

noncomputable def DescriptiveComplexity.tqBlankExClause : tqSOLang.Sentence

There is a blank symbol.

Equations

• DescriptiveComplexity.tqBlankExClause = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.tqBlankF (Sum.inr 0))

noncomputable def DescriptiveComplexity.tqBlankUniqClause : tqSOLang.Sentence

There is only one blank symbol.

Equations

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

noncomputable def DescriptiveComplexity.tqAccClause : tqSOLang.Sentence

At the highest time the state is accepting.

Equations

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

noncomputable def DescriptiveComplexity.tqKernel : tqSOLang.Sentence

The kernel: well-formedness of the instance, then that the guess is a run – the six functionality clauses, the initial clause, the step clause and the accepting clause.

Equations

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

theorem DescriptiveComplexity.realize_tqStateExClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqStateExClause ↔ ∀ (t : A), ∃ (q : A), ρ TMIdx.state ![t, q]

theorem DescriptiveComplexity.realize_tqStateUniqClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqStateUniqClause ↔ ∀ (t q q' : A), ρ TMIdx.state ![t, q] → ρ TMIdx.state ![t, q'] → q = q'

theorem DescriptiveComplexity.realize_tqHeadExClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqHeadExClause ↔ ∀ (t : A), ∃ (p : A), ρ TMIdx.head ![t, p]

theorem DescriptiveComplexity.realize_tqHeadUniqClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqHeadUniqClause ↔ ∀ (t p p' : A), ρ TMIdx.head ![t, p] → ρ TMIdx.head ![t, p'] → p = p'

theorem DescriptiveComplexity.realize_tqTapeExClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqTapeExClause ↔ ∀ (t p : A), ∃ (a : A), ρ TMIdx.tape ![t, p, a]

theorem DescriptiveComplexity.realize_tqTapeUniqClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqTapeUniqClause ↔ ∀ (t p a a' : A), ρ TMIdx.tape ![t, p, a] → ρ TMIdx.tape ![t, p, a'] → a = a'

theorem DescriptiveComplexity.realize_tqAccClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqAccClause ↔ ∀ (t : A), MaxPos TMLe TMPosn t → ∀ (q : A), ρ TMIdx.state ![t, q] → TMAcc q

theorem DescriptiveComplexity.realize_tqInitClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqInitClause ↔ ∀ (t : A), MinPos TMLe TMPosn t → (∀ (q : A), ρ TMIdx.state ![t, q] → TMStart q) ∧ (∀ (p : A), ρ TMIdx.head ![t, p] → MinPos TMLe TMPosn p) ∧ ∀ (p a : A), ρ TMIdx.tape ![t, p, a] → TMInp p a ∨ (∀ (b : A), ¬TMInp p b) ∧ TMBlank a

theorem DescriptiveComplexity.realize_tqReflClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqReflClause ↔ ∀ (a : A), TMLe a a

theorem DescriptiveComplexity.realize_tqTransClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqTransClause ↔ ∀ (a b c : A), TMLe a b → TMLe b c → TMLe a c

theorem DescriptiveComplexity.realize_tqAntisymClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqAntisymClause ↔ ∀ (a b : A), TMLe a b → TMLe b a → a = b

theorem DescriptiveComplexity.realize_tqTotalClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqTotalClause ↔ ∀ (a b : A), TMLe a b ∨ TMLe b a

theorem DescriptiveComplexity.realize_tqPosnExClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqPosnExClause ↔ ∃ (p : A), TMPosn p

theorem DescriptiveComplexity.realize_tqInpFunClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqInpFunClause ↔ ∀ (p a b : A), TMInp p a → TMInp p b → a = b

theorem DescriptiveComplexity.realize_tqBlankExClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqBlankExClause ↔ ∃ (b : A), TMBlank b

theorem DescriptiveComplexity.realize_tqBlankUniqClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqBlankUniqClause ↔ ∀ (a b : A), TMBlank a → TMBlank b → a = b

theorem DescriptiveComplexity.realize_tqStepClause {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqStepClause ↔ ∀ (t t' : A), SuccPos TMLe TMPosn t t' → (∃ (τ : A), TMTr τ ∧ (∀ (q : A), ρ TMIdx.state ![t, q] → TMSrc τ q) ∧ (∀ (p a : A), ρ TMIdx.head ![t, p] → ρ TMIdx.tape ![t, p, a] → TMRead τ a) ∧ (∀ (q : A), ρ TMIdx.state ![t', q] → TMDst τ q) ∧ (∀ (p a : A), ρ TMIdx.head ![t, p] → ρ TMIdx.tape ![t', p, a] → TMWrite τ a) ∧ (∀ (p a : A), ¬ρ TMIdx.head ![t, p] → (ρ TMIdx.tape ![t, p, a] ↔ ρ TMIdx.tape ![t', p, a])) ∧ ((TMRight τ ∧ ∀ (p p' : A), ρ TMIdx.head ![t, p] → ρ TMIdx.head ![t', p'] → SuccPos TMLe TMPosn p p') ∨ ¬TMRight τ ∧ ∀ (p p' : A), ρ TMIdx.head ![t, p] → ρ TMIdx.head ![t', p'] → SuccPos TMLe TMPosn p' p)) ∨ (∀ (q : A), ρ TMIdx.state ![t, q] → TMAcc q) ∧ (∀ (q : A), ρ TMIdx.state ![t', q] ↔ ρ TMIdx.state ![t, q]) ∧ (∀ (p : A), ρ TMIdx.head ![t', p] ↔ ρ TMIdx.head ![t, p]) ∧ ∀ (p a : A), ρ TMIdx.tape ![t', p, a] ↔ ρ TMIdx.tape ![t, p, a]

theorem DescriptiveComplexity.realize_tqKernel {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : tmGuessBlock.Assignment A) : A ⊨ tqKernel ↔ (tmData A).WellFormed ∧ (tmData A).RelWalk (fun (t q : A) => ρ TMIdx.state ![t, q]) (fun (t p : A) => ρ TMIdx.head ![t, p]) fun (t p a : A) => ρ TMIdx.tape ![t, p, a]

The kernel says exactly what it should: the instance is well formed and the guessed relations are a run.

The definability theorems

theorem DescriptiveComplexity.ntmAccept_sigmaSODefinable : SigmaSODefinable 1 NTMAccept

Machine acceptance is Σ₁-definable: one existential block guesses the run – the state, the head cell and the tape contents at each time – and the first-order kernel checks that it is one.

theorem DescriptiveComplexity.ntmAccept_mem_NP : NP.Mem NTMAccept

Machine acceptance is in NP.