透過克里普克框架輕鬆實現 Payorian 合作

Lesswrong·28 天前

我試圖解釋為什麼我認為使用克里普克框架與 Payor 引理來證明自我合作的方法更有前景，這種方法能將邏輯決策理論的推理過程轉化為直觀且易於理解的博弈樹結構。

這篇文章的背景是 MIRI 對艾克羅德（Axelrod）囚徒困境競賽的變體。
艾克羅德的參賽者是程式，在重複的囚徒困境中互相對抗。
MIRI 的競賽則是單次博弈的囚徒困境，但程式可以讀取對手的程式碼。
更準確地說，是讀取該程式碼在哥德爾-勒布（Gödel-Löb）可證明性邏輯中的行為描述，而這足以決定它們在該設定下的行為。

論文開頭一個有趣的結果是關於一個名為 FairBot（公平機器人）的程式，其行為定義為：「如果你（可證明地）與我合作，我就與你合作」。
儘管看起來存在循環定義，FairBot 會與自身合作。
其證明涉及勒布定理（Löb's theorem），因此我們稱之為「勒布式合作」（Löbian cooperation）。

Andrew Critch 提出了另一種證明自我合作的方法。
他不使用勒布定理，而是使用他所謂的「付款人引理」（Payor's lemma）。
這暗示了定義 FairBot 的另一種方式，更像是：「如果當我假設性地與你合作時，你會與我合作，那麼我就真的會合作。」

這篇文章是我試圖解釋為什麼我認為這種方法更有前景，或者至少為什麼我更喜歡它。

當使用模態邏輯思考這類反射問題（reflection problems）時，我會使用克里普克框架（Kripke frames），即由可能世界組成的有向圖。
我的幻想是，當我們搞清楚這種邏輯決策論時，其推理過程將涉及樹狀的克里普克框架，且能直觀地解釋為類似博弈樹的東西。
例如：「如果我這樣做，他就會那樣做，因為他知道我會做另一件事。但如果我那樣做……」

對於勒布式合作，我用這種方法毫無進展。
但 Critch 的文章是我幻想即將實現的第一道曙光。
然而，要向你傳達我從中看到了什麼，唯一的方法就是帶領你透過克里普克框架完成一次自我合作的證明。

勒布式 FairBot

首先，在不使用克里普克框架的情況下，回顧一下勒布式 FairBot 和勒布式合作。

我們考慮一個以另一個程式作為輸入的程式，並輸出 True（合作）或 False（背叛）。
因此，

mjx-container[jax="CHTML"] {
line-height: 0;
}

mjx-container [space="1"] {
margin-left: .111em;
}

mjx-container [space="2"] {
margin-left: .167em;
}

mjx-container [space="3"] {
margin-left: .222em;
}

mjx-container [space="4"] {
margin-left: .278em;
}

mjx-container [space="5"] {
margin-left: .333em;
}

mjx-container [rspace="1"] {
margin-right: .111em;
}

mjx-container [rspace="2"] {
margin-right: .167em;
}

mjx-container [rspace="3"] {
margin-right: .222em;
}

mjx-container [rspace="4"] {
margin-right: .278em;
}

mjx-container [rspace="5"] {
margin-right: .333em;
}

mjx-container [size="s"] {
font-size: 70.7%;
}

mjx-container [size="ss"] {
font-size: 50%;
}

mjx-container [size="Tn"] {
font-size: 60%;
}

mjx-container [size="sm"] {
font-size: 85%;
}

mjx-container [size="lg"] {
font-size: 120%;
}

mjx-container [size="Lg"] {
font-size: 144%;
}

mjx-container [size="LG"] {
font-size: 173%;
}

mjx-container [size="hg"] {
font-size: 207%;
}

mjx-container [size="HG"] {
font-size: 249%;
}

mjx-container [width="full"] {
width: 100%;
}

mjx-box {
display: inline-block;
}

mjx-block {
display: block;
}

mjx-itable {
display: inline-table;
}

mjx-row {
display: table-row;
}

mjx-row > * {
display: table-cell;
}

mjx-mtext {
display: inline-block;
text-align: left;
}

