QSAT is in PSPACE

The membership half: the truth of a fully quantified Boolean formula is SO(TC) definable, hence in DescriptiveComplexity.PSPACE.

The walk is the classical depth-first evaluation of the game tree, which is where the polynomial space of PSPACE is spent: the stack is a set of variables, and a set is one monadic relation variable. Four relation variables make up a state:

• D (unary) – the variables already given a value, i.e. the current branch of the game tree; the variable played next is the prefixLt-least one outside D (DescriptiveComplexity.QLeast) and the one returned to is the greatest one inside it;
• T (unary) – the values they were given;
• up (nullary – a relation variable of arity 0 is a bit) – the mode: descending towards a leaf, or returning a value;
• res (nullary) – the value being returned.

No accumulator is needed, and that is what keeps the transition sentence short: the evaluation short-circuits. Having returned the value v of the first branch of a variable x, the walk pops x immediately when v already settles the node (v true at an existential x, v false at a universal one) and otherwise plays the second branch, whose value is then the value of the node. So a value is never combined with a remembered one, and each of the four transitions merely edits the state (DescriptiveComplexity.qsSpec_step_iff).

Why the walk computes the game value

The transition relation is deterministic (DescriptiveComplexity.qsSpec_step_unique), and the run started at a position (D, τ) in descending mode comes back to D in returning mode carrying exactly QsatWins D τ (DescriptiveComplexity.qsSpec_run, by induction on the number of variables outside D). Determinism turns that into an equivalence: the returning state at D = ∅ is a dead end, and two dead ends reachable from one state coincide, so a walk accepting the specification has to be the run.

Well-formedness is checked by the source sentence, so a malformed instance – where the prefix order is not a linear order on the variables, and neither the next nor the last variable of a position need exist – has no starting state at all.

Generic sentence shapes

Each shape is built over an arbitrary vocabulary and an arbitrary variable type, so that the same builder and the same realization lemma serve the current copy of the block, the next one, and the nesting inside a quantifier.

def DescriptiveComplexity.bitF {L' : FirstOrder.Language} {γ : Type} (R : L'.Relations 0) : L'.Formula γ

A relation variable of arity 0 read as a formula: a propositional bit.

Equations

• DescriptiveComplexity.bitF R = R.formula Fin.elim0

