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.

翻译：1928年，Bernays与Schoenfinkel证明了不含函数符号的前束范式语句的可判定性，该语句类现称为Bernays-Schoenfinkel（BS）类。本文研究所有哥德尔逻辑中BS类的可判定性问题。我们的有效性论证基于以下事实：Skolem化方法适用于前束哥德尔逻辑，而1-可满足性则源于前束公式的结构性质。我们证明在任意哥德尔逻辑中，BS类的有效性与1-可满足性均是可判定的，且这些性质在所有无限哥德尔逻辑中均保持成立。