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

この本で勉強している人、意見交換や質問につかいませう。

第７章サパーリわからん。

/ヘ;;;;;　
';=r=‐ﾘ　
ヽ二/　

age

倉田の本が、漏れは、好きだーーーーーーーーー

http://science.2ch.net/test/read.cgi/math/1044067158/
こちらもよろしく

p.137の問2（「wffのset Kがω無矛盾のとき、Kに決定不能命題を追加して
得られるset K'もω無矛盾であることを証明せよ」といった内容です）
が解けないのですが教えていただけませんでしょうか、、、？

ヒントにあるように、K'がω矛盾することを仮定したとき
Kがω矛盾することを示そうとしたのですが、Kのω矛盾の条件のうち
後半部分のほうが計算できませんでした。
よろしくお願いいたします。

基礎論は数学ではない。ロジック遊びである。

数学はロジックではない。基礎論遊びである。

ロジックは基礎論ではない。数学遊びである。

>>7

余談だけど
「wffのset Kがω無矛盾のとき、
　Kに決定不能命題の否定を追加して
　得られるset K'はω矛盾である」
ことは証明できるかな？

>>11
はい、できます。（テキストのp.128にも書いてありました）
K'からただちに決定不能命題の否定を導出できますので、
これと定理8.8の1を合わせればただちにω矛盾であることがわかります。
しかしこのときK'は無矛盾です。

>>12 簡単だったね（ｗ

で、>>7だけど、決定不能命題Gと、G⇒X（Xは任意の命題）が
元のKでω無矛盾であることを使えばいいんじゃないかな？
（間違ってたらｽﾏｿ）

>>13 今のところ、うまくいっておりませんです。

>>14

君が？

できました。おさわがせしました。
証明を記します　（turn styleは「ト」を使いました。）：

(∀n)[K' ト F(n)] かつ　K' ト ¬∀xF(x) を仮定する。
R(y)∧(∀xR(x)→F(y)) を G(y) とおく。
以下、　(∀n)[K ト G(n)] かつ K ト ¬∀yG(y) を示す。

(1)
　(∀n)[K' ト F(n)]
⇔(∀n)[K∪{∀xR(x)} ト F(n)]
⇒(∀n)[K ト ∀xR(x)→F(n)] deduction theorem
　(∀n)[K ト R(n)] 定理8.8の2
∴(∀n)[K ト R(n)∧∀xR(x)→F(n)]
∴(∀n)[K ト G(n)]

(2)
　K' ト ¬∀xF(x)
⇔K∪{∀xR(x)} ト ¬∀xF(x)
⇔K∪{∀xR(x)} ト ∃x¬F(x)
⇒K∪{∀xR(x)} ト ¬F(a)　
⇒K∪{∀xR(x)} ト ∀xR(x)∧¬F(a)
⇒K ト ∀xR(x) → (∀xR(x)∧¬F(a))　　deduction theorem
　K ト R(a) → (∀xR(x)∧¬F(a))
　K ト ¬R(a) ∨ (∀xR(x)∧¬F(a))
　K ト ¬R(a) ∨ (∀xR(x)∧¬F(a))
　K ト ∃y (¬R(y) ∨ (∀xR(x)∧¬F(y)))
　K ト ¬∀y (¬R(y) ∨ (∀xR(x)∧¬F(y)))
　K ト ¬∀y (R(y) ∧ ¬(∀xR(x)∧¬F(y)))
　K ト ¬∀y (R(y) ∧ (¬∀xR(x)∨F(y))) de Morgan則と二重否定の除去
　K ト ¬∀y (R(y) ∧ (∀xR(x)→F(y)))　　
∴K ト ¬∀yG(y)　　　　　
　　　　　　　　　　　　　　　　　　　（証明終わり）

>>17
＞K ├ ∀xR(x) → (∀xR(x)∧¬F(a))
から
＞K ├　R(a) → (∀xR(x)∧¬F(a))
はいえないよ。

>>18 御指摘ありがとうございます。
すみません、>17は間違っていました。もう一度考えます。

K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xF(x)
K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬F(a)　
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀xR(x) → ¬F(a)　
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀y (R(y) ∧ (∀xR(x)→F(y)))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(a) ∧ (∀xR(x)→F(a))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀xR(x)→F(a)
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬R(b)
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀y (R(y) ∧ (∀xR(x)→F(y)))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b) ∧ (∀xR(x)→F(b))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b)
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト⊥
K ト ¬∀y (R(y) ∧ (∀xR(x)→F(y)))　

で、どーよ？

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

>>22
をひをひ、ちゃんと見たのか？

>>21の証明だけど、
＞K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xF(x)
から
＞K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬F(a)　
を導くところと、
＞K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)
から
＞K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬R(b)
を導くところは、問題アリ

>>23
そうだね、ちゃんと
「ただしaはここまでの証明で現れていない項」
「ただしbはここまでの証明で現れていない項」
と但し書きをつけておいたほうがいいね。

>>23
存在例化とかいちいち断らなきゃいけないのか（苦笑

悪いがもれはそこまで親切ではない。初頭の計算がきっちり分かってれば、
>>24 のように自分で行間うめられると思うんだがね？

>>25
日本語が嫌いなのかな（ｗ

形式に無用な愛着を持っているのでないならば
証明の構造を示す為に必要な文章を書けるはずだがね。

てゆーか、存在例化の使い方マチガッテル。教科書嫁。

>>27
そうかな？
但し書きさえ埋めれば、この使い方でもあまり問題ないんじゃ。
日本語を愛する人なら「存在例化」ではなく「∃消去」と書かなくては
いけないとかそういうこと？

>>28
全然違うな。
存在例化（あるいは∃消去）は自然演繹法の推論規則だろう？
教科書をみればわかるが、この場合

