2022 Developer Survey is open! Take survey.
11 votes
Accepted

Standard reference for basic model theory definitions

Here is one possibility, but other people might use different words. I will use first-order logic as a running example. Language The language is a collection of expressions, which are syntactic ...
user avatar
  • 26.4k
8 votes
Accepted

Is graph connectivity definable in existential MSO with vertices and edges?

You can express that $s$ is connected to $t\ne s$ in $G=(V,E)$ by the $\exists\mathrm{MSO}_2$ formula “there exists $E'\subseteq E$ such that in the graph $(V,E')$, $s$ and $t$ have degree $1$, and ...
user avatar
7 votes

Is Eulerian Path (or Eulerian Cycle) definable in Monadic Second Order Logic?

Parity cannot be expressed in MSOL (see for instance http://www.cs.technion.ac.il/~janos/COURSES/236331-15/Lec-1.pdf), but connectedness Yes. Using instead $C_2$MSOL, one can express the existence of ...
user avatar
  • 1,026
6 votes
Accepted

Expressiveness of Infinitary Logic

There is a famous example of Cai, Fürer and Immerman, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express ...
user avatar
5 votes
Accepted

Turing machines over a structure

You could start with the survey article by Peter Hinman, Recursion on Abstract Structures, Chapter 11 of the Handbook on Computability Theory (editor E. R. Griffor). If you follow the references there ...
user avatar
  • 26.4k
5 votes

Descriptive model theory classification of Counting hierarchy

This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment. $PSPACE$ has the following (equivalent) descriptive characterizations: $FO[2^{n^{O(1)}}]...
user avatar
4 votes

What is First-Order Rewritable (and FO-Query)?

Here is another attempt at a more comprehensive answer. Your question already contains the formal definition of FO-rewritability, which at its core says that you can reduce a query answering problem: ...
user avatar
  • 454
4 votes
Accepted

What is the impact of encodings of sparse structures on the complexity of the model checking problem?

I don't know of any natural logic, but the following is in any case a logic for which the combined complexity of the model-checking problem is different for matrix and list encodings. First, we know ...
user avatar
2 votes

Is there any second-order logic finite satisfiability checker?

There are Nitpick and Nunchaku that are model finders for higher-order logic. Nunchaku is more recent and can build models for axioms containing higher-order quantification. But, as the problem is ...
user avatar
  • 333
2 votes
Accepted

FO(TC) lower bounding games?

As mentioned above: question answered by reference to FO(TC) games presented in Finite Model Theory by Ebbinghaus and Flum.
user avatar
2 votes

Understanding least-fixed point logic

this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require. ...
user avatar
  • 21
1 vote

What is First-Order Rewritable (and FO-Query)?

As a complement to Janoma's answer above: it's 'very good'--- from the point of view of implementation --- because given a FO-rewritable language, we can use the powerful engines (for evaluating ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible