The machine of a formula, written in first-order logic

DescriptiveComplexity.AltQbf.altAccepts_iff_qbf says that the alternating machine built in an ordered QBF instance accepts exactly when the formula is true. This file writes that machine down: an FOInterpretation of the alternating-machine vocabulary in the ordered QBF vocabulary, dimension two, tagged by DescriptiveComplexity.AltQbf.AltTag.

The shape is the one of DescriptiveComplexity.SatTM.satTuringInterp:

• every defining formula matches on the base tag of its arguments, the sweep index being a static number – so a side condition like “this is a real sweep” is ⊤ or ⊥, decided when the formula is built, not a subformula;
• the payload conditions are the three shapes a tag can have: both coordinates least (DescriptiveComplexity.AltQbf.acstF), one element carried (DescriptiveComplexity.AltQbf.aoneF), or a clause condition read off the instance;
• the order is DescriptiveComplexity.lexLeF, whose linearity is inherited from the LinearOrder on DescriptiveComplexity.AltQbf.AltTag, which is the very order the machine runs on.

The block marks are new here: blk i holds of a state exactly when DescriptiveComplexity.AltQbf.altBlockOf returns i, which is a function of the tag alone, so those formulas are ⊤ or ⊥ too.

The ordered vocabulary of the source

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.qbfOrd (k : ℕ) : FirstOrder.Language

The vocabulary of ordered QBF instances.

Equations

• DescriptiveComplexity.AltQbf.qbfOrd k = (FirstOrder.Language.qbf k).sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.isClSym {k : ℕ} : (qbfOrd k).Relations 1

Being a clause.

Equations

• DescriptiveComplexity.AltQbf.isClSym = Sum.inl FirstOrder.Language.qbfIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.posInSym {k : ℕ} : (qbfOrd k).Relations 2

Occurring positively.

Equations

• DescriptiveComplexity.AltQbf.posInSym = Sum.inl FirstOrder.Language.qbfPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.negInSym {k : ℕ} : (qbfOrd k).Relations 2

Occurring negatively.

Equations

• DescriptiveComplexity.AltQbf.negInSym = Sum.inl FirstOrder.Language.qbfNegIn

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.blkSym {k : ℕ} (i : Fin k) : (qbfOrd k).Relations 1

Carrying the mark of the i-th block.

Equations

• DescriptiveComplexity.AltQbf.blkSym i = Sum.inl (FirstOrder.Language.qbfBlock i)

@[reducible, inline]

abbrev DescriptiveComplexity.AltQbf.ordSym {k : ℕ} : (qbfOrd k).Relations 2

The ambient order.

Equations

• DescriptiveComplexity.AltQbf.ordSym = Sum.inr FirstOrder.Language.leSymb

The formula builders

def DescriptiveComplexity.AltQbf.clF {k : ℕ} {α : Type} (x : α) : (qbfOrd k).Formula α

x is a clause.

Equations

• DescriptiveComplexity.AltQbf.clF x = DescriptiveComplexity.AltQbf.isClSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.AltQbf.posF {k : ℕ} {α : Type} (c x : α) : (qbfOrd k).Formula α

x occurs positively in c.

Equations

• DescriptiveComplexity.AltQbf.posF c x = DescriptiveComplexity.AltQbf.posInSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.AltQbf.negF {k : ℕ} {α : Type} (c x : α) : (qbfOrd k).Formula α

x occurs negatively in c.

Equations

• DescriptiveComplexity.AltQbf.negF c x = DescriptiveComplexity.AltQbf.negInSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.AltQbf.blkF {k : ℕ} {α : Type} (i : Fin k) (x : α) : (qbfOrd k).Formula α

x carries the mark of the i-th block.

Equations

• DescriptiveComplexity.AltQbf.blkF i x = (DescriptiveComplexity.AltQbf.blkSym i).formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.AltQbf.ordF {k : ℕ} {α : Type} (x y : α) : (qbfOrd k).Formula α

x ≤ y in the ambient order.

Equations

• DescriptiveComplexity.AltQbf.ordF x y = DescriptiveComplexity.AltQbf.ordSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.AltQbf.eqF {k : ℕ} {α : Type} (x y : α) : (qbfOrd k).Formula α

x = y.

Equations

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

def DescriptiveComplexity.AltQbf.ordLtF {k : ℕ} {α : Type} (x y : α) : (qbfOrd k).Formula α

x < y in the ambient order.

Equations

• DescriptiveComplexity.AltQbf.ordLtF x y = DescriptiveComplexity.AltQbf.ordF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.AltQbf.eqF x y)

noncomputable def DescriptiveComplexity.AltQbf.minF {k : ℕ} {α : Type} (x : α) : (qbfOrd k).Formula α

x is the least element.

