- 403 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 16:24:20 ]
- Pr'（ｘ）≡∃ｙ（Prov(y,x)∧¬∃ｚ＜ｙDispr(z,x))
これだけを見ると、よく文意がわからないんですよね
∃ｙが全体にかかってて、で、∃ｚ＜ｙってのは、例のごとくなんかの省略なわけで、ｙが縛られているのかどうかもよくわかんねえし（有界量化子ってなんだよ、という上の質問もここらへんの関係から）
ということは、コレ自体がなんかの目的で作られたというよりは、なんかを変形して流れ着いたのが、これなんじゃないか、というように勘ぐってたら、
今、『数学基礎論講義』という本を読んでるんですが、
＞Pr'（ｘ）≡∃ｙ（Prov(y,x)∧¬∃ｚ＜ｙDispr(z,x)) の意味は、
＞「φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも¬φの証明ではない」
とあって、
ふ〜ん、そうなんだ、と、よくわかんないまま、そのまま引用したのが
>>399
の書きこみです。
>>402
もうひとこと、さらなる書きこみ、ﾏｯﾃﾏｽ