Γト∃ｘP(x)　および　Δ、P(a)トC　ならばΓ、ΔトC
(aは他のどの仮定にも自由変数として現れないもの）

の形で用いられる。

>>29
それはLKだろ！
今の体系はLKじゃねえんだｳﾞｧｶ！

>>30
ハァ？
LKに消去なんてないだろ。
（∃右）とか（∃左）とかいうのはあるが。

無知な奴は必ず他人がヴァカだと思うから困る（ｗ

>>31
じゃあ
> Γト∃ｘP(x)　および　Δ、P(a)トC　ならばΓ、ΔトC
これは自然演繹のつもりなのか？

>>32
それは23に言ってくれ

もしかしてLK（シークエント計算）と
NK（自然演繹法）の区別がついてない？

どっちにしても存在例化はあんな推論規則じゃないぞ。
もしかして、推論規則だけタブロー法の教科書見てないか？（ｗ

>>33

とにかく、君の今見ている本の名前を書け。

>>29
だいたいなんで>>21が自然演繹なんだよ。
Hilbert/Lukasiewiczだと解釈すれば済む話じゃん。

>>37

とにかく、君のいってる存在例化が出ている本の名前を書け。

無知な奴に限ってHilbert/Lukasiewiczとか
知ったかぶりでハッタリかますから困る（ｗ

だから自然演繹でもLKでもなくてHilbert/Lukasiewiczの体系だって。
それにあれを存在例化って書いたのは俺じゃない。

>>39
話をする気がないんなら相手しないけど？

>>40

多分、その理解はマチガッテル。

>>41

自分が正しいというなら説明できるだろ。

ま、言い訳できないなら黙りな

>>43
説明したじゃん、>>21の体系は自然演繹でもLKでもないって。
それ以外に体系を知らんから説明して欲しい、ってんなら
そう書けばいいのに。

>>45

説明できてないな。君がただ自分で言い張ってるだけ。
ウソはいけないな。ウソは。

>>21はうっかり戸田山の「論理学をつくる」の
タブロー法の推論規則を使ってしまった、に
１億円（ｗ

>>21
見てたら出てきな。マツシンっぽい人が1億円くれるってよ。

∃xP(x)が証明できれば、ある項aが存在してP(a)が証明できる
というのは、常識的にみて、かなり胡散臭い。

これって結局ω無矛盾性と同じだから。

>>21はマツシン以下の厨房

>>49
>∃xP(x)が証明できれば、ある項aが存在してP(a)が証明できる
>というのは、常識的にみて、かなり胡散臭い。
というか、一般的にはできません。
でも>>21が書いてるのはそういうことじゃないんじゃない？

いつのまにか>>21が悪者にされてるな。
面目ない。

>>51

いや、¬∀ｘP(x)は、∃ｘ¬P(x)だから同じだよ。

>>53
>>49の∃を¬∀¬に変えても>>51で言いたかったことは同じ。
あんたは>>21の書きたかったことがたぶんわかってない。
まあ俺が>>21の意図を誤解してないという保証もないけど。

>>54

ちゃんと説明してごらん。
説明できないんじゃ君が誤解しているといわれても仕方ないよ

いっとくけど、背理法だからいいと思ってるなら誤解だよ。

>>55
長くなるから嫌なんだが。

>>23
> >>21の証明だけど、
> ＞K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xF(x)
> から
> ＞K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬F(a)　
> を導くところと、
> ＞K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)
> から
> ＞K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬R(b)
> を導くところは、問題アリ

といって、>>21が「導いている」つもりだと理解するのがおかしいんだろ。

しかし俺も>>21が自然演繹のつもりかもしれないという気はしてきた。
どっちみち、どの体系か明記してないので「・・・の体系の規則でないと
いけない」という議論は意味ないが、後半だけ書くとこうか？

(1) K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)
(2) K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬R(b)　　　　仮定、ただしbはこれまでに現れていない項
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀y (R(y) ∧ (∀xR(x)→F(y)))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b) ∧ (∀xR(x)→F(b))
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b)
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト⊥
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト⊥ 　　　(1), (2)より仮定消去（∃消去）
K ト ¬∀y (R(y) ∧ (∀xR(x)→F(y)))

でもそれなら

K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)
K,∀y (R(y) ∧ (∀xR(x)→F(y))), ¬R(b)　ト⊥
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト⊥ 　　　(1), (2)より（∃消去）
K ト ¬∀y (R(y) ∧ (∀xR(x)→F(y)))

と書きそうな気もするな。

>>58

>>49がおかしいと思ってるなら、どっちみちダメじゃん。

>>59
ほらやっぱり俺の書いたこと読まずにレスする。
>>57に書いたように、
> >>21が「導いている」つもりだと理解する
のであれば>>49があてはまっておかしくなるが、そうじゃなくて
>>58のように理解すればその限りではない、って。

うーむ、なるほど。すばらしい（ｗ

ところで、>>21の
＞∀y (R(y) ∧ (∀xR(x)→F(y)))
って何を意味するの？

■■わりきり学園■■

コギャルから熟女まで

素敵な出会い

ゲイ、レズビアンなどコンテンツ豊富

http://kgy999.net/

>>61
前原昭二：数学基礎論入門をよもうよな。

ほい、21です。１億円もらいにきました（笑。
>>51 さん、もうしわけないなあ。すまんす。

基本的には、Hilbert/Lukasiewicz スタイルで書きましたが、
めんどくさかったので存在例化もどきを使って書いたよ。

Hilbertスタイルに慣れてれば分かると思うけど、存在例化と
同じことができます。そのことを知っていれば、あれだけ
書いておけば正確な Hilbertスタイルの証明を再現可能です。
質問者は慣れてるっぽかったので手を抜かせてもらったんだけど。

例えば、

　　Γ ト ∃ｘP(x)
　　Γ , P(b) ト ∃ｘP(x)
　　Γ , P(b) ト P(b) <- この b を存在例化の仮に導入された定項として用いる。
　　・・・・・・・・・・
　　Γ , P(b) ト A　<- で、なんか結論が出る
　　Γ ト P(b)→A
　　Γ ト ∃ｘP(x)→A
　　Γ ト A

んな感じで、清書できるよ。

適当に推敲せずに書いたのでかなりリダンダントな証明になってる
ことはみとめざるをえないでつ。そのへんは質問者が改良してくれ。

>>49
これはゲーデルの不完全性定理の証明するという流れの中での
練習問題だから、システムがω無矛盾で別に問題ないという説もあったり
なかったり（笑）。

>>64

要するに言語障害の二人が、テレパシーで交信したってわけだね（ｗ

>>63

>>16に書いてあった（ｗ

