一個問題關於高階邏輯推理的表現力形式主義

Question

我真的不知道這是科學證明，但我在一本書中（這是一個比較現代的AI書彼得·諾維格）是二線閱讀順序邏輯編程可能比現有的一階語言更具表現力。

的問題是：是否有統計學/象徵性地證明，較高階謂詞邏輯超過他們的表現力的一階謂詞？或者他們只是將模塊化/便利性/可維護性帶入知識庫？如果有某種堅定的方向，我可以去尋求比我具有更強大的表達能力（我的意思就是我在給定的語義/語法中寫的符號的描述性潛力） - 那麼我會很高興聽到幾乎所有的東西:)

謝謝。

Answer 1

二階邏輯比一階邏輯更強大和更有表現力。二階邏輯允許除了變量之外還對關係進行量化;因此有可能使用二階邏輯的單個句子來表達需要無限數量的一階邏輯句子的事物。這種關係類似於FOL和命題邏輯之間的關係。

作爲一個例子，考慮SOL語句：

\forall R \exists x \exists y (x R y) 

此指出，對於任何關係R有x和y，使得個R y成立。爲了在FOL中表達這一點，人們需要對語言中的每個關係R進行陳述，這顯然可以是無限的。

對於一個更有意思的例子，我們可以看一下證明關係的傳遞閉包是不是在FOL表達。如果你想看到它，我可以發佈它;但爲了簡潔起見，除非有人願意，否則我會省略它。

編輯：您可能也有興趣Descriptive Complexity - 本質上，它將複雜性和可表達性的概念聯繫在一起 - 如果您可以完全陳述某個邏輯片段中的問題，那麼您知道它包含在相應的複雜等級。例如，如果一個問題可以在存在二階邏輯中陳述，那麼它在NP中;如果它可以在一階邏輯+最小定點運算符中說明，那麼它在P中。如果你能證明存在性二階邏輯的每個語句都可以轉換爲FOL（LFP），那麼你已經證明了P = NP 。 （好吧，你已經證明了NP \ subset P，但是因爲另一個遏制已經是已知的，所以你已經證明是平等的......）

Answer 2

你可能想看看dependent type theories。