Index / Reload / Edit
体系における証明検査述語BとB*が外延として同じものだとしても、それを体系内で証明することはできません。似たような話として、カットのない証明においては無矛盾性は簡単に証明でき、またカット除去が出来る場合には「証明が存在する」と「カットのない証明が存在する」は同値になりますが、肝心のカット除去の証明が体系内ではできません。
通りすがりさん、こんにちは。関係 B(m,n) と B*(m,n) は個別の具体的な自然数に対して同値であるにもかかわらず、論理式 B(x,y)←→ B*(x,y) は体系内で証明できないということでしょうか。もちろん証明できてしまったら大変なことになりますが。で、カットの方は申しわけないのですが、さらに不勉強にて全く分かりませんが、なんとなくおっしゃられることの雰囲気は。というわけで、コメントありがとうございました。
＞妥当であるかどうかは別としてこのあたりのことは「確かさを求めて」（培風館）のRosser体系T^Rに関するところで多少詳しく議論されているようです。B*が成り立つときのみに論理式が証明された、と考えることにすると、βが{δ1,.........,δn}から導出でき、δ1,.........,δnがそれぞれの否定よりも先に導出可能だとしても、この二つから直ちにβが「¬βより先に」導出可能であると結論することが出来ません。つまり導出済みの定理を公理と同様に扱う事が出来る、という規則（つまりLK/LJなどにおけるcutに相当する規則）が成り立たないわけです。ほかにもFefermanやMostowskiなども似たような注意をしているらしく、それらがなぜ第二不完全性定理の意義を下げるものでないかが解説されています。集合論についてはせいぜい反映原理などまでが紹介されているくらいであまり詳しくありませんが、良い本だと思います。
Standard Modelさんに質問ですが、体系内の証明のカット除去可能性は、体系の"健全性"を示すような何らかの命題に対応するものなのでしょうか？
＞通りすがりさん私は別に特にこういう話題に詳しいわけではないので、通りすがりさんの望むような返答は出来ません。カット除去という用語をsequent計算に限定された狭い意味ともっと広い意味のどちらで使われているのか、また「健全性」というのをどういう意味で言っておられるのかわかりませんが、前掲書のエンドノートに、＞Feferman（1982,1989）は、「何が形式的理論の標準的な提示方法とよべるか」ということに説明をつける道を切り開いた。とありますのでもしかしたら何か関係があるかもしれません。
Standard Model さん、こんにちは。反応が遅れて申しわけございませ。やっとご紹介の本を読み終わりました。ご指摘の通り B* で cut に対応する推論が出来ないことが分かりました。本文で何度も引用されている Feferman（1982,1989) の著作はとても面白そうです。機会があったら読んでみたいと思います。余談ですが、T^F に関しては完全性定理の証明を連想しました。ちょっと反則気味かなと。
体系における証明検査述語BとB*が外延として同じものだとしても、それを体系内で証明することはできません。似たような話として、カットのない証明においては無矛盾性は簡単に証明でき、またカット除去が出来る場合には「証明が存在する」と「カットのない証明が存在する」は同値になりますが、肝心のカット除去の証明が体系内ではできません。
通りすがりさん、こんにちは。関係 B(m,n) と B*(m,n) は個別の具体的な自然数に対して同値であるにもかかわらず、論理式 B(x,y)←→ B*(x,y) は体系内で証明できないということでしょうか。もちろん証明できてしまったら大変なことになりますが。
で、カットの方は申しわけないのですが、さらに不勉強にて全く分かりませんが、なんとなくおっしゃられることの雰囲気は。
というわけで、コメントありがとうございました。
＞妥当であるかどうかは別として
このあたりのことは「確かさを求めて」（培風館）のRosser体系T^Rに関するところで多少詳しく議論されているようです。B*が成り立つときのみに論理式が証明された、と考えることにすると、βが{δ1,.........,δn}から導出でき、δ1,.........,δnがそれぞれの否定よりも先に導出可能だとしても、この二つから直ちにβが「¬βより先に」導出可能であると結論することが出来ません。つまり導出済みの定理を公理と同様に扱う事が出来る、という規則（つまりLK/LJなどにおけるcutに相当する規則）が成り立たないわけです。
ほかにもFefermanやMostowskiなども似たような注意をしているらしく、それらがなぜ第二不完全性定理の意義を下げるものでないかが解説されています。集合論についてはせいぜい反映原理などまでが紹介されているくらいであまり詳しくありませんが、良い本だと思います。
Standard Modelさんに質問ですが、体系内の証明のカット除去可能性は、体系の"健全性"を示すような何らかの命題に対応するものなのでしょうか？
＞通りすがりさん
私は別に特にこういう話題に詳しいわけではないので、通りすがりさんの望むような返答は出来ません。
カット除去という用語をsequent計算に限定された狭い意味ともっと広い意味のどちらで使われているのか、また「健全性」というのをどういう意味で言っておられるのかわかりませんが、前掲書のエンドノートに、
＞Feferman（1982,1989）は、「何が形式的理論の標準的な提示方法とよべるか」ということに説明をつける道を切り開いた。
とありますのでもしかしたら何か関係があるかもしれません。
Standard Model さん、こんにちは。
反応が遅れて申しわけございませ。やっとご紹介の本を読み終わりました。ご指摘の通り B* で cut に対応する推論が出来ないことが分かりました。本文で何度も引用されている Feferman（1982,1989) の著作はとても面白そうです。機会があったら読んでみたいと思います。余談ですが、T^F に関しては完全性定理の証明を連想しました。ちょっと反則気味かなと。