＞(∀n)[K' ト F(n)] かつ　K' ト ¬∀xF(x) を仮定する。
＞R(y)∧(∀xR(x)→F(y)) を G(y) とおく。
＞以下、　(∀n)[K ト G(n)] かつ K ト ¬∀yG(y) を示す。

>>64

K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xF(x)　（１）
---
K,∀xR(x) ,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬F(a)　（２）　仮定
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀xR(x) → ¬F(a)　（３）
---
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀y (R(y) ∧ (∀xR(x)→F(y))) （４）
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(a) ∧ (∀xR(x)→F(a))　（５）
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀xR(x)→F(a)　（６）
---
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬∀xR(x)　（７）　（１）、（３）、（６）より
---
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト¬R(b)　（８）　仮定
---
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト∀y (R(y) ∧ (∀xR(x)→F(y)))　（９）
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b) ∧ (∀xR(x)→F(b))　（１０）
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　トR(b)　（１１）
---
K,∀y (R(y) ∧ (∀xR(x)→F(y)))　ト⊥　（１２）　（８）、（１１）より
K ト ¬∀y (R(y) ∧ (∀xR(x)→F(y)))　（１３）　

>>66
マツシン痰、もう1億円は用意できた？

>>46
>ウソはいけないな。ウソは。
>>47
>>>21はうっかり戸田山の「論理学をつくる」の
>タブロー法の推論規則を使ってしまった、に
>１億円（ｗ

もってけドロボー（ｗ
　　＿＿＿＿＿＿
　／いちおくえん／｜
／＿＿＿＿＿／　｜
｜　　　　　　　｜　｜
｜＿＿＿＿＿｜／

ウソつきマツシン痰（・∀・）ﾆﾔﾆﾔ

なんでもかんでもマツシンだな（・∀・）ﾆﾔﾆﾔ

http://www.agemasukudasai.com/bloom/

ところで
∀y(R(y) ∧ (∀xR(x)→F(y)))
の代わりに
∀ｙ(∀xR(x)→F(y))
でやってみても、
Kト¬∀xR(x)
までは求まるね。

でも、それだけだと、単に
「K'では∀ｙ(∀xR(x)→F(y))が証明できない」
っていうだけで、否定が証明できるところまではいかない。
Kでω矛盾するというためには、やっぱ、R(y)をつけないとダメか。

ﾌｰﾝ

マツシンちゃんじゃないと思うんだがなあ。

>>7のいう「後半部分」が>>17の（２）なのね。
で、>>21の証明はつまり
∀xR(x)→¬∀xF(x)　ト　¬∀y(R(y) ∧ (∀xR(x)→F(y)))
ってわけだね。

この証明のタネは>>16にある通り
「(∀n)[K ト G(n)] かつ K ト ¬∀yG(y)　なる
　 G(y)として、R(y)∧(∀xR(x)→F(y)) を考える」
ところで、それが分かれば（２）は単純な述語論理の
証明問題だったんだね。
（述語論理の自動証明器SPASS
　http://spass.mpi-sb.mpg.de/
　にかけたらすぐ証明したよ）

>>77
＞（述語論理の自動証明器SPASS

結局、一座の述語しか出てこない一階の述語論理の計算でしかないから
機会にとってはお手のものってところだよね。絶対止まるからね。

Hilbert/Lukasiewiczの次は一座か。

>>79
また基地外が「そんな言葉はない」とか暴れるかもな（爆笑

すいません、今苦しいので一億円いただきたいのですがまだですか？
>>70 これだとちょっとつかえないんれすが？

百年ほどお待ちください（ｗ

∧＿∧　 >81 チョコでも食べませんか…？　
　（ ´･ω･)　
　（つ■と）　
　 と＿）＿）■■■■■■■■■■■■■■■■■■■■■■■■

>>79=>>39

さては前原の本を読んだことがないな。
前原はこの本で論理にLukasiewiczの公理系を
使ってるんだよ。
ま、漏れもなんでこんなものわざわざ使うのか
気が知れないと思うけどね。

>>84
厨な質問ですまないが，前原の本のはしがきに
「型の理論の体系を採用した．」
と書かれているように記憶している．
前原本の型の理論＝ウカシェヴィチの公理系なの？

>>85
型とかいう以前の話

第２章　命題論理　の
公理�U．１ Ａ→（Ｂ→Ａ）
公理�U．２　[Ａ→（Ｂ→Ｃ）]→[（Ａ→Ｂ）→（Ａ→Ｃ）]
と、
推論規則１　Ａ、Ａ→Ｂ　ならば　Ｂ
がLukasiewiczの公理系だってこと。

本のはしがきのその先のほうには
「第２章の全体の構成は、本質的には、昭和初期の岩波講座’数学’に
　故黒田成勝先生の書かれた「数学基礎論」における命題論理の部分に
　従っており、わが国の数学基礎論の大先輩である黒田先生のお仕事の
　形骸をここに残すことになった」
とある。

つまり、黒田の本がLukasiewiczの公理系を使ってたってことだな。

>>84
もともと原論文がPMを採用してるんだから、Hilbert スタイル採用するのは
自然な流れですがなにか。

っていうか、日本の教科書でも最近は Hilbert スタイル採用してるやつのが
多くないか？

>>87

命題論理や述語論理のスタイルは、
不完全性定理とは全く別の問題。

したがって"Hilbertスタイル"に
こだわる理由は何一つない。

何か不満があるかい？

>>87

PMを用いる利点は、記述の点で一階の算術より便利だから。

ところでHofstadterによると、Marvin Minskyは
「GoedelはLISPを思いつくべきだった。
　そうすれば、もっと簡単に不完全性定理を
　証明できたのに。」
と冗談をいったそうな。

>>89

これに対してHofstadterが考えた３つの答
（メタマジック・ゲームより）

１．Goedelの目的はPMの破壊にあるのだから
　　LISPを思いついたって仕方ない
２．Goedelの方法は、言及できる能力以上に
　　高級な符号化を使ってないから価値がある。
３．いや、Goedelは実質的にLISPを発明したんですよ。
　　Goedelの関数Bewの46個の関数定義こそ
　　世界最初の「プログラム」なんです。

>>88
不満は大有りですが（爆笑）読まないで書いてるだろ？

ゲーデルのもともとの論文がPMの体系を対象としていて、かつ前原本は
基本的にはゲーデルのもともとの方法を忠実にトレースするという方針で
書かれてるんだから、Gentzen style ではなく、Hilbert style を
とるのは当たり前のはなしだろ。こだわる理由は前原先生には思いっきり
あるとおもうが？

で、命題論理の公理として simplification + Fregean syllogismを
採用したのは、普通の選択だろ。Kleene をはじめとして Hilbert style で
書かれたテキストでほかの公理採用したテキストのほうが珍しいですが？

それとも君は PM のもともとの命題論理の公理系がお好みですか？
あれはかなりめんどいですが？

スマリヤンのテキストも論理部分は同じ公理系だったような気が。

