Class Description

SO[LFP]: Second-Order logic with least fixed point

SO[LFP] is to SO what FO[LFP] is to FO. The LFP operator can now also take second-order variable as argument.

In Descriptive complexity we can see that SO[LFP] is equal to EXPTIME.

Linked From

SO[]: Iterated Second-Order logic

SO[] is to SO as FO[] is to FO. But we now also have second-order quantifier in the quantifier block.

In Descriptive complexity we can see that :

More about...