贝恩伯斯-施欟纳克尔类在哥德尔逻辑中的斯科莱姆化与可判定性
计算机科学中的逻辑
2025-12-08 v1
摘要
1928年，贝恩伯斯和施欟纳克尔证明了预面积句（prenex sentences）的可判定性，这些句子的矩阵中不包含函数符号，后被称为贝恩伯斯-施欟纳克尔（BS）类。我们研究了BS类在所有哥德尔逻辑中的可判定性。我们的有效性论证依赖于斯科莱姆化对预面积哥德尔逻辑的适用性，而1-满足性则源于预面积公式的结构性质。我们证明了在每一个哥德尔逻辑中，BS类的有效性和1-满足性都是可判定的，并且这些性质在所有无限哥德尔逻辑中都得以保持。
引用
@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}
}
备注
Submitted to IEEE International Symposium on Multiple-Valued Logic ISMVL 2026