变量分离性——关于可判定一阶片段的新视角
计算机科学中的逻辑
2019-11-27 v1
摘要
古典判定问题，按当今理解，是基于优雅的句法准则对一阶逻辑中可判定与不可判定部分进行界定的探索。本文中，我们处理变量分离性的概念并探讨其对古典判定问题的适用性。若两个不相交的一阶变量集在给定公式中从不共同出现在任何原子内，则它们在公式中分离。这一简单概念有助于显著扩展许多著名的可判定一阶片段，且以保持可判定的方式进行。我们将针对若干前缀片段、若干守护片段、两变量片段以及 flute 片段予以演示。总体而言，我们将更仔细地考察其中九种扩展。有趣的是，每一种都包含无等号的关系一元一阶片段。尽管这些扩展展现出与各自原片段相同的表达能力，某些逻辑性质却可以更为简洁地表达。在三种情形下，简洁性差距无法用任何初等函数界定。
引用
@article{arxiv.1911.11500,
title = {Separateness of Variables -- A Novel Perspective on Decidable First-Order Fragments},
author = {Marco Voigt},
journal= {arXiv preprint arXiv:1911.11500},
year = {2019}
}
备注
44 pages, 1 figure