An element, quantified in front of a fixed point

The theorem: FO(≤, IFP) definability – hence membership in DescriptiveComplexity.PTIME – is closed under existential quantification over one element (DescriptiveComplexity.IFPDefinable.exElement, DescriptiveComplexity.mem_PTIME_exElement). If a problem R over the vocabulary extended by a mark (DescriptiveComplexity.newLang, one unary symbol) is definable, then so is “some element, marked, makes R hold”.

Semantically there is nothing to it – trying every element multiplies the work by the size of the instance – but a fixed point cannot be restarted once per element, so the construction runs all of them at once: every relation variable gains one argument, the parameter, and every stage of the iteration then holds the stages of all the instances side by side (DescriptiveComplexity.StepDef.inflStage_param). The mark is not a symbol of the new vocabulary any more, so the atom old t becomes the equation t = parameter; nothing else changes, since the universe does not.

This is the deterministic counterpart of DescriptiveComplexity.SOTCDefinable.exBlock, which prefixes a walk with a guessed relation – a walk may guess, a fixed point may not, and one element is what a fixed point can afford instead.

Where it is used

DescriptiveComplexity.Exponential.FreeTime: the order-free reading of DescriptiveComplexity.EXPTIME has to say “some copy of the order-guessing expansion answers yes”, and a copy is named by any one of its points.

A structure with one marked element

@[instance_reducible]

def DescriptiveComplexity.oneMark {N : Type} (c : N) : FirstOrder.Language.oldMark.Structure N

The mark of a single element, as a structure over the marking vocabulary.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.markOne (L : FirstOrder.Language) {N : Type} [inst : L.Structure N] (c : N) : (newLang L).Structure N

The instance with one element marked, over DescriptiveComplexity.newLang.

Equations

• DescriptiveComplexity.markOne L c = L.sumStructure FirstOrder.Language.oldMark N

The block, with a parameter argument

DescriptiveComplexity.SOBlock.withParam and its reading at a parameter are SecondOrderParam.lean's; what is here is the one statement that mentions the empty assignment.

theorem DescriptiveComplexity.SOBlock.atParam_bot {N : Type} (B : SOBlock) (c : N) : B.atParam (B.withParam.botAssign N) c = B.botAssign N

The parameter substitution

def DescriptiveComplexity.paramTerm {L : FirstOrder.Language} [L.IsRelational] (B : SOBlock) {β : Type} : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Term β → ((L.sum FirstOrder.Language.order).sum B.withParam.lang).Term β

A term of the marked vocabulary, read in the parameterized one: over relational vocabularies a term is a variable, so there is nothing to do.

Equations

• DescriptiveComplexity.paramTerm B (FirstOrder.Language.var x_1) = FirstOrder.Language.var x_1
• DescriptiveComplexity.paramTerm B (FirstOrder.Language.func f _ts) = isEmptyElim f

def DescriptiveComplexity.paramLift {L : FirstOrder.Language} [L.IsRelational] (B : SOBlock) {α : Type} (p : α) {n : ℕ} : (((newLang L).sum FirstOrder.Language.order).sum B.lang).BoundedFormula α n → ((L.sum FirstOrder.Language.order).sum B.withParam.lang).BoundedFormula α n

The parameter substitution: the mark becomes “equal to the parameter”, every fixed-point variable takes the parameter as a further argument, and everything else is left alone – in particular the quantifiers, the universe being unchanged.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.paramLift B p FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• DescriptiveComplexity.paramLift B p (φ.imp ψ) = (DescriptiveComplexity.paramLift B p φ).imp (DescriptiveComplexity.paramLift B p ψ)
• DescriptiveComplexity.paramLift B p φ.all = (DescriptiveComplexity.paramLift B p φ).all

theorem DescriptiveComplexity.realize_paramTerm {L : FirstOrder.Language} [L.IsRelational] {N : Type} {B : SOBlock} [L.Structure N] [LinearOrder N] {β : Type} (ρ : B.withParam.Assignment N) (c : N) (v : β → N) (t : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Term β) : FirstOrder.Language.Term.realize v (paramTerm B t) = FirstOrder.Language.Term.realize v t

theorem DescriptiveComplexity.realize_paramLift {L : FirstOrder.Language} [L.IsRelational] {N : Type} {B : SOBlock} {α : Type} {p : α} [L.Structure N] [LinearOrder N] (ρ : B.withParam.Assignment N) (v : α → N) {n : ℕ} (φ : (((newLang L).sum FirstOrder.Language.order).sum B.lang).BoundedFormula α n) (xs : Fin n → N) : (paramLift B p φ).Realize v xs ↔ φ.Realize v xs

