The matrix of the constructed instance

What the matrix of the QSAT instance built by the Savitch reduction says, clause tag by clause tag.

A clause is satisfied when one of the literals of its list (DescriptiveComplexity.qLits) is (DescriptiveComplexity.ClSat), and a literal is satisfied when the variable its link points at gets the literal's sign (DescriptiveComplexity.LitSat). Since every link pins the coordinates of that variable, the existential quantifier of a literal collapses (DescriptiveComplexity.litSat_atP and its companions, one per DescriptiveComplexity.QLink), and each clause tag turns into a plain condition on what the valuation reads (DescriptiveComplexity.clSat_cSrc and its companions).

def DescriptiveComplexity.LitSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (σ : QM A → Prop) (p q : A) (l : QLit) : Prop

A literal of a clause sitting at (p, q) is satisfied by the valuation σ: the variable its link points at gets its sign.

Equations

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

def DescriptiveComplexity.ClSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (σ : QM A → Prop) (c : QClTag) (p q : A) : Prop

A clause of the constructed instance is satisfied by the valuation σ.

Equations

• DescriptiveComplexity.ClSat σ c p q = ∃ l ∈ DescriptiveComplexity.qLits c, DescriptiveComplexity.LitSat σ p q l

Collapsing the quantifier of a literal

Every link pins the coordinates of the variable it points at, except the two that range over the literals of a clause of the input.

@[simp]

theorem DescriptiveComplexity.litSat_atP {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.atP } ↔ QVarOn vt p (qBot A) ∧ (σ (qVar vt p (qBot A)) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_atQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.atQ } ↔ QVarOn vt q (qBot A) ∧ (σ (qVar vt q (qBot A)) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_botBoth {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.botBoth } ↔ QVarOn vt (qBot A) (qBot A) ∧ (σ (qVar vt (qBot A) (qBot A)) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_same {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.same } ↔ QVarOn vt p q ∧ (σ (qVar vt p q) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_maxAtP {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.maxAtP } ↔ ∃ (m : A), IsMaxSV m ∧ QVarOn vt m p ∧ (σ (qVar vt m p) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_minAtQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.minAtQ } ↔ IsMinSV p ∧ QVarOn vt q (qBot A) ∧ (σ (qVar vt q (qBot A)) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_predAtQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.predAtQ } ↔ ∃ (d : A), IsPredSV d p ∧ QVarOn vt d q ∧ (σ (qVar vt d q) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_occPos {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.occPos } ↔ ∃ (r : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, r] ∧ QVarOn vt r (qBot A) ∧ (σ (qVar vt r (qBot A)) ↔ sgn = true)

@[simp]

theorem DescriptiveComplexity.litSat_occNeg {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} : LitSat σ p q { vt := vt, sign := sgn, link := QLink.occNeg } ↔ ∃ (r : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, r] ∧ QVarOn vt r (qBot A) ∧ (σ (qVar vt r (qBot A)) ↔ sgn = true)

What each clause says

@[simp]

theorem DescriptiveComplexity.and_isSV_of_isMaxSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {m : A} {P : Prop} : IsMaxSV m ∧ IsSV m ∧ P ↔ IsMaxSV m ∧ P

@[simp]

theorem DescriptiveComplexity.and_isSV_of_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {d ℓ : A} {P : Prop} : IsPredSV d ℓ ∧ IsSV d ∧ P ↔ IsPredSV d ℓ ∧ P

theorem DescriptiveComplexity.clSat_cSrc {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (p q : A) : ClSat σ QClTag.cSrc p q ↔ ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, x] ∧ valS σ x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, x] ∧ ¬valS σ x

A copy of a source clause reads its literals on the source valuation.

def DescriptiveComplexity.LevSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (b w s : Bool) (ℓ x : A) : Prop

What one of the eight clauses of a level says: the branch of the universal bit, the component of the pair it constrains, and the value that component must copy – the midpoint, or the endpoint the level receives from above.

Equations

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