>>85
ラッセルのパラドックスを回避するために考案された算術をその上で
展開できるパワーを持ったシステムのことだよ。

詳しくは、

Russell, Bertrand, 1908, "Mathematical Logic as Based on the Theory of Types

か、Principia Mathematica でもよんでくり。

前原先生がタイプ理論を採用したのは、原論文をなぞることのほかに、
当時タイプ理論やι記号について解説してるものが少なかったから
ということも理由としてあげてなかったっけ？

>>94
型理論の本がないから，というのも理由に上がっている．

で，またまた厨な質問で申し訳ないのだが，
公理1．A→(B→A)
公理2．(A→(B→C))→((A→B)→(A→C))
推論規則．MP
っていうのはヒルベルトの体系だよな．
ヒルベルトの体系＝ウカシェヴィチの体系なの？

>>91

「ゲーデルのもともとの方法を忠実にトレースする」ことが
不完全性定理を理解する唯一の方法ではないだろう。
Fortranでなければプログラムが書けないというわけではないのと同じ。

GoedelのBewの定義を根本的にいじらないなら、
命題論理の推論規則をMPだけに限るしかないが
それは消極的な態度である。

>>95
Hilbert-Ackermannの体系というのは、
PMの命題論理の公理系を改良した
以下のもの。
Goedelは論文ではこれを使っている。

Ｐ∨Ｐ→Ｐ
Ｐ→Ｐ∨Ｑ
Ｐ∨Ｑ→Ｑ∨Ｐ
（Ｐ→Ｑ）→（Ｒ∨Ｐ→Ｒ∨Ｑ）

>>96は>>91の

> 前原本は
> 基本的にはゲーデルのもともとの方法を忠実にトレースするという方針で
> 書かれてるんだから

とスレタイの

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

とを交互に256回読み直した後
生命保険に入り回線で首を吊って1億円捻出するのがいいと思う

>>91=>>21は基地外

>>98
いうに事欠いて（笑）さっさと1億円用意しろよ。

>>99
>>39=>>47=>>79=>>98の逃亡によりこのスレ終了

　　　　　∧∧　　ミ　＿　ドスッ
　　　　 (　 　;)　┌─┴┴─┐
　　　　/'　　　つ　終　 了 │
　　〜′　/´　└─┬┬─┘
　　　∪ ∪　 　 　　││　_ε３

>>82とかも、なにが"（ｗ"なのかぜんぜん理解できないんですが、
こういう人のせいで論理関係のスレッドはいつも荒れるんでしょうね。

>>95
こういうタイプの公理系の記述を Hilbert スタイルっていうのです。

公理そのものは、Elements of mathematical logic、1928 とかで
ウカシェビッツが採用したもの。

まあ、スレとはあまり関係ないので、このての話題を続けるのなら
本スレに行こうね。

>>102
じゃ、スレにあった質問。

第二不完全性定理が成立するための
”自然な条件”についてだけど
これって証明可能性述語の条件
１）　TトA　ならば　TトP(A)
２）　TトP(A→B)→(P(A)→P(B))
３）　TトP(A)→P(P(A))
とは違うの？

あげておく

むむむ，自分の書き込み読み返すとただの煽り厨ですな>>101
スレの流れを止めてしまったようです．ごめんなさい．

いいんじゃない。
何も言うことがないなら
黙っているのが一番

個人的には入門者には田中一之の方を読んで欲しい

>>107

残念ながら現在品切れだ。

>>105
いや、やふーがアク禁だったんで、書き込めなかっただけだし。

ＹＢＢ規制解除！らしいです。

よいしょ

よいしょ

ふぅ、これでレス数が一緒になった

チャンコは氏ねよ

おまえら、古いな（藁

>>103
それでいいんだと思うが。

あげ

turn style age

|-

こっちの方が良くない？

|=

応用。
下らないカキコでスマソ。

├

>>1
バカモン！

前原の｢数学基礎論入門｣に限らず、｢数学基礎論なる、学問そのもの｣が
｢蒙昧暗愚なる、２０世紀的論理学」の産物であり、故に
遠からぬ将来、滅ぼされる運命にあるってことが分からんのか！

# 貴様に多少なりとも良識あらば、貴様の立てた、この糞スレッドの
削除依頼を *即刻* 出して参れ！

>>122は、前原の「数学基礎論入門」を読んだが
理解できず、その理由を２０世紀論理学のせいに
した、蒙昧暗愚なる御仁

貴殿に多少なりとも良識あらば、貴殿の作った
以下のホームページを即刻削除されたし。
http://www.apionet.or.jp/~eurms/Ronri_Kaikaku.html

（＾＾）

下がりすぎだｙｏ！

>>126

タワケ！

かような｢２０世紀的蒙昧に基づく糞スレッド｣に上げる価値など、そもそも在りはせぬワ。

>>108

図書館で読めます。

>>122

> 前原の｢数学基礎論入門｣

今日買てきます

買てきた
3900円だつた

¬A→（A→B）
が分からんのです。
誰か教えてくださいな。

矛盾律

何ページでつか？
また、どういう風に分からないのか分からない。

とりあえず、

B→（A→B）

これはトートロジーでつ。

なぜなら、その論理式がトートロジーであるためには、
Bが偽、或いは（A→B）が真であればよい。（→の定義より。）
（A→B）が真であるためには、A が偽、或いはBが真であればよい。
ところで、Bが真であれば、（A→B）は真。故に、B→（A→B）も真。
したがつて、B→（A→B）はトートロジーでつ。

＜→の定義＞
A 　B　A→B
ｔ　　ｔ　 　ｔ
ｔ　　ｆ 　　ｆ
ｆ　　ｔ 　　ｔ
ｆ　　ｆ 　　ｔ

あとは、

B→（A→B）

ここから（A→B）の対偶を取れば、

B→（¬B→¬A）

AにB 、Bに¬A を代入すれば、

¬A→（A→B）

となりまつ。

>>133
２０ページです。
基礎論ははじめてなのでよく分からないのです。。。
＜→の定義＞は一応知ってますが、
ここでは（２０ページでは）使ってはいけませんよね？？

証明が分からないということでつか？
ということであれば、p.20の証明では、
まずp.13にある推論規則2.1を使っています。
AとBは任意の論理式でつから、
Aに¬A、Bに¬Bを代入することができまつ。
するとp.20の証明図の二段目までが出来るでしょう。

>>133
>なぜなら、その論理式がトートロジーであるためには、

「トートロジー」じゃなくて「真」でした。

>>136
そうでつ。証明できないのです。
確かに、「¬Aが証明できる」ならば「（A→B）が証明できる」のは分かるのですが、
これと、「仮定¬Aのもとで（A→B）が証明できる」ことは違うと思うのですが。
いかがでしょうか？？
（初めは同じものと思ってたのですが、よく考えてみると納得いかんのです。）

p.13の
『「A→Bという論理式が証明できる」ことがすでにわかっているものとすると、
推論規則1により、「Aが証明できればBも証明できる」ということがわかる。』

これと

p.15の
『「論理式C→Aが証明できる」ことを「仮定Cのもとで論理式Aが証明できる」ともいう。』

これを合わせて考えれば、

『「仮定Aのもとで論理式Bが証明できる」ことがすでにわかっているものとすると、
推論規則1により、「Aが証明できればBも証明できる」ということがわかる。』

>>139
しかし、その逆は成り立たない、というか分かりませんよね。

すなわち、
『「Aが証明できればBも証明できる」ということがわかっているとき、
「仮定Aのもとで論理式Bが証明できる」ということが分かる』
とはいえないと思うのです。

>>140

私も書いていて同じことを思いました。
本の記述だけからでは分からないということに
なりそうでつね。（他の方々は如何思われますか？）

しかし、逆の成立は簡単に示せそうでつね。
例えばAとしてA（そのまま）、BとしてA→（A→B）を取れば、
MP（推論規則1）より、A→Bが証明できまつ。
つまり、間接的には書いてあると。

したがつて、両者は同値であると。

↑全然ダメかも。ヒルベルト流良く分からん。
どなたかに解説を希望しまつ。

「AとしてA（そのまま）、BとしてA→（A→B）を取れば、
MP（推論規則1）より、A→B」
は
「Aが証明できれば、（A→B）が証明できる」ということ
これだけではなんとも解決しませんが。。。

問題提起しておいて、自分で解決してしまったかもしれません。
自信がないので、報告します。意見ください。

公理�@　A→(B→A)を¬A→(¬B→¬A)に変形
これと推論2.3　「A→BとB→Cが証明できれば、A→Cは証明できる」
と公理�B　(¬B→¬A)→(A→B)
より
「¬A→(A→B)は証明できる」

いかがでしょう？？
ただこれがあってたとしても、
他の公式も証明法が間違ってそうなので大変だ。。。

ここはあふぉの巣窟ですか？

>>146

> 他の公式も証明法が間違ってそうなので大変だ。。。

本が間違っているという発想はやばいでしょう。
こちらが本に書いてあることを理解できていない
というだけのことだと思いまつ。

>>147

> ここはあふぉの巣窟ですか？

できれば>>140-141にコメントください。

A
―
B

から、

A→B

の間の（自分の脳内に生じている）溝は
どうやって埋まるんでつか。

>>130
私は別の本買っちゃいました。
1995円でした。

ところで、竹内外史の本はどうなの？

やっと分かりました。
かんぺきです！！

>>148
たしかに、本が間違いということはなく、
私が未熟なだけでした。。。
でも、「入門」書ですよ！？

どうもご迷惑をおかけしました。。。

> やっと分かりました。
> かんぺきです！！

どのように分かりました？

ちなみに自分は>>148に書いたような（脳内に生じている）溝を
次のような仕方で埋めました。（公理�U.1と推論規則1を使う）

A
―
B　B→A→B
――――――
A→B

>>151

カッコが抜けました。

A
―
B　B→（A→B）
―――――――
A→B

竹内外史他の「証明論入門」が欲しいが
絶版だし古本屋にもない・・・

>>151
「『Aが証明できるならばBが証明できる』ことが分かっているとき、
Aが証明できるならばA→Bも証明でき」ますね。
これは
「『Aが証明できるならばBが証明できる』ことが分かっているとき、
A→Bが証明できる」
ということとは違うと思います。

>どのように分かりました？

私が示したいのは、
「¬A→(A→B)」が証明できることでしたから、、、
>>146 間違ってますか？？
一般に
「『Aが証明できるならばBが証明できる』ことが分かっているとき、
A→Bが証明できる」
ということはないと思います。
（だから本にも載ってない！）
しかし、
「仮定Aの下で『Aが証明できるならばBが証明できる』ことが分かっているとき、
A→Bが証明できる」
んだとおもいます。。。

竹内先生の本はものによってはエラーが多いらしいので素人にはお勧めできない。

>>154
「『Aが証明できるならばBが証明できる』ことが分かっているとき、
A→Bが証明できる」

これは述語論理や様相論理では成立しない。

反例：A = F(x) 、B = ∀xF(x)
反例：A = A, B = □A

ただし、話を命題論理に限れば、成立するよ。

様相論理だと大雑把だね。S4, S5, K とかでね。

>>156
ごめん、うそうそ。命題論理でもあやしいや。すんまそん。

問題となっている命題の前件『Aが証明できるならばBが証明できる』が
真であるのは、「Bが証明できる」ときか「Aが証明できない」時である。

組み合わせを書き尽くすと、

1) Aが証明でき、Bも証明できる
2) Aが証明できないで、Bも証明できない
3) Aが証明できないで、Bは証明できる

の3種類の組み合わせになる。

問題となるのは「Aが証明できなく、Bも証明できない」時。

反例：A=原子命題 p1 B=原子命題 p2

>>154

> 「『Aが証明できるならばBが証明できる』ことが分かっているとき、
> Aが証明できるならばA→Bも証明でき」ますね。
> これは
> 「『Aが証明できるならばBが証明できる』ことが分かっているとき、
> A→Bが証明できる」
> ということとは違うと思います。

感覚的に分かります。
となると>>152の図式的表現は
上の意味でなくて下の意味ということになりそうですね。

> >>146 間違ってますか？？

それはそれで間違っていないと思います。



ただ、

「『Aが証明できるならばBが証明できる』ことが分かっているとき、
Aが証明できるならばA→Bも証明できる」

「仮定Aのもとで『Aが証明できるならばBが証明できる』ことが
分かっているとき、 A→Bが証明できる」

これらは感覚的には納得できるのですが、
本のどのあたりの記述から導けるのでしょうか。

>>160の訂正

（誤）上の意味でなくて下の意味ということになりそうですね。
（正）下の意味でなくて上の意味ということになりそうでつね。

