Skip to main content
Share Your Experience: Take the 2024 Developer 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 ...
Andrej Bauer's user avatar
  • 29.1k
9 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 ...
Emil Jeřábek's 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 ...
M. kanté's user avatar
  • 1,046
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 ...
Andrej Bauer's user avatar
  • 29.1k
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)}}]...
Sam McGuire's 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: ...
mak's user avatar
  • 504
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 ...
Reijo Jaakkola's user avatar
3 votes

Why is order/choice an issue for a logic for PTIME

But what would be the issue if we extended IFP to just have an order and made it that a structure satisfies a formula if it satisfies for an arbitrary order? If done this way, it is difficult to see ...
Reijo Jaakkola's 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. ...
Ramit's user avatar
  • 21
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 ...
selig's 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.
Will Asness's user avatar
2 votes

Why is order/choice an issue for a logic for PTIME

My interpretation of your question is something along the lines of, "why should we care whether there is a logic that captures PTIME?" This is a fair question: there are good reasons for ...
Siddharth's user avatar
  • 851
1 vote

Why is order/choice an issue for a logic for PTIME

If you treat an integer in terms of, say, it's binary expansion, and the FO structure you use for that is a single unary relation on a set of size n (indicating which bits of your length-n string are ...
Joshua Grochow's user avatar
1 vote

Proper terminology for input, parameter or variable fixing. Refinement? Projection? Fixation? Partial valuation?

"Fixing" inputs or parameters to specific values can be a valid approach, but it may not be the most appropriate term to use depending on the context. "Refining" a specification ...
Likar's user avatar
  • 11
1 vote

Finding a finite model

In addition to the answers which were already given: a very good reference about the (un)decidability of fragments of first-order logic is the book The classical decision problem by Börger, Grädel, ...
f-h's user avatar
  • 588
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 ...
Julio Lemos's user avatar

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