2022 Developer Survey is open! Take survey.

Tag Info

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 ...
• 26.4k
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 ...
• 14.7k

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 ...
• 1,026
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 ...
• 1,106
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 ...
• 26.4k

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)}}]...
• 136

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: ...
• 454
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 ...

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 ...
• 333
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.