証明可能性論理における難民のフォークロア
ここで述べられているが，この話がそもそも誰に由来するのかはわからないらしい．
以下引用．
地球の何処かに定住国を求める難民$ xがいる．
地球の国の数は有限である．
それぞれの国には渡航できる国は決まっているとする．
$ xは次のルールに沿って，母国から移住していく．
R1. 既に訪れた国には二度と戻れない．（非反射性）
R2. $ Aから渡航可能な国$ A'から渡航可能な国$ Bには，$ Aからでも渡航可能．（推移性）
R3. 今いる国から渡航可能な国には，「その国に定住しないこと」を証明したなら必ず移動する．
このとき，$ xは最終的にどうなるのか？
L1. $ xの定住国は必ずどこかに一国だけある．
R1と国の有限性より．
L2. 定住国が母国でない$ Aなら，「$ Aに定住しない」ことを証明しているはず．
R3より．
SnO2WMaN.icon「定住しない」と証明しておいて定住するってどういうことだよとは思うが，一旦受け入れる
L3. 定住国が$ Aで，$ Bが$ Aに渡航可能であるなら，「$ Bに定住しない」ことは証明できない．
もし証明出来たならR3より$ Bに移動しなければならない．ところが$ Aに定住しているのでそれはない．
L4. $ xが$ Aにいずれ渡航するが$ Aが定住国でない場合，$ Aから渡航可能などこかの国が定住国でなければならない．
R2より．
定住国となった場合$ xが幸せになれる国とそうでない国があるとする．$ xは自分が幸せになれることをなんとか証明したいとする．
母国でない$ Aが定住国とする．
H1. $ Aから渡航可能な国が全部幸せになれる国だったとする．
L2より，「$ Aには定住しない」ことは証明しているはず．
L4より，「$ A国から渡航可能などこかの国は定住可能である」ことが証明される．
仮定より，そのような国は全部幸せになれる国であることがわかっている．
結果，「$ xは幸せになれる」ことが証明できる．
H2. $ Aから渡航可能な国に幸せになれない国$ Bがある場合
仮に「$ xは幸せになれる」と証明できたとする．
このとき，「$ Bには定住しない」ということが証明されなければならない．
ところがそれはL3に反する．
なので「$ xは幸せになれる」ことは証明できない．
$ xは自分が証明した通りに動いて定住するとすると，結局母国からは一度も動くことは出来ない．
そのような$ xは一度移動すると延々に移動しなければならないが，国は有限だからそれは出来ない．
ここまでを纏めると
国$ Aを定住国とすれば$ xが幸せになれることを$ A \vDash Hと表す．
$ Aから移動可能な全ての国で幸せになれることは$ A \vDash \Box Hと表せる．
remark:$ A \vDash \Box H$ \iff$ A \rightsquigarrow A'な任意の$ A'で$ A' \vDash H
$ xが$ Aを定住国とすることを$ \beta_Aとする．
とすると
H1は$ \beta_Aかつ$ A \vDash \Box Hならば$ \mathrm{Pr}(H)
H2は$ \beta_Aかつ$ A \vDash \lnot\Box Hならば$ \lnot \mathrm{Pr}(H)
よって$ \Boxと$ \mathrm{Pr}が上手く対応する．