# Questions tagged [finite-model-theory]

The tag has no usage guidance.

8 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ...
193 views

### Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties

Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)? Motivation As you ...
60 views

### Short $\exists$SO sentences over strings that define an NP-complete problem

[Q1] I'm wondering if there are some "official" SHORT existential second order sentences with ONE binary relation, over strings (over a small alphabet) that define an NP-complete set. (Something ...
55 views

### Inexpressibility of Second order

In finite model theory, Ehrenfeucht-Fraïssé games gives us tools to prove inexpressibility results for FOL. Pebble games do the same for infinitary logic with finitely many variables. Do we have such ...
57 views

### Decidability of the monadic second-order theory of a class of finite structures

Let $L$ be the set of sentences in some logic. I am interested in cases where $L$ is the set of sentences in monadic second-order logic, or it is its $\Pi^1_1$ fragment. Let $K$ be a class of finite ...
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 ...
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 ...