# Questions tagged [finite-model-theory]

The tag has no usage guidance.

31 questions
Filter by
Sorted by
Tagged with
1k views

### Is there a logic without induction that captures much of P?

The Immerman-Vardi theorem states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ...
603 views

### What is the minimal extension of FO that captures the class of regular languages?

Context: relations between logic and automata Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that ...
1k views

### Ambiguity and Logic

In automata theory (finite automata, pushdown automata, ...) and in complexity, there is a notion of "ambiguity". An automaton is ambiguous if there is a word $w$ with at least two distinct accepting ...
290 views

### Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
457 views

### Finding a finite model

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. Could anyone give me a link or a book which give the answer for finite models. If I have a first ...
4k views

115 views

### Applications of FMT in Algebra

Most of the applications of Finite Model Theory I have seen are in graphs, using FMT one can prove that certain properties of finite graphs are not FO definable. I am interested in similar kind of ...
89 views

### Is there a signature of a first-order language that characterize the class of regular languages?

A previous question on this site was about extending the first-order logic with logical constants (quantifiers, fixed-point operators, etc.) to obtain a logical characterization of the class of ...
Suppose $\sigma$ is a vocabulary consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence. Is it decidable whether there is a finite directed graph $G$, with all in- and out-degrees ...