【数学】前原昭二：数学基礎論入門【基礎論】

だ　れ　も　い　な　い　の　か　？

シグマトートロジー

3

第10章4節、p.159にある

1) 論理式x=yは表現可能

の証明の手順について教えていただけませんでしょうか。
考えてみたのですがわかりませんでした。
どうぞよろしくお願いいたします。

>>267
証明すべき論理式は書けますか？
それができるならば、次を使うことを考えてください。

x=y, F(x) -> F(y)

否定の方も証明しなければならないけど、
これは、定理 7.1 の 2 の証明をなぞればよい。

>>268, 269 レスありがとうございますm(_ _)m
証明すべき論理式は

x=y→BEW{x=y}
¬(x=y)→BEW{¬(x=y)}

ただし、{A}は、論理式AのGodel numberに対応する対象式
を表すものとする

です。特に前者についてですが、268でいただいたヒントから

x=y, BEW{x=x} -> BEW{x=y}

という形で使えばよいかと考えましたがを
そのためには、BEW{x=x}が証明できることが必要かと思いました。
定理7.1の証明にあったように、
公式4.1 x=x は証明できる論理式ですので、このことを内容的な数論では
Bew[x=x]と表せますが、それに対応すると考えられるBEW{x=x}
の証明が今のところできないでおります。

とりあえず、以上のような考え方でよろしいでしょうか…?

BEW{x=x}の証明できました。
定理8.1と同様に考えればよいのでした。

ありがとうございました。

たびたびすみません。第10章4節にある1) 論理式x=yは表現可能
の証明についてですが、>>269で教えていただいたにも関わらず

否定のほう: ¬(x=y)→BEW{¬(x=y)}

がやっぱり示せませんでした。
そもそもテキストにある定理7.1の2の証明を理解しきれていないのです。
定理7.1の1はわかったのですが、2はテキストとはおそらく異なる方法で
証明しました (nについての数学的帰納法で、公理1.1, 公理1.2また
対偶: 公式2.6を使いました）。

ですので、まずテキストの定理7.1の2の証明について
説明をいただけませんでしょうか…？またさらに、上の論理式の証明での
その用い方についても教えていただけると助かります。
よろしくお願いいたします。

age

>>273
定理 7.1 の 2 の証明ですが、お考えになっている証明は次の方針だと
思いますが、これが著者の意図している証明のはずです。

1) 公式 4.3 の対偶を用いれば m>n と仮定してよい。
2) 公理 I.1 から始めて公理 I.2 の対偶を n 回用いて m≠n を証明する。

この本の体系に沿った形での正確な証明に直すことは既にできていると
思います。


¬(x=y)→BEW{¬(x=y)} の証明ですが、上の 1) 2) の証明を形式化する
ことになります。そのためには、公式 4.3 公理 I.1 公理 I.2 を形式化
した次の論理式が証明できることを確認しておく必要がありますが、
これは定理 8.1 でやってあります。

BEW{x=y→y=x}, BEW{¬(x'=0)}, BEW{x'=y'→x=y}

具体的には、¬(x=y)→ (x>y)∨(y>x) なので
x>y→BEW{¬(x=y)} と y>x→BEW{¬(x=y)} を証明すればよいわけですが、

2') x>y→BEW{¬(x=y)} は y に関する数学的帰納法 (これが 2) の形式化)
1') y>x→BEW{¬(x=y)} は y>x→BEW{¬(y=x)} が上と同様に証明できるので、
これと BEW{x=y→y=x} を用いて導く (これが 1) の形式化)

とすれば、証明できるはずです。

おまいら、揃いも揃って、レヴェル低いな（爆笑

# 偽と矛盾との違いさえ分からんだろ？

6

26

>>275
そんなカキコされると、なんか、白けてしまうなぁ・・・。

866

この本と同じシリーズで『集合論』というのがあったけど、あれは復刊しない
のかな。圏論を扱ってる貴重な本だったのに。

>>275
そういう御大は、アリストテレスとフレーゲの違いがわからない（笑

>>281＝「�dデモ助平町人マツシン炭」ですた（ｗ

>>282＝「エムシラ御大」でつか（ｗ

つがわん

>>275
真理概念と証明可能概念の違いが分からないのは直観主義者でつ(w

コピペと知って敢えてレス。半分冗談なので、ロジシャンの人は聞き流して
下さいね。

>真理概念と証明可能概念の違いが分からないのは直観主義者

そうなん？
違いがあるからこそ、「あえてそれらを同じと見なそう」という
直観主義的視点が成立するんでネーノ？
間違ってたら許せや(w

>>286
う〜ん、違いが分からんのはむしろヴィトゲンシュタインなのでは。

おまいら、「古い」な（ｗ

あげなきゃ

さげなきゃ

>>285
ゲーデル
「だからぁ、漏れの命題は証明できないから正しいんだって」
ヴィト
「ハァ？証明できないんだろ？じゃ正しいわけないじゃん」
ゲーデル
「よく嫁。漏れの命題は「これは証明できない」っていうものなの。
　で、証明できないんだから正しいだろってこと。わかる？」
ヴィト
「あのなあ、証明できないっていうためには
　証明できないことを証明しなくっちゃダメなんだよ。
　証明できないことも証明できないんじゃ
　証明できないっていえないんだよ。」

ゲーデル
「そう、そこだよ。>>291
　漏れの命題は、”証明できない”ならば
　”証明できないことが証明できない”
　わけなんだよ。どんどん続いちゃうんだよ
　だから証明できないんだよ。」
ヴィト
「そのどんどん続いちゃうってのが問題だな。
　全部やりきったわけじゃないだろ？
　判断できることは全て有限なんだ。
　そうだからこそ数学で証明という手続きを用いるんだろ？
　なんで肝心なところだけ無限の神学というか形而上学を持ち出すんだ？」

ゲーデル
「>>292　証明は方便にすぎないよ。
　形式ヲタのヒルベルトは論破できても
　プラトニストの漏れはそうはいかない。
　肝心なのは数学的真理を感じるセンス」
ヴィト
「･･･コイツ神秘主義者だったのか（汗
　それならそれで、証明なんかやめて、
　全てセンスだけでやればいいじゃないか」
ゲーデル
「う、それを言われると正直イタイ（汗」

>”証明できないことが証明できない”
> わけなんだよ。どんどん続いちゃうんだよ

これは、何故でつか？　いや、”証明できないことが証明できない”のは
構わないのですが。その後の、「どんどん続いちゃうんだよ」ってとこ。

例えば、”証明できないことが証明できない”ことが証明されても、命題の
中身である「証明できない」に反する訳ではないし、またもちろん「証明
できる」ことが証明された訳でもないのだから、やはり何ら矛盾はないです
よね？

要するに、”証明できないことが証明できない”ことが証明されても、特に
問題ないと考えても良いのけ？

>>294
＞これは、何故でつか？
ゲーデルの命題がそうなっているから。

　「この文は証明できない」
＝「「この文は証明できない」は証明できない」
＝「「「この文は証明できない」は証明できない」は証明できない」
＝･･･

これがいえるだけ、決して
「”証明できないことが証明できない”ことが証明される」
ことはないんだ。わかるね。

あい、４日間ほど考えて、ようやく分かりますた(w

ところで、>>293でゲーデルがいきなり「センス」などという語を用いて
いますが。これってセンスの問題なんすか？

645

この本少しやり方が古くない？

古い本ですが何か？

前原先生って真偽概念を前面に押し出した不完全性定理の証明には
ヒステリックな反応を示してたみたいだね。

>>299
しかも、中でオリジナルに忠実に従っていると宣言している。

>>300
数学者って人格的に問題ある人が少なくないからね。

そうかな？極端な人もいるにはいるが、概して
良い人が多いと思うけど。

さがりすぎ

おまいら、揃いも揃って、レヴェル低いな（爆笑

# 偽と矛盾との違いさえ分からんだろ？

うわぁ〜クサいクサい（ｗ

やはり、これからの時代は、何と言っても、御大の「論*狸*学」でしょう。

http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html

282

386

誰か型理論（タイプ理論）の事に詳しいような本
（出来れば日本語で）ご存じないですか？
今図書館etc.で何とか読めるのが
『プリンキピア・マテマティカ序論』なる本と
『数理論理学とタイプ理論―証明による真理へ』
とかいう古い本しかないのですが。

ところで型理論が（ZFCなどに比して相対的に）廃れたのは
解析学がその上にのらないから、という理解で良いのでしょうか。

>>310
「リーディングス　数学の哲学　ゲーデル以後」飯田隆編　
の第2章にクルト・ゲーデルの書いた「ラッセルの数理論理学」
って論文があるから読んでみ。

ゲーデルは自分の構成可能集合の理論は、ラッセルのオーダーの理論
（分岐タイプ理論）を非構成主義的＝実在論的に用いたものだって
いってるね。

>>311
thx.
学校の図書館に置いているみたいなんで
今読んでいる本が終わったら
手を出してみようかと思います。

704