关于高阶逻辑推理形式主义表达能力的问题
我真的不知道这是否得到科学证明，但我在一本书中读到（这是 Peter Norvig 写的一本相对现代的人工智能书籍），二阶逻辑编程可能比现有的一阶语言更具表现力。
问题是：统计/符号证明高阶谓词逻辑的表达能力超过一阶谓词吗？或者他们只是为您的知识库带来了模块化/便利性/可维护性？
另外：如果有某种坚定的方向，我可以去寻求比我更多的表达能力（我的意思正是我在给定语义/语法中编写的符号的描述潜力） - 那么我会很高兴听到几乎一切：）
谢谢。
I do not really know if this is scientifically proven, but I've read in a book (It was a relatively modern AI book by Peter Norvig) that second-order logical programming could be more expressive than existing first-order languages.
The question is: Is it statistically/symbolically proven that higher-order predicate logics exceed first-order predicates in their expressive power? Or they just bring the modularity/convenience/maintainability to your knowledge bases?
Additionally: If there is some kind of firm direction in which I could go seeking more expressive power than I have (I mean exactly the descriptive potential of the symbols I write in given semantics/syntax) - then I would be glad to hear just almost everything :)
Thank you.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
二阶逻辑比一阶逻辑更强大且更具表现力。二阶逻辑允许人们量化除变量之外的关系；因此，可以使用单个二阶逻辑句子来表达需要无限多个一阶逻辑句子的事物。这种关系类似于 FOL 和命题逻辑之间的关系。
作为一个例子，考虑 SOL 语句：
这表明对于任何关系 R，都存在 x 和 y，使得 x R y 成立。为了在 FOL 中表达这一点，需要为该语言中的每个关系 R 提供一个声明，该关系显然可能是无限的。
举一个更有趣的例子，我们可以看看关系的传递闭包在 FOL 中不可表达的证明。如果你想看我可以发布它；但为了简洁起见，除非有人想要，否则我将省略它。
编辑：您可能还对描述复杂性感兴趣——本质上，它将复杂性和可表达性的概念联系在一起——如果您可以在某个逻辑片段中完整地陈述问题，那么您就知道它包含在相应的复杂性类中。例如，如果一个问题可以用存在二阶逻辑来描述，那么它就是NP；如果它可以用一阶逻辑 + 最小不动点运算符来表示，那么它就在 P 中。如果您可以证明存在二阶逻辑的每个语句都可以转换为 FOL(LFP)，那么您就证明了 P=NP 。 （好吧，你已经证明了 NP\子集 P，但由于另一个包含已经已知，所以你已经证明了相等性......）
Second order logic is more powerful and expressive than first order logic. Second order logic allows one to quantify over relations in addition to variables; thus it is possible, using a single sentence of second order logic, to express something that would require an infinite number of first order logic sentences. The relationship is similar to that between FOL and propositional logic.
As an example, consider the SOL statement:
This states that for any relation R there are x and y such that x R y holds. In order to express this in FOL, one would need a statement for each relation R in the language, which clearly could be infinite.
For a more interesting example, one could look at the proof that the transitive closure of a relation is not expressible in FOL. I can post it if you want to see it; but for the sake of succinctness I will omit it unless someone wants it.
Edit: You may also be interested in Descriptive Complexity -- essentially, it ties together the notions of complexity and expressibility -- if you can fully state a problem in a certain fragment of logic, then you know it is contained within the corresponding complexity class. For example, if a problem can be stated in Existential Second Order Logic, then it's in NP; if it can be stated in First Order Logic + a Least Fixed Point operator, then it's in P. If you can show that every statement of existential second order logic can be translated to FOL(LFP), then you've proven P=NP. (well, you've proven NP\subset P, but since the other containment is already known, you've proven equality...)
您可能需要研究依赖类型理论。
You may want to look into dependent type theories.