Talk:Descriptive complexity theory: Difference between revisions

Revision as of 21:40, 15 February 2022

Revision as of 21:46, 15 February 2022

Line 28:

Analogously to first-order least-fixed point logic, second-order logic can be augmented by a least-fixed point operator that takes second-order variables as arguments. SO(LFP) is to SO what [[FO (complexity)#Least Fixed Point is P|FO(LFP)]] is to [[FO (complexity)|FO]]. The LFP operator can now also take second-order variable as argument. SO(LFP) is equal to [[EXPTIME]].

Indeed, SO(LFP) is depicted as EXPTIME on the illustration on the cover of Immerman (1999). However, I couldn't find any discussion of it inside the book, and Ebbinghaus and Flum (Finite model theory, 2nd Ed. 1999, Theorem 8.5.1) sayssay that SO(PFP), which should certainly be at least as expressive as SO(LFP), reduces to FO(PFP) (which equals PSPACE) on ordered structures. Any insight would be much appreciated! [[User:Felix QW|Felix QW]] ([[User talk:Felix QW|talk]]) 21:40, 15 February 2022 (UTC)