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 :
- SO[
] is equal to PSPACE it is also another way to write SO(TC) - SO[
] is equal to EXPTIME it is also another way to write SO(LFP)
More about...