墓標

オタク思想とオタク地獄とラブコメと萌え4コマ漫画

PFAの無矛盾性証明についてのノート


おはようございます。

 

PFAの無矛盾性証明を読んだのでそのノートを書きました。

 

PFAはMAの強化版みたいなやつで、無矛盾性証明のアナロジーも似通っているところがある気がします。

 

MA_ω1の無矛盾性はsizeがcontinuum未満のc.c.c.を並べてiterationしまくるというもので、これだけで良かったのは任意のc.c.c.とω1コのdenseについてそれと交わるfilterを作るのにはsizeがcontinuum未満の部分順序を見ればよかったからですが、

 

properはc.c.c.に比べてとても広いclassなのでそういう事が出来ないっぽい。

 

ではどうするのかというとκをsupercompactとして、それによるLaver functionを使って長さκのCS-iteration P_κを定義して、任意にPFAの仮定となる(P,D)を取ってきたらj(P_κ)_κ番目にそのPが来るようにしてやろう、みたいなことをやります。

 

 

実際はその(P,D)の中に道中のposetが埋め込める事を示そう、みたいな事やりますがそこはわりとelementary embeddingで伸ばして超準元みたいなもの取ってj(κ)未満に良いwitnessがあるからκ未満にもあるよヤッターみたいないつもの論法ですね。

 

いや〜頭いいですねこの証明。本が採用しているであろうiterationの定式化と自分の定式化が違ってnotationが煩雑になった事を除けばめちゃくちゃ気分が良いです。

 

それとPFAはある意味でω2にsupercompactnessを載せてるようなもんだよ、と言われたことがあるんですけど実際このposetはsupercompact κをω2につぶしてくるんですね。



それはそれとしてまんがタイムきららで連載中の「放課後すとりっぷ」を皆読みましょう。

 

 

 

www.dropbox.com

 

(追記)

PFAはSCHを導いたりsupercompactっぽい振る舞いをするのでPrikry type forcingとかするとすぐに壊れる。まあPrikry type forcingはそもそもsupercompactness壊すのでそれはそうなんですけど