おはようございます。
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につぶしてくるんですね。
それはそれとしてまんがタイムきららで連載中の「放課後すとりっぷ」を皆読みましょう。
(追記)
PFAはSCHを導いたりsupercompactっぽい振る舞いをするのでPrikry type forcingとかするとすぐに壊れる。まあPrikry type forcingはそもそもsupercompactness壊すのでそれはそうなんですけど