Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics
Mariami Gamsakhurdia, Matthias Baaz, Anela Lolic
TL;DR
This work investigates the Bernays–Schoenfinkel ($BS$) class in Gödel logics, demonstrating that semantic Skolemization yields validity checks that reduce to ground propositional reasoning and that 1-satisfiability aligns with classical behavior under the gluing framework. It shows that the $BS$ class is decidable for both validity and 1-satisfiability across all Gödel logics, with particular structure guiding the construction of Skolem terms and ground Herbrand disjunctions. The paper further clarifies how the gluing lemma connects satisfiability across various Gödel logics, highlighting distinctions between finite-valued and infinite-valued logics and outlining extensions to other prenex fragments and alternative satisfiability notions. Together, these results deepen our understanding of decidability in many-valued logics and suggest avenues for further exploration of Gödel fragments and related intermediate logics.
Abstract
In 1928, Bernays and Schoenfinkel proved the decidability of prenex sentences whose matrices contain no function symbols, now known as the Bernays-Schoenfinkel (BS) class. We investigate the decidability of the BS class for all Goedel logics. Our validity argument relies on the fact that Skolemization works for prenex Goedel logics, while 1-satisfiability follows from structural properties of prenex formulas. We show that validity and 1-satisfiability for the BS class are decidable in every Goedel logic, and that these properties persist across all infinite Goedel logics.