>>160
「仮定Aのもとで『Aが証明できるならばBが証明できる』ことが
分かっているとき、」
これは、
「『A→Aが証明できるときA→Bが証明できる』ことが分かっているとき、」
と同じ意味（これは本に載ってるはず。）で、
これと、
「仮定AのもとでAが証明できる」
をくみあわせると、
「A→Bが証明できる」
と考えました。

>>146
＞公理�@　A→(B→A)を¬A→(¬B→¬A)に変形

これは言い方がおかしい。それは変形ではなく、¬A→(¬B→¬A)も
公理である。

p.10の最後からp.11 の冒頭までを読むこと。

>>163
なにぶん初心者なもので、、、

>>162
了解しました

>>150

前原の本がそうであるとは言わないが
この世には「入門」と題されているに
も拘わらず全然入門書とは言えないよ
うな本が沢山あるので注意されたし

>>86

Lukasiewiczによる公理系ということで
あれば公理が一つ足りない

>>167
確かに。否定に関する公理図式がついて、全部で三つだからね。

手元に資料がないので、オリジナルがなんだったか確実なことは
いえないんだが、対偶か二重否定除去のどちらかだったんじゃな
いかな。

（＾＾）

>>168
対偶でつ。それは前原の本にも書いてあります。
（ただし、最初の二つとは離れた場所に書いてあります。）

　　 ∧＿∧
　　（　　＾＾ ）＜ ぬるぽ（＾＾）

「.....数学基礎論は"ロジック"とひとまとめ。
ロジックなんてのはもう純粋数学か不純な数学かといったものではなく、
そもそも数学ではない！
そういうものはデキの悪い学生か、
歳を取って頭が悪くなった時に趣味としてやるものであって、
将来のある若いモンがそういう事に手を出しちゃいかん.....」
（『純粋数学至上主義』より）
http://laplace.theory.cs.ritsumei.ac.jp/~takayama/MathEssays/puremath.html

そもそも、将来のある若いモンは手を出さない。

logicとset theoryはちがうな。

後者は純粋に数学だろう。ちなみにオツムのデキは良くないとダメだと思う。
（とはいえ、そういうオツムのデキが有意義かどうかは別の問題。
　いっとくけど、この批判は、代数幾何や整数論にも当てはまること）

前者については数学のセンスとは別のセンスが必要。
例えばプログラマ的センスとか、哲学的センスとか

first order logicの重要な結果は、
Goedelのcompleteness theoremに尽きる。
彼がこの結果を出したとき23だったと思うが、
この後>>172でいう意味の数学について、
何の結果も出していないので「出来が悪い」
と考えることもできる。

しかし、Goedelは上の結果と、incompleteness
theoremで、歴史に名を残したので、logicに
手を出したら将来がないとはいえないと思う。
（ただ、Goedelの後では、大した問題は残ってないので、
一度限りだということは言えるかもしれない）

>>175
帰納的関数やアルゴリズムの理論も含めた広い意味でのlogicなら整数論に応用されてる。

いや、帰納的関数やアルゴリズムの理論は、
計算comptationにかかわるものであって、
普通"logic"とは言わないだろ。

その意味では、>>174でlogicとset theoryだけを
挙げたのは不十分だったな。

>>172
なんてじじいの自虐的な昔話のたわ言にマジレスする必要はないと思うが。

>>177
数学的に意味のあるのは logic でないという定義ならそうだろうね（w

スレ違いだから、本スレでね？

>>179

そんなこといってないじゃん。頭ｵｶｼｲんじゃない？

logicといったとき連想するのは、例えば
modal logicとかintuitionistic logicとか
linear logicとかなんだよ。

それって帰納的関数とかアルゴリズムの理論とか
とはちがうだろ？どうよ。同じとか言い張る？

> logicといったとき連想するのは、例えば
> modal logicとかintuitionistic logicとか
> linear logicとかなんだよ。

それは可算名詞の``logic''じゃん。

不可算名詞の``logic''ならmathematical logicを
入れてもいいんじゃないの？
少なくとも帰納的関数は入るよ。

＞それは可算名詞の"logic"じゃん。

ﾊｧ？なに知ったかぶりなこといってんの？（笑）

＞不可算名詞の"logic"ならmathematical logicを
＞入れてもいいんじゃないの？

だからｵﾏｴのいうmathematical logicって何だよ。（笑）

＞少なくとも帰納的関数は入るよ。

何でそう言い張るのか分からん。
たまたま見た基礎論の本に帰納的関数という言葉があったから
ロジックだと言い張ってるんなら、ｵﾏｴの判断は全く根拠のない
思い込みだから、冷水百回浴びて出直せ（笑

いっとくけど、ロジックと帰納的関数の理論が無関係とか
いってるんじゃないぞ。トポロジーで微分をつかうからって
微分自体をトポロジーの概念とは言わないだろ。

「言い張る」って、俺は181が初めての書き込み
だよ・・・。

＞logicといったとき連想するのは、例えば
＞modal logicとかintuitionistic logicとか
＞linear logicとかなんだよ。

これこそ全く根拠のない妄想だろ。

>>182
> だからｵﾏｴのいうmathematical logicって何だよ。（笑）

``mathematical logic''という言葉を知らなかったのかな・・・。
↓みたいに``Mathematical Logic''という題の教科書もあるから
勉強してよ。5章がrecursionで、6章がGodel's theoremsだから。
まあそれでも、G\"odel's theoremsはlogicだけどrecursionは
logicじゃない、と言い張るのかもしれないね・・・。

http://www.oup.co.uk/isbn/0-19-850050-5
Mathematical Logic: A Course with Exercises - Part 2: Recursion Theory, Godel's Theorems, Set Theory, Model Theory

>>181って「”」の出し方知らないのかな？
２のキーボードの上にこの文字が書いてあるだろ。
シフトキーを押しながら２のキーを押すんだよ。
こんな初歩的なこと知らない奴って珍しい（笑

そんなことより、"Mathematical Logic"という題の
本を挙げるならまずSchoenfieldだろ。
http://www.aslonline.org/books-other.html
これには、recursion theoryもincompleteness theoremも
consistencyも、set theoryもあるよ。
何をいいたいのか分かるよね。つまり、題名と本の目次だけで
判断する貴様はｳﾞｧｶってことさ（ｗ

＞G\"odel's theoremsはlogicだけど

それは、どうかな？（ニヤニヤ）

186 名前： 181
＞``mathematical logic''という言葉を知らなかったのかな・・・。
＞↓みたいに``Mathematical Logic''という題の教科書もあるから

