Existential second-order tableau sentence on Fin B

Given a deterministic multi-tape Turing machine tm : MultiTapeTM m Bool State ([Fintype State] [DecidableEq State]) and a language L₀ equipped with a strict linear order lt on Fin B and unary relations uLenRel and uBitRel describing an input prefix u : List Bool, this file constructs an existential second-order sentence FO.tableauESOSentence lt uLenRel uBitRel tm over L₀.

On Fin B with u.length + 1 < B, FO.tableauESOSentence lt uLenRel uBitRel tm is realized if and only if there exists a certificate word w : List Bool with u.length + w.length + 1 < B such that tm, started on u ++ w, halts within B - 1 steps with output [true] — equivalently, by Cslib.Complexity.CookLevin.tableau_satisfiable_iff, if and only if CookLevin.tableau tm u L (B - 1) is satisfiable for some L with u.length + L + 1 < B.

The relation-symbol bundle FO.TableauRels and component first-order formulas are defined in Complexity.Computability.Complexity.Fagin.Tableau.Defs, and the configuration-agreement predicate (FO.TableauRels.AgreesAt) and realization equivalences are proved in Complexity.Computability.Complexity.Fagin.Tableau.Semantics; both are re-exported here.

Main definitions

• Cslib.Logic.FO.tableauRels, Cslib.Logic.FO.tableauMatrix: the canonical relation-symbol bundle in the matrix language and the first-order matrix of the sentence.
• Cslib.Logic.FO.tableauESOSentence: the existential second-order sentence encoding an accepting computation of tm on u ++ w within B - 1 steps.
• Cslib.Logic.Vocabulary.tableauESOSentence: specialization to v.powerLanguage.sum v.inputVarLanguage.

Main results

• Cslib.Logic.FO.realize_tableauESOSentence: on Fin B, tableauESOSentence holds iff some certificate w with u.length + w.length + 1 < B is accepted within B - 1 steps.
• Cslib.Logic.Vocabulary.realize_tableauESOSentence: on Fin B, v.tableauESOSentence tm holds iff CookLevin.tableau tm u L (B - 1) is satisfiable for some L with u.length + L + 1 < B.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity
• C. H. Papadimitriou, Computational Complexity, Theorem 8.3

Full ESO tableau sentence

@[reducible, inline]

abbrev Cslib.Logic.FO.tableauMatrixLanguage {L₀ : FirstOrder.Language} (m : ℕ) (State : Type) : FirstOrder.Language

The language of the first-order matrix of tableauESOSentence.

def Cslib.Logic.FO.tableauRels {L₀ : FirstOrder.Language} (lt : L₀.Relations 2) (uLenRel uBitRel : L₀.Relations 1) {m : ℕ} {State : Type} : TableauRels (tableauMatrixLanguage m State) m State

The canonical TableauRels bundle in tableauMatrixLanguage.

noncomputable def Cslib.Logic.FO.tableauMatrix {L₀ : FirstOrder.Language} (lt : L₀.Relations 2) (uLenRel uBitRel : L₀.Relations 1) {m : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM m Bool State) : (tableauMatrixLanguage m State).Sentence

The first-order matrix of tableauESOSentence.

noncomputable def Cslib.Logic.FO.tableauESOSentence {L₀ : FirstOrder.Language} (lt : L₀.Relations 2) (uLenRel uBitRel : L₀.Relations 1) {m : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM m Bool State) : ESO.Sentence L₀

The existential second-order sentence asserting that tm, started on u ++ w for some certificate w with u.length + w.length + 1 < B, halts within B - 1 steps with output [true].

theorem Cslib.Logic.FO.realize_tableauESOSentence {L₀ : FirstOrder.Language} (lt : L₀.Relations 2) (uLenRel uBitRel : L₀.Relations 1) {m : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM m Bool State) {B : ℕ} [L₀.Structure (Fin B)] (hlt0 : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap lt x ↔ x 0 < x 1) {u : List Bool} (huB : u.length + 1 < B) (huLen0 : ∀ (z : Fin B), FirstOrder.Language.Structure.RelMap uLenRel ![z] ↔ ↑z = u.length) (huBit0 : ∀ (p : Fin B), ↑p < u.length → (FirstOrder.Language.Structure.RelMap uBitRel ![p] ↔ u[↑p]? = some true)) : (tableauESOSentence lt uLenRel uBitRel tm).Realize (Fin B) ↔ ∃ (w : List Bool), u.length + w.length + 1 < B ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) (B - 1)).state = none ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) (B - 1)).output = [true]

Correctness of tableauESOSentence on Fin B.

noncomputable def Cslib.Logic.Vocabulary.tableauESOSentence {L : FirstOrder.Language} (v : Vocabulary L) {m : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM m Bool State) : ESO.Sentence (v.powerLanguage.sum inputVarLanguage)

Specialization of FO.tableauESOSentence to v.powerLanguage.sum inputVarLanguage.

theorem Cslib.Logic.Vocabulary.realize_tableauESOSentence {L : FirstOrder.Language} (v : Vocabulary L) {m : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM m Bool State) (a : EncodedStructure) (B : ℕ) (I_in : (b : Bool) → Set (Fin ((fun (x : Bool) => 1) b) → Fin B)) {u : List Bool} (huB : u.length + 1 < B) (huLen : ∀ (z : Fin B), ![z] ∈ I_in true ↔ ↑z = u.length) (huBit : ∀ (p : Fin B), ↑p < u.length → (![p] ∈ I_in false ↔ u[↑p]? = some true)) : (v.tableauESOSentence tm).Realize (Fin B) ↔ ∃ (L : ℕ), u.length + L + 1 < B ∧ (Complexity.CookLevin.tableau tm u L (B - 1)).Satisfiable

Correctness of v.tableauESOSentence on Fin B. When I_in satisfies the layout specification for u, (v.tableauESOSentence tm).Realize (Fin B) holds if and only if CookLevin.tableau tm u L (B - 1) is satisfiable for some certificate length L with u.length + L + 1 < B.