mjx-mstyle {
display: inline-block;
}

mjx-merror {
display: inline-block;
color: red;
background-color: yellow;
}

mjx-mphantom {
visibility: hidden;
}

_::-webkit-full-page-media, _:future, :root mjx-container {
will-change: opacity;
}

mjx-math {
display: inline-block;
text-align: left;
line-height: 0;
text-indent: 0;
font-style: normal;
font-weight: normal;
font-size: 100%;
font-size-adjust: none;
letter-spacing: normal;
border-collapse: collapse;
word-wrap: normal;
word-spacing: normal;
white-space: nowrap;
direction: ltr;
padding: 1px 0;
}

mjx-container[jax="CHTML"][display="true"] {
display: block;
text-align: center;
margin: 1em 0;
}

mjx-container[jax="CHTML"][display="true"][width="full"] {
display: flex;
}

mjx-container[jax="CHTML"][display="true"] mjx-math {
padding: 0;
}

mjx-container[jax="CHTML"][justify="left"] {
text-align: left;
}

mjx-container[jax="CHTML"][justify="right"] {
text-align: right;
}

mjx-mi {
display: inline-block;
text-align: left;
}

mjx-c {
display: inline-block;
}

mjx-utext {
display: inline-block;
padding: .75em 0 .2em 0;
}

mjx-mo {
display: inline-block;
text-align: left;
}

mjx-stretchy-h {
display: inline-table;
width: 100%;
}

mjx-stretchy-h > * {
display: table-cell;
width: 0;
}

mjx-stretchy-h > * > mjx-c {
display: inline-block;
transform: scalex(1.0000001);
}

mjx-stretchy-h > * > mjx-c::before {
display: inline-block;
width: initial;
}

mjx-stretchy-h > mjx-ext {
/* IE / overflow: hidden;
/ others */ overflow: clip visible;
width: 100%;
}

mjx-stretchy-h > mjx-ext > mjx-c::before {
transform: scalex(500);
}

mjx-stretchy-h > mjx-ext > mjx-c {
width: 0;
}

mjx-stretchy-h > mjx-beg > mjx-c {
margin-right: -.1em;
}

mjx-stretchy-h > mjx-end > mjx-c {
margin-left: -.1em;
}

mjx-stretchy-v {
display: inline-block;
}

mjx-stretchy-v > * {
display: block;
}

mjx-stretchy-v > mjx-beg {
height: 0;
}

mjx-stretchy-v > mjx-end > mjx-c {
display: block;
}

mjx-stretchy-v > * > mjx-c {
transform: scaley(1.0000001);
transform-origin: left center;
overflow: hidden;
}

mjx-stretchy-v > mjx-ext {
display: block;
height: 100%;
box-sizing: border-box;
border: 0px solid transparent;
/* IE / overflow: hidden;
/ others */ overflow: visible clip;
}

mjx-stretchy-v > mjx-ext > mjx-c::before {
width: initial;
box-sizing: border-box;
}

mjx-stretchy-v > mjx-ext > mjx-c {
transform: scaleY(500) translateY(.075em);
overflow: visible;
}

mjx-mark {
display: inline-block;
height: 0px;
}

mjx-msub {
display: inline-block;
text-align: left;
}

mjx-mn {
display: inline-block;
text-align: left;
}

mjx-mtable {
display: inline-block;
text-align: center;
vertical-align: .25em;
position: relative;
box-sizing: border-box;
border-spacing: 0;
border-collapse: collapse;
}

mjx-mstyle[size="s"] mjx-mtable {
vertical-align: .354em;
}

mjx-labels {
position: absolute;
left: 0;
top: 0;
}

mjx-table {
display: inline-block;
vertical-align: -.5ex;
box-sizing: border-box;
}

mjx-table > mjx-itable {
vertical-align: middle;
text-align: left;
box-sizing: border-box;
}

mjx-labels > mjx-itable {
position: absolute;
top: 0;
}

mjx-mtable[justify="left"] {
text-align: left;
}

mjx-mtable[justify="right"] {
text-align: right;
}

mjx-mtable[justify="left"][side="left"] {
padding-right: 0 ! important;
}

