一阶逻辑方面定义了可决定性？

Question

我已经阅读了一阶逻辑，通常是不可决定的，只有在与单一操作员合作时，这才能决定。 （我认为这是命题逻辑，如果我错了，请纠正我）

问题是 为什么Arity会导致不确定的问题？

我想看看一些参考材料，或者至少一些简单 例子 其中，作为一种从单一到n-ary的段落中思考的一种方式，以及为什么会导致不确定的问题。

Answer 1

逻辑与一般 谓词 （不是操作员），称为 monadic. 。所谓的东西 命题 逻辑只有 无效 谓词，即常数 true 和 false, ，也没有量化器。

这 谓词逻辑的不可证明性 以下是因为谓词逻辑（至少有一个二进制谓词）足够强大 描述图灵机的工作原理, ，因此我们可以在逻辑中表达有关图灵机的充分复杂的陈述，以获得不可证明的性能。相比之下，在我们只有一单位谓词的Monadic Logic中，我们无法描述Turing Machine的工作。我在这里故意含糊地说一个想法，而不会陷入技术上。

Answer 2

正如拉斐尔（Raphael）在评论中指出的那样，您可能正在询问与一阶逻辑片段的经典决策问题的可决定性，并询问一阶逻辑的片段。

搜索公式有效性的一阶逻辑的句法限制片段是一个超过100年的积极研究领域。很早就知道，变量之间的依赖性使决策问题变得困难。当两个变量发生在谓词的参数中时，最好表达依赖项。因此，二进制谓词或功能符号（如果允许函数符号）对于不可证明性至关重要。

是洛文海姆（Löwenheim），他于1915年为一阶逻辑提供了一阶谓词的决策程序。如果您有兴趣，您可能会发现吸引着名为“关于古典决策问题“由尤里·古里维奇（Yuri Gurevich）以两个虚构字符的对话形式撰写。该论文首次发表在《伊特克（Eatcs）公报》上。

本文不仅引入了问题，还解释了如何从量词前缀中找到可决定和不可决定的片段的完整分类。