PSPACE is contained in FO(≤, PFP)

The hard half of the capture theorem FO(≤, PFP) = PSPACE, by iterating the PSPACE-complete deterministic machine problem: a partial fixed-point definition DescriptiveComplexity.SpaceTM.mPfp whose block holds one machine configuration – the block of the SO(TC) membership proof of DescriptiveComplexity.Problems.Machine.Space – and whose step formulas advance it:

• from the empty assignment (recognized by its empty state mark, which no configuration has), one step loads the initial configuration – start state, head on the lowest position, initial tape;
• from a configuration that can move – some applicable transition with a destination, a written symbol and a neighboring position to move to (DescriptiveComplexity.SpaceTM.GoOn) – and is not yet accepting, one step is the machine step, determinism making the step formulas functional;
• from an accepting or stuck configuration, the step stutters, so that a halting run is exactly a converging iteration.

A machine that loops forever diverges the iteration, and under the convergence-requiring semantics of DescriptiveComplexity.FixedPointPartial that alone makes the definition false – no divergence detection, no counter. The output sentence checks well-formedness and determinism (conditions on the instance only) and reads acceptance off the stable configuration (DescriptiveComplexity.dtmAcceptSpace_pfpDefinable).

Whence the capture: every PSPACE problem reduces to the machine problem by a relativized ordered reduction (DescriptiveComplexity.le_dtmAcceptSpace_of_mem_PSPACE), and FO(≤, PFP) definability crosses such reductions (DescriptiveComplexity.PFPDefinable.of_relOrderedReduction), so DescriptiveComplexity.pfpDefinable_of_mem_PSPACE and, with the converse inclusion of DescriptiveComplexity.FixedPointPartialSpace, the capture theorem DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE.

Formula builders

In the parameterized style of DescriptiveComplexity.Problems.Machine.Space: each builder takes the relation symbols it reads, so realization lemmas are stated over RelMap and specialize to any expansion.

noncomputable def DescriptiveComplexity.SpaceTM.markMeetF {L' : FirstOrder.Language} {γ : Type} (s r : L'.Relations 1) : L'.Formula γ

Some element carries both marks.

Equations

• DescriptiveComplexity.SpaceTM.markMeetF s r = FirstOrder.Language.Formula.iExs (Fin 1) (s.formula₁ (FirstOrder.Language.var (Sum.inr 0)) ⊓ r.formula₁ (FirstOrder.Language.var (Sum.inr 0)))

noncomputable def DescriptiveComplexity.SpaceTM.someArgF {L' : FirstOrder.Language} {γ : Type} (r : L'.Relations 2) (x : γ) : L'.Formula γ

The binary relation holds of x and some element.

Equations

• DescriptiveComplexity.SpaceTM.someArgF r x = FirstOrder.Language.Formula.iExs (Fin 1) (r.formula₂ (FirstOrder.Language.var (Sum.inl x)) (FirstOrder.Language.var (Sum.inr 0)))

noncomputable def DescriptiveComplexity.SpaceTM.applF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (τ : γ) : L'.Formula γ

τ is an applicable transition: a transition whose source is the marked state and whose read symbol is the one held by the marked cell.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.moveToF {L' : FirstOrder.Language} {γ : Type} (right : L'.Relations 1) (le : L'.Relations 2) (posn h : L'.Relations 1) (τ p' : γ) : L'.Formula γ

The head can move from the marked cell to p', in the direction the transition names.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.goF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd dst wr : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (acc right : L'.Relations 1) (le : L'.Relations 2) (posn : L'.Relations 1) : L'.Formula γ

The machine takes a step: no accepting mark, and some applicable transition with a destination, a written symbol, and a position to move to.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.initTapeAtF {L' : FirstOrder.Language} {γ : Type} (inp : L'.Relations 2) (blank : L'.Relations 1) (x y : γ) : L'.Formula γ

The cell initially holds this symbol: its input symbol, or the blank when no input is given for it.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.minPosAtF {L' : FirstOrder.Language} {γ : Type} (le : L'.Relations 2) (posn : L'.Relations 1) (x : γ) : L'.Formula γ

x is the lowest position.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_markMeetF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (s r : L'.Relations 1) : (markMeetF s r).Realize v ↔ ∃ (q : M), FirstOrder.Language.Structure.RelMap s ![q] ∧ FirstOrder.Language.Structure.RelMap r ![q]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_someArgF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (r : L'.Relations 2) (x : γ) : (someArgF r x).Realize v ↔ ∃ (b : M), FirstOrder.Language.Structure.RelMap r ![v x, b]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_applF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (τ : γ) : (applF tr src rd s h t τ).Realize v ↔ FirstOrder.Language.Structure.RelMap tr ![v τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![v τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![v τ, a]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_moveToF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (right : L'.Relations 1) (le : L'.Relations 2) (posn h : L'.Relations 1) (τ p' : γ) : (moveToF right le posn h τ p').Realize v ↔ ∃ (p : M), FirstOrder.Language.Structure.RelMap h ![p] ∧ (FirstOrder.Language.Structure.RelMap right ![v τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p (v p') ∨ ¬FirstOrder.Language.Structure.RelMap right ![v τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v p') p)

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_goF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd dst wr : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (acc right : L'.Relations 1) (le : L'.Relations 2) (posn : L'.Relations 1) : (goF tr src rd dst wr s h t acc right le posn).Realize v ↔ (¬∃ (q : M), FirstOrder.Language.Structure.RelMap s ![q] ∧ FirstOrder.Language.Structure.RelMap acc ![q]) ∧ ∃ (τ : M) (p' : M), (FirstOrder.Language.Structure.RelMap tr ![τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![τ, a]) ∧ (∃ (b : M), FirstOrder.Language.Structure.RelMap dst ![τ, b]) ∧ (∃ (b : M), FirstOrder.Language.Structure.RelMap wr ![τ, b]) ∧ ∃ (p : M), FirstOrder.Language.Structure.RelMap h ![p] ∧ (FirstOrder.Language.Structure.RelMap right ![τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p p' ∨ ¬FirstOrder.Language.Structure.RelMap right ![τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p' p)

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_initTapeAtF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (inp : L'.Relations 2) (blank : L'.Relations 1) (x y : γ) : (initTapeAtF inp blank x y).Realize v ↔ FirstOrder.Language.Structure.RelMap inp ![v x, v y] ∨ (∀ (b : M), ¬FirstOrder.Language.Structure.RelMap inp ![v x, b]) ∧ FirstOrder.Language.Structure.RelMap blank ![v y]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_minPosAtF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (le : L'.Relations 2) (posn : L'.Relations 1) (x : γ) : (minPosAtF le posn x).Realize v ↔ MinPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v x)

noncomputable def DescriptiveComplexity.SpaceTM.writeNewF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t wr : L'.Relations 2) (y : γ) : L'.Formula γ

The transition applies, with a destination, a written symbol, and this new symbol written in the marked cell.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.dstNewF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t dst : L'.Relations 2) (y : γ) : L'.Formula γ

The transition applies and moves to this new state.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.headNewF {L' : FirstOrder.Language} {γ : Type} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (right : L'.Relations 1) (le : L'.Relations 2) (posn : L'.Relations 1) (y : γ) : L'.Formula γ

The transition applies and moves the head to this new position.

Equations

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

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_writeNewF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t wr : L'.Relations 2) (y : γ) : (writeNewF tr src rd s h t wr y).Realize v ↔ ∃ (τ : M), (FirstOrder.Language.Structure.RelMap tr ![τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![τ, a]) ∧ FirstOrder.Language.Structure.RelMap wr ![τ, v y]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_dstNewF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t dst : L'.Relations 2) (y : γ) : (dstNewF tr src rd s h t dst y).Realize v ↔ ∃ (τ : M), (FirstOrder.Language.Structure.RelMap tr ![τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![τ, a]) ∧ FirstOrder.Language.Structure.RelMap dst ![τ, v y]

@[simp]

theorem DescriptiveComplexity.SpaceTM.realize_headNewF {L' : FirstOrder.Language} {M : Type} [L'.Structure M] {γ : Type} {v : γ → M} (tr : L'.Relations 1) (src rd : L'.Relations 2) (s h : L'.Relations 1) (t : L'.Relations 2) (right : L'.Relations 1) (le : L'.Relations 2) (posn : L'.Relations 1) (y : γ) : (headNewF tr src rd s h t right le posn y).Realize v ↔ ∃ (τ : M), (FirstOrder.Language.Structure.RelMap tr ![τ] ∧ (∀ (q : M), FirstOrder.Language.Structure.RelMap s ![q] → FirstOrder.Language.Structure.RelMap src ![τ, q]) ∧ ∀ (p a : M), FirstOrder.Language.Structure.RelMap h ![p] → FirstOrder.Language.Structure.RelMap t ![p, a] → FirstOrder.Language.Structure.RelMap rd ![τ, a]) ∧ ∃ (p : M), FirstOrder.Language.Structure.RelMap h ![p] ∧ (FirstOrder.Language.Structure.RelMap right ![τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) p (v y) ∨ ¬FirstOrder.Language.Structure.RelMap right ![τ] ∧ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v y) p)

The iterated definition and its semantics

def DescriptiveComplexity.SpaceTM.StateEmptyOn {A : Type} (ρ : mBlock.Assignment A) : Prop

The state mark is empty: how the iteration recognizes the not-yet-started assignment, which no configuration resembles.

Equations

• DescriptiveComplexity.SpaceTM.StateEmptyOn ρ = ¬∃ (q : A), DescriptiveComplexity.SpaceTM.mState ρ q

The step formulas

noncomputable def DescriptiveComplexity.SpaceTM.emptyF {γ : Type} : mLang₁.Formula γ

The empty-state test, as a formula.

Equations

• DescriptiveComplexity.SpaceTM.emptyF = FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SpaceTM.someF DescriptiveComplexity.SpaceTM.mS₁)

noncomputable def DescriptiveComplexity.SpaceTM.mGoF {γ : Type} : mLang₁.Formula γ

The step condition, at the machine's symbols.

Equations

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

The step formulas mean the semantic step

The iteration follows the run

theorem DescriptiveComplexity.SpaceTM.not_stateEmptyOn_cfgAssign {A : Type} (c : Config A) : ¬StateEmptyOn (cfgAssign c)

theorem DescriptiveComplexity.SpaceTM.stateEmptyOn_botAssign {A : Type} : StateEmptyOn (mBlock.botAssign A)

The capture theorem

theorem DescriptiveComplexity.dtmAcceptSpace_pfpDefinable : PFPDefinable DTMAcceptSpace

The deterministic space-bounded machine problem is FO(≤, PFP) definable: iterate the machine, stuttering on halting configurations.

theorem DescriptiveComplexity.pfpDefinable_of_mem_PSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : PSPACE.Mem P) : PFPDefinable P

PSPACE is contained in FO(≤, PFP): reduce to the machine problem and pull the iteration back through the relativized reduction. Registered in the Lax archive as Lax134656.PartialFixedPointCapture.pfpDefinable_of_mem_PSPACE.

theorem DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PFPDefinable P ↔ PSPACE.Mem P

The capture theorem FO(≤, PFP) = PSPACE (Abiteboul–Vianu 1989; Ebbinghaus–Flum 1995, ch. 7): a problem is FO(≤, PFP) definable exactly when it is in PSPACE. Registered in the Lax archive as Lax134656.PartialFixedPointCapture.pfpDefinable_iff_mem_PSPACE.

theorem DescriptiveComplexity.pfpDefinable_iff_sotcDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : PFPDefinable P ↔ SOTCDefinable P

The capture theorem, logic to logic: FO(≤, PFP) and SO(TC) define the same problems.