mjx-mtable[justify="left"][side="right"] {
padding-left: 0 ! important;
}

mjx-mtable[justify="right"][side="left"] {
padding-right: 0 ! important;
}

mjx-mtable[justify="right"][side="right"] {
padding-left: 0 ! important;
}

mjx-mtable[align] {
vertical-align: baseline;
}

mjx-mtable[align="top"] > mjx-table {
vertical-align: top;
}

mjx-mtable[align="bottom"] > mjx-table {
vertical-align: bottom;
}

mjx-mtable[side="right"] mjx-labels {
min-width: 100%;
}

mjx-mtr {
display: table-row;
text-align: left;
}

mjx-mtr[rowalign="top"] > mjx-mtd {
vertical-align: top;
}

mjx-mtr[rowalign="center"] > mjx-mtd {
vertical-align: middle;
}

mjx-mtr[rowalign="bottom"] > mjx-mtd {
vertical-align: bottom;
}

mjx-mtr[rowalign="baseline"] > mjx-mtd {
vertical-align: baseline;
}

mjx-mtr[rowalign="axis"] > mjx-mtd {
vertical-align: .25em;
}

mjx-mtd {
display: table-cell;
text-align: center;
padding: .215em .4em;
}

mjx-mtd:first-child {
padding-left: 0;
}

mjx-mtd:last-child {
padding-right: 0;
}

mjx-mtable > * > mjx-itable > *:first-child > mjx-mtd {
padding-top: 0;
}

mjx-mtable > * > mjx-itable > *:last-child > mjx-mtd {
padding-bottom: 0;
}

mjx-tstrut {
display: inline-block;
height: 1em;
vertical-align: -.25em;
}

mjx-labels[align="left"] > mjx-mtr > mjx-mtd {
text-align: left;
}

mjx-labels[align="right"] > mjx-mtr > mjx-mtd {
text-align: right;
}

mjx-mtd[extra] {
padding: 0;
}

mjx-mtd[rowalign="top"] {
vertical-align: top;
}

mjx-mtd[rowalign="center"] {
vertical-align: middle;
}

mjx-mtd[rowalign="bottom"] {
vertical-align: bottom;
}

mjx-mtd[rowalign="baseline"] {
vertical-align: baseline;
}

mjx-mtd[rowalign="axis"] {
vertical-align: .25em;
}

mjx-msubsup {
display: inline-block;
text-align: left;
}

mjx-script {
display: inline-block;
padding-right: .05em;
padding-left: .033em;
}

mjx-script > mjx-spacer {
display: block;
}

mjx-c::before {
display: block;
width: 0;
}

.MJX-TEX {
font-family: MJXZERO, MJXTEX;
}

.TEX-B {
font-family: MJXZERO, MJXTEX-B;
}

.TEX-I {
font-family: MJXZERO, MJXTEX-I;
}

.TEX-MI {
font-family: MJXZERO, MJXTEX-MI;
}

.TEX-BI {
font-family: MJXZERO, MJXTEX-BI;
}

.TEX-S1 {
font-family: MJXZERO, MJXTEX-S1;
}

.TEX-S2 {
font-family: MJXZERO, MJXTEX-S2;
}

.TEX-S3 {
font-family: MJXZERO, MJXTEX-S3;
}

.TEX-S4 {
font-family: MJXZERO, MJXTEX-S4;
}

.TEX-A {
font-family: MJXZERO, MJXTEX-A;
}

.TEX-C {
font-family: MJXZERO, MJXTEX-C;
}

.TEX-CB {
font-family: MJXZERO, MJXTEX-CB;
}

.TEX-FR {
font-family: MJXZERO, MJXTEX-FR;
}

.TEX-FRB {
font-family: MJXZERO, MJXTEX-FRB;
}

.TEX-SS {
font-family: MJXZERO, MJXTEX-SS;
}

.TEX-SSB {
font-family: MJXZERO, MJXTEX-SSB;
}

.TEX-SSI {
font-family: MJXZERO, MJXTEX-SSI;
}

.TEX-SC {
font-family: MJXZERO, MJXTEX-SC;
}

