Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

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
14
votes
0answers
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 ...
5
votes
0answers
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 ...
4
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
2
votes
0answers
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 ...
1
vote
0answers
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 ...
1
vote
0answers
93 views

Decidability one relation, binary FOL over finite models

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