Equations

• DescriptiveComplexity.AltQbf.minF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.AltQbf.ordF (Sum.inl x) (Sum.inr 0))

noncomputable def DescriptiveComplexity.AltQbf.minClF {k : ℕ} {α : Type} (c : α) : (qbfOrd k).Formula α

c is the lowest clause.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.maxClF {k : ℕ} {α : Type} (c : α) : (qbfOrd k).Formula α

c is the highest clause.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.nextClF {k : ℕ} {α : Type} (c c' : α) : (qbfOrd k).Formula α

c' is the clause immediately above c.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.noClF {k : ℕ} {α : Type} : (qbfOrd k).Formula α

There is no clause at all.

Equations

• DescriptiveComplexity.AltQbf.noClF = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.AltQbf.clF (Sum.inr 0)))

def DescriptiveComplexity.AltQbf.litF {k : ℕ} {α : Type} (v : Bool) (c x : α) : (qbfOrd k).Formula α

The cell of x holding the value v satisfies the clause c: the literal test the check phase performs.

Equations

• DescriptiveComplexity.AltQbf.litF v c x = if v = true then DescriptiveComplexity.AltQbf.posF c x else DescriptiveComplexity.AltQbf.negF c x

Realization of the builders

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_clF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {x : α} : (clF x).Realize v ↔ QbfCl k (v x)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_posF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {c x : α} : (posF c x).Realize v ↔ QbfPos k (v c) (v x)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_negF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {c x : α} : (negF c x).Realize v ↔ QbfNeg k (v c) (v x)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_blkF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {i : Fin k} {x : α} : (blkF i x).Realize v ↔ QbfBlk i (v x)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_ordF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_eqF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_ordLtF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordLtF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_minF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {x : α} : (minF x).Realize v ↔ ∀ (a : A), v x ≤ a

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_minClF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {c : α} : (minClF c).Realize v ↔ QbfMinCl k (v c)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_maxClF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {c : α} : (maxClF c).Realize v ↔ QbfMaxCl k (v c)

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_nextClF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {c c' : α} : (nextClF c c').Realize v ↔ QbfNextCl k (v c) (v c')

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_noClF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} : noClF.Realize v ↔ ∀ (e : A), ¬QbfCl k e

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_litF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {v : α → A} {b : Bool} {c x : α} : (litF b c x).Realize v ↔ QbfLit k (v c) (v x) b

The shapes of the machine's elements, as formulas

def DescriptiveComplexity.AltQbf.sideF {k : ℕ} (α : Type) (p : Prop) [Decidable p] : (qbfOrd k).Formula α

A side condition decided when the formula is built: the sweep indices are static, so “this is a real sweep” is a truth value, not a subformula.

Equations

• DescriptiveComplexity.AltQbf.sideF α p = if p then ⊤ else ⊥

@[simp]