.TEX-T {
font-family: MJXZERO, MJXTEX-T;
}

.TEX-V {
font-family: MJXZERO, MJXTEX-V;
}

.TEX-VB {
font-family: MJXZERO, MJXTEX-VB;
}

mjx-stretchy-v mjx-c, mjx-stretchy-h mjx-c {
font-family: MJXZERO, MJXTEX-S1, MJXTEX-S4, MJXTEX, MJXTEX-A ! important;
}

@font-face /* 0 */ {
font-family: MJXZERO;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Zero.woff") format("woff");
}

@font-face /* 1 */ {
font-family: MJXTEX;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Main-Regular.woff") format("woff");
}

@font-face /* 2 */ {
font-family: MJXTEX-B;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Main-Bold.woff") format("woff");
}

@font-face /* 3 */ {
font-family: MJXTEX-I;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Math-Italic.woff") format("woff");
}

@font-face /* 4 */ {
font-family: MJXTEX-MI;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Main-Italic.woff") format("woff");
}

@font-face /* 5 */ {
font-family: MJXTEX-BI;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Math-BoldItalic.woff") format("woff");
}

@font-face /* 6 */ {
font-family: MJXTEX-S1;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Size1-Regular.woff") format("woff");
}

@font-face /* 7 */ {
font-family: MJXTEX-S2;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Size2-Regular.woff") format("woff");
}

@font-face /* 8 */ {
font-family: MJXTEX-S3;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Size3-Regular.woff") format("woff");
}

@font-face /* 9 */ {
font-family: MJXTEX-S4;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Size4-Regular.woff") format("woff");
}

@font-face /* 10 */ {
font-family: MJXTEX-A;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_AMS-Regular.woff") format("woff");
}

@font-face /* 11 */ {
font-family: MJXTEX-C;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Calligraphic-Regular.woff") format("woff");
}

@font-face /* 12 */ {
font-family: MJXTEX-CB;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Calligraphic-Bold.woff") format("woff");
}

@font-face /* 13 */ {
font-family: MJXTEX-FR;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Fraktur-Regular.woff") format("woff");
}

@font-face /* 14 */ {
font-family: MJXTEX-FRB;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Fraktur-Bold.woff") format("woff");
}

@font-face /* 15 */ {
font-family: MJXTEX-SS;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_SansSerif-Regular.woff") format("woff");
}

@font-face /* 16 */ {
font-family: MJXTEX-SSB;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_SansSerif-Bold.woff") format("woff");
}

@font-face /* 17 */ {
font-family: MJXTEX-SSI;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_SansSerif-Italic.woff") format("woff");
}

@font-face /* 18 */ {
font-family: MJXTEX-SC;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Script-Regular.woff") format("woff");
}

@font-face /* 19 */ {
font-family: MJXTEX-T;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Typewriter-Regular.woff") format("woff");
}

@font-face /* 20 */ {
font-family: MJXTEX-V;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Vector-Regular.woff") format("woff");
}

@font-face /* 21 */ {
font-family: MJXTEX-VB;
src: url("https://cdn.jsdelivr.net/npm/mathjax@3/es5/output/chtml/fonts/woff-v2/MathJax_Vector-Bold.woff") format("woff");
}

mjx-c.mjx-c1D434.TEX-I::before {
padding: 0.716em 0.75em 0 0;
content: "A";
}

mjx-c.mjx-c28::before {
padding: 0.75em 0.389em 0.25em 0;
content: "(";
}

mjx-c.mjx-c1D435.TEX-I::before {
padding: 0.683em 0.759em 0 0;
content: "B";
}

mjx-c.mjx-c29::before {
padding: 0.75em 0.389em 0.25em 0;
content: ")";
}

mjx-c.mjx-c1D439.TEX-I::before {
padding: 0.68em 0.749em 0 0;
content: "F";
}

mjx-c.mjx-c1D44B.TEX-I::before {
padding: 0.683em 0.852em 0 0;
content: "X";
}

mjx-c.mjx-c2194::before {
padding: 0.511em 1em 0.011em 0;
content: "\2194";
}

