Second-order fixed points: SO(LFP) and SO(PFP) #

A second-order fixed point is a first-order fixed point read over a structure whose universe is the assignments of a second-order block.

A relation over an exponential expansion of A is a set of tuples of second-order objects of A, so iterating a definable operator on it is a second-order induction; and the first-order fixpoint logics, read there, are the second-order ones. That is the definition of DescriptiveComplexity.SOLFPDefinable and DescriptiveComplexity.SOPFPDefinable, and the two classes DescriptiveComplexity.EXPTIME and DescriptiveComplexity.EXPSPACE are named after them.

No third-order syntax is introduced, and none is needed. The fixpoint variable of SO(LFP) is a relation over the expanded universe, hence a third-order object over A; but the expansion has already made those objects the first-order elements of a new sort, so the syntax is the ordinary FirstOrder.Language.BoundedFormula layer and the fixpoint is the ordinary DescriptiveComplexity.LFPDefinable. This is the standard type-lowering translation of higher-order logic into many-sorted first-order logic over the power type (Henkin 1950), which is why “SO(LFP) over A” and “FO(LFP) over the expansion of A” are two presentations of one object.

The bridge theorems #

DescriptiveComplexity.solfpDefinable_iff_expDefinable and DescriptiveComplexity.sopfpDefinable_iff_expDefinable say that the two logics are DescriptiveComplexity.ExpDefinable at PTIME and at PSPACE. Each is a congruence down to the library's own capture theorem (DescriptiveComplexity.lfpDefinable_iff_mem_PTIME, DescriptiveComplexity.pfpDefinable_iff_mem_PSPACE) applied at the expanded vocabulary, which is relational by the eRelational field of an expansion. There is no mathematics in them, and that is the point of the design: they let every later statement be proved once, about DescriptiveComplexity.ComplexityClass.exp at an arbitrary class, and read off at the exponential classes.

Literature #

These are definitions here, so nothing is claimed. Naming the classes after these logics follows Abiteboul–Vardi–Vianu 1997, which parameterizes fixpoint logic by operator and iteration construct and obtains characterizations up to EXPTIME. That work is stated in the relational (order-free, generic) setting, so it must not be cited as a capture theorem for the classes defined here; what this development proves in its place are the bridge theorems above, which are about this library's own classes and owe the literature nothing. The order these two definitions carry is nevertheless removable (DescriptiveComplexity.solfpDefinable_iff_free, DescriptiveComplexity.sopfpDefinable_iff_free): the expansion can guess it, and the resulting union of copies costs one existential – paid for by guessing the copy in DescriptiveComplexity.Exponential.FreeSpace, and by naming it with a point in DescriptiveComplexity.Exponential.FreeTime.

The two logics #

source

def DescriptiveComplexity.SOLFPDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) :

Prop

SO(≤, LFP): a least fixed point over a second-order universe. The problem holds of A exactly when an FO(≤, LFP) definition holds of an exponential expansion of A. The order the expansion's own sentences read can be removed (DescriptiveComplexity.solfpDefinable_iff_free), by guessing it into the block.

Equations

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

Instances For

Dependency graph

source

def DescriptiveComplexity.SOPFPDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) :

Prop

SO(≤, PFP): a partial fixed point over a second-order universe. The order the expansion's own sentences read can be removed (DescriptiveComplexity.sopfpDefinable_iff_free), by guessing it into the block.

Equations

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

Instances For

Dependency graph

The bridge theorems #

source

theorem DescriptiveComplexity.solfpDefinable_iff_expDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) :

SOLFPDefinable P ↔ ExpDefinable PTIME P

SO(≤, LFP) is polynomial time over an expanded universe: the Immerman–Vardi capture theorem, read at the expanded vocabulary.

Dependency graph

source

theorem DescriptiveComplexity.sopfpDefinable_iff_expDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) :

SOPFPDefinable P ↔ ExpDefinable PSPACE P

SO(≤, PFP) is polynomial space over an expanded universe: the Abiteboul–Vianu capture theorem, read at the expanded vocabulary.

Dependency graph

Closure under reductions, inherited #

The three membership obligations of DescriptiveComplexity.ComplexityClass.ofMem are borrowed through the bridge theorems rather than proved: DescriptiveComplexity.Exponential.Class proved them once, for ExpDefinable C at an arbitrary C.

source