比較 Payor 與 Löb

Lesswrong·

這篇文章比較了羅布定理與 Payor 引理，探討不同的可證明性條件如何影響一個系統對其自身一致性與證明進行推理的能力。

萊布定理 (Löb's Theorem)：

佩奧爾引理 (Payor's Lemma):

  • 如果 ⊢□(□x→x)→x，則 ⊢x。
  • 或者，作為一個公式：□(□(□x→x)→x)→□x。

在接下來的討論中，我將用「現實」代表 x，「信念」代表 □x，「可靠性」代表 □x→x（即，當信念隱含現實時，信念是可靠的），以及「信任」代表 □(□x→x)（對可靠性的信念）。

萊布定理說，如果你擁有信任，你就擁有了信念。

佩奧爾引理說，如果你能證明信任隱含現實，那麼你就擁有了信念。

因此，這兩個結果都給出了信念的條件。事實上，這兩個結果給出的條件都等同於信念，因為在這兩種情況下，推論都可以反向進行：

  • 雙向萊布：⊢□x→x⟺⊢x
  • 雙向佩奧爾：⊢□(□x→x)→x⟺⊢x

此外，這兩個結果都透過信任這個中介，將可靠性與信念聯繫起來。

萊布定理通常被視為一個負面陳述，即你只有在已經擁有信念時才能擁有信任。對此的一種解釋是，萊布定理是信任的「平凡」情況的反面，在平凡情況下，你從簡單的信念中導出信任：□x→□(□x→x)。（回想一下，這是佩奧爾引理證明中關鍵的第 2 步。）萊布定理只是將其反轉；結合兩者，我們知道信任與信念是同義的：□x↔□(□x→x)。「我們能擁有信任的唯一情況就是平凡的情況：信念。」

但這並不完全破滅了對信任進行生產性使用的希望，正如萊布定理的負面解讀可能暗示的那樣。在萊布定理的決策論應用中，我們可以利用萊布定理來幫助確保理想的結果：

對於某些理想的命題 x，我們可以安排事情使得 □x→x（可靠性），且是可證明的（信任）。應用萊布定理，我們得到 □x（信念）。但我們已經安排了 □x→x；所以現在我們從這筆交易中得到了 x。這可以允許基於邏輯的代理人之間進行合作握手。

我們可以透過搜尋以此方式能使之成真的最佳 x，將其轉化為一般的決策程序。更準確地說，我們搜尋每個行動可能的影響，並採取我們能找到最理想影響的那個行動。因此，我們在採取某個行動的假設背景下，搜尋 x 的相對可證明性；如果我們喜歡所看到的結果，我們就透過採取該行動來使該背景成為現實。

誠然，這是一種怪異且令人毛骨悚然的方式來描述一個相當直觀的演算法（搜尋具有良好後果的行動）；其目的是盡我所能澄清與萊布定理的聯繫。

這裡的大問題是，上述內容在不確定性下都無法很好地退化。將萊布定理讀作「信任與信念同義」給了我們一個提示，即它不能應用於機率推理；顯然，我可以認為「我關於 x 的信念極大機率是非常準確的」，而不需要給 x 分配很高的機率。（特別是，如果我給 x 分配了極低的機率。）

這導致了一個實際問題，即基於萊布定理的合作非常脆弱，特別是對於上述提到的一般決策程序。結果對參與者的證明強度非常敏感。直覺上，如果我對 PA 和 PA+1 這兩個系統的完備性都分配了很高的機率，那麼我使用哪一個作為我的基礎推理系統應該沒有太大關係。對於基於萊布定理的握手，這種差異可能會決定合作的成敗。

佩奧爾引理看起來更適合機率推廣，因此類比於前面提到的基於萊布定理的決策程序，制定一個基於佩奧爾引理的決策程序將會很有趣。

萊布定理應用於使 □x 隱含 x（對於理想的 x），而佩奧爾引理則透過將 □(□x→x) 與 x 聯繫起來應用。因此，萊布定理建議的策略是讓（好的）信念隱含現實，而佩奧爾引理建議的策略是讓對（好的事物）的信任隱含現實。

Critch 給出了一個策略範例：「如果你知道如果每個人都相信每個人都在合作，那麼每個人確實都會合作，那麼就選擇合作」。然而，這是一個針對已知遊戲的固定策略（它需要預先定義「合作」）。我們如何將其轉化為一個可以應用於各種決策問題的一般決策程序？

嘗試強行類比：

| 萊布 (Löb) | 佩奧爾 (Payor)
--- | --- | ---
定理陳述 | □(□x→x)→□x | □(□(□x→x)→x)→□x
信念的條件 | □(□x→x) | □(□(□x→x)→x)
對於好的 x，我們希望安排使其（可證明地）為真 | □x→x | □(□x→x)→x
上述的條件 | □x | □(□x→x)
以行動為條件的結果 | □(a→x) | □(a→(□x→x))
要搜尋什麼證明（為任何 a 尋找最佳 x） | a→x | a→(□x→x)

當 □ 被解釋為可證明性時，這兩個決策程序似乎密切相關，因為正如我之前提到的 ⊢□x→x⟺⊢x。這可能是一個好兆頭；基於萊布定理的程序在基於證明的決策論中運作良好。然而，由於這種等價性本身是基於萊布定理的，它在機率情況下會失效。我還不確定如何為機率情況推導出一個實際建議的決策程序。我甚至不確定這是否是強行類比的正確方式。（我不認為它推廣了 Critch 提出的策略……但我不知道在沒有給定其他代理人數據的情況下該如何做到這一點，而這似乎是非自然主義的。）

— Lesswrong

相關文章

  1. 貝氏定理的快速優雅推導

    3 個月前

  2. 數論的非理性深度

    4 個月前

  3. 後人類論證

    3 個月前

  4. 標記化的黑暗藝術，或：我如何學會開始憂慮並擁抱大型語言模型的未解碼輸出

    6 個月前

  5. 運用模糊邏輯從說謊者悖論中挽救數學的真理

    5 個月前

其他收藏 · 0