mjx-c.mjx-c25FB.TEX-A::before {
padding: 0.689em 0.778em 0 0;
content: "\25A1";
}

mjx-c.mjx-c1D43B.TEX-I::before {
padding: 0.683em 0.888em 0 0;
content: "H";
}

mjx-c.mjx-c2192::before {
padding: 0.511em 1em 0.011em 0;
content: "\2192";
}

mjx-c.mjx-c1D443.TEX-I::before {
padding: 0.683em 0.751em 0 0;
content: "P";
}

mjx-c.mjx-c1D444.TEX-I::before {
padding: 0.704em 0.791em 0.194em 0;
content: "Q";
}

mjx-c.mjx-c2261::before {
padding: 0.464em 0.778em 0 0;
content: "\2261";
}

mjx-c.mjx-c1D464.TEX-I::before {
padding: 0.443em 0.716em 0.011em 0;
content: "w";
}

mjx-c.mjx-c30::before {
padding: 0.666em 0.5em 0.022em 0;
content: "0";
}

mjx-c.mjx-c31::before {
padding: 0.666em 0.5em 0 0;
content: "1";
}

mjx-c.mjx-c32::before {
padding: 0.666em 0.5em 0 0;
content: "2";
}

mjx-c.mjx-c25CA.TEX-A::before {
padding: 0.716em 0.667em 0.132em 0;
content: "\25CA";
}

mjx-c.mjx-cAC::before {
padding: 0.356em 0.667em 0 0;
content: "\AC";
}

mjx-c.mjx-c2227::before {
padding: 0.598em 0.667em 0.022em 0;
content: "\2227";
}

mjx-c.mjx-c22A9.TEX-A::before {
padding: 0.694em 0.722em 0 0;
content: "\22A9";
}

mjx-c.mjx-c2193::before {
padding: 0.694em 0.5em 0.194em 0;
content: "\2193";
}

mjx-c.mjx-c2C::before {
padding: 0.121em 0.278em 0.194em 0;
content: ",";
}

mjx-c.mjx-cA0::before {
padding: 0 0.25em 0 0;
content: "\A0";
}

mjx-c.mjx-c2032::before {
padding: 0.56em 0.275em 0 0;
content: "\2032";
}

mjx-c.mjx-c1D43F.TEX-I::before {
padding: 0.683em 0.681em 0 0;
content: "L";
}

mjx-c.mjx-c34::before {
padding: 0.677em 0.5em 0 0;
content: "4";
}
表示當對手是時，合作。

對於 FairBot，我們有：

也就是說，FairBot 合作若且唯若其對手可證明會合作。

作為勒布式合作的一個例子，考慮 FairBot 與自身對局。
將替換為：

這是一個亨金語句（Henkin sentence），即一個斷言自身可證明性的語句：

這類語句實際上是可證明的。
這是由勒布在他證明了我們現在稱為勒布定理的論文中確立的（來自 SEP 的一些歷史背景）。
當考慮兩個程式碼不同但行為一致的 FairBot 時，情況會變得更有趣，它們也會互相合作，但讓我們繼續看另一種 FairBot。

佩約式 FairBot

讓我們把之前討論的稱為「勒布式 FairBot」，接下來考慮「佩約式 FairBot」（Payorian FairBot）。
我仍然想稱它為 "FairBot"，因為我認為以下內容確實表達了一種公平性：

實際上，我更傾向於去掉所有括號，並用表示 FairBot 合作，用表示其對手合作。
如果你願意，可以看作且。
那麼條件是：

我們不再檢查對手是否合作，而是檢查「FairBot 的可證明合作」是否隱含「對手合作」。
但要注意這裡的「隱含」；它是實質蘊涵（material implication），並不表示真實的依賴關係。
例如，如果對手無條件合作，那麼這個蘊涵式平凡地為真——我們稍後會詳細討論這種情況。

佩約式 FairBot 看起來更複雜。
但對其進行推理要簡單得多，至少使用克里普克框架時是如此。

克里普克框架