theorem DescriptiveComplexity.realize_bitF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (R : L'.Relations 0) (v : γ → M) : (bitF R).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![]

theorem DescriptiveComplexity.realize_bitS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (R : L'.Relations 0) : M ⊨ bitF R ↔ FirstOrder.Language.Structure.RelMap R ![]

noncomputable def DescriptiveComplexity.leastF {L' : FirstOrder.Language} {γ : Type} (mark d : L'.Relations 1) (prec : L'.Relations 2) (x : L'.Term γ) : L'.Formula γ

“x is marked, lies outside d, and no marked element outside d precedes it”: the element a position plays next.

Equations

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

theorem DescriptiveComplexity.realize_leastF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (mark d : L'.Relations 1) (prec : L'.Relations 2) (x : L'.Term γ) (v : γ → M) : (leastF mark d prec x).Realize v ↔ FirstOrder.Language.Structure.RelMap mark ![FirstOrder.Language.Term.realize v x] ∧ ¬FirstOrder.Language.Structure.RelMap d ![FirstOrder.Language.Term.realize v x] ∧ ∀ (y : M), FirstOrder.Language.Structure.RelMap mark ![y] → ¬FirstOrder.Language.Structure.RelMap d ![y] → ¬FirstOrder.Language.Structure.RelMap prec ![y, FirstOrder.Language.Term.realize v x]

noncomputable def DescriptiveComplexity.greatestF {L' : FirstOrder.Language} {γ : Type} (mark d : L'.Relations 1) (prec : L'.Relations 2) (x : L'.Term γ) : L'.Formula γ

“x is marked, lies inside d, and precedes no marked element of d”: the element a position returns to.

Equations

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

theorem DescriptiveComplexity.realize_greatestF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (mark d : L'.Relations 1) (prec : L'.Relations 2) (x : L'.Term γ) (v : γ → M) : (greatestF mark d prec x).Realize v ↔ FirstOrder.Language.Structure.RelMap mark ![FirstOrder.Language.Term.realize v x] ∧ FirstOrder.Language.Structure.RelMap d ![FirstOrder.Language.Term.realize v x] ∧ ∀ (y : M), FirstOrder.Language.Structure.RelMap mark ![y] → FirstOrder.Language.Structure.RelMap d ![y] → ¬FirstOrder.Language.Structure.RelMap prec ![FirstOrder.Language.Term.realize v x, y]

noncomputable def DescriptiveComplexity.coveredF {L' : FirstOrder.Language} {γ : Type} (mark d : L'.Relations 1) : L'.Formula γ

“Every marked element lies in d”: the position is a leaf.

Equations

• DescriptiveComplexity.coveredF mark d = FirstOrder.Language.Formula.iAlls (Fin 1) ((mark.formula₁ (FirstOrder.Language.var (Sum.inr 0))).imp (d.formula₁ (FirstOrder.Language.var (Sum.inr 0))))

theorem DescriptiveComplexity.realize_coveredF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (mark d : L'.Relations 1) (v : γ → M) : (coveredF mark d).Realize v ↔ ∀ (y : M), FirstOrder.Language.Structure.RelMap mark ![y] → FirstOrder.Language.Structure.RelMap d ![y]

noncomputable def DescriptiveComplexity.emptyF {L' : FirstOrder.Language} {γ : Type} (d : L'.Relations 1) : L'.Formula γ

“No element lies in d”.

Equations

• DescriptiveComplexity.emptyF d = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (d.formula₁ (FirstOrder.Language.var (Sum.inr 0))))

theorem DescriptiveComplexity.realize_emptyF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (d : L'.Relations 1) (v : γ → M) : (emptyF d).Realize v ↔ ∀ (y : M), ¬FirstOrder.Language.Structure.RelMap d ![y]

noncomputable def DescriptiveComplexity.matrixF {L' : FirstOrder.Language} {γ : Type} (cl mark : L'.Relations 1) (pos neg : L'.Relations 2) (t : L'.Relations 1) : L'.Formula γ

The matrix: every clause holds a literal on a marked element that t makes true.

Equations

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

theorem DescriptiveComplexity.realize_matrixF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (cl mark : L'.Relations 1) (pos neg : L'.Relations 2) (t : L'.Relations 1) (v : γ → M) : (matrixF cl mark pos neg t).Realize v ↔ ∀ (c : M), FirstOrder.Language.Structure.RelMap cl ![c] → ∃ (y : M), FirstOrder.Language.Structure.RelMap mark ![y] ∧ (FirstOrder.Language.Structure.RelMap pos ![c, y] ∧ FirstOrder.Language.Structure.RelMap t ![y] ∨ FirstOrder.Language.Structure.RelMap neg ![c, y] ∧ ¬FirstOrder.Language.Structure.RelMap t ![y])

def DescriptiveComplexity.sameF {L' : FirstOrder.Language} {γ : Type} (a' a : L'.Relations 1) (y : L'.Term γ) : L'.Formula γ

“a' holds of y exactly when a does”: an unchanged component.

Equations

• DescriptiveComplexity.sameF a' a y = (a'.formula₁ y).iff (a.formula₁ y)

theorem DescriptiveComplexity.realize_sameF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (a' a : L'.Relations 1) (y : L'.Term γ) (v : γ → M) : (sameF a' a y).Realize v ↔ (FirstOrder.Language.Structure.RelMap a' ![FirstOrder.Language.Term.realize v y] ↔ FirstOrder.Language.Structure.RelMap a ![FirstOrder.Language.Term.realize v y])

def DescriptiveComplexity.updF {L' : FirstOrder.Language} {γ : Type} (a' a : L'.Relations 1) (φ : L'.Formula γ) (x y : L'.Term γ) : L'.Formula γ

“a' is a with the value of x set to φ”: the one update shape the walk needs – adding x (φ = ⊤) and removing it (φ = ⊥).

Equations

• DescriptiveComplexity.updF a' a φ x y = (a'.formula₁ y).iff (y.equal x ⊓ φ ⊔ FirstOrder.Language.BoundedFormula.not (y.equal x) ⊓ a.formula₁ y)

theorem DescriptiveComplexity.realize_updF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (a' a : L'.Relations 1) (φ : L'.Formula γ) (x y : L'.Term γ) (v : γ → M) : (updF a' a φ x y).Realize v ↔ (FirstOrder.Language.Structure.RelMap a' ![FirstOrder.Language.Term.realize v y] ↔ FirstOrder.Language.Term.realize v y = FirstOrder.Language.Term.realize v x ∧ φ.Realize v ∨ FirstOrder.Language.Term.realize v y ≠ FirstOrder.Language.Term.realize v x ∧ FirstOrder.Language.Structure.RelMap a ![FirstOrder.Language.Term.realize v y])

Well-formedness

The prefix order is a strict linear order on the marked elements.

noncomputable def DescriptiveComplexity.wfMarkedF {L' : FirstOrder.Language} {γ : Type} (mark : L'.Relations 1) (prec : L'.Relations 2) : L'.Formula γ

The prefix order only relates marked elements.

Equations

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

noncomputable def DescriptiveComplexity.wfIrreflF {L' : FirstOrder.Language} {γ : Type} (prec : L'.Relations 2) : L'.Formula γ

The prefix order is irreflexive.

Equations

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

noncomputable def DescriptiveComplexity.wfTransF {L' : FirstOrder.Language} {γ : Type} (prec : L'.Relations 2) : L'.Formula γ

The prefix order is transitive.

Equations

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

noncomputable def DescriptiveComplexity.wfTotalF {L' : FirstOrder.Language} {γ : Type} (mark : L'.Relations 1) (prec : L'.Relations 2) : L'.Formula γ

The prefix order is total on the marked elements.

Equations

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

noncomputable def DescriptiveComplexity.wfF {L' : FirstOrder.Language} {γ : Type} (mark : L'.Relations 1) (prec : L'.Relations 2) : L'.Formula γ

The instance is well formed: the prefix order is a strict linear order on the marked elements.

Equations

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

theorem DescriptiveComplexity.realize_wfF {L' : FirstOrder.Language} {γ M : Type} [L'.Structure M] (mark : L'.Relations 1) (prec : L'.Relations 2) (v : γ → M) : (wfF mark prec).Realize v ↔ (∀ (x y : M), FirstOrder.Language.Structure.RelMap prec ![x, y] → FirstOrder.Language.Structure.RelMap mark ![x] ∧ FirstOrder.Language.Structure.RelMap mark ![y]) ∧ (∀ (x : M), ¬FirstOrder.Language.Structure.RelMap prec ![x, x]) ∧ (∀ (x y z : M), FirstOrder.Language.Structure.RelMap prec ![x, y] → FirstOrder.Language.Structure.RelMap prec ![y, z] → FirstOrder.Language.Structure.RelMap prec ![x, z]) ∧ ∀ (x y : M), FirstOrder.Language.Structure.RelMap mark ![x] → FirstOrder.Language.Structure.RelMap mark ![y] → x ≠ y → FirstOrder.Language.Structure.RelMap prec ![x, y] ∨ FirstOrder.Language.Structure.RelMap prec ![y, x]

theorem DescriptiveComplexity.realize_wfS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark : L'.Relations 1) (prec : L'.Relations 2) : M ⊨ wfF mark prec ↔ (∀ (x y : M), FirstOrder.Language.Structure.RelMap prec ![x, y] → FirstOrder.Language.Structure.RelMap mark ![x] ∧ FirstOrder.Language.Structure.RelMap mark ![y]) ∧ (∀ (x : M), ¬FirstOrder.Language.Structure.RelMap prec ![x, x]) ∧ (∀ (x y z : M), FirstOrder.Language.Structure.RelMap prec ![x, y] → FirstOrder.Language.Structure.RelMap prec ![y, z] → FirstOrder.Language.Structure.RelMap prec ![x, z]) ∧ ∀ (x y : M), FirstOrder.Language.Structure.RelMap mark ![x] → FirstOrder.Language.Structure.RelMap mark ![y] → x ≠ y → FirstOrder.Language.Structure.RelMap prec ![x, y] ∨ FirstOrder.Language.Structure.RelMap prec ![y, x]

theorem DescriptiveComplexity.realize_emptyS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (d : L'.Relations 1) : M ⊨ emptyF d ↔ ∀ (y : M), ¬FirstOrder.Language.Structure.RelMap d ![y]

The nine conjuncts of the transition sentence

One conjunct per case of the walk and per kind of component: the two unary components are edited under a ∀ x y, the two bits under a ∀ x. All are built over an arbitrary vocabulary, with the current copy of the block (d, t, u, r) and the next one (d', t', u', r') as parameters.

def DescriptiveComplexity.popF {L' : FirstOrder.Language} (allv t : L'.Relations 1) (r : L'.Relations 0) {γ : Type} (x : L'.Term γ) : L'.Formula γ

“The subtree of x is finished”: either its second value has been played already, or the value just returned settles the node – true at an existential x, false at a universal one.

Equations

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

theorem DescriptiveComplexity.realize_popF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (allv t : L'.Relations 1) (r : L'.Relations 0) {γ : Type} (x : L'.Term γ) (v : γ → M) : (popF allv t r x).Realize v ↔ FirstOrder.Language.Structure.RelMap t ![FirstOrder.Language.Term.realize v x] ∨ FirstOrder.Language.Structure.RelMap allv ![FirstOrder.Language.Term.realize v x] ∧ ¬FirstOrder.Language.Structure.RelMap r ![] ∨ ¬FirstOrder.Language.Structure.RelMap allv ![FirstOrder.Language.Term.realize v x] ∧ FirstOrder.Language.Structure.RelMap r ![]

noncomputable def DescriptiveComplexity.downSetS {L' : FirstOrder.Language} (mark d t d' t' : L'.Relations 1) (prec : L'.Relations 2) : L'.Sentence

Descending one step: the next variable joins the quantified set with the value false.

Equations

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

theorem DescriptiveComplexity.realize_downSetS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark d t d' t' : L'.Relations 1) (prec : L'.Relations 2) : M ⊨ downSetS mark d t d' t' prec ↔ ∀ (x y : M), (FirstOrder.Language.Structure.RelMap mark ![x] ∧ ¬FirstOrder.Language.Structure.RelMap d ![x] ∧ ∀ (z : M), FirstOrder.Language.Structure.RelMap mark ![z] → ¬FirstOrder.Language.Structure.RelMap d ![z] → ¬FirstOrder.Language.Structure.RelMap prec ![z, x]) → (FirstOrder.Language.Structure.RelMap d' ![y] ↔ y = x ∧ True ∨ y ≠ x ∧ FirstOrder.Language.Structure.RelMap d ![y]) ∧ (FirstOrder.Language.Structure.RelMap t' ![y] ↔ y = x ∧ False ∨ y ≠ x ∧ FirstOrder.Language.Structure.RelMap t ![y])

noncomputable def DescriptiveComplexity.downBitsS {L' : FirstOrder.Language} (mark d : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : L'.Sentence

Descending one step: the mode stays descending and the value is carried along.

Equations

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

theorem DescriptiveComplexity.realize_downBitsS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark d : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : M ⊨ downBitsS mark d prec u' r' r ↔ ∀ (x : M), (FirstOrder.Language.Structure.RelMap mark ![x] ∧ ¬FirstOrder.Language.Structure.RelMap d ![x] ∧ ∀ (z : M), FirstOrder.Language.Structure.RelMap mark ![z] → ¬FirstOrder.Language.Structure.RelMap d ![z] → ¬FirstOrder.Language.Structure.RelMap prec ![z, x]) → ¬FirstOrder.Language.Structure.RelMap u' ![] ∧ (FirstOrder.Language.Structure.RelMap r' ![] ↔ FirstOrder.Language.Structure.RelMap r ![])

noncomputable def DescriptiveComplexity.leafSetS {L' : FirstOrder.Language} (mark d t d' t' : L'.Relations 1) : L'.Sentence

At a leaf the two unary components are unchanged.

Equations

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

theorem DescriptiveComplexity.realize_leafSetS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark d t d' t' : L'.Relations 1) : M ⊨ leafSetS mark d t d' t' ↔ (∀ (z : M), FirstOrder.Language.Structure.RelMap mark ![z] → FirstOrder.Language.Structure.RelMap d ![z]) → ∀ (y : M), (FirstOrder.Language.Structure.RelMap d' ![y] ↔ FirstOrder.Language.Structure.RelMap d ![y]) ∧ (FirstOrder.Language.Structure.RelMap t' ![y] ↔ FirstOrder.Language.Structure.RelMap t ![y])

noncomputable def DescriptiveComplexity.leafBitsS {L' : FirstOrder.Language} (cl mark d t : L'.Relations 1) (pos neg : L'.Relations 2) (u' r' : L'.Relations 0) : L'.Sentence

At a leaf the walk starts returning, carrying the value of the matrix.

Equations

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

theorem DescriptiveComplexity.realize_leafBitsS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (cl mark d t : L'.Relations 1) (pos neg : L'.Relations 2) (u' r' : L'.Relations 0) : M ⊨ leafBitsS cl mark d t pos neg u' r' ↔ (∀ (z : M), FirstOrder.Language.Structure.RelMap mark ![z] → FirstOrder.Language.Structure.RelMap d ![z]) → FirstOrder.Language.Structure.RelMap u' ![] ∧ (FirstOrder.Language.Structure.RelMap r' ![] ↔ ∀ (c : M), FirstOrder.Language.Structure.RelMap cl ![c] → ∃ (y : M), FirstOrder.Language.Structure.RelMap mark ![y] ∧ (FirstOrder.Language.Structure.RelMap pos ![c, y] ∧ FirstOrder.Language.Structure.RelMap t ![y] ∨ FirstOrder.Language.Structure.RelMap neg ![c, y] ∧ ¬FirstOrder.Language.Structure.RelMap t ![y]))

noncomputable def DescriptiveComplexity.upExS {L' : FirstOrder.Language} (mark d : L'.Relations 1) (prec : L'.Relations 2) : L'.Sentence

Returning is only possible from a nonempty branch.

Equations

• DescriptiveComplexity.upExS mark d prec = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.greatestF mark d prec (FirstOrder.Language.var (Sum.inr 0)))

theorem DescriptiveComplexity.realize_upExS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark d : L'.Relations 1) (prec : L'.Relations 2) : M ⊨ upExS mark d prec ↔ ∃ (x : M), FirstOrder.Language.Structure.RelMap mark ![x] ∧ FirstOrder.Language.Structure.RelMap d ![x] ∧ ∀ (z : M), FirstOrder.Language.Structure.RelMap mark ![z] → FirstOrder.Language.Structure.RelMap d ![z] → ¬FirstOrder.Language.Structure.RelMap prec ![x, z]

noncomputable def DescriptiveComplexity.popSetS {L' : FirstOrder.Language} (mark allv d t d' t' : L'.Relations 1) (prec : L'.Relations 2) (r : L'.Relations 0) : L'.Sentence

Popping a finished variable: it leaves the quantified set, the values are unchanged.

Equations

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

noncomputable def DescriptiveComplexity.flipSetS {L' : FirstOrder.Language} (mark allv d t d' t' : L'.Relations 1) (prec : L'.Relations 2) (r : L'.Relations 0) : L'.Sentence

Playing the second value of an unfinished variable.

Equations

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

noncomputable def DescriptiveComplexity.popBitsS {L' : FirstOrder.Language} (mark allv d t : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : L'.Sentence

Popping a finished variable: the walk keeps returning, with the same value.

Equations

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

noncomputable def DescriptiveComplexity.flipBitsS {L' : FirstOrder.Language} (mark allv d t : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : L'.Sentence

Playing the second value: the walk goes back to descending.

Equations

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

theorem DescriptiveComplexity.realize_popSetS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark allv d t d' t' : L'.Relations 1) (prec : L'.Relations 2) (r : L'.Relations 0) : M ⊨ popSetS mark allv d t d' t' prec r ↔ ∀ (x y : M), DescriptiveComplexity.isLastM✝ mark d prec x → DescriptiveComplexity.isPopM✝ allv t r x → (FirstOrder.Language.Structure.RelMap d' ![y] ↔ y = x ∧ False ∨ y ≠ x ∧ FirstOrder.Language.Structure.RelMap d ![y]) ∧ (FirstOrder.Language.Structure.RelMap t' ![y] ↔ FirstOrder.Language.Structure.RelMap t ![y])

theorem DescriptiveComplexity.realize_flipSetS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark allv d t d' t' : L'.Relations 1) (prec : L'.Relations 2) (r : L'.Relations 0) : M ⊨ flipSetS mark allv d t d' t' prec r ↔ ∀ (x y : M), DescriptiveComplexity.isLastM✝ mark d prec x → ¬DescriptiveComplexity.isPopM✝ allv t r x → (FirstOrder.Language.Structure.RelMap d' ![y] ↔ FirstOrder.Language.Structure.RelMap d ![y]) ∧ (FirstOrder.Language.Structure.RelMap t' ![y] ↔ y = x ∧ True ∨ y ≠ x ∧ FirstOrder.Language.Structure.RelMap t ![y])

theorem DescriptiveComplexity.realize_popBitsS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark allv d t : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : M ⊨ popBitsS mark allv d t prec u' r' r ↔ ∀ (x : M), DescriptiveComplexity.isLastM✝ mark d prec x → DescriptiveComplexity.isPopM✝ allv t r x → FirstOrder.Language.Structure.RelMap u' ![] ∧ (FirstOrder.Language.Structure.RelMap r' ![] ↔ FirstOrder.Language.Structure.RelMap r ![])

theorem DescriptiveComplexity.realize_flipBitsS {L' : FirstOrder.Language} {M : Type} [L'.Structure M] (mark allv d t : L'.Relations 1) (prec : L'.Relations 2) (u' r' r : L'.Relations 0) : M ⊨ flipBitsS mark allv d t prec u' r' r ↔ ∀ (x : M), DescriptiveComplexity.isLastM✝ mark d prec x → ¬DescriptiveComplexity.isPopM✝ allv t r x → ¬FirstOrder.Language.Structure.RelMap u' ![] ∧ (FirstOrder.Language.Structure.RelMap r' ![] ↔ FirstOrder.Language.Structure.RelMap r ![])

The block and the vocabularies

@[reducible, inline]

abbrev DescriptiveComplexity.qsBlock : SOBlock

The block of the SO(TC) specification of QSAT: two unary relation variables – the quantified set and the values it gave – and two relation variables of arity 0, i.e. two bits – the mode and the value being returned.

Equations

• DescriptiveComplexity.qsBlock = { ι := Bool ⊕ Bool, ιFinite := ⋯, arity := fun (i : Bool ⊕ Bool) => match i with | Sum.inl val => 1 | Sum.inr val => 0 }

def DescriptiveComplexity.qsSym₁ (i : Bool) : qsBlock.lang.Relations 1

The unary relation variable of index i: the quantified set at false, the valuation at true.

Equations

• DescriptiveComplexity.qsSym₁ i = ⟨Sum.inl i, ⋯⟩

def DescriptiveComplexity.qsSym₀ (i : Bool) : qsBlock.lang.Relations 0

The nullary relation variable of index i: the mode at false, the value being returned at true.

Equations

• DescriptiveComplexity.qsSym₀ i = ⟨Sum.inr i, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.qsBase : FirstOrder.Language

The input vocabulary together with the order, over which the sentences of an SO(TC) specification live.

Equations

• DescriptiveComplexity.qsBase = FirstOrder.Language.qsat.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.qsLang₁ : FirstOrder.Language

The vocabulary of the endpoint sentences: one copy of the block.

Equations

• DescriptiveComplexity.qsLang₁ = DescriptiveComplexity.qsBase.sum DescriptiveComplexity.qsBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.qsLang₂ : FirstOrder.Language

The vocabulary of the transition sentence: two copies of the block.

Equations

• DescriptiveComplexity.qsLang₂ = DescriptiveComplexity.qsLang₁.sum DescriptiveComplexity.qsBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.qsIn₁ {n : ℕ} (r : FirstOrder.Language.qsat.Relations n) : qsLang₁.Relations n

An input symbol, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.qsIn₁ r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.qsVar₁ (i : Bool) : qsLang₁.Relations 1

A unary relation variable, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.qsVar₁ i = Sum.inr (DescriptiveComplexity.qsSym₁ i)

@[reducible, inline]

abbrev DescriptiveComplexity.qsBit₁ (i : Bool) : qsLang₁.Relations 0

A bit of the block, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.qsBit₁ i = Sum.inr (DescriptiveComplexity.qsSym₀ i)

@[reducible, inline]

abbrev DescriptiveComplexity.qsIn₂ {n : ℕ} (r : FirstOrder.Language.qsat.Relations n) : qsLang₂.Relations n

An input symbol, in the transition vocabulary.

Equations

• DescriptiveComplexity.qsIn₂ r = Sum.inl (Sum.inl (Sum.inl r))

@[reducible, inline]

abbrev DescriptiveComplexity.qsCur₂ (i : Bool) : qsLang₂.Relations 1

A unary relation variable of the current state.

Equations

• DescriptiveComplexity.qsCur₂ i = Sum.inl (Sum.inr (DescriptiveComplexity.qsSym₁ i))

@[reducible, inline]

abbrev DescriptiveComplexity.qsCurBit₂ (i : Bool) : qsLang₂.Relations 0

A bit of the current state.

Equations

• DescriptiveComplexity.qsCurBit₂ i = Sum.inl (Sum.inr (DescriptiveComplexity.qsSym₀ i))

@[reducible, inline]

abbrev DescriptiveComplexity.qsNext₂ (i : Bool) : qsLang₂.Relations 1

A unary relation variable of the next state.

Equations

• DescriptiveComplexity.qsNext₂ i = Sum.inr (DescriptiveComplexity.qsSym₁ i)

@[reducible, inline]

abbrev DescriptiveComplexity.qsNextBit₂ (i : Bool) : qsLang₂.Relations 0

A bit of the next state.

Equations

• DescriptiveComplexity.qsNextBit₂ i = Sum.inr (DescriptiveComplexity.qsSym₀ i)

noncomputable def DescriptiveComplexity.qsSpec : SOTCSpec FirstOrder.Language.qsat

The SO(TC) specification of QSAT: the depth-first evaluation of the game tree. Descending, the walk plays the next variable with the value false, or – at a leaf – turns round carrying the value of the matrix; returning, it pops the last variable when its subtree is settled and otherwise plays its second value.

Equations

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

Reading the specification back

def DescriptiveComplexity.qsPred {A : Type} (ρ : qsBlock.Assignment A) (i : Bool) : A → Prop

The unary component i of a state.

Equations

• DescriptiveComplexity.qsPred ρ i a = ρ (Sum.inl i) fun (x : Fin (DescriptiveComplexity.qsBlock.arity (Sum.inl i))) => a

def DescriptiveComplexity.qsBit {A : Type} (ρ : qsBlock.Assignment A) (i : Bool) : Prop

The bit i of a state.

Equations

• DescriptiveComplexity.qsBit ρ i = ρ (Sum.inr i) Fin.elim0

@[reducible, inline]

abbrev DescriptiveComplexity.qsSet {A : Type} (ρ : qsBlock.Assignment A) : A → Prop

The quantified set of a state.

Equations

• DescriptiveComplexity.qsSet ρ = DescriptiveComplexity.qsPred ρ false

@[reducible, inline]

abbrev DescriptiveComplexity.qsVal {A : Type} (ρ : qsBlock.Assignment A) : A → Prop

The valuation of a state.

Equations

• DescriptiveComplexity.qsVal ρ = DescriptiveComplexity.qsPred ρ true

@[reducible, inline]

abbrev DescriptiveComplexity.qsUp {A : Type} (ρ : qsBlock.Assignment A) : Prop

The mode of a state: True while returning a value.

Equations

• DescriptiveComplexity.qsUp ρ = DescriptiveComplexity.qsBit ρ false

@[reducible, inline]

abbrev DescriptiveComplexity.qsRes {A : Type} (ρ : qsBlock.Assignment A) : Prop

The value a state is returning.

Equations

• DescriptiveComplexity.qsRes ρ = DescriptiveComplexity.qsBit ρ true

def DescriptiveComplexity.qsLift {A : Type} (D T : A → Prop) (u r : Prop) : qsBlock.Assignment A

The state built from its four components.

Equations

• DescriptiveComplexity.qsLift D T u r (Sum.inl false) v = D (v 0)
• DescriptiveComplexity.qsLift D T u r (Sum.inl true) v = T (v 0)
• DescriptiveComplexity.qsLift D T u r (Sum.inr false) x_2 = u
• DescriptiveComplexity.qsLift D T u r (Sum.inr true) x_2 = r

@[simp]

theorem DescriptiveComplexity.qsSet_qsLift {A : Type} (D T : A → Prop) (u r : Prop) : qsSet (qsLift D T u r) = D

@[simp]

theorem DescriptiveComplexity.qsVal_qsLift {A : Type} (D T : A → Prop) (u r : Prop) : qsVal (qsLift D T u r) = T

@[simp]

theorem DescriptiveComplexity.qsUp_qsLift {A : Type} (D T : A → Prop) (u r : Prop) : qsUp (qsLift D T u r) = u

@[simp]

theorem DescriptiveComplexity.qsRes_qsLift {A : Type} (D T : A → Prop) (u r : Prop) : qsRes (qsLift D T u r) = r

theorem DescriptiveComplexity.qsAssignment_ext {A : Type} {ρ σ : qsBlock.Assignment A} (hD : ∀ (a : A), qsSet ρ a ↔ qsSet σ a) (hT : ∀ (a : A), qsVal ρ a ↔ qsVal σ a) (hu : qsUp ρ ↔ qsUp σ) (hr : qsRes ρ ↔ qsRes σ) : ρ = σ

A state is determined by its four components.

theorem DescriptiveComplexity.relMap_qsVar₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) (i : Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (qsVar₁ i) w ↔ qsPred ρ i (w 0)

theorem DescriptiveComplexity.relMap_qsBit₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) (i : Bool) (w : Fin 0 → A) : FirstOrder.Language.Structure.RelMap (qsBit₁ i) w ↔ qsBit ρ i

theorem DescriptiveComplexity.relMap_qsIn₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {n : ℕ} (ρ : qsBlock.Assignment A) (r : FirstOrder.Language.qsat.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (qsIn₁ r) w ↔ FirstOrder.Language.Structure.RelMap r w

theorem DescriptiveComplexity.relMap_qsCur₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (i : Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (qsCur₂ i) w ↔ qsPred ρ i (w 0)

theorem DescriptiveComplexity.relMap_qsNext₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (i : Bool) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (qsNext₂ i) w ↔ qsPred σ i (w 0)

theorem DescriptiveComplexity.relMap_qsCurBit₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (i : Bool) (w : Fin 0 → A) : FirstOrder.Language.Structure.RelMap (qsCurBit₂ i) w ↔ qsBit ρ i

theorem DescriptiveComplexity.relMap_qsNextBit₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (i : Bool) (w : Fin 0 → A) : FirstOrder.Language.Structure.RelMap (qsNextBit₂ i) w ↔ qsBit σ i

theorem DescriptiveComplexity.relMap_qsIn₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {n : ℕ} (ρ σ : qsBlock.Assignment A) (r : FirstOrder.Language.qsat.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (qsIn₂ r) w ↔ FirstOrder.Language.Structure.RelMap r w

Splitting the connectives of a sentence

Instance search does not see through a specification's block, so the propositional connectives of the three sentences are split by hand.

theorem DescriptiveComplexity.qsRealize_inf₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) (φ ψ : qsLang₁.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

theorem DescriptiveComplexity.qsRealize_inf₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (φ ψ : qsLang₂.Sentence) : A ⊨ φ ⊓ ψ ↔ A ⊨ φ ∧ A ⊨ ψ

theorem DescriptiveComplexity.qsRealize_imp₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (φ ψ : qsLang₂.Sentence) : A ⊨ FirstOrder.Language.Formula.imp φ ψ ↔ A ⊨ φ → A ⊨ ψ

theorem DescriptiveComplexity.qsRealize_not₂ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) (φ : qsLang₂.Sentence) : A ⊨ FirstOrder.Language.BoundedFormula.not φ ↔ ¬A ⊨ φ

The walk, read back

def DescriptiveComplexity.QGreatest {A : Type} [FirstOrder.Language.qsat.Structure A] (D : A → Prop) (x : A) : Prop

The last variable of a branch: the prefixLt-greatest variable of D.

Equations

• DescriptiveComplexity.QGreatest D x = (DescriptiveComplexity.IsQVar x ∧ D x ∧ ∀ (y : A), DescriptiveComplexity.IsQVar y → D y → ¬DescriptiveComplexity.QPrec x y)

theorem DescriptiveComplexity.QGreatest.unique {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) {D : A → Prop} {x y : A} (hx : QGreatest D x) (hy : QGreatest D y) : x = y

The last variable of a branch is unique.

def DescriptiveComplexity.QPop {A : Type} [FirstOrder.Language.qsat.Structure A] (T : A → Prop) (r : Prop) (x : A) : Prop

The subtree of x is settled by the value r just returned: either x has been played twice already, or r is decisive for its quantifier – true at an existential x, false at a universal one.

Equations

• DescriptiveComplexity.QPop T r x = (T x ∨ DescriptiveComplexity.IsQAll x ∧ ¬r ∨ ¬DescriptiveComplexity.IsQAll x ∧ r)

def DescriptiveComplexity.qRem {A : Type} (D : A → Prop) (x : A) : A → Prop

Removing a variable from the quantified set.

Equations

• DescriptiveComplexity.qRem D x y = (y ≠ x ∧ D y)

theorem DescriptiveComplexity.qsSpec_step_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ σ : qsBlock.Assignment A) : qsSpec.Step ρ σ ↔ (¬qsUp ρ → ((∀ (x y : A), QLeast (qsSet ρ) x → (qsSet σ y ↔ qUpd (qsSet ρ) x true y) ∧ (qsVal σ y ↔ qUpd (qsVal ρ) x false y)) ∧ ∀ (x : A), QLeast (qsSet ρ) x → ¬qsUp σ ∧ (qsRes σ ↔ qsRes ρ)) ∧ ((∀ (z : A), IsQVar z → qsSet ρ z) → ∀ (y : A), (qsSet σ y ↔ qsSet ρ y) ∧ (qsVal σ y ↔ qsVal ρ y)) ∧ ((∀ (z : A), IsQVar z → qsSet ρ z) → qsUp σ ∧ (qsRes σ ↔ QsatMatrix (qsVal ρ)))) ∧ (qsUp ρ → (∃ (x : A), QGreatest (qsSet ρ) x) ∧ ((∀ (x y : A), QGreatest (qsSet ρ) x → QPop (qsVal ρ) (qsRes ρ) x → (qsSet σ y ↔ qRem (qsSet ρ) x y) ∧ (qsVal σ y ↔ qsVal ρ y)) ∧ ∀ (x : A), QGreatest (qsSet ρ) x → QPop (qsVal ρ) (qsRes ρ) x → qsUp σ ∧ (qsRes σ ↔ qsRes ρ)) ∧ (∀ (x y : A), QGreatest (qsSet ρ) x → ¬QPop (qsVal ρ) (qsRes ρ) x → (qsSet σ y ↔ qsSet ρ y) ∧ (qsVal σ y ↔ qUpd (qsVal ρ) x true y)) ∧ ∀ (x : A), QGreatest (qsSet ρ) x → ¬QPop (qsVal ρ) (qsRes ρ) x → ¬qsUp σ ∧ (qsRes σ ↔ qsRes ρ))

The transition of the walk, read back: descending, either the next variable is played with the value false or the leaf is evaluated; returning, the last variable of the branch is popped or played a second time.

theorem DescriptiveComplexity.qsRealize_not₁ {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) (φ : qsLang₁.Sentence) : A ⊨ FirstOrder.Language.BoundedFormula.not φ ↔ ¬A ⊨ φ

theorem DescriptiveComplexity.qsSpec_isSrc_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) : qsSpec.IsSrc ρ ↔ QsatWf A ∧ (∀ (y : A), ¬qsSet ρ y) ∧ ¬qsUp ρ

The starting states: a well-formed instance at the initial position – nothing quantified, about to descend.

theorem DescriptiveComplexity.qsSpec_isTgt_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (ρ : qsBlock.Assignment A) : qsSpec.IsTgt ρ ↔ (∀ (y : A), ¬qsSet ρ y) ∧ qsUp ρ ∧ qsRes ρ

The accepting states: back at the initial position, returning the value true.

The walk is the depth-first evaluation

theorem DescriptiveComplexity.qUpd_true_eq_qAdd {A : Type} (D : A → Prop) (x : A) : qUpd D x true = qAdd D x

Setting a variable to true is adding it.

theorem DescriptiveComplexity.qUpd_false_eq_qRem {A : Type} (D : A → Prop) (x : A) : qUpd D x false = qRem D x

Setting a variable to false is removing it.

theorem DescriptiveComplexity.qsLift_congr {A : Type} {D D' T T' : A → Prop} {u u' r r' : Prop} (hD : ∀ (y : A), D y ↔ D' y) (hT : ∀ (y : A), T y ↔ T' y) (hu : u ↔ u') (hr : r ↔ r') : qsLift D T u r = qsLift D' T' u' r'

def DescriptiveComplexity.QDownClosed {A : Type} [FirstOrder.Language.qsat.Structure A] (D : A → Prop) : Prop

The quantified set of a position is downward closed for the prefix order: the variables already played are an initial segment.

Equations

• DescriptiveComplexity.QDownClosed D = ∀ (y z : A), DescriptiveComplexity.IsQVar y → DescriptiveComplexity.QPrec y z → D z → D y

theorem DescriptiveComplexity.qDownClosed_empty {A : Type} [FirstOrder.Language.qsat.Structure A] : QDownClosed fun (x : A) => False

theorem DescriptiveComplexity.QLeast.qDownClosed_qAdd {A : Type} [FirstOrder.Language.qsat.Structure A] {D : A → Prop} {x : A} (hx : QLeast D x) (hD : QDownClosed D) : QDownClosed (qAdd D x)

theorem DescriptiveComplexity.QLeast.qGreatest_qAdd {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D : A → Prop} {x : A} (hx : QLeast D x) (hD : QDownClosed D) : QGreatest (qAdd D x) x

The variable just played is the last one of the branch.

theorem DescriptiveComplexity.QLeast.qRem_qAdd {A : Type} [FirstOrder.Language.qsat.Structure A] {D : A → Prop} {x : A} (hx : QLeast D x) : qRem (qAdd D x) x = D

Popping the variable just played returns to the position before it.

The four transitions

theorem DescriptiveComplexity.qsStep_leaf {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {D τ : A → Prop} (hcov : ∀ (z : A), IsQVar z → D z) (r : Prop) : qsSpec.Step (qsLift D τ False r) (qsLift D τ True (QsatMatrix τ))

theorem DescriptiveComplexity.qsStep_push {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} (hx : QLeast D x) (r : Prop) : qsSpec.Step (qsLift D τ False r) (qsLift (qAdd D x) (qUpd τ x false) False r)

theorem DescriptiveComplexity.qsStep_pop {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} {v : Prop} (hx : QGreatest D x) (hp : QPop τ v x) : qsSpec.Step (qsLift D τ True v) (qsLift (qRem D x) τ True v)

theorem DescriptiveComplexity.qsStep_flip {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} {v : Prop} (hx : QGreatest D x) (hp : ¬QPop τ v x) : qsSpec.Step (qsLift D τ True v) (qsLift D (qUpd τ x true) False v)

The next and the last variable exist

theorem DescriptiveComplexity.exists_qLeast {A : Type} [FirstOrder.Language.qsat.Structure A] [Finite A] (hwf : QsatWf A) {D : A → Prop} (h : ∃ (z : A), IsQVar z ∧ ¬D z) : ∃ (x : A), QLeast D x

On a finite well-formed instance a position that is not a leaf has a next variable.

theorem DescriptiveComplexity.exists_qGreatest {A : Type} [FirstOrder.Language.qsat.Structure A] [Finite A] (hwf : QsatWf A) {D : A → Prop} (h : ∃ (z : A), IsQVar z ∧ D z) : ∃ (x : A), QGreatest D x

On a finite well-formed instance a nonempty branch has a last variable.

The walk is deterministic

theorem DescriptiveComplexity.qsSpec_step_unique {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] (hwf : QsatWf A) {ρ σ σ' : qsBlock.Assignment A} (h : qsSpec.Step ρ σ) (h' : qsSpec.Step ρ σ') : σ = σ'

The transition relation is functional: every state has at most one successor, which is what turns the run of the walk into the only walk there is.

theorem DescriptiveComplexity.qsSpec_no_step_of_empty {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {ρ σ : qsBlock.Assignment A} (hempty : ∀ (y : A), ¬qsSet ρ y) (hup : qsUp ρ) : ¬qsSpec.Step ρ σ

A state returning a value at the empty branch is a dead end: the walk is over.

The run of the walk

theorem DescriptiveComplexity.qsSpec_run {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] (hwf : QsatWf A) (n : ℕ) (D τ : A → Prop) : QDownClosed D → {y : A | IsQVar y ∧ ¬D y}.ncard ≤ n → ∀ (r : Prop), ∃ (τ' : A → Prop), (∀ (y : A), D y → (τ' y ↔ τ y)) ∧ qsSpec.Reach (qsLift D τ False r) (qsLift D τ' True (QsatWins D τ))

The run of the walk computes the game value: started at the position (D, τ) in descending mode, the walk comes back to D in returning mode carrying QsatWins D τ, having changed nothing on D.

Correctness of the specification

theorem DescriptiveComplexity.qsatHolds_iff_accepts {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] : QsatHolds A ↔ qsSpec.Accepts A

The specification is correct: the walk accepts an instance exactly when the quantified formula it describes is true.

theorem DescriptiveComplexity.qsat_sotcDefinable : SOTCDefinable QSAT

QSAT is SO(TC) definable: the walk is the depth-first evaluation of the game tree, whose stack is the set of variables already played.

theorem DescriptiveComplexity.qsat_mem_PSPACE : PSPACE.Mem QSAT

QSAT is in PSPACE.