PSPACE is closed under FO(LFP) reductions

DescriptiveComplexity.mem_PSPACE_of_lfpReduction: a problem reducing to a polynomial-space problem by a polynomial-time reduction is in polynomial space. With it, every class of this library from PTIME to PSPACE – and every level of the polynomial hierarchy in between – is closed under ≤ˡᶠᵖ, hence under ≤ᵗᶜ and ≤ᵈᵗᶜ.

The route, and why it is the fixed-point one

DescriptiveComplexity.PSPACE is defined by SO(TC), so the natural attempt is to absorb the reduction's induction into the walk: give the walk's state a copy of the induction's variables, iterate the induction in it, freeze, then run the original walk. That works, and it is the same construction as the one carried out here – but on the fixed-point side of the capture theorem it costs one construction instead of two, because the pullback half is already built: DescriptiveComplexity.StepDef.pullRel pulls a simultaneous iteration through a relativized interpretation, where SO(TC) would need that written afresh.

So the proof goes: FO(≤, PFP) is PSPACE (DescriptiveComplexity.PSPACE through DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE); the membership witness of Q is pulled back through the reduction's interpretation (DescriptiveComplexity.StepDef.pfpHolds_pullRel); and the reduction's own induction is absorbed by DescriptiveComplexity.StepDef.pfpHolds_stratifyPFP – an inflationary stratum gating a partial one, which is the walk-with-a-preliminary-phase written as an iteration.

That last step is where the earlier pessimism about FO(PFP) was wrong: what a partial iteration cannot do is gate itself, and it does not have to – the gate is an arity-0 variable of the state, set by the inflationary stratum, and the partial stratum is merely conjoined with it.

theorem DescriptiveComplexity.PFPDefinable.of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : LFPReduction P Q) (h : PFPDefinable Q) : PFPDefinable P

FO(≤, PFP) definability is closed under FO(LFP) reductions: the membership iteration is pulled back through the (order-extended) interpretation, and the reduction's induction is absorbed as an inflationary stratum gating it.

theorem DescriptiveComplexity.mem_PSPACE_of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : LFPReduction P Q) (h : PSPACE.Mem Q) : PSPACE.Mem P

PSPACE is closed under FO(LFP) reductions.

theorem DescriptiveComplexity.mem_PSPACE_of_tcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : TCReduction P Q) (h : PSPACE.Mem Q) : PSPACE.Mem P

PSPACE is closed under FO(TC) reductions.

theorem DescriptiveComplexity.mem_PSPACE_of_dtcReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : DTCReduction P Q) (h : PSPACE.Mem Q) : PSPACE.Mem P

PSPACE is closed under FO(DTC) reductions.

theorem DescriptiveComplexity.SOTCDefinable.of_lfpReduction {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (f : LFPReduction P Q) (h : SOTCDefinable Q) : SOTCDefinable P

SO(TC) definability is closed under FO(LFP) reductions – the same statement as DescriptiveComplexity.mem_PSPACE_of_lfpReduction, at the logic PSPACE is defined by.