theorem DescriptiveComplexity.AltQbf.realize_sideF {k : ℕ} {α A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {p : Prop} [Decidable p] {v : α → A} : (sideF α p).Realize v ↔ p

noncomputable def DescriptiveComplexity.AltQbf.acstF {k : ℕ} (s t' : AltTag k) : (qbfOrd k).Formula (Fin 2 × Fin 2)

The second argument is the constant of the tag s: the right tag, and both coordinates least.

Equations

• DescriptiveComplexity.AltQbf.acstF s t' = if t' = s then DescriptiveComplexity.AltQbf.minF (1, 0) ⊓ DescriptiveComplexity.AltQbf.minF (1, 1) else ⊥

noncomputable def DescriptiveComplexity.AltQbf.aoneF {k : ℕ} (s : AltTag k) (x : Fin 2 × Fin 2) (t' : AltTag k) : (qbfOrd k).Formula (Fin 2 × Fin 2)

The second argument is the tag s carrying the value of x.

Equations

• DescriptiveComplexity.AltQbf.aoneF s x t' = if t' = s then DescriptiveComplexity.AltQbf.eqF (1, 0) x ⊓ DescriptiveComplexity.AltQbf.minF (1, 1) else ⊥

The block of a state, read off its tag

def DescriptiveComplexity.AltQbf.altBlockOfTag {k : ℕ} (t : AltTag k) : ℕ

The quantifier block of a state, as a function of its tag alone: this is what makes the block marks statically decided formulas.

Equations

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

theorem DescriptiveComplexity.AltQbf.altBlockOf_eq_tag {k : ℕ} {A : Type} (q : AltV k A) : altBlockOf q = altBlockOfTag q.1

The defining formulas

One per symbol of FirstOrder.Language.turingAlt, each matching on the base tag of its arguments. The sweep index is static: a condition on it is sideF, and so is the block a state belongs to.

noncomputable def DescriptiveComplexity.AltQbf.posnF {k : ℕ} : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for posn.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.trF {k : ℕ} (cnf : Bool) : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for tr: the payload promises of DescriptiveComplexity.AltQbf.AltTr, the index conditions decided statically.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.startF {k : ℕ} : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for start.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.accF {k : ℕ} : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for acc: acceptance is read off the base tag alone.

Equations

• DescriptiveComplexity.AltQbf.accF t = match t.1 with | DescriptiveComplexity.AltQbf.AltBase.qAcc => ⊤ | x => ⊥

noncomputable def DescriptiveComplexity.AltQbf.blankF {k : ℕ} : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for blank.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.rightF {k : ℕ} : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for right: a static condition on the tag.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.inpF {k : ℕ} : AltTag k → AltTag k → (qbfOrd k).Formula (Fin 2 × Fin 2)

Defining formula for inp, the initial tape.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.tsrcF {k : ℕ} (cnf : Bool) : AltTag k → AltTag k → (qbfOrd k).Formula (Fin 2 × Fin 2)

Defining formula for tsrc.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.treadF {k : ℕ} : AltTag k → AltTag k → (qbfOrd k).Formula (Fin 2 × Fin 2)

Defining formula for tread.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.tdstF {k : ℕ} (cnf : Bool) : AltTag k → AltTag k → (qbfOrd k).Formula (Fin 2 × Fin 2)

Defining formula for tdst: the one place the instance is consulted, in the check clause, through DescriptiveComplexity.AltQbf.litF.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.twriteF {k : ℕ} : AltTag k → AltTag k → (qbfOrd k).Formula (Fin 2 × Fin 2)

Defining formula for twrite.

Equations

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

noncomputable def DescriptiveComplexity.AltQbf.blkStF {k : ℕ} (i : Fin k) : AltTag k → (qbfOrd k).Formula (Fin 1 × Fin 2)

Defining formula for the i-th block mark: the block of a state is a function of its tag.

Equations

• DescriptiveComplexity.AltQbf.blkStF i t = DescriptiveComplexity.AltQbf.sideF (Fin 1 × Fin 2) (↑i = DescriptiveComplexity.AltQbf.altBlockOfTag t)

noncomputable def DescriptiveComplexity.AltQbf.altTuringInterp (k : ℕ) (cnf : Bool) : FOInterpretation (qbfOrd k) (FirstOrder.Language.turingAlt k) (AltTag k) 2

The interpretation of alternating machine instances in ordered QBF instances: the machine M_φ of the formula, written down.

Equations

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

The realization lemmas

One per symbol, each saying that its defining formula defines the corresponding predicate of DescriptiveComplexity.AltQbf.altMachine. The universe of the interpreted structure is definitionally DescriptiveComplexity.AltV k A.

def DescriptiveComplexity.AltQbf.altMapEquiv {k : ℕ} {A : Type} (cnf : Bool) : AltV k A ≃ (altTuringInterp k cnf).Map A

The identity equivalence between the tagged tuples and the interpreted universe.

Equations

• DescriptiveComplexity.AltQbf.altMapEquiv cnf = Equiv.refl (DescriptiveComplexity.AltQbf.AltV k A)

@[simp]

theorem DescriptiveComplexity.AltQbf.altMapEquiv_apply {k : ℕ} {A : Type} (cnf : Bool) (p : AltV k A) : (altMapEquiv cnf) p = p

theorem DescriptiveComplexity.AltQbf.relMap_posn {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMPosn ((altMapEquiv cnf) p) ↔ AltPosn p

theorem DescriptiveComplexity.AltQbf.relMap_tr {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMTr ((altMapEquiv cnf) p) ↔ AltTr cnf p

theorem DescriptiveComplexity.AltQbf.relMap_start {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMStart ((altMapEquiv cnf) p) ↔ AltStartSt p

theorem DescriptiveComplexity.AltQbf.relMap_acc {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMAcc ((altMapEquiv cnf) p) ↔ AltAccSt p

theorem DescriptiveComplexity.AltQbf.relMap_blank {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMBlank ((altMapEquiv cnf) p) ↔ AltBlank p

theorem DescriptiveComplexity.AltQbf.relMap_right {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p : AltV k A) : ATMRight ((altMapEquiv cnf) p) ↔ AltRight p

theorem DescriptiveComplexity.AltQbf.relMap_le {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (p q : AltV k A) : ATMLe ((altMapEquiv cnf) p) ((altMapEquiv cnf) q) ↔ tagTupleLe p q

theorem DescriptiveComplexity.AltQbf.relMap_blk {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) (hk : 0 < k) (j : ℕ) (p : AltV k A) : ATMBlk j ((altMapEquiv cnf) p) ↔ AltBlkOf j p

The machines agree, and the reduction