Talk:Descriptive complexity theory

Modal logic

Does anyone know how different modal logics can be used to describe complexity classes? Traversal of Kripke structures etc. I know the complexities of showing satisfiability in different modal logics; how does that relate to classes of languages expressible in those logics? --Spug (talk) 14:05, 8 March 2010 (UTC)

Merge

The following discussion is closed. Please do not modify it. Subsequent comments should be made in a new section. A summary of the conclusions reached follows.

Merge since there was nothing but support for more than a week.

---

The current coverage of descriptive complexity is quite unsatisfactory. We have what should be the parent article, Descriptive complexity theory, but which really is a stubby list of characterisations of complexity classes. Then we have three pages giving more detailed description of these characterisations, FO (complexity), SO (complexity) and HO (complexity). The main context is provided at FO (complexity) rather than here, and SO (complexity) and HO (complexity) make little sense without that context. Most problematically, however, none of the descriptions adequately distinguish between the classes of structures on which a given characterisation holds. For instance, Fagin's theorem (ESO = NP) holds on all classes of finite structures, while the Immermann-Vardi Theorem (FO(LFP) = P) holds only for ordered structures, and Grädel's theorem (Second-order Horn logic = P) only holds in the presence of a successor relation.

In my opinion, a much better organisation would be to order the characterisations by the complexity classes they are representing, and by the classes of structures on which they are representing them. The first step would be to merge the existing articles into Descriptive complexity theory, and then we could take it from there. Felix QW (talk) 19:01, 6 February 2022 (UTC)

Agreed on all accounts. Caleb Stanford (talk) 01:53, 7 February 2022 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

SO(LFP)

The page on SO (complexity) contained the following section:

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(LFP) is to 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) say 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! Felix QW (talk) 21:40, 15 February 2022 (UTC)

You might consider emailing Immerman directly -- I emailed him a couple years ago about FO(REGULAR) and he was kind enough to explain the definition directly to me :) By the way, good work on the article so far, it's looking much improved. Lead probably needs a rewrite to be more accessible, I will try to take a pass sometime if I get some free time for it. Caleb Stanford (talk) 22:19, 15 February 2022 (UTC)

Thank you very much for your suggestion, and your kind words! Any improvements to the lead (or elsewhere) would be highly appreciated – I just tried to rearrange, smooth out and verify what was there already, and I am sure one can do better at several places.

In fact, I will hopefully be attending an algorithmic and finite model theory workshop in March, so I could also use this puzzle for some breaktime discussion :). Felix QW (talk) 22:53, 15 February 2022 (UTC)