Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

TL;DR

This paper introduces a framework using symbolic structures to establish decidability in certain fragments of first-order logic, expanding the scope of decidable logical fragments.

Contribution

It generalizes symbolic structures to any base theory with a standard model and proves decidability for new logical fragments with relaxed quantifier constraints.

Findings

Symbolic model property holds for several extended fragments.

Decidability is achieved via model-checking of symbolic structures.

A generic construction method for symbolic models is developed.

Abstract

Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model. Symbolic structures induce a symbolic model property, which holds for a fragment of first-order logic if every satisfiable formula in the fragment has a symbolic model. The symbolic model property implies decidability, since the model-checking problem for symbolic structures is decidable. We use the symbolic model property to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.