Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics
Logic in Computer Science
2025-12-08 v1
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.
Keywords
Cite
@article{arxiv.2512.05772,
title = {Skolemization and Decidability of the Bernays-Schoenfinkel Class in Goedel Logics},
author = {Mariami Gamsakhurdia and Matthias Baaz and Anela Lolic},
journal= {arXiv preprint arXiv:2512.05772},
year = {2025}
}
Comments
Submitted to IEEE International Symposium on Multiple-Valued Logic ISMVL 2026