11/12/13 02:26:39.96
>>631
レス遅くなりましたが、解説ありがとうございます。おかげで疑問点は解消できました。
もう1つ質問させて下さい。（何度もすみません）
このスレでも何度か書いていますが、私はどうしてもLoebの可導性条件、特に
D3 PA|- Pr([A])→Pr([Pr([A])])
の証明が理解できません。
以下、私がどこまで理解しているかを簡単に書きます。
D3を証明するためには、任意のΣ1文Fに対して、
PA|- F→Pr([F])
が証明できればよく、そのためにはFの構成に関する帰納法で証明すればよいわけですよね。
つまり、以下の１から４の順番で証明すればよいと。
１、F ⇔ x=y, 0=x, Sx=y, x+y=z, x・y=z のとき、PA|- F→Pr([F])
２、F ⇔ G∧Hのとき、PA|- F→Pr([F])
３、F ⇔ ∃xG(x)のとき、PA|- F→Pr([F])
４、F ⇔ ∀x<y G(x)のとき、PA|- F→Pr([F])
以上の１以降が理解できなく困っています。たとえば、
PA|- x+y=z→Pr([x+y→z])
はどのようにして証明すればよいのでしょうか。
文献[1]には、これの証明が載っているのですが私にはよく理解できませんでした。
使用している文献は
[1] Boolos「THE LOGIC OF PROVABILITY」
[2] 田中他「数学基礎論講義」
の2冊です。
長くなりましたが、どうぞよろしくお願いします。