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 ...
- 26.6k
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 ...
- 14.8k
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 ...
- 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 ...
- 1,096
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 ...
- 26.6k
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)}}]...
- 136
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:
...
- 464
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 ...
- 776
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 ...
- 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.
- 41
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.
...
- 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 ...
- 11
Only top scored, non community-wiki answers of a minimum length are eligible