Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics

TL;DR

This paper proves that the Bernays-Schoenfinkel class's validity and 1-satisfiability are decidable across all infinite Goedel logics, extending classical results to a broader logical framework.

Contribution

It demonstrates that Skolemization and decidability results for the Bernays-Schoenfinkel class hold in all infinite Goedel logics, a significant extension of classical logic theory.

Findings

Validity and 1-satisfiability are decidable in all infinite Goedel logics.

Skolemization works for prenex Goedel logics.

Decidability persists across all infinite Goedel 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.