An Extension of Trakhtenbrot's Theorem

TL;DR

This paper extends Trakhtenbrot's theorem by proving that the finite satisfiability problem for any fragment of first-order logic with certain properties is RE-complete, highlighting the computational complexity of these logical fragments.

Contribution

It introduces a generalization showing RE-completeness of finite satisfiability for broad classes of first-order logic fragments with specific conditions.

Findings

Finite satisfiability problem is RE-complete for these fragments.

The result applies to any fragment with effective syntax, finite model expressiveness, and closure under conjunction.

Extends classical undecidability results to a wider range of logical fragments.

Abstract

The celebrated Trakhtenbrot's theorem states that the set of finitely valid sentences of first-order logic is not computably enumerable. In this note we will extend this theorem by proving that the finite satisfiability problem of any fragment of first-order logic is RE-complete, as long as it has an effective syntax, it is equi-expressive with first-order logic over finite models and it is effectively closed under conjunction.