The parameter substitution is correct: read at an assignment of the extended block, the substituted formula says what the original said in the instance whose mark is the parameter, at that assignment read at the parameter.

@[instance_reducible]

def DescriptiveComplexity.markOneOrd (L : FirstOrder.Language) {N : Type} [L.Structure N] [LinearOrder N] (c : N) : ((newLang L).sum FirstOrder.Language.order).Structure N

The instance with one element marked, ordered.

Equations

• DescriptiveComplexity.markOneOrd L c = DescriptiveComplexity.sumOrderStructure (DescriptiveComplexity.newLang L) N

The definition, run at every parameter at once

noncomputable def DescriptiveComplexity.StepDef.param {L : FirstOrder.Language} [L.IsRelational] (d : StepDef ((newLang L).sum FirstOrder.Language.order)) : StepDef (L.sum FirstOrder.Language.order)

Every instance at once: the same simultaneous induction, every relation variable carrying the parameter as a further argument, and the output existentially quantified over it.

Equations

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

theorem DescriptiveComplexity.StepDef.next_param {L : FirstOrder.Language} [L.IsRelational] {d : StepDef ((newLang L).sum FirstOrder.Language.order)} {N : Type} [L.Structure N] [LinearOrder N] (ρ : d.param.B.Assignment N) (c : N) : d.B.atParam (d.param.next ρ) c = d.next (d.B.atParam ρ c)

One step of the parameterized definition, read at a parameter, is one step of the original in the instance that parameter marks.

theorem DescriptiveComplexity.StepDef.inflStep_param {L : FirstOrder.Language} [L.IsRelational] {d : StepDef ((newLang L).sum FirstOrder.Language.order)} {N : Type} [L.Structure N] [LinearOrder N] (ρ : d.param.B.Assignment N) (c : N) : d.B.atParam (d.param.inflStep ρ) c = d.inflStep (d.B.atParam ρ c)

The inflationary step of the parameterized definition, read at a parameter.

theorem DescriptiveComplexity.StepDef.inflStage_param {L : FirstOrder.Language} [L.IsRelational] {d : StepDef ((newLang L).sum FirstOrder.Language.order)} {N : Type} [L.Structure N] [LinearOrder N] (c : N) (k : ℕ) : d.B.atParam (d.param.inflStage N k) c = d.inflStage N k

Every stage of the parameterized iteration holds the stages of all the instances side by side.

theorem DescriptiveComplexity.StepDef.inflLimit_param {L : FirstOrder.Language} [L.IsRelational] {d : StepDef ((newLang L).sum FirstOrder.Language.order)} {N : Type} [L.Structure N] [LinearOrder N] (c : N) : d.B.atParam (d.param.inflLimit N) c = d.inflLimit N

The value of the parameterized iteration, read at a parameter.

theorem DescriptiveComplexity.StepDef.ifpHolds_param {L : FirstOrder.Language} [L.IsRelational] {d : StepDef ((newLang L).sum FirstOrder.Language.order)} {N : Type} [L.Structure N] [LinearOrder N] : d.param.IFPHolds N ↔ ∃ (c : N), d.IFPHolds N

What the parameterized definition defines: the original one, at some element of the instance.

The closure theorems

theorem DescriptiveComplexity.IFPDefinable.exElement {L : FirstOrder.Language} [L.IsRelational] {R : DecisionProblem (newLang L)} {P : DecisionProblem L} (hR : IFPDefinable R) (h : ∀ (N : Type) [inst : L.Structure N] [Finite N] [Nonempty N], P.Holds N ↔ ∃ (c : N), R.Holds N) : IFPDefinable P

FO(≤, IFP) definability is closed under existential quantification over an element: the parameter is carried by every relation variable of the induction.

theorem DescriptiveComplexity.mem_PTIME_exElement {L : FirstOrder.Language} [L.IsRelational] {R : DecisionProblem (newLang L)} {P : DecisionProblem L} (hR : PTIME.Mem R) (h : ∀ (N : Type) [inst : L.Structure N] [Finite N] [Nonempty N], P.Holds N ↔ ∃ (c : N), R.Holds N) : PTIME.Mem P

PTIME is closed under existential quantification over an element.