＞まあそれでも、G\"odel's theoremsはlogicだけどrecursionは

187
＞>>181って「”」の出し方知らないのかな？
＞２のキーボードの上にこの文字が書いてあるだろ。
＞シフトキーを押しながら２のキーを押すんだよ。
＞こんな初歩的なこと知らない奴って珍しい（笑

晒しage

http://homepage.mac.com/hitomi18/

>>188

晒されてるのは186だろうな。

穿った見方をすれば186でG\"odelと打ってるのに
187が「"の出し方知らないんんじゃない？」という
のはマヌケだという指摘にも取れるが、それなら
それで、186が"について本来の使い方をせずに
わざわざウムラウトのためだけに"を使うという
おｳﾞｧｶなことをやってる事実が際立つので、
どっちみち186がより惨めになるだけのこと。
もしかして186は"がウムラウトだとマジで信じてる
のかもしれん（ﾌﾟﾌﾟ

ところで、ウムラウトとトレマはちがう。
トレマの典型的な使用例は、naiveという
単語のiの上に用いるものである。
その昔流行ったナウシカの綴りの最後のaに
つくのはトレマであって、ウムラウトではない。
こう言ったことは、まともな教養などない
ヲタクどもに一泡吹かせるにはちょうどイイ
ツッコミなのだが、残念なことに一度も
披露するチャンスがない（笑

何を藁われているのかまだ気付かないおｳﾞｧｶもう一度晒しage

ナウシカはギリシャ神話に出てくる姫君の名前で
正しくはナウシカアと発音するらしい。
どうせ書くならΝΑΥΣΙΚΑΑとギリシャ文字で
書くのがペダンティックというものである。
（少なくともﾊﾞｶﾓﾝをロシア文字で書くよりは
　よほどﾏｼである）

>>192

笑われてるのが自分だと気づかないおｳﾞｧｶ
自ら晒しage。まるでfj.sci.mathの御大そっくり（笑

333 名前： １３２人目の素数さん 投稿日： 03/04/25 17:17
エムシラは数学的に反論できなくなると、とにかく相手を
マツシンだということにして、自分の自尊心を守ろうとす
るんですよね。

エムシラにとって、「マツシン」は、自分が追い詰められ
た時に、最後に逃げ込む脳内の安全地帯。「マツシン」と
いう文字列が出てきたら、それは「もう許して」のサイン。

334 名前： １３２人目の素数さん 投稿日： 03/04/25 17:21
マツシンがエムシラを持ち出すのも「もう許して」のサインですものね。

>>187
J. Symbolic LogicでもUniversal Diophantine Equationに関する論文は存在しますが何か？
少なくともJ. Number Theoryよりは相応しい雑誌だと思いますが何か？


っていうか俺が一連の論争のもとになった>>176書いたんだけど、
もともと俺が念頭においてたのは>>172の｢数学基礎論は"ロジック"とひとまとめ｣云々という文章なんだよ。で、
そういう意味での"ロジック"ならそれなりに純粋数学で役に立ってるよと言いたかったの。

晒しsage

>>196
雑誌の名前だけで判断するのはｳﾞｧｶ。

ところで、貴様はMaclaneが
「帰納的関数論なんて数学的には全く不毛な分野だ」
と批判したことを知らないようだな。

そもそも漏れは>>172の｢数学基礎論は"ロジック"とひとまとめ｣という
主張は間違っているといってるわけだ。だから>>196も>>172と同罪

おまいら皆、天才。

っていうかさあ、てめえら、えんえんスレ違いの話題を引っ張ってんじゃんーよ。
かすが。

そういうダベリをしたければ本スレに行けって言ってんだ。

本スレへ。
http://science.2ch.net/test/read.cgi/math/1043049229/

二階論理の練習問題がどうしても解けません。
問題が間違っているのではないかとも思うのですが・・・。
だれか教えてください。
＜問題＞
∀X∀z [ ∀y { Ryz → ( ∀x ( Rxy → Xx ) → Xy ) }
→ ∀y { Ryz → Xy } ]
ならば
∀x∀y∀z [ ( Rxy and Ryz ) → Rxz ]
であることを示せ。
■

>>203
ちょっとやってみたけど、解けないなあ。

ところでその問題のタネは、もしかしたら様相論理の
クリプキセマンティクスからとってるかもしれない。
別の本にこんな問題があった
∀xRxx≡∀X∀x{∀y[Rxy→Xy]→Xx}　(reflexive)
∀x∀y[Rxy→Ryx]≡∀X∀x{∃y[Rxy and ∀z(Ryz→Xz)]→Xx}　(symmetry)
∀x∀y∀z[(Rxy and Ryz)→Rxz]
≡∀X∀x{∀y[Rxy→Xy]→∀y∀z[(Rxy and Ryz)→Xz]}　(transitivity)

おまいらできれば出典を明示してくれ・・

>>204
>ちょっとやってみたけど、解けないなあ。
早速レスポンスありがとう。そうでしょう？

>∀xRxx≡∀X∀x{∀y[Rxy→Xy]→Xx}　(reflexive)
これは、X=入t.Rxt　とおけば<==はいえますね。
>∀x∀y[Rxy→Ryx]≡∀X∀x{∃y[Rxy and ∀z(Ryz→Xz)]→Xx}　(symmetry)
これは、X=入t.Ryt とおく。
>∀x∀y∀z[(Rxy and Ryz)→Rxz]
≡∀X∀x{∀y[Rxy→Xy]→∀y∀z[(Rxy and Ryz)→Xz]}　(transitivity)
これも、X=入t.Rxt とおく。

>>205
203 "Computability and Logic"

>>205
204はMelvin Fittingの"Types,Tableaus,and Goedel's God"

>>206
ええ、最初の例題は確かにX=λt.Rxtです。

>>203
俺の手元にある第４版だと含意の向きが逆。

二番目の式から一番目の式を導き出す問題。

>>208
>二番目の式から一番目の式を導き出す問題。
だけど二番目の式から一番目の式は、無から有をうむようなもので出るわけないし・・・。

>>203
この問題は、多分正しいよ。
今気づいたけど、これって、様相論理でLoebの公理
□(□Ａ→Ａ）→□Ａ
を設定した場合、そのクリプキモデルが
Transitiveになるっていう言明だから。

>>208
上が正しいとすると逆向きってことはない。
Loebの公理を満足する様相論理はirreflexiveだから。
（Transitiveだけだとreflexiveであってもよい）

こう書き直すと多少分かりやすいかも
---
∀X∀x [ ∀y { Rxy → ( ∀z ( Ryz → Xz ) → Xy ) }
→ ∀y { Rxy → Xy } ]
ならば
∀x∀y∀z [ ( Rxy and Ryz ) → Rxz ]

おまいら、もちろんできればでいいんだが、
ページの明示、いくつかエディションがある場合は
それの明示、を頼む・・
その方がスムーズに行くかもしれない。

"Computability and Logic" Third edition
18 Second-order logic p.206
Exercise 18.6

Show that ∀x∀y∀z (xRy&yRz → xRz) follows from
∀X∀z[∀y(yRz → [∀x(xRy → Xx) → Xy)]) → ∀y(Ryz → Xy)].

あれ？
"Computability and Logic" Fourth edition
22 Second-Order Logic p.285
Problems 22.5
Show that (a) implies (b):
(a) ∀x∀y∀z[(Rxy & Ryz) → Rxz]
(b) ∀X∀z[∀y(Ryz → [∀x(Rxy → Xx) → Xy]) → ∀y(Ryz → Xy)]

>>213
>>208,210の問題ですね。
おそらく第4版のは誤植でしょう。

おまえら、程度低いな（ｗ

オマエガナー

>>216
おまえが一番程度低そうだな（ｗ

愚か者よ、質問スレで215-217のような事言われても困る。

おまえら、程度低いな。 やはり（ｗ

一番程度が低いのは自己に甘え他人をせせら笑う事さ。
人間の書き込みである以上、それよりは程度が上であって欲しい物だが…
219とかもあるし、なかなか難しい物だねぇ。

>>220
キミ馬鹿かい？ここは２ちゃんだよ？

つまり、荒らしは放置

>>218,>>220
おい、>>216はomaeのカキコと同じ意味だぞ。

みなさんは"Computability and Logic"を
何のために読んでいるのでしょうか？

"Computability and Logic"は誤植が多いらしい

てか、誤植の全く無い本は珍しい。

そりゃそうだけど、多いとか少ないとかは言えるでしょう…
正誤表ハケーンしたけど…

>>213, >>214
そこって正誤表には載ってないんだけど…

正誤表はこちら
http://www.princeton.edu/~jburgess/addenda.htm

で、203の問題、当人でも他人でもいいけど、誰か解けたかい？

それにしても前原スレで何故に・・・

━―━―━―━―━―━―━―━―━[JR山崎駅（＾＾）]━―━―━―━―━―━―━―━―━―

ほしゅったらageろ！

解けてるけど

初心者です．
むかし古典論理の完全性くらいまで勉強したのですが，最近
不完全性定理を勉強したくなったので質問させていただきます．

前原さんの本と「数学基礎論講義」（田中ほか，日本評論社）
との違い，特色はどういったところでしょうか？

また他にも入門に良い本がありましたら教えてください．

オンライン読書会について
名前： １３２人目の素数さん
E-mail：
内容：
オンライン読書会、或いはネット勉強会について
その方法や可能性を考えるスレ！

というのを立てようと思ったが、立てられなかったぞ。
というわけで、誰か頼む。

スレ立て代行依頼所　-弐-
http://ex.2ch.net/test/read.cgi/entrance/1051680440/
ここで他の板のスレッドを立てる事による見返りを貰うべし。

　　　 　∧＿∧
ﾋﾟｭ.ｰ　(　　＾＾ ） ＜これからも僕を応援して下さいね（＾＾）。
　　＝〔~∪￣￣〕
　　＝ ◎――◎ 　　　　　　　　　　　　　　　　　　　　　山崎渉

不完全性定理を完全に理解することは可能なんですか！

「完全な理解」がどんなものかによる。

「完全な理解」の定義が不完全だったら、どーなるほい？

しょうもない言葉遊びしてないで勉強汁！

ＭＲＫで recursive function が回帰関数と訳されていた。
これってどーよ？

>>243
最近じゃあ珍しい訳語の選び方けど、まあ、いいんじゃないの？
別に、間違いじゃないし。

どんな訳語がベストでしょうか。通例では「帰納的関数」だと
思いますが、"recursive"は再帰という意味で英語ではこれを
帰納（induction）と区別するらしいから「再帰的関数」かなぁ？

今日からこの本を読みます。

今日は1章（p.12まで）を読みますた。

今日は読めませんですた。
平日に電車の中で読むしかない・・・

この人放送大学でラジオの授業すごいわかった。
秋山よりいい！相対論の本も面白い
でもおなくなりになったんだよね

えらく退屈なので、他の本を手にしてしまいますた。
でも、この本も読み通します。

>>245
最近は「再帰的関数」がメジャーと思われ。「回帰関数」は統計のあれと
かぶるんでマイナーな訳語だよね。

基礎論本スレの２ぐらいで「回帰関数」なんてことばはないとか、
大暴れした半可通がいるぐらいマイナー（笑

>>251
ぱーと２でなくてぱーと１ですた。

あの時暴れてたやつ、恥ずかしくないか（笑）？

たーん

p.20の問というのは、
定理2.5 いかなる仮定のもとでも公理は証明できる
において、空の仮定の場合を考えれば良い、って、
これだけでいいんでしょうか。

>>255
2.5 の証明を見よ。君の言う内容が答えなら、2.5を使うことすら
不要ではないでしょか？

>>254 だ。すまん。

>>254 よ。問いの前の段落をよく読め。そうすればわかるから。

Fregean Syllogism と simplification で「含意」の性質をほぼ規定できる
という基礎知識の確認になっているんだよ、ここは。

II-1 の証明
1: A,B からAが証明できる（2.6)
2: A から B →A が証明できる(1, 2.7)
3: 仮定なしで A →(B →A ) が証明できる(2, 2.7)

こんな感じ？しかし、たしかにわかりにくいわな、先生の書き方は。

あはいないのかにょ？

どうも最近ピンチ状態の＿あ＿です。
勿論、まったく進んでいません。

>>255,>>256
ご教示どうもありがとうございます。
やっぱりダメなんですね・・・
該当箇所、あとで読み返してみます。

山場通り越したらまた読み始めよう・・・

　__∧＿∧_
　|（　　＾＾ ）|　＜寝るぽ（＾＾）
　|＼⌒⌒⌒＼
　＼ |⌒⌒⌒~|　　　　　　　　　山崎渉
　　 ~￣￣￣￣

5

3

だ　れ　も　い　な　い　の　か　？

シグマトートロジー

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