事實上，這非常簡單，我認為它是學習使用克里普克框架的一個合適的入門練習。
所以我希望即使你以前從未用過它們，也能繼續讀下去，這篇文章可以作為一個教學。
為了推銷一下，我把它們看作是一種用於追蹤引用層級（quotation levels）的樹狀資料結構。
在囚徒困境競賽中，這些層級分別是：基礎現實、你想像你的對手、你想像你的對手想像你，依此類推。
它們最終位於樹的不同深度。

它們出現在囚徒困境競賽中的方式是，我們使用可證明性邏輯來解決對局。
但我們不寫證明，而是使用語義（semantics）。
如果你不知道語義是什麼意思，我希望這樣說會有幫助：它類似於使用真值表來解決命題邏輯中的問題。
命題邏輯的語義是，一個語句可以被真值表中的某一行滿足或不滿足。
或者換句話說，真值表中的一行可以作為命題邏輯語句的模型。
那麼，模態邏輯語句的模型長什麼樣呢？
（實際上我們會將其應用於一組語句，但它們可以通過合取合併為單個語句）。

我們從克里普克框架開始，它是一組可能世界以及該集合上的一個關係。
我一直聽說這被稱為「可達性」（accessibility）關係，但 Arbital 頁面稱之為「可見性」（visibility）關係，所以我將沿用這個說法。

在可證明性邏輯的特殊情況下，可見性關係必須是傳遞的。
當我畫出像這樣的克里普克框架時，我不會畫從到的箭頭，但從是可見的。
因此，圖表將是有向圖，而可見性就是沿著箭頭的可達性。
我假設這個有向圖不一定是樹，但只有在樹的情況下我才有直覺，即樹中較深處的可能世界被嵌套在我們正在考慮的任何引用層級中更深的地方。

克里普克模型是一個克里普克框架，加上對每個可能世界中哪些語句為真的賦值。
我們反證一個可證明性邏輯語句的策略，將是證明它不能被任何克里普克模型滿足。
（而要證明一個語句，我們將反證其否定項。）

我們分配給可能世界的語句不僅僅是命題邏輯的「基本」語句，還可以包括模態語句（包含或的語句）。
一個世界中的模態語句對其他世界中必須為真的語句具有暗示作用。
可能性斷言要求在某個可見世界中為真；在樹中，節點處的要求在某個後代節點（不一定是直接子節點）處為真。
必然性斷言要求在所有可見世界中為真；在樹中，節點處的要求在所有後代節點中為真。

世界不一定對自身可見，因為這是可證明性邏輯，所以我們通常不能從推導到。

好吧，這並不是最好的克里普克框架初學者指南。
如果你想要更完整的解釋，請查看 Arbital 頁面或 SEP。
但至少我已經重複了我要實際使用的實事，所以讓我們繼續將這些想法應用於佩約式 FairBot。

使用克里普克框架證明合作，以及 CooperateBot

我們證明合作的策略是假設 FairBot 背叛，寫下這對克里普克模型施加了什麼條件，並尋找矛盾。
矛盾意味著沒有克里普克模型能滿足前提，因此 FairBot 必須合作。

假設 FairBot 背叛意味著假設：

或者等價地：

這是一個可能性陳述。
我們將這個陳述為真的世界稱為，並將這對其他可能世界的暗示寫成如下形式：

我們通過在一個可見世界中使命題為真，滿足了根世界中關於「這些東西是可能的」之命題。

無論如何，現在我們可以證明 FairBot 會與 CooperateBot（合作機器人）合作。
CooperateBot 總是合作，這意味著為真。
因此，我們將添加的假設是，也就是說，合作是 可證明的。
FairBot 的行為取決於它能證明對手的什麼，所以我們總是會像這樣包裝對手行為的描述。

在處的意味著在所有下游世界中為真，這與處的矛盾。
因此，不存在能同時滿足 FairBot 的不合作與的克里普克模型，所以 FairBot 必須合作。

這種行為證明了 "FairBot" 這個名字的合理性。
它通過與 CooperateBot 合作來表現公平，而不是通過剝削它來追求獲勝。

更仔細地寫出來。
讓我們把這些命題放在根部。
首先，我們 FairBot 的行為：

接著，其對手 CooperateBot 的行為，但包裝成可證明性陳述：

最後，我們假設 FairBot 背叛：

我希望你會同意，第一個陳述和第三個陳述合起來等同於我們之前放在根部的內容。

因此，要模擬這些陳述，我們需要一個在根部所有陳述都為真的克里普克模型：

由於這隱含了之前的可能性陳述，我們加入隱含的可見世界：

由於我們在根部有，這隱含了下游的：

這就是我們的矛盾。
沒有克里普克模型能滿足這些要求。

一個佩約式 FairBot 會與另一個合作

現在，讓我們假設雙方都是 FairBot。
在讓它們對局之前，讓我們先寫下它們的不合作對克里普克模型意味著什麼，就像之前一樣。
兩個獨立的克里普克框架，並排排列：

現在，考慮一個對手也是 FairBot 的 FairBot。
這看起來就像是將上述第二個克里普克框架嫁接到第一個框架上。
為了設定它，如前一節所述，我們在根世界放置三個前提：我們 FairBot 的行為、其對手的行為（包裝在可證明性模態中），以及我們 FairBot 背叛的假設。

在處產生矛盾。
這就是佩約式 FairBot 會與另一個 FairBot 合作的證明。

但讓我們慢下來看看發生了什麼。
在處，我們「拆開」了對另一個 FairBot 的描述。
因為我們在處也有，這個世界現在看起來就像我們之前的。
所以在處，我們擁有之前中的一切。
但因為我們在處有，我們在處拆開它，導致了矛盾。

為什麼這個過程對我來說感覺是對的

我將看作是我們的 FairBot 正在模擬的一個世界。
它在問：「如果我可證明地合作，我的對手會做什麼？」
當對手本身也是 FairBot 時，變得很熟悉：它看起來就像我們考慮 FairBot 對陣 CooperateBot 時的樣子，只是和互換了。

我將想像成由模擬中的對手 FairBot 所進行的模擬。
我們避免了無限遞迴，因為我們已經假設在這個模擬中，模擬的對手發現第一個 FairBot 合作了。

這對我來說感覺是正確的深度。
我想像你想像我，然後我們就結束了。
這感覺就像當我在思考類紐科姆問題（Newcomb-like problems）時實際所做的事情。
在紐科姆問題中，我思考歐米茄（Omega）對我的模擬，如果我對歐米茄的心理「模擬」是在中，那麼我認為歐米茄的模擬就是在中。

在何種意義上這比勒布式合作更簡單

但我覺得，除非我將其與我在勒布式合作中遇到的複雜性進行對比，否則我還沒有真正展示出它的吸引力。
在我知道佩約式合作之前，我嘗試將這些前提放在根世界：

我不喜歡必須引入勒布語句。
我覺得我是在手動加入它，而我希望一切都是自動化的。
但有了這些前提，我可以機械地在克里普克框架上掛載要求，直到我發現矛盾——在中。

在 Critch 的文章中，他也指出佩約式方法避免了輔助語句。
他通過計算他在「自然演繹」型系統中的證明行數，論證了這種方法更簡單。

克里普克框架方法暗示了另一種量化複雜性的方式：在排除一致的克里普克模型之前，你必須深入到克里普克框架的第幾層？
對於佩約式合作，你需要深入兩層世界，這感覺是對的。
對於勒布式合作，你需要深入四層世界，這感覺不對勁。

我把這篇文章標題定為「使用克里普克框架，佩約式合作很簡單」。
你也可以說，一旦你使用佩約式合作，使用克里普克框架證明合作就很簡單。
在個人層面上，這就是其意義所在。
幾年前當我第一次開始做這類證明時，我對以這種方式定義邏輯決策論感到樂觀，即用克里普克框架結構追蹤決策演算法。
我以為證明 FairBot 與自身合作會是教學關卡，但對於勒布式 FairBot，它感覺更像是最終魔王。
偶然發現 Critch 的文章恢復了我對這種方法潛力的信心。

參與討論

https://lesswrong.com/posts/LaCP6WyNzX8kiZn3w/payorian-cooperation-is-easy-with-kripke-frames