An Extension of Trakhtenbrot's Theorem

2021/12/30 by Jaakkola, Reijo
#F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2112.14996

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.

Related

• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
• Trakhtenbrot theorem and first-order axiomatic extensions of MTL
• Fragments of first-order logic over infinite words
• Zero-one laws for provability logic: Axiomatizing validity in almost all\n models and almost all frames
• Enumeration Reducibility in Closure Spaces with Applications to Logic and Algebra