"Forcing in proof theory" (Jeremy Avigad)

yoriyukiさん経由、論文はこちら。
minimal logic (直観主義マイナス矛盾律)や直観主義のクリプキモデルと、古典論理上ZFCの強制法の関係について、今までよく分からなかったのだが、少しだけ分かったような気がします。

1. 古典論理の論理式 を二重否定翻訳（のversion）により*1に翻訳する。ちなみに、は、の略。
2. 直観主義論理のフレームの成立関係をで表現する。さて、直観主義論理では、はと同値であり、また任意の p に関して が成立する。
3. を仮定する。これはと同値であり、上のに関する条件より、と同値になる。これはと同値。
4. このように、古典論理上の強制法のdensity conditionは、直観主義のフレームのに関する条件と、また二重否定翻訳から導出される（もちろん、nameに関する話など、いろいろ他にもありますが、当論文ではあまり触れていないので略）。
5. ちなみに、generic filterの役割は、denseなconditionをもつ論理式を全て集めてくることである。

二階算術のモデル構成の箇所の話を飛ばしているので、「読了」はしていません。

*1:はの Kuroda translation