A sentence as an alternating prefix, played one variable at a time

The first of the two normal forms that let a machine evaluate a fixed first-order sentence with a finite control. A machine simulating an DescriptiveComplexity.SOGameSpec has to decide the specification's four sentences, and the only shape its control can have is a finite set of phases carrying a tuple of elements. This file supplies the shape:

every sentence is an alternating quantifier prefix over a quantifier-free matrix, and the prefix is a walk through the indices 0, 1, …, n - 1, choosing the value of one variable at each step.

DescriptiveComplexity.altQuantFrom is that walk. Its state is exactly the state of the machine that plays it: an index j – the phase – and a valuation Fin n → A – the tuple – of which only the coordinates below j matter. Each step updates one coordinate, existentially or universally as the polarity pol j says, and at j = n the matrix is read off.

DescriptiveComplexity.exists_altQuant produces the data (the length n, the polarities and the matrix) for an arbitrary sentence, by FirstOrder.Language.BoundedFormula.toPrenex followed by an induction on FirstOrder.Language.BoundedFormula.IsPrenex.

Why the valuation is total, and updated in place

A prenex prefix is usually peeled with Fin.snoc, the valuation growing one coordinate at a time; the matrix then sits at a level that changes during the induction and the arithmetic (k + 1) + m = k + (m + 1) has to be transported along a cast at every step. Here the total length n is fixed by the induction hypothesis and it is the number k of variables already bound that grows, so the matrix never moves, no cast appears, and – this is the point – the resulting predicate is literally the transition system a machine runs: one phase index, one tuple, one coordinate written per step.

The prefix as a walk

def DescriptiveComplexity.altQuantAux {A : Type u_1} {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → A) → Prop) : ℕ → ℕ → (Fin n → A) → Prop

The walk of DescriptiveComplexity.altQuantFrom, with an explicit fuel so that the recursion is structural. The fuel is the number of variables left to choose.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.altQuantAux pol P 0 x✝¹ x✝ = P x✝

def DescriptiveComplexity.altQuantFrom {A : Type u_1} {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → A) → Prop) (j : ℕ) (v : Fin n → A) : Prop

An alternating quantifier prefix, from the j-th variable on: the variables j, j + 1, …, n - 1 are chosen in turn, the i-th by the player pol i names, and the predicate P is then read off the resulting valuation.

Only the coordinates below j of the valuation matter (DescriptiveComplexity.altQuantFrom_congr_val), so a machine playing the prefix may carry an arbitrary tuple and overwrite it as it goes.

Equations

• DescriptiveComplexity.altQuantFrom pol P j v = DescriptiveComplexity.altQuantAux pol P (n - j) j v

theorem DescriptiveComplexity.altQuantFrom_of_le {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {j : ℕ} (h : n ≤ j) (v : Fin n → A) : altQuantFrom pol P j v = P v

Past the last variable, the prefix is the matrix.

theorem DescriptiveComplexity.altQuantFrom_last {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} (v : Fin n → A) : altQuantFrom pol P n v = P v

The prefix at its end is the matrix.

theorem DescriptiveComplexity.altQuantFrom_ex {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {j : ℕ} (h : j < n) (hp : pol j = true) (v : Fin n → A) : altQuantFrom pol P j v ↔ ∃ (a : A), altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)

One existential step of the prefix: the j-th variable is chosen by the existential player.

theorem DescriptiveComplexity.altQuantFrom_all {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {j : ℕ} (h : j < n) (hp : pol j = false) (v : Fin n → A) : altQuantFrom pol P j v ↔ ∀ (a : A), altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)

One universal step of the prefix: the j-th variable is chosen by the universal player.

theorem DescriptiveComplexity.altQuantFrom_congr_pol {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {pol' : ℕ → Bool} {j : ℕ} (hagree : ∀ (i : ℕ), j ≤ i → pol i = pol' i) (v : Fin n → A) : altQuantFrom pol P j v = altQuantFrom pol' P j v

The prefix only reads the polarities of the variables it still has to choose.

theorem DescriptiveComplexity.altQuantFrom_congr_val {A : Type u_1} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {j : ℕ} (v v' : Fin n → A) (hagree : ∀ (i : Fin n), ↑i < j → v i = v' i) : altQuantFrom pol P j v = altQuantFrom pol P j v'

The prefix only reads the coordinates already chosen: a machine playing it may carry an arbitrary tuple and overwrite it as it goes.

theorem DescriptiveComplexity.snoc_castLE_update {A : Type u_1} {k n : ℕ} (hk : k < n) (hkn : k + 1 ≤ n) {v : Fin n → A} {xs : Fin k → A} (hagree : ∀ (i : Fin k), xs i = v (Fin.castLE ⋯ i)) (a : A) (i : Fin (k + 1)) : Fin.snoc xs a i = Function.update v ⟨k, hk⟩ a (Fin.castLE hkn i)

Extending a restricted valuation by one element is updating the unrestricted one at the next coordinate: the step the prefix takes, read on Fin.snoc.

Every sentence is an alternating prefix

theorem DescriptiveComplexity.exists_altQuant_of_isPrenex {M : FirstOrder.Language} {k : ℕ} {ψ : M.BoundedFormula Empty k} : ψ.IsPrenex → ∃ (n : ℕ) (hkn : k ≤ n) (pol : ℕ → Bool) (mat : M.BoundedFormula Empty n), mat.IsQF ∧ ∀ (A : Type) [inst : M.Structure A] (v : Fin n → A) (xs : Fin k → A), (∀ (i : Fin k), xs i = v (Fin.castLE hkn i)) → (ψ.Realize default xs ↔ altQuantFrom pol (fun (w : Fin n → A) => mat.Realize default w) k v)

A prenex formula is an alternating prefix over its matrix, stated for a formula with k variables already bound: the matrix has n ≥ k variables, the first k of them being the ones already bound, and the prefix chooses the remaining n - k.

The total length n comes from the induction hypothesis and never changes, so the matrix is never transported along an arithmetic identity; what grows is the number of bound variables.

theorem DescriptiveComplexity.exists_altQuant {M : FirstOrder.Language} (φ : M.Sentence) : ∃ (n : ℕ) (pol : ℕ → Bool) (mat : M.BoundedFormula Empty n), mat.IsQF ∧ ∀ (A : Type) [inst : M.Structure A] [Nonempty A] (v : Fin n → A), A ⊨ φ ↔ altQuantFrom pol (fun (w : Fin n → A) => mat.Realize default w) 0 v

Every sentence is an alternating quantifier prefix over a quantifier-free matrix, the prefix played one variable at a time.

This is the shape a machine can run: the phase is the index of the variable being chosen, the tuple is the valuation, and the matrix is read off at the end. The initial valuation is arbitrary – the prefix overwrites every coordinate it reads.