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

def DescriptiveComplexity.SpaceTM.ApplOn {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : mBlock.Assignment A) (τ : A) : Prop

The transition applies in the marked state, reading the marked cell.

Equations

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

def DescriptiveComplexity.SpaceTM.GoOn {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : mBlock.Assignment A) : Prop

The machine takes a step from this assignment: 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.

def DescriptiveComplexity.SpaceTM.mInitAssign (A : Type) [FirstOrder.Language.turing.Structure A] : mBlock.Assignment A

The initial assignment: start states, lowest positions, the initial tape. On a well-formed deterministic instance with a start state this is a configuration – the initial one.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.SpaceTM.mInitAssign A none = fun (x : Fin (DescriptiveComplexity.SpaceTM.mBlock.arity none) → A) => (DescriptiveComplexity.tmData A).InitTape (x 0) (x 1)
• DescriptiveComplexity.SpaceTM.mInitAssign A (some false) = fun (x : Fin (DescriptiveComplexity.SpaceTM.mBlock.arity (some false)) → A) => DescriptiveComplexity.TMStart (x 0)

def DescriptiveComplexity.SpaceTM.mNextAssign {A : Type} [FirstOrder.Language.turing.Structure A] (ρ : mBlock.Assignment A) : mBlock.Assignment A

One application of the step formulas, semantically: load the initial configuration from the empty assignment, take the machine step when one is available and the state is not accepting, stutter otherwise.

Equations

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

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.

noncomputable def DescriptiveComplexity.SpaceTM.stepTapeF : mLang₁.Formula (Fin 2)

The step formula of the tape variable.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.stepStateF : mLang₁.Formula (Fin 1)

The step formula of the state variable.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.stepHeadF : mLang₁.Formula (Fin 1)

The step formula of the head variable.

Equations

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

noncomputable def DescriptiveComplexity.SpaceTM.mPfp : StepDef mBase

The machine iteration: one configuration in the block, one machine step per stage, stuttering on halting configurations; the output checks the instance and reads acceptance off the stable configuration.

Equations

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

The step formulas mean the semantic step

theorem DescriptiveComplexity.SpaceTM.realize_emptyF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) {γ : Type} (v : γ → A) : emptyF.Realize v ↔ StateEmptyOn ρ

theorem DescriptiveComplexity.SpaceTM.realize_mGoF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) {γ : Type} (v : γ → A) : mGoF.Realize v ↔ GoOn ρ

theorem DescriptiveComplexity.SpaceTM.realize_stepTapeF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (x : Fin 2 → A) : stepTapeF.Realize x ↔ mNextAssign ρ none x

theorem DescriptiveComplexity.SpaceTM.realize_stepStateF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (x : Fin 1 → A) : stepStateF.Realize x ↔ mNextAssign ρ (some false) x

theorem DescriptiveComplexity.SpaceTM.realize_stepHeadF {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) (x : Fin 1 → A) : stepHeadF.Realize x ↔ mNextAssign ρ (some true) x

theorem DescriptiveComplexity.SpaceTM.next_mPfp {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) : mPfp.next ρ = mNextAssign ρ

One application of the step formulas is 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)

theorem DescriptiveComplexity.SpaceTM.mNextAssign_of_stateEmpty {A : Type} [FirstOrder.Language.turing.Structure A] {ρ : mBlock.Assignment A} (h : StateEmptyOn ρ) : mNextAssign ρ = mInitAssign A

From an empty state mark, one step loads the initial assignment.

theorem DescriptiveComplexity.SpaceTM.mNextAssign_cfgAssign_of_not_goOn {A : Type} [FirstOrder.Language.turing.Structure A] {c : Config A} (hng : ¬GoOn (cfgAssign c)) : mNextAssign (cfgAssign c) = cfgAssign c

On a configuration from which the machine takes no step, the iteration stutters.

theorem DescriptiveComplexity.SpaceTM.mNextAssign_cfgAssign_of_acc {A : Type} [FirstOrder.Language.turing.Structure A] {c : Config A} (hacc : (tmData A).Acc c.state) : mNextAssign (cfgAssign c) = cfgAssign c

On an accepting configuration, the iteration stutters.

theorem DescriptiveComplexity.SpaceTM.step_of_goOn {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] {c : Config A} (hgo : GoOn (cfgAssign c)) : ∃ (d : Config A), (tmData A).Step c d

A configuration from which the step condition fires can take a machine step.

theorem DescriptiveComplexity.SpaceTM.mNextAssign_cfgAssign_of_step {A : Type} [FirstOrder.Language.turing.Structure A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) {c d : Config A} (hnacc : ¬(tmData A).Acc c.state) (hstep : (tmData A).Step c d) : mNextAssign (cfgAssign c) = cfgAssign d

On a non-accepting configuration that steps, the iteration takes the machine step.

theorem DescriptiveComplexity.SpaceTM.mInitAssign_eq_cfgAssign {A : Type} [FirstOrder.Language.turing.Structure A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) {c₀ : Config A} (hinit : (tmData A).IsInit c₀) : mInitAssign A = cfgAssign c₀

The initial assignment of a well-formed deterministic instance with an initial configuration is that configuration.

theorem DescriptiveComplexity.SpaceTM.partStage_one {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] : mPfp.partStage A 1 = mInitAssign A

The first stage of the iteration is the initial assignment.

theorem DescriptiveComplexity.SpaceTM.partStage_run {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) {c₀ : Config A} (hinit : (tmData A).IsInit c₀) (n : ℕ) (c : Config A) : (tmData A).StepsIn n c₀ c → (∀ k < n, ∀ (e : Config A), (tmData A).StepsIn k c₀ e → ¬(tmData A).Acc e.state) → mPfp.partStage A (n + 1) = cfgAssign c

The stages follow the run: as long as no accepting configuration has been reached, stage n + 1 is the n-th configuration of the run.

theorem DescriptiveComplexity.SpaceTM.stepsIn_of_reflTransGen {A : Type} [FirstOrder.Language.turing.Structure A] {c d : Config A} (h : Relation.ReflTransGen (tmData A).Step c d) : ∃ (n : ℕ), (tmData A).StepsIn n c d

The run reaches a configuration in some number of steps.

theorem DescriptiveComplexity.SpaceTM.realize_mOut {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (ρ : mBlock.Assignment A) : A ⊨ mPfp.out ↔ (tmData A).WellFormed ∧ (tmData A).Deterministic ∧ ∃ (q : A), mState ρ q ∧ TMAcc q

The semantics of the output sentence.

theorem DescriptiveComplexity.SpaceTM.pfpHolds_mPfp_of_acceptsSpace {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] (hwf : (tmData A).WellFormed) (hdet : (tmData A).Deterministic) (hacc : (tmData A).AcceptsSpace) : mPfp.PFPHolds A

A well-formed deterministic accepting instance makes the iteration converge with an accepting output: run to the first accepting configuration and stutter there.

theorem DescriptiveComplexity.SpaceTM.acceptsSpace_of_pfpHolds_mPfp {A : Type} [FirstOrder.Language.turing.Structure A] [LinearOrder A] [Finite A] (h : mPfp.PFPHolds A) : (tmData A).WellFormed ∧ (tmData A).Deterministic ∧ (tmData A).AcceptsSpace

A converging accepting iteration means the instance is well-formed, deterministic and accepting: the stages only ever hold the empty assignment, the initial assignment, or a configuration of the run.

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.

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.

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.