ホームへ戻る
  • Theorem II.8.10証明中， RCA_0がcut-freeな証明システムを扱えること．

    • まだ確証を得られていません．いわゆるLKなどをRCA_0上でコード化してカット除去を示せばよいと思うのですが，ちゃんと証明をするのは大変そうです．調べたところ Petr Hájek, Pavel Pudlák"Metamathematics of First-Order Arithmetic" のChapter V（projecteuclid.orgに落ちています）が良さそうですので，いつか確認したいと思っています．

  • 算術的超限再帰公理を表す論理式

    • ATR_0はテキスト中で若干インフォーマルに定義されていてはじめは困ったので形式化したそれを置いておきます．

  • 普遍 light face Π01 論理式

    • VII章がはじまるや否やいきなり定義されますが，構成は非自明なのでアイデアを説明します．ただ，上記のpdfとは少し違う思想で同様の普遍性を満たす論理式を作ることもできます．詳しくはホームにある「RCA_0 上で動作する Turing functional を作る」を見てください（いずれにせよ形式的な定義が非常に大変なことには変わりはありませんが...）．

  • βモデルがΠ1∞-TI0 のモデルになること

    • Lemma VII.2.15の上で説明されていましたが，これはメタ（ZFCなど）の帰納法を使えばよいです．

  • VII.3節のTheorem3.27以降

    • 形式的に示すには少し根気が必要なものが多いです．つらくなったら先にVIII章に進むと嬉しい気持ちになれます．TheoremVII.3.29とVII.3.31（＋α）からATR0のモデルの圏（射はΣ11埋め込み）とATR0setの圏（射は推移的埋め込み）が同値であることが従います．そのうちPDFを作るかも知れません．

  • VII.4節

    • Thoerem VII.4.8が成り立つと思えません．誰か助けて． ホームへ戻る