数学基礎論の質問スレッド　その３

立てます。

　今だ！2ｹﾞｯﾄｫｵ
￣￣￣￣￣∨￣￣￣　　　　　　　(´´
　　　　 ∧∧　　　)　　　　　　(´⌒(´
　　⊂（ﾟДﾟ⊂⌒｀つ≡≡≡(´⌒;;;≡≡≡
　　　　　　 ￣￣　 (´⌒(´⌒;;
　　　　　　ｽﾞｻﾞｰｰｰｰｰｯ

前スレ>>999

濃度の比較可能定理⇔AC

いいことを教えてやろう。
こんなスレを立ててくれたんだからな。
スペイン語で数字の「５」のことを「Cinco」って言うんだ。
OK、あぁ、わかってる。
お前のことだからとりあえずチンコを連想しただろ？
読み方をカタカナで表すとシンコって感じなんだが、
まぁ、今はそんなことどうだっていいんだ。
いいか、よく聞け。
これからは２ゲットの時代じゃなく、５に Cinco って書くことが流行る。
そう、５に合わせてただ Cinco とだけ書くんだ。
読み方のわからない厨房はチンコを連想するだろ？
まさにそれが狙いなんだ。
頭のいいお前には「５」ってことがわかるが、厨房には「チンコ」だ。
わかるか？それがお前と厨房の差なんだ。
これからはそうやって５をゲットすることでお前のすごさを見せ付けてほしい。

↓さぁ！

ちんこ

いつつ

べつに基礎論って言うけど基礎でもなんでもないくせに

とりあえず前スレから

116 名前：１３２人目の素数さん[sage] 投稿日：2006/05/12(金) 12:15:28
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野で、
非古典論理、証明論、構成的数学、モデル論や意味論、集合論、計算論
などの分野群の総称です
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです）

応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何（Hrushovskらiによる研究）などを含み、多岐にわたります
（cf. 数学セミナー98年6月号、「数学基礎論の学び方」）
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります
他のスレで御質問なさるようにお願いします

>>8
前スレ958で修正されてたバージョンの方が良かったのでは

>>7は多分ツンデレ

前スレ
数学基礎論の質問スレッド　その２
http://science5.2ch.net/test/read.cgi/math/1143943264/
数学基礎論の質問スレッド
http://science4.2ch.net/test/read.cgi/math/1097659610/

建築物基礎論

PrawitzのNatural Deduction買ってきたお（　^ω^）
これから読むお（　^ω^）

>>13
一緒に読も

「数学基礎論」は誰が命名したの？

数学建築家が

英語だと「数学基礎論」じゃなくてFoundations of mathematics。
独語ではGrundlagen der Mathematikで、同名のHilbertとBernaysによる著書が
1939年に出版されていて、日本語の抄訳がSpringerから「数学の基礎」の題名で出ている。

いつ誰が分野名として「Grundlagen der Mathematik」という言葉を使ったのが最初か、
誰が「数学基礎論」と命名したのかはちょっと謎。
上のHilbert/Bernaysが起源となっている可能性も高いと思うけど、
きちんと調べて見ないと自信持って答えられないんじゃないかな。

「キソロン」みたいな語感は日本に特有だと思う。
英語名だともっと「数学の基礎（付け）」って感じじゃないかな。
分野名としても使われてる言葉だとは思うけど。

「現代思想」臨時増刊の渕野先生の記事ﾜﾛﾀ

基礎論と位相幾何ってあんまり接点ないですかね？

あるよ。基本群とか。

>>20
具体的に論文とかありますかね

今出せないけどいくらでもあるから探してみたら？

四次元多様体が位相同型で分類不可能であることの証明にそれっぽいことを使っていたかも。

あまり接点はないよ

>>22-24
ありがとうございます。さがしてみます

どちらかというとトポロジーそのものよりも組み合わせ群論とか幾何学的群論とかで関係するといった感じかな。

Jech って何て読むんですか？

いえっく？

いぇっち　でしょ！！

定義式の質問です。

ある物体oに曜日の設定を１つしたい場合

week(o) = {mon, tue, wen, thu, fri, sat, sun}

とすると７つとも設定すると言う意味でしょうか？
∨などを曜日の略記の間に挟んだりしなければならないのですか？

宜しくお願いします。

何だそりゃ

>>31
week関数に曜日を設定する定義式の書き方です。
weekは・・・ああー自決しました。頭悪かったです。
失礼しました。

(^ω^；)

基礎論のスレで基礎論と全然無関係の質問して
あげくに首つったか腹掻っ捌いたか知らんが自決とは……

何、いまどきの日本人ってこんなに低レベルなんだっけ？

基礎論で、ゲーデル達の完全性／不完全性定理以降、それに匹敵するくらい
重要かつ興味深い結果って何か出てるんですか？

人によって興味とか違うからなあ

むしろ不完全性定理が大して興味深くない

>>35
Lowenheim-Skolemの定理（実数論の可算モデルを作ったり出来る）とか、
証明論ならcut除去定理とか、集合論を含めるならCohenのforcingとか。
それにプログラミングが好きならCurry-Howardとかも興味深いだろうし
さらに人によっては自然数論とか「解析」の無矛盾性証明が興味深くて重要かもしれないし。

>>36>>37にだいたい同意。
不完全性定理のインパクトの強さは人による。

完全性定理に匹敵する結果が無いって事はないんじゃないかなあ。

巨大集合にかんする話や計算可能実数とか順序極小理論とか計算量に関する話とか。
証明論だと巨大基数類似可算順序数を利用した数学の無矛盾性プログラムなんてのもある。

>>35が予想あるいは期待していた答は「ない」であったという方に
病院にいる花京院の魂を賭けるぜ

パッと見で>>40に花右京メイド隊と書かれているように空目しました。

>>38
人によって違うのはそうだけど、基礎論に与えた影響という意味で重要性を測るとしたら、
不完全性定理に比べたら、cut除去定理とか自然数論の無矛盾性とかかなり見劣りするように思う。

「どんな命題も真か偽かどちらかなんだから証明か反証ができるはず」と素朴に思ってる人には不完全性定理は驚異的。
だけど「証明や反証できるのはラッキーな場合だけで、いつもそんなにうまくいくはずがない」と思ってる人とか、更には「そもそも命題が真か偽かどちらかだという考えがおかしい。」という直観主義者にとっては不完全性定理なんて「ふうん。当たり前じゃん」で終わり。

「当たり前じゃん」と思う問題でも、「そんなことどうやって証明すんだよ」っていう類のものであれば、
やっぱり感嘆の対象になるでしょう。不完全性定理はそういう結果だと思う。
あんな証明方法思いつくところがすごい。

公理系の強弱を測るモノサシができたのはよかった

＞「証明や反証できるのはラッキーな場合だけで、いつもそんなにうまくいくはずがない」
こういう常識的感覚を生んだのが不完全性定理だから
ちょっとアレだけどね。

>>42
それは証明論の基礎論での位置をどのくらい重要だと評価するかの問題が大きいと思う

突然ですが、記号論理学でいう“話の世界”と確率でいう“場合”は同じだと思いませんか？

どうしても解けなくて困ってます。

abcde-fghi=33333
abcdefghiは1から9までのいずれかの数字が入り。同じ数字は使えない。

よろしくお願いします

基礎
質問

というキーワードが含まれているからだなｗ

abcde-fghi=33333=3 mod 10
=33 mod 100
=333 mod 1000
=3333 mod 10000
=33333 mod 100000

数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。

（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。

http://blog.livedoor.jp/dankogai/archives/50764943.html
＞ヒルベルトの「幾何学基礎論」は、そのまま中学の教科書に使えるのではないかというぐらい平易で、
＞「本物に教えてもらう」快感を「ふつうの人」でも存分に味わうことができる。

↑こういうことを言う人のブログが日本で9番目に多く読まれてるらしいです（・・

そう書いておけばamazonのアフィリエイト収入が期待できるからだろう

ああdankogaiかｗ
おとなしくスクリプトでも書いてりゃいいのに

Azriel Levy のBasic Set Theory ではどのような内容のことが
扱われているのでしょうか。amazon.comのページを見る限り、
Boole代数、無限組み合わせ論や巨大基数について触れられてるのは分かるのですけど、
例えば強制法などについては載っているのでしょうか。

友隣社やマテマティカなどにも置いてないようで、ちょっと内容が分からないのでご存知の方いらっしゃったら教えて下さい。

ビギナーです。

「数学の楽しみ」２００６秋「ゲーデルと現代ロジック」で、p.47脚注13に、
「矛盾する命題が一つ証明できれば、それからすべての命題が証明されてしま
うので、体系が無矛盾であることは、ある命題がその体系から証明できない
ことと同値である」との記述があります。
「ある命題」には、「体系が無矛盾であること」も含まれるのでしょうか。
そうであれば、第二不完全性定理から、（初等数論の体系を含む）公理系は、
自身の無矛盾性を証明できないので、そのことは、体系が無矛盾であることと
同値であるということになり、結局、体系が無矛盾であることを示していると
なりそうなのですが、どこが間違っているのでしょうか。

第二不完全性定理から、（初等数論の体系を含む）公理系は、
「無矛盾ならば」自身の無矛盾性を証明できないので、

が正しい。

あと「体系が無矛盾であること」をその体系で表現できるか、という問題もありますね。
例えていえば微分積分の理論が無矛盾であることを微分方程式や級数なんかを使って
命題で表現しろというわけですからtrivialからは程遠いでしょう？

その条件が「（初等数論の体系を含む）」となってるわけですが。

あと無矛盾性は、具体的に証明のどこで使ってるんですか？と言われると
きちんと勉強してないと答えるのが難しいね。

> 「矛盾する命題が一つ証明できれば、それからすべての命題が証明されてしま
> うので、体系が無矛盾であることは、ある命題がその体系から証明できない
> ことと同値である」との記述があります。

これの意味はおｋ？なにか誤解してそうなんだけど

>>55
modelの話は扱わないという方針。
だから、forcingも出てこない。

うーん、強制法載ってないんですか…
強制法の載っている教科書はやっぱり高いなあ…

強制法なしで巨大基数の話してるのか・・・

有理数と複素数の中間体である代数的閉体のうちで、
その存在証明に真に選択公理を必要とするものがありますか？

日本語の教科書で強制法について詳しく書いてあるのってありますか？

強制法って何よ

フォーシング

定理を強制列車に乗せること（ｗ

>>64
洋書嫁。最近の和書は絶版か品切ればかり。

>>35
＞基礎論で、ゲーデル達の完全性／不完全性定理以降、
＞それに匹敵するくらい重要かつ興味深い結果って
＞何か出てるんですか？

コーエンのフォーシングと、これを用いた選択公理・連続体仮説の独立性

>>38
＞Lowenheim-Skolemの定理とか
これ、ゲーデルの完全性/不完全性定理より古いんじゃなかった？
＞Curry-Howardとか
これも、結構古い。もともとはCurryがλ計算と
論理との関連を研究していて見つけたもの。

基本的なところを読みたいなあ〜と思ったりする日々
「数学と論理」に挙がってるこの本っておすすめですか？

Stephen G. Simpson : Subsystems of second order arithmetic
Springer 1991

>>58
＞「体系が無矛盾であること」をその体系で表現できるか
残念ながらできません。

>>71
それは二階算術の部分体系を用いて、代数・解析・幾何などをやろうっていう本なので、
基礎論の基本的な勉強をしたいというときに使う本ではないぞ

>>73
あらら、逆数学というのを勉強したら、数学基礎論で使う証明の形式の
枠組みが（弱い体系限定かもしれませんが）きちんと理解できるのかと
思ってたんですが、必ずしもそういう印象ではないのですか？

逆数学にしろ何にしろ、そういう応用分野は、
まず基礎論で使う基本的な枠組みは理解してから取り組むものだと思う

というか、そういう類の本は、
読者が基礎論のそれなりの知識を既に持ってることを前提として書いてあるもんだが

このチグハグっぷりはなんとしたことだ

とりあえず、あと１０日もしたら

「ゲーデルと２０世紀の論理学」の３巻が出ることになってて

それに「逆数学と２階算術」の章があるみたいだぞ

数理論理学 (数学基礎論) とはどんな学問かという話が出たときに、
自分の意見を言ってみたら、逆数学はその定義に当てはまらなかった。

逆数学が数学であるとしても数学でないとしても矛盾が出た。どうしよう。

逆数学が存在しないことの証明だね。

近傍について質問です。

Vがxの近傍というのは、x∈U⊂Vを満たす開集合Uが存在するということですけど、Vの開核が存在すればそれはUになりえるので、必然的にVは近傍になっちゃうと思うのですがどうなんですか？

○・←x

有限の立場ってのがいまいちよくわかりません

ご教授お願いします。。。。。。

>>81
>>51

http://science6.2ch.net/test/read.cgi/math/1149259755/330
にちょっとレスしました

すいません、よろしくおねがいします

LKでψが証明可能である⇒入力¬ψに対してタブローが停止する
はどうやって証明したらよいのでしょうか

>>85
完全性定理を使えば自明

いや、それで完全性定理を説明しようと思っているのですが

>>85
林晋の数理論理学（コロナ社）にのっていたと思う。証明長いからここじゃ無理。

このスレで質問していいか不安ですがお願いします。
廣瀬健の「帰納的関数」（共立出版）に次のように有りました。
（＊）「1変数の原始帰納的関数はすべて1変数の関数のみで構成できる」
上記の本には証明の概略しか載っていないため、（しかもその概略がよくわか
らない）どうしても示せないのです。どなたかご教示いただけないでしょうか？

（＊）をもう少し詳しく記述します。
初期関数として
（１）s(x)=x+1（後者関数）
（２）L(x)（定義後述）
（３）R(x)（定義後述）
（４）0(x)=0（常に0をとる定数関数）
以上の初期関数から初めて、
（５）2つの関数f(x),g(x)からJ(f(x),g(x))を作る。（J(x,y)の定義は後述）
（６）2つの関数f(x),g(x)からf(g(x))を作る。
（７）2つの関数f(x),g(x)から次のようにh(x)を作る。
　　　　h(0):=f(0),　　h(x+1):=g(h(x))
を有限回繰り返し適用するだけで、1変数の原始帰納的関数をすべてつくる
ことができる。

J,L,Rの定義（というか、単なる説明というか）
J(x,y):=(x+y)(x+y+1)/2+x
L,Rはz=J(x,y)⇔「L(z)=x∧R(z)=y」となるような関数

例えばL(z)+R(z)やL(z)・R(z)なんかはどうやって作るんでしょう？
どなたか偉い方お願いします。

>>89
昔全く同じところで悩んだ記憶があるよ
J をうまく使えばできるはず

Robinson の結果だったような気がする。

>>83
私も良く知らないんですが、（Hilbertの）「有限の立場」は大雑把に言って
「有限の具体的図形に関する具体的な性質、具体的な操作、および具体的な推論のみを許す立場」
のことみたいです。ということで、良いんじゃないかな。多分。


参照文献

Web上の文章では、以下で引用する
・Hilbert's Program (Stanford Encyclopedia of Philosophy)
ttp://plato.stanford.edu/entries/hilbert-program/ が一番詳しく纏まっていると感じました。

・ヒルベルト・プログラムとは - はてなダイアリー
ttp://d.hatena.ne.jp/keyword/%A5%D2%A5%EB%A5%D9%A5%EB%A5%C8%A1%A6%A5%D7%A5%ED%A5%B0%A5%E9%A5%E0
は数学の哲学専攻の大学院生の方が書かれたようです。（慶應大かどこか？）

・Hilbert's program - Wikipedia, the free encyclopedia
ttp://en.wikipedia.org/wiki/Hilbert%27s_program
Wikipediaの記事

・数学基礎論三つの神話
ttp://www.shayashi.jp/HistorySociology/HistoryOfFOM/myth.html
終わりのほうに有限の立場に関するGoedelの認識がどうだったかが載っています。

・自然演繹の正規化定理に基づく算術の無矛盾性証明
ttp://research.nii.ac.jp/~terui/mita03.pdf
ぐぐって出て来たので一部ちょっとだけ参考にさせて貰いました。

・Hilbert's Program
http://members.at.infoseek.co.jp/nbz/ref/hprogram.html
逆数学がHilbertのプログラムの部分的実現となっているという喧伝。

・有限の立場（独; finiten Standpunkt/英; finitistic standpoint)とは何であったか

Stanford 哲学百科事典 のHilbertのプログラムの記事から必要そうなところだけごく一部引用。
文献番号省略。finitary standpointとfinitist point of view、
有限の立場と有限主義はほぼ同義語として使われているような感じです。


1.　Hilbeltのプログラムの歴史的発展

1.3　有限主義と無矛盾性証明の探求

Hilbertによると、内容的な算術という「具体的記号に関する純粋に直観的な基礎にのみ依拠する」
特別な数学の分野があり、その対象は「全ての思考に先立って直観的に直接経験として存在する」、
「それらの対象の存在、それらの差異、それらの並びは
（それらの対象自身と同じように）何か別のものに還元できない」

これらは記号列は意味を持たず、つまり抽象的な対象を表さず、然しながら演算を受け
（例えば連結され）比較される。これらの性質や関係の知識は直観的で論理的推論を介さない。
Hilbertによると、このようにして展開された内容的な算術は確実であり、
内容的数論の命題には論理的な構造がないのであるから、いかなる矛盾も起きない。


3.　形式主義、還元主義、道具主義

理念的な手法によって証明される実在的命題が「正しい」こと、
つまり有限の計算によって直接的に確かめられることが求められる。
これをSmorynskiが、実在的数学に理念的数学を付け加えて保存拡大になること、
と言い換えていることが4.　HilbertのプログラムとGoedelの不完全性定理に述べられている。

2. 有限の立場（この項目が本題なんだけど長いので箇条書きで）

この方法論的な立場は、数学的思考を「全ての思考に先立ち直観的に直接経験として存在」
するような対象、またそのような対象に関する抽象的概念の導入を必要とせず、特に、
完結した無限の総体に訴えることをしないような、演算と推論の方法に制限することより成っている。

2.1　有限的な対象と有限主義者の認識論

・Hilbertが数項（numeral、数字とも訳す）をどれくらい正確に理解していたか？

Bernaysの提示した最も円熟した有限主義においては、有限主義の対象は
繰り返しの過程によって再帰的に生成される形式的な対象として特徴付けられる。

・有限主義における対象の認識論的な意義についてどう考えていたか？
・当時までの学者達のHilbert及びBernaysへの影響。

2.2　有限的に意味のある命題と有限的な推論

・特性函数が再帰的に、典型的には原始再帰法によって定義されるような関係は受け入れられる。
・このような関係から論理積∧、論理和∨、否定¬、限定量化によって出来た命題。

「任意のnに対してn+1=1+nとなる」のような数項に関する一般的事実を述べる命題は
問題のある有限的命題である。「どうしたって全ての数について試すわけにはいかない。」
有限的な一般命題は無限な連言∧_{x} φ(x)としてではなく、
「ただ、一つ数項が任意に与えられたときに何かを主張するような仮言的判断φ(x)として」
理解されねばならない。
このように一般的有限的命題に問題があるとしても、この種の命題は特に重要である。

2.3　有限的な操作と有限的な証明

・どのような演算、どのような原理が有限の立場で許されるのか、という問題は決定的に重要である。

Hilbertは一般的な説明を与えず、ただ許容される内容的算術の演算と推論方法の例を与えただけ。
Hilbertは直観的な思考は「再帰法と有限主義的に存在する総体に対する直観的帰納法」を含むと述べて
累乗法（冪）を例に挙げ、Bernaysは累乗法が如何にして数項に関する有限的演算と理解されるかを述べた。

・彼らが述べたことによれば原始再帰法により定義された演算と、
（仮言的）帰納法による証明が許されることになる。

・これらは原始再帰法による函数定義と量化記号なしの論理式の上の帰納法を認める
原始再帰算術（primitive recursive arithmetic; PRA）として形式化できる。

・しかしHilbertもBernaysも原始再帰法「しか」有限的だと見做されないと主張したわけではないし、
実際彼らは原始再帰的でない方法を用いて、表面的には有限的な無矛盾性証明を既に1923年に得ている。
（ε計算を使うらしいから「数学の基礎」に載ってるやつか？）

・どんな演算が有限的だと見做される「べき」であるか。

Parsons(1998)は有限主義の直観との関係を重視。
・有限的とみなせるのは、せいぜいが加法と乗法から限定再帰法（bounded recursion）で得られた算術的演算。
・累乗法と一般再帰法は許容されるものではない。

Tait(1981)は有限主義は原始再帰的な推論と一致するという主張を広く受け入れられるしかたで強力に擁護。
・直観により表現されるという点を有限主義の特徴づけとは考えず、
有限主義的推論を「全てのnon-trivialな数学的推論に前提される最小限度の推論」と考える。
・有限的な演算と手法を分析して有限列の形の数の概念に潜在的なものであるとした。

また別の、興味深いが哲学的に詳細な正当化を与えるわけではない有限的証明の分析が
Kreisel(1960)により提案され、有限的な函数とはPAで全域的であると証明できる函数であるとされた。
またKreisel(1970)は「可視化出来る」という事に商店をあてた別の分析を与え、やはり有限的に
証明可能であるということとPAで証明可能であるということは実は同等である、という結論を導いた。

・Primitive recursive arithmetic - Wikipedia, the free encyclopedia
http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic

>>92

有限の立場が
「有限の具体的図形に関する具体的な性質云々」
は全然違うと思うけど……。
　

>>96
PAはPRAかな

>>97
神話としてはいいんじゃない？現代的な解釈はともかく

原文ではPAになってるね

聞いててもはや「数学」という感じがしないのは気のせい･･･？

うん

書いた本人ですがそもそも数学の話じゃないと思いますよ。
基礎論での「直観」などというのはKant的な意味合いが大きいみたいです。
そもそも有限の立場での絶対的な無矛盾性の証明は実現不可能なんだから
体系を限定することに昔ほど大きな重要性はないんのではないでしょうか。

>>98
Hilbertたちはどう考えていたか、というあくまで「Hilbert（学派）の有限の立場」の話なので。
最後の項には竹内外史の仕事だとか逆数学だとかも書いてありましたけど
直接的に関係がないので省略しました。

>>97
でも>>92の照井一成先生のpdfではそういう説明がされてるし、
大雑把に一言で説明するならこういう説明になりそうな気がするのですが
どういうところがおかしいですか？

「図形」というのは証明図のような
「有限個の記号から作られた有限的なもの」程度の意味です。

（↓「ゲーデルの世界」廣瀬健、横田一正より）

　すなわちこの立場は，直観的に確かめられうる対象とそれらに対する
　有限の操作の過程というものに方法を限定したものであった．

（↓岩波文庫「不完全性定理」の「内容的な数学」の説明）

　ポイントは、これらの表現が全て有限個の記号から構成された有限的存在であり，
　また，それに関する議論も有限的であるという事実である．内容的な数学とは，
　本質的に有限的な数学なのである．そして，そこには直観的な議論があるだけで，
　過程すべき公理も論理法則もないのである．（中略）
　これが後に有限の立場と呼ばれるようになるものの原型である．

>>83　>>92　>>97　>>102
そもそも
「有限の具体的図形に関する
　具体的な性質、具体的な操作、
　および具体的な推論」
の全体を有限個の文字で記述
しつくすことは不可能。

つまり「有限の立場」は有限ではない。

？

誰も許される推論全体が有限だとか全て書き尽くせるだとか
そういうことは言ってないけど…

finitary「有限個のものに関するような、有限的な」と
finite「有限個の」じゃだいぶ意味が違うような

>>103
有限の立場ってのは、
個々の証明について、必ず具体的な有限の操作で行うってことじゃないのか

>>90,91
レスありがとう。

忘れ去られてるっぽいけど、どなたか気が向いた方、ご教示お願いいたします。
>>89

>>89は要約すると、ゼロ関数C0、後者関数S、L、Rから
（1変数関数合成） h(x) := f(g(x)),
（1変数原始帰納法） h(0) := f(0) & h(x+1) :=g(h(x)),
（2変数から1変数への圧縮）J(f, g)(x) := J(f(x), g(x))
で作られた関数全体が1変数の原始帰納関数全体と等しいことを示せということ。

まず恒等関数idはid(0) := C0(0) & id(x+1) := S(id(x)) でOK。

さて、A := J(L(x), R(y)) を使うと(x1, x2, x3)をA(x1, A(x2, x3))、
(x1, x2, x3, x4)をA(x1, A(x2, A(x3, x4)))みたいな感じで全単射で1変数に圧縮することが出来る。
この(x1,........., xn)が圧縮されたものを[x1,........., xn]と表すことにする。
逆にyをn変数に圧縮されたy :=[x1,........., xk]とみてxiたちへ「解凍」することも出来る。(*)
xi = d_{n, i}(y) := L^i(y) if i < n, xn = d_{n, n}(y) := R(L^(n-1)(y))
原始帰納関数はC_0、S、射影I_{n,i}（1≦i≦n）から
（関数合成） h := f(g1,......, gm)
（原始帰納法） h(x1,......, xm, 0) := f(x1,......, xm) & h(x1,......, xm, x+1) := g(h(x1,......, xm, t), x1,......, xm ,x)
で作られるのでその帰納的定義を模倣emulateするようなf '[x1,.........,xn]を作れば良い。
実際f(x) = f '(d_{1,1})([x])である。

(*)
Aや圧縮[ ]自体は>>89では使えないがg1'、g2' が得られていれば
J(x1, x2) = J(d_{2,1}, d_{2,2})[x1, x2]は任意の[x1, x2]に対して計算できる！
のでこれを[g1', g2']と書こう。3変数以上のときも同様。解凍のほうは大丈夫。）

C_0、後者Sは与えられており射影I_{n, i}' := d_{n, i} （1≦i≦n）ももう作った。
関数合成h := f(g1,......, gm) はh '[x1,........., xm] := f '([g1',......, gm']) で OK。
原始帰納的定義
h(x1,......, xm, 0) := g(x1,......, xm) & h(x1,......, xm, t) := f(h(x1,......, xm, t), x1,......, xm ,t)は
h '([x1,......, xm, 0]) = g' ([x1,......, xm]) := g' [d_{n+1, 1}[x1,......, xm, 0], d_{n+1, 2}, ........., d_{n+1, n}[x1,......, xm, 0], ]
（[d_{n+1,1},........., d_{n+1, n}]でn+1変数をn変数に直す） &
はh '(x1,......, xm, t) := f' [h '[x1, ......, xm, t], x1,......, xm ,t]
よってこれで全てemulate出来ている。

>>107
h'の定義が
h(0):=f(0),h(x+1):=g(h(x))
と一致していないような

>>107
をを！これから解読しまつっ！thx!

>>107
やっぱり原始帰納的定義のところが、どーしてもわかりましぇん。例えばH(z):=L(z)+R(z)
なんてどうやって構成すればいいのやら。おばかですみません。もう少しヒントを。

有限の立場って、
「証明論等のメタ数学では、自然数論の範囲を超えた方法は使わない」
っていうような感じに捉えてたんだけど。
例えば、cut除去定理を証明する場合に、数学的帰納法は使ってもいいが、
超限帰納法は使っちゃダメ、みたいな。
ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、
まさにこれを実践するためでしょ？

>>104
＞誰も許される推論全体が有限だとか
＞全て書き尽くせるだとか
＞そういうことは言ってないけど…

本来、有限の立場とは、何が推論として許されるかが
有限個の文字数で書き表せ、有限ステップの操作で
検査可能である、という主張。

したがって、>>92のような立場は、有限の立場から逸脱している。
なお、専門家の中にも、この手の誤りをおかす者は少なくない。

お、専門家の間違いをびしびし指摘してくだいますね
さすがドクトル

誤りというか宗教論争の気がする・・・

その「本来、有限の立場とは〜」の
「本来」ってのはどの文献にそういうことが載ってるの？

Hilbertがどこでそういうことを言ったんですか？

>>89の疑問をいまだに解決できず、悶々としているものです。ところで、
Raphael M. Robinson , Primitive recursive functions,
Bull. Amer. Math. Soc., vol.53 (1947), no. 10, pp. 925-942.
を一般人が手に入れる方法はないのでしょうか？
http://arxiv.org/
とかいうところで検索しても出てきませんでした。Daniel E. Severinと言う方の
「Unary Primitive Recursive Functions」を今解読中ですが、どうも私の疑問を解決しては
くれなさそうな．．．。（英語も苦手なんで、四苦八苦中）
おやさしい方、どうかご教示ください。

¬（A→B）→（A∧¬B）の自然演繹の証明方法をどなたかよろしくおねがいします。
¬（A→B）を仮定して、¬（A→B）からどう動けばよいのか、別に何を仮定したらよいかがわかりません

よろしくおねがいします。

¬A, A |- Bだから¬A |- A→B
¬(A→B), ¬A |- （矛盾）
だから ¬(A→B) |- ¬¬A、あとはNKの二重否定除去を使う。
NJでは出来なさそうな気がする。

B |- A→Bだから¬(A→B), B |- （矛盾）
だから¬(A→B) |- ¬B、こっちは楽ー

>>115
HilbertはGoedelの不完全性定理の証明の後
表向き「有限の立場」だといいつつ、実際には
かつて主張していた「有限の立場」を完全に
否定する論文を書いた。

Goedelはこれをみて
「よくもまあこんなものが書けたものだ」
といったそうだ。

文献名（論文の表題）を教えて下さい。
Grattan-Guinnessに書いてあるだとか、
Ewaldに載ってただとかそういうのでも構いません。

その不完全性定理後にHilbertによって修正された立脚点のことを
「本来の有限の立場」と言ってるのだとしたら苦しすぎないですか？

Königsbergの会議が1930年7月だから
せいぜい30年の年内くらいまでのHilbertの有限主義が「本来の有限の立場」だと思いますが。

>>116
> Raphael M. Robinson , Primitive recursive functions,
> Bull. Amer. Math. Soc., vol.53 (1947), no. 10, pp. 925-942.
大学の図書館にならありそうだよ。
http://webcat.nii.ac.jp/cgi-bin/shsproc?id=AA00578276

>>118
それってシーケント計算じゃない？

おお、sequentっぽくなってるｗ
単にNKの公理を一段メタな立場から書いたつもりだったんだけど。
ちょうど今「完全性定理とモデル理論」
のLKのカット除去のとこ読んでたからそれが影響したのかねｗ

こんな感じ↓

　[B]1
------
A→B,　¬(A→B)
---------------1
　　　　¬B

>>121
ありがとう。でも一般人が大学から資料もらえるのかな？（もちろんコピーだけど）電話で聞けばいいのかな？
でもここから大学まで車で片道2時間。日曜日って大学やってないよね？

>>124
休日やってるとこもあるよ。
web で簡単な利用案内があると思うから、確認してみては。

あるいは、公立の図書館通じてコピーを送ってもらうとか。
どこでも対応してくれるわけじゃなさそうだけど、運がよければ。

>>120
>>119はその通り「修正前が本来」と
言ってるように思ったけどな

>>126
漏れもそう思う。>>119は日本語が読めてない。
北朝鮮に帰れ。

修正前の有限の立場が>>112で、それに対して、
修正された有限の立場、もしくは修正後流布した俗説が>>92ってこと？

でも>>119の主張を裏付ける（可能性がある）ものは
具体的にどの論文か良く分からないが
「Hilbertが不完全性定理の発見後に書いたらしいかつての立場を放棄する論文」しかない。

一方でStanford 哲学百科 はHilbertが書いたものだけでも20くらいの文章、本から
翻訳引用して、彼はここではこういっているし別のこれでもこういうことを言っている。
だから当時のHilbertの考えはこういうことなのだろう、というふうに推測している。
そのうち"Grundlagen der Mathematik" 1 & 2以外は全て不完全性定理発見前の文献。

Stanford 哲学百科の記事が正しいのだとしたらそれを大雑把に
（Kantに馴染みの薄い現代の日本の読者に対しても意味があるように）
要約したものとしては>>92の説明で間違っているとはいえないような気がするけどなあ。

「有限の立場」の>>112みたいな説明はここ以外で読んだことない。

>>103は「具体的」というものが何を意味するのかわからないから駄目だ、
とか言っているのかもしれないし、曖昧であることは確かで、実際は
Hilbertは例えば |、||、||| みたいな棒を並べたものを「具体的図形」の例として提示して
たとえば||と|||の連結は|||は||に等しい、というのが2 + 3 = 3 + 2の意味だ、とか言っている。

「具体的」というのがきちんとformalに表現できて、
「有限的にある推論が許されるかどうかが、有限的に確かめられる」為にはそもそも
超数学自体が形式化されないといけないような気もするけど、
「直接経験」だとか「直観により論理を介さず」とか言ってたHilbertが
そういうことを考えてたとは思わないけどなあ。

ジャキントの本（田中一之 監訳）読んでからレスしたかったけど、まあとりあえず。

×||と|||の連結は|||は||に等しい
○||と|||の連結は|||と||の連結に等しい

連結はconcatenationの訳です

>>128
＞でも>>119の主張を裏付ける（可能性がある）ものは

119のいう「不完全性定理証明後の変節論文」は
115の問いの答えではなくて、問い自体の
ナンセンスさを指摘するものかと。

＞「有限の立場」の>>112みたいな説明はここ以外で読んだことない。
いったいどこでどんな説明を読んだの？
君こそ今までに読んだ文献を全て挙げてごらんよ。

>>128
＞「具体的」というのがきちんとformalに表現できて、
＞「有限的にある推論が許されるかどうかが、有限的に確かめられる」為には
＞そもそも超数学自体が形式化されないといけないような気もするけど、

安易にformalとか形式化とかいってるけど、
君はその意味を説明できるかい？
その説明は112の主張を否定するものかい？

さすがドクトル

マギステルかも

>>112と>>119は違う人である可能性も無いでは無いと今思ったのですが
私が特に間違いだと思っているのは>>119ではなくて、>>112の「有限の立場」の説明に関してです。


>>112はHilbertたちの本来の「有限の立場」がこうだ、という主張なのですから、
Hilbertや周りの人たちの書いたり述べたりしたものが根拠に無ければなりません。
その一次資料が何か（或いは、それは何という二次資料を読めば分かるか）を教えてくれ、
という問いはナンセンスではない有意味な質問だと思いますが。
少なくとも「Hilbertはひっきりなしに態度を変えていて一貫していなかったから、
本来の立場と呼べるものなど無いのだ」などの主張は>>112のレスと両立しません。


Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など
ある種の具体性を要求しています。
それが有限の文字数で書き表せるかどうかというのは別問題です
（いやもちろん、曖昧な説明でも良いなら、Hilbertの著作中に現れる文字数は
明らかに有限なのだからこの条件は自明に満たされることになりますが。。）
それに対して
＞何が推論として許されるかが有限個の文字数で書き表せ」
というような、「許される推論の説明に要する文字数」について
Hilbeltや周囲の人間が何か要求していたというのは聞いたことがありません。


＞君こそ今までに読んだ文献を全て挙げてごらんよ。
私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから
このスレ以外に>>112のような説明が決して無いことは立証出来ません。

そもそも、今までに読んだ文献を「全て」挙げろ、というのは
幾らなんでも無茶な主張じゃないですか？あなたは出来ますか？
私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを2ch以外で
「少なくとも一つ」教えてくれ、といっているだけなので、出来て当然だと思いますが。

あ、またtypoだ
Hilbelt→Hilbert

>>134
＞>>112はHilbertたちの本来の「有限の立場」がこうだ、
＞という主張なのですから

112にはHilbertの名前は出てこないよ。
128が勝手に「有限の立場はHilbertが言い出したんだから
Hilbertの言葉がなければ根拠にならない」とわめいてるだけ。
しかも128は当のHilbertの論文を理解できていない可能性大。
だから馬鹿にされるんだよ。

>>134
＞Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など
＞ある種の具体性を要求しています。
＞それが有限の文字数で書き表せるかどうかというのは別問題です

やっぱり数学が判らずに、言葉だけで勝手な憶測しちゃってるな。

＞＞何が推論として許されるかが有限個の文字数で書き表せ」
＞というような、「許される推論の説明に要する文字数」について
＞Hilbeltや周囲の人間が何か要求していたというのは
＞聞いたことがありません。

ほら、君、やっぱりHilbertの論文読めてないよ。

>>134
＞私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから

もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。

＞ そもそも、今までに読んだ文献を「全て」挙げろ、というのは
＞幾らなんでも無茶な主張じゃないですか？

一つも挙げられないのは、いくらなんでもヒドイんじゃないか？ｗ

＞私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを
＞2ch以外で「少なくとも一つ」教えてくれ、といっているだけなので、
＞出来て当然だと思いますが。

そもそも112は、Hilbertが言ったとはいっていないのだが。
むしろ、Hilbertが言ってることとは違うというなら、
君がHilbertの言葉を引用すべきであって、112にそれを
求めるのは間違ってる。

具体的に指摘しないとトンデモの強がりと区別がつかんぞ
思わせぶりじゃなくちゃんと書いたらどうだ？

あっ、>139は>137へのレス

>>139
なに、泣きわめいてるんだ。この馬鹿ｗ
貴様は三歳のガキか。

>>140
自分でHilbert読め。馬鹿がｗ

マツシンみたいな奴だな
そういう書き方しかできないのならトンデモ扱いされても仕方ないだろう
最初から具体的に書けばすむことなのになあ

>>143
＞最初から具体的に書けばすむことなのになあ
ほんとだよ115=128=143君ｗ
自己矛盾はマツシン以下の馬鹿だよｗ

＞そういう書き方しかできないのならトンデモ扱いされても仕方ないだろう

ガキって自分にモノを教えてくれないと、
拗ねて相手をトンデモ呼ばわりするよねｗ

まあ君自身がマツシンレベルと理解できたならおれはどうでもいいや
以後は気をつけな

哲学屋のにおいがプンプンします

数学も哲学も生齧りの半可通でしょ

>>146
マツシンマニアってキモイ

>>147
トンデモの便臭を漂わすなよ（ｗ

>>148
君は全然不可通だけどな（ｗ

基礎論スレッドの質問でいいのかなという気もちょっとだけしますが、
Scott位相とか領域理論について丁寧に書いてある本ありますか？

読書のスピードからいくと、できれば和書がいいのですが、
無いということであれば洋書でも大丈夫です

>>152
自分で探せ

>>153
おすすめがなければ、こいつに突撃かと思ってるんですけど
高いしごっつそうだし、もう少し何か無いものかと・・

http://www.amazon.co.jp/Continuous-Lattices-Encyclopedia-Mathematics-Applications/dp/0521803381/ref=sr_1_1/503-7608567-7147966?ie=UTF8&s=english-books&qid=1173424058&sr=1-1

>>136>>137
いやHilbertじゃなくてBernaysでもAckermannでもNeumannでも良いですよ。
「有限の立場」というのは彼らGoettingenの公理論者の
主義主張を指す言葉だから彼らがそういう主張をしていた、ということでしょう。
一次文献かせめて二次文献くらいの根拠はあるものだと思いましたが。
もう啓蒙書とかブルーバックスとかでも構いませんけど。

竹内外史なんかは多少違った主張をしますけど、
彼の主張はどちらかというと異端的ですし、歴史的にみて明らかに後発で
彼を持って先行者を「本来の立場」ではなかったとすることは出来ません。


「当のHilbertの論文」とは具体的にどれですか？と言ってるのに
それに答えられないで読めてないなあ誤解してるなあばかり連発されても困ります。
Hilbertのどの論文を読めてないのかもわかりません。
その論文には表題は付いてなかったんですか？


>>138
＞もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。
「全て」と言われているのにニ、三冊だけ挙げても答えになっていないし
それだけしか読んでないのか、なんて言って莫迦にする人も居るかもしれませんしね。

「たとえばニ三冊挙げるなら」Stanford哲学百科とか岩波文庫の「不完全性定理」とか
（きちんと全部読んでないけど）Heijenoortとかまだ一部しか読んでないけどジャキントとかですけど。

あなたが読まれたHilbert計画に関する文献を全部挙げて下さい。

＞Hilbertが言ってることとは違うというなら、君がHilbertの言葉を引用すべきであって
「全ての思考に先立ち直観的に直接経験として存在」
「どうしたって全ての数について試すわけにはいかない。」だとか
「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか
全部Hilbertたちが書いたものそのままの引用なんですよ。

「許される推論の説明に要する文字数」について
Hilbertや周囲の人間が何か要求していたことを示す文献は無いと言っているんですが。


112が「本来の有限の立場」とは違うというなら、
112が「本来の有限の立場」を示す分権を引用するべきだと思いますけど

「本来の有限の立場」と言えばHilbertの周囲の者、
もしくはHilbert自身の立場だとみなすのはごく当たり前かと。
それに>>92にも（Hilbertの）有限の立場だとことわってあります。


>>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、
というのにたいして、それは違う、と言ってるのが>>112でしょ。
で、そういう文献は知られていない、というレスに対して

途中で送信しちゃった。

>>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、
というのにたいして、それは違う、本来はこうだ、と言ってるのが>>112でしょ。
で、そういう文献は知られていない、というレスに対して、
じゃあ>>112を否定する文献を挙げろ、と求めてるのがレスの流れ。

どうして>>112は根拠を挙げなくて良いんですかね。

まだ相手する気なの？
基礎論スレの初心者？

どういうことですか？

マツシンという奴（か“それと同レベルの奴”）が
基礎論関係のスレには永遠に住み着いていて
こいつ（ら）と言い争いになったらスルーが基本。
マツシン（かそれと同レベルの奴）が誤りを認めることは
基本的にありえない。人工無能のように必ずレスを返して
いつまでも食い下がっては鸚鵡返しで煽り、はぐらかす。
無理に調伏しようとするとスレがぐだぐだに荒れる。

「お前マツシン並だな」と言われたときに
普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
何故か「お前はマツシン以下だな」と返す、などの習性がある。

>>160
横レスですが、大変勉強になりました。ありがとうございます

有限の立場って怖いね

>>155
112は誰の名前も出していないよ。
「「有限の立場」はHilbertとその仲間のものだ」
という128こそ一次文献でも二次文献でも啓蒙書でも
ブルーバックスでもいいから文献名と引用文で
示せばいいが、ドイツ語どころか漢字も読めないかい？

>>155
＞竹内外史なんかは多少違った主張をしますけど、
＞彼の主張はどちらかというと異端的ですし、
＞歴史的にみて明らかに後発で
＞彼を持って先行者を「本来の立場」ではなかった
＞とすることは出来ません。

>>92のほうが碍子っぽいけどな。
そういえば>>120でも
＞不完全性定理後にHilbertによって修正された立脚点のことを
＞「本来の有限の立場」と言ってるのだとしたら
なんて真逆な誤読してるヤシがいたけど、マジで日本語読めないのか？

>>155
＞「たとえばニ三冊挙げるなら」
＞Stanford哲学百科とか
＞岩波文庫の「不完全性定理」とか
＞（きちんと全部読んでないけど）Heijenoortとか
＞まだ一部しか読んでないけどジャキントとかですけど。
じゃ、それぞれの中で君が読んだという箇所を上げてごらん。
岩波文庫もハイエノールトもジャキントもここにあるから
君が読んだかどうかは確認できるよ。さあ、やってごらん。

「「有限の立場」はHilbertとその仲間のものだ」ってどういう意味ですか？
誰もHilbertたちの占有物だ、とは言ってませんよ。
「「有限の立場」はHilbertとその仲間の提唱したものだ」と同じ意味にとって良いんですかね。
これくらい基礎論では常識だと思ったんですが。

>>156
＞「全ての思考に先立ち直観的に直接経験として存在」
＞「どうしたって全ての数について試すわけにはいかない。」だとか
＞「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか
＞全部Hilbertたちが書いたものそのままの引用なんですよ。

ふーん、つまらない文章を引用するね。
まず、はじめの文章は何も述べていないに等しい。
次の文章はあまりにも自明で、引用するだけ無駄。
問題は最後の文章で、再帰法や直観的帰納法として
どこまで考えているかってこと。

>>156
＞「許される推論の説明に要する文字数」について
＞Hilbertや周囲の人間が何か要求していたことを
＞示す文献は無いと言っているんですが。

だから無限に書き続けていいというのが
「不完全性定理後に修正された立脚点」
であって、ゲーデルにバカにされたこと
なんだがな。

>>166の通りに解して良いんですね。じゃあ文献名つきで論拠を。
＞The consistency proof itself was to be carried out using only what Hilbert called "finitary" methods.

＞On the conceptual side,
＞the finite standpoint and the strategy for a consistency proof were
＞elaborated by Hilbert (1928); Hilbert (1923); Hilbert (1926) and Bernays (1928b);
＞Bernays (1922)</a>; Bernays (1930),
＞of which Hilbert's article "On the infinite"(1926)
＞provides the most detailed elaboration of the finitary standpoint.

・Hilbert, David, 1928 Die Grundlagen der Mathematik", Abhandlungen aus dem Seminar der Hamburgischen Universität, 6: 65-85.
・Hilbert, David, 1923, "Die logischen Grundlagen der Mathematik", Mathematische Annalen, 88: 151-165. Lecture given at the Deutsche Naturforscher-Gesellschaft, September 1922. Reprinted in Hilbert (1935, 178-191).
・Hilbert, David, 1926, "Über das Unendliche", Mathematische Annalen, 95: 161-90. Lecture given Münster, 4 June 1925.
・Bernays, Paul, 1928b, "Zusatz zu Hilberts Vortrag über "Die Grundlagen der Mathematik"", <em>Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 88-92.
・Bernays, Paul, 1922</a>, "Über Hilberts Gedanken zur Grundlegung der Arithmetik", Jahresbericht der Deutschen Mathematiker-Vereinigung</em>, 31: 10-19.
・Bernays, Paul, 1930</a>, "Die Philosophie der Mathematik und die Hilbertsche Beweistheorie", Blätter für deutsche Philosophie, 4: 326-67. Reprinted in Bernays (1976, 17-61).

http://plato.stanford.edu/entries/hilbert-program/

これで満足？

>>167
別にその文章で「有限の立場」がどういうものか完璧に分かるって言ってんじゃないですよ。
Hilbertの別の著作から普通に解釈すれば原始再帰算術になるって何十年か昔から言われてるし、
その解釈に対する議論も為されてるじゃないですか。それで何が問題が？

>>92の「有限の立場」の大雑把な説明は上から五番目のpdfから
ほぼそのまま取ってきたものですけど、著者はPRAくらい当然知ってて
その大雑把な説明を与えているんだと思いますけど。
誰もあれが完璧な説明だなんて思ってないでしょう。

>>112だと超数学のレベルでどんな抽象的でよく訳の分からないidealな対象でも
使って良いことになりますよね。例えば自然数の任意の部分集合とか。
証明が正しいことは有限的に判定できますから。
一方で超数学における推論の説明には普通一般に言われてるよりもきつい条件を貸すことになる。
どんなに具体的でrealで、誰もがよく知っているようなものでも、
よく説明出来ないものは使っちゃいけないことになる。
そんなことHilbertが言っていましたか？

無限に続けるってのは、多分、何が許される推論か、Hilbertが無限に説明を続けるんじゃなくて
「有限ステップの操作で検査可能である」の方に反するんじゃないですか？

具体的にどの文献のどこのなんと言う文言か教えてくれるつもりがないようなので確かめようが無いんだけど。

>>170
＞>>112だと超数学のレベルでどんな抽象的でよく訳の分からない
＞idealな対象でも使って良いことになりますよね。

112にはそんなことは全く書いてないが。

＞例えば自然数の任意の部分集合とか。
＞証明が正しいことは有限的に判定できますから。

やっぱり日本語がまったく読めない人なんだな。
自然数の任意の部分集合全体なんて、
有限個の文字数で書き表わせないが。

ああ「有限個の文字数で書き表わす」と言う場合の
有限個は文字の種類数ではなく、例えば「２００字以内で書け」
という意味の純然たる字数のことである。

>>170
＞無限に続けるってのは、多分、何が許される推論か、
＞Hilbertが無限に説明を続けるんじゃなくて
＞「有限ステップの操作で検査可能である」の方に
＞反するんじゃないですか？

見苦しい言い訳だな。バカなんじゃないのか？

>>169
＞On the conceptual side,
＞the finite standpoint and the strategy for a consistency proof were
＞elaborated by Hilbert (1928); Hilbert (1923); Hilbert (1926) and Bernays (1928b);
＞Bernays (1922)</a>; Bernays (1930),
＞of which Hilbert's article "On the infinite"(1926)
＞provides the most detailed elaboration of the finitary standpoint.

これが「有限の立場」がどういうものか完璧に分かる文章なのかい？
バカなんじゃないのか？

>>160
＞誤りを認めることは基本的にありえない。
＞人工無能のように必ずレスを返して
＞いつまでも食い下がっては鸚鵡返しで煽り、
＞はぐらかす。

128だな。二言目には文献とわめき
サルでもできる検索の結果をどうだと
ばかりにひけらかす。まったく恥かしい。

＞無理に調伏しようとするとスレがぐだぐだに荒れる。

「調伏」なんて聞いたことがないので、
もしかして朝鮮語かと思って検索したら、
「加持や祈祷を用いて、悪霊や物の怪を屈服させること。」
なんて奇怪な意味の言葉らしい。
やっぱり数学よりも妖怪に詳しいオカシナ奴らしいな。

>>170
＞超数学における推論の説明には普通一般に言われてるよりも
＞きつい条件を貸すことになる。
＞どんなに具体的でrealで、誰もがよく知っているようなものでも、
＞よく説明出来ないものは使っちゃいけないことになる。

なんかまったく見当違いなことをいってるな。
半可通を笑う四半可通、といったところか。
もちろん、1/2よりも1/4のほうが小さい。

>>170
＞>>92の「有限の立場」の大雑把な説明は
＞上から五番目のpdfからほぼそのまま
＞取ってきたものですけど、

>>102では「照井一成先生のpdf」と自慢げに名前を出してたがｗ
で、しかも、>>92を見ると
＞ぐぐって出て来たので一部ちょっとだけ参考にさせて貰いました。
なんて臆面もなく書いてるね。

上記のpdfを拝見したが、そもそも碍子チックな臭いが
プンプンするわけで、92の説明もそういう立場を理解した
上で読まないと間違う。

０を正当化するのに１、１を正当化するのに２・・・
とつづけていって、１も２も・・・も全部有限だからＯＫ
みたいな屁理屈は、体系の強さの順序付けとかいう後から
出てきた御利益を除けば、本来の無矛盾性証明の目的を
全く達成していない点で無意味。

碍子もテリーも、ゲンツェンのカット消去の”魔法”に
幻惑されてるように思える。
カット消去は数学的には興味深いが、哲学的な基礎付けの問題を
解決するようなものではない。

岡田光弘氏も現代思想の「ゲーデル」特集号の中で、
ゲーデルの不完全性定理から考えてカット消去は
正しいとしても体系内では証明できないことが
明らかであり、竹内外史は竹内予想を提出する際
この点について”楽観的”だったのではないか
と指摘している。

>>171
使っていけない、と書いてない以上>>112の条件さえ満たされたら
使って良いと考えるのはごく当然だと思うけど。

＞自然数の任意の部分集合全体なんて、
＞有限個の文字数で書き表わせないが。

「書き表せる」ってのは何のことを言ってるんですかね。

一つ変数を用いれば自然数の任意の部分集合なんて
いくらでも表記のしようがあると思いますが。
例えば「偶数全体の集合」（七文字）だとか円周率だとかは
有限の文字数で書き表せるの？そうじゃないの？
「偶数全体」は書き表せないから、「偶数」という概念は使っちゃ駄目ってことなんですか？

>>173
>>163で「有限の立場」がHilbertやその周囲の人物の提唱した立場であることを
示せとか言い出すから根拠を書いたんですが。
本当はこんなこと常識以外の何ものでもないと思うけど。
「有限の立場がHilbertのものだとは言ってない」とやたら強調されてたけど
Hilbert以外の誰が提唱したとおっしゃるんですかね。

＞どうだとばかりにひけらかす。
自分で文献を挙げろと言っておいてそりゃないだろう。自分が何言ったか覚えてないのか？

＞もちろん、1/2よりも1/4のほうが小さい。
はあ？

定年退職後に数学博士号　大阪大の７１歳男性
http://www.chunichi.co.jp/flash/2007031001000102.html

何々世代まえの人数を出す方程式が知りたいんですがどなたか知っていますか？

>>180
それと基礎論と何の関係が?

>>112 >>115 >>119 >>120ときてその後いきなりgdgdになりはじめたな
120までは普通の流れなのに
なんで文献名が出ないんだ？

「質問スレッド」で検索して最初に見つかったスレに突撃する人が
どこの板にもいるものだ。「基礎」とか書いてあるしｗ

>>182
文献文献と＊＊の一つ覚えで騒ぐ＊違いか

>>178
128は形式化が全く理解できていない四半可通

551

結局>>112の

>本来､有限の立場とは、何が推論として許されるかが
>有限個の文字数で書き表せ、有限ステップの操作で
>検査可能である、という主張。

これって本当なの？
一連の流れは
「本来」って書いてるぐらいだから有限の立場を唱えていた学者のうちの誰かがそれを唱えてたんでしょ？
それは誰よ？
って質問なんじゃないの？

>>187
自分の主張を逸脱といわれて逆上し
＊＊の一つ覚えを繰り返す＊違い

>>111
＞ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、

ヒルベルトの弟子であるアッカーマンが実質的に
PRA（原始帰納的算術）を有限の立場と考え、
その無矛盾性を「証明」していたから。
（「不完全性定理」岩波文庫ｐ229）

ただし上記の文献にもあるように、上の「証明」は
実際には超限帰納法を用いている。
実際、不完全性定理から明らかなように、
PRA自身の無矛盾性はPRAでは証明できない。

Derivability ConditionってPRAで証明できましたっけ。
と思ってぐぐったら出来るっぽいですね。

しかし文献を示せというから言われた通り示したら
「どうだとばかりにひけらかす」とか言われてビックリしたよ
何かの罠みたいなもんだったのかなー

自然数の無矛盾性証明なんて別にGentzenに限らず
多くの人が行っていて、何通りもある。
ただ「有限の立場」はHilbertの書きものを素直に読めばPRAとほぼ同一視でき、
全ての証明はPRAを逸脱した立場で行なわれているから
Hilbert計画の達成とは見做されない、それだけの話なのにね。

>>112は多分そういうことを知らないんだろうけど、
Gentzenの自然数論の無矛盾性証明を
「有限の立場で認められる無矛盾性証明」から排除するために
「本来の有限の立場」なんてのを後付けでデッチアゲてしまっているんだろう。
それでいて後から主張を翻したHilbertを批判してるんだから御目出度いものだ。

だからHilbert学派がそういうことを述べていたソースを出せ、と言われても
答えられないし、挙句の果てには「有限の立場」はHilbertたちのものじゃない、
などと馬鹿げたことを言い出す。
きっと「本来の有限の立場」なるものは「オレ流・真・有限の立場」な感じで
>>112の脳内のなかにしかないんでしょ。

しかし結局>>160の言うとおりになってしまったなあ、

素直に>>160の言うことを聞いておけば良かった。
スレ汚し申し訳ない。

お疲れさん

何だよ結局>>111が答えってことかよ

＞きっと「本来の有限の立場」なるものは「オレ流・真・有限の立場」な感じで
＞>>112の脳内のなかにしかないんでしょ。

なるほど納得
>>112も始めから「『俺が思うに』有限の立場とは本来こういうものなんだよ！」
て書けばいいのに

>>190
＞自然数の無矛盾性証明なんて別にGentzenに限らず
＞多くの人が行っていて、何通りもある。
＞ただ「有限の立場」はHilbertの書きものを素直に読めば
＞PRAとほぼ同一視でき、全ての証明はPRAを逸脱した立場で
＞行なわれているからHilbert計画の達成とは見做されない、
＞それだけの話なのにね。

やっぱり肝心なことがわかってないな。
超数学で元の体系より強いものを使ったらダメなんだが。
有限の立場は「内容的な数学」だとかいうのは、
不完全性定理以後では、そういう無茶を押し通すための
強弁に成り下がってしまった。

>>190
＞Gentzenの自然数論の無矛盾性証明を
＞「有限の立場で認められる無矛盾性証明」から排除するために
＞「本来の有限の立場」なんてのを後付けでデッチアゲて
＞しまっているんだろう。

Gentzenの「証明」の問題点は、有限の立場とかいう以前に
対象理論では定義してないことを、後だしジャンケンのように
超数学の理論で持ち出していることにある。
「超限帰納法だって定義できるからいいだろう」というかも
しれないが、そうやって、後だしジャンケンを無限につづければ
いいという発想で、全体をなし崩しに正当化するのは、結局有限の
立場自体を否定するものである。

なんか重い空気のなかすみません

自然演繹で
∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である
（ただし、∃ｘA（ｘ）はaを含んではいけない）、というのは、
例えば、
∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか

∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから、きっと、ｓ０と０は別物で、ｓ０は入れていいのだ、と勝手な判断をして導出を続けていったら、
いろいろなものがでてきて、ちょっと今、困ってます

>>197
> ∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか
これ自体は正しいけど、その前の部分とこのことをあなたがどうやって関係付けたのかわからない

> ∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから
よくないよ

もしかして∃と∀を混同してない？

一つ確認

> ∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら
ここの a は変数？

すみません
書き方が良くなかったです

前のはなかったことにして、
定項（数項）０、１、２、・・・があって
関数記号ｓがなし、
関数記号＋があって、
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメですか？
ということでした

>>200
普通の自然演繹の体系ならダメ

関数記号を含んだ項の扱いかたがいまひとつよくわからないのですが、

例えば、
＝除去規則
ｓx＝ｓxとx＝０＋xが導出可能であるならばｓ（０＋x）＝ｓxが導出可能である、というような代入のしかたはOKでしょうか

>>202
導出自体は問題ないと思うけど、
1. = の除去規則
2. その規則をどう使ったら sx=sx, x=0+x から s(0+x)=sx が出るのか
を正確に書ける？

そのまま
１＝除去規則
A（a）とa＝bが導出可能であるならばA（ｂ）が導出可能である、（A(ｂ）はA（a）のaのところを（全部でなくてよい）ｂにおきかえたもの
よって２
としたのではまずいでしょうか

>>204
よさそうだけど一応確認を。
2 で A(a) に対応する論理式と b に対応する項は？

A(a) に対応するのがsx=sxでb に対応するのが0+xだと思いますが

ところで
>>201
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ
ということなので
>>１９７
の、
>（ただし、∃ｘA（ｘ）はaを含んではいけない）
は（ただし、∃ｘA（ｘ）はaに含まれる項を含んではいけない
のようなことになるのでしょうか

>>206
どこでおかしくなってるのか分かったような気がする。
あなたの知っている∃除去規則を正確に述べてみてください。

>>204
等号に関する公理（equality axiom）というのがあります。
教科書などの、この公理に関する記述を参照。

あと∃の除去則（∃-elimination）のところも要復習。
要は>>207さんの言う事を良く聞きましょう、という事で。

０変数関数記号を定数と呼ぶ
∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である
（ただし、∃ｘA（ｘ）はaを含んではいけない）
aは新しい定数
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ
０＋１は定数ではなくて項だからダメ
でした。

aって新しい"定数"なの？変数じゃないの？まあ、新しい定数を言語に導入してしまうってのもありかもしれんけど。
もしかしてそこらへんにわかってない原因があるんじゃないの？ちなみに
＞０＋１は定数ではなくて項だからダメ
これはとてもとんちんかんに感じる。

なんかいまいち良く分かってないみたいだなあ、、

まあ良いや

先週買った本、郵便屋さんキター！！
読むべし、読むべし

　　　　集合の本？　ボコボコにしてやんよ
　 ∧＿∧
　 (　･ω･)＝つ≡つ
　 (っ　≡つ＝つ
　 /　　　) ﾊﾞﾊﾞﾊﾞﾊﾞ
　( /￣∪

http://2ch-news.net/up/up50539.jpg

古本屋さんか？
よく手に入ったね
しかし田中をこれから読むのにカナモリさんも一緒に買うとはなかなか

それは俺も思ったが
こういうのは手に入るときに手に入れておこう

というかｸﾞｯｼﾞｮﾌﾞ

つ図書館

まあ英語版の二版は手に入るみたいですけどね
（邦訳は初版）

KunenとかJechがまだ訳書出てないのに意味無いよね、はっきり言って

それは言えた

set theory? 今や時代はsubstructural logicだYO!

それはさすがにない

220は世間知らず

あほか

"世間"が構成可能集合でなければ、知らなくてもどうということもない　ノ

>>223
集合論研究者のいう世間とは、同業者の集まりことらしい

烏合の衆

人の脳を読む能力を悪用する奴を潰せ。

最先端の研究テーマは何ですか？

なんか４分冊のごつい本でたね

>>228
どんな本？

>>228
わしも聞きたい

>>77のかな？

20世紀の論理学は、あまりゴツくはないような。
どちらかというと読み物風というスタイルな気がする。

>>232
とはいえ、”４分冊”で思いつくのは>>77だけ。
228にはゴツいんだろう。他にどんな本を読んだか知らないけど

「20世紀の論理学」のような内容で、証明もちゃんとのせてくれているような本ってないですか？
もちろんそうすると辞書みたいに分厚くなるだろうし、洋書しかないんでしょうけど、どなたか
わかるかた、教えて著。

日本語の本なら「数学基礎論入門」とか「入門数学基礎論」とか

日本語の本なら「数理論理学」とか「数理論理学」とか「数理論理学」とか
「公理的集合論」とか「公理論的集合論」とか「公理論的集合論」とか
「証明論入門」とか「現代集合論入門」とか

数学基礎論入門は2種類以上あるし
数理論理学も4種類上あるみたいだけどね

前原昭二のは最近復刊されたらしい。

「前原昭二の」って「数学基礎論入門」かな？
それとも「数理論理学」かな。

たぶん復刊されたというから前者だと思うけど
数学基礎論入門は少なくとも数年前には単行本化されてたし
今でも手に入ると思うけどね

>>234
「20世紀の論理学」には割ときちんと証明が載ってる気がするけど

難波完爾「集合論」の最初の数ページに
カテゴリーがどうのこうのとか書いてあるけど
最初読んだときは良く意味が分からなかった。

最近哲学系の本を読んでやっとcategorial grammerとか
型理論とかと関係があるんだろうなあ、と想像がつくようになった。

モダン過ぎて初学者には全然意味が分からないと思うんだけどなあ、あの書き方じゃ。

>>240
1975年当時はもっとモダンに見えただろうなあ、
難波さんの翻訳した本か何かにそれについての論考があったと思うので、
気が向いたら探してみて。

Davisの「超準解析」にわざわざ付録として書いたアレとか
数学セミナー増刊「数学基礎論の応用」とか

このスレの人たちにとっては「超積と超準解析」「圏論の基礎」
「代数幾何学」（ハーツホーン）とかはやっぱりデフォなの？

>>241>>242
おお、なんかどうもありがとうございます。
今度図書館に行ったときにでも読んでみます。

変な質問ですが、{ }が空集合である( ⇔ ∀x[¬(x∈{ })] )ことを用いずに、
「 { }は空集合である または { }は無限集合である 」
を証明することは可能ですか？

>>245
どういう論理体系でやるのかをはっきりさせないと答えようがないような

えーん、全然知らなかったよ〜

http://www.technobahn.com/cgi-bin/news/read2?f=200704031617&ref=rss

フィールズ賞を受賞したから著名、みたいな書き方ｗ

とか思ってたら連続体仮説を「証明」かｗ

Wikipediaは訃報に関しては仕事が早い。

記事へのリンクがあった
http://www.sfgate.com/cgi-bin/article.cgi?f=/c/a/2007/03/30/BAG8DOUKEG1.DTL
http://www.nytimes.com/2007/04/02/us/02cohen.html?_r=2&oref=slogin&oref=slogin

>>245
{ }を特徴付ける公理が何もないなら、ほとんど何も証明できないんでないの？（恒真式なら証明できるけど
そんなの意味ないでしょ。）

>>250
空集合の公理は、実は無限下降列の非存在（と他のいくつかの公理）から引き出せる

空集合の存在を認めるのと、無限下降列の存在を認めないのと、どちらがいいのかは哲学

{_}という表現が何を意味してるのか、
どういう風に定義されてるに拠るんじゃないの。

何か{_}に関する性質が前もって与えられてないと証明できるわけ無いじゃん。
定数記号cが∀x¬x∈cを満たすことを
cに関する論理式を使わないで証明できるわけが無いのと全く同じで。

naiveな集合論しか知らない人にはそういう見通しが立たないのかもしれないけど。

フィールズ章を受賞したから著名、ってのは必ずしも間違ってないんじゃないの。
特にロジックの非専門家や一般人にとってはね。

連続体仮説を解決じゃなくて証明とか書いてるのは
記者がわかってないんだろうなあ。
連続体仮説はZFCから証明出来ないことを証明した、と書けば良いのに。

その前のパラグラフではちゃんと独立であることを証明と書いてるのが余計に謎だｗ

こんな顔になってたんだなあ

>>250>>251>>252
やっぱりそうですよね。ありがとうございます。
もう1つ質問があるのですが(また変な質問ですが)、f,g：{1,2,3}→{1,2}を
f(1)＝1,f(2)＝2,f(3)＝1
g(x)＝1 (x∈{1,2,3}が奇数のとき),2 (x∈{1,2,3}が偶数のとき)
と定義するとき、
(1)「f(1)＝1である」ことを使わずに「f(1)＝1または1＝2」を示すことは可能でしょうか？
(2)「g(1)＝1である」ことを使わずに「g(1)＝1または1＝2」を示すことは可能でしょうか？

fとgの定義は使って良いの？
だとしたら〜を使わずに、というのは意味不明なんだけど。

何が言いたいの？

トンデモのにほいがしてきた。

そういえば、コーエンの伝記ってどんなんだっけと思って
久しぶりに「アメリカの数学者たち」を部屋の奥から掘り出した俺

>>257
うーん、何と説明したらいいんだろう…
と考えていたら、自分でも質問の意味が分からなくなってきました。
>>256は取り下げます。

ひとつ言えることは、>>256は今の勉強法は即刻とりやめて
ちゃんとした先生にちゃんとした授業で教えを受けること。
まだ大学に行ける年齢でないならそれまで我慢すること。

>>256はどの辺がどういう感じに基礎論に関係してくるんだ?

P.コーエンの連続体仮説論文の原書持ってるよ
それだけだけどｗ

全ページスキャンしてZIPでくれ

>>263
全頁和訳してdvi/ps/pdfでくれ

論文？モノグラフとかじゃなくて？

>>245
>{ }が空集合である･･･ことを用いずに、
>「 { }は空集合である または { }は無限集合である 」
>を証明することは可能ですか？

{ }が無限集合である可能性なんてあるのか？（ｗ

>>264-266
持ってるのこれの昔の版↓だよ

Set Theory and the Continuum Hypothesis (Paperback)

たぶん国会図書館や大学図書館で閲覧可能でしょう

やっぱGoedelが査読した原論文じゃなくて本じゃん。
国会図書館には洋書の専門書ってあまり無い気がするよ。
大学図書館にはあるだろうけど（原論文もあるだろう）。

訳書のほうは国会図書館にもあるだろうね。

糞スレ

Goedelってだれ？

>>271
http://ja.wikipedia.org/wiki/%C3%96

「連続体仮説」が Amazon で4500円だ。
古本屋で 8000円出して買った私は少し悲しい・・

そのうち、文庫本になるか再版されるから、買い直せば平均単価がさがるよ。

されるか？望み薄いと思うけどなー

古本屋で売ってAmazonで買い直せば少しは救われるかも

しばらくぶりに復刊とか新刊ないかな。

明倫館にカナモリが出てますな

>巨大基数の集合論 販売価格　：　\8,000
>
>著者名　：　カナモリ，A．著　淵野昌訳
>出版社　：　シュプリンガー・フェアラーク東京
>発行年度　：　1998年

>>278
むむ、今確認したらもう無くなってる
漏れの書き込みは役にたったんだろうか？？

もう無くなったのか。
欲しかった……。

>>279
ありがとう

>>281
もしかして買った人？　なら、書いて良かった　ノ
（自分の分のときも結構探したので・・）

>>282
＞もしかして買った人？
そうです。もう半分あきらめていたところでした。本当にありがとうございました。

だからホントに勉強したいなら洋書で買えと。

そこまで真面目に勉強する気はないけど、ちょっと興味があるみたいな

選択公理を使わずに、ボレル非可測なルベーグ可測集合は作れるのでしょうか？
ボレル非可測なルベーグ可測集合の例を
ttp://www-an.acs.i.kyoto-u.ac.jp/~kigami/analysis1-9.pdf
で読んだのですが、ルベーグ非可測集合を使って構成しています。しかし、
ルベーグ非可測集合を作るには選択公理が必須だと聞いたことがあります。

ド素人の質問で申し訳ありませんが…

Fermatの最終定理って解決しましたよね。
でもあれっていわゆる集合論の枠組みの中での証明な訳ですよね。
ってことは、コツコツ計算していったら
ある日Fermatの最終定理の反例が見つかる
(系として集合論が無矛盾でないことが分かる)という可能性は
残っている訳なんですか？

> いわゆる集合論の枠組みの中での証明

って何？
先生がいいと言うまで廊下に立ってなさい。

ここで質問する人って、ホントに素人かキ印ばっかだね

>>287
まあ残ってますけど、でもZFより弱い枠組みで証明できるはずですよ。
初等整数論の定理はZFCから証明できる場合は選択公理を使わないで証明できる、
とか、どうやらそういう種類の定理があるようで。（数学セミナー増刊号に載ってた）

>>289
まあネットだし2chだし。

先日本屋にシグルイの新刊を買いに行ったら、レジ前に「お薦めライトノベル」コーナーが特設されていたのね。
でも、んなもんに興味のない俺は、特に気にすることもなく目当てのものを探して、レジで並んでた。
次は俺の会計だな、と思ってたら後ろから怒号が飛んできて、近くにいた人が一斉にそっちに向いたわけ。
一瞬、誰もしゃべらない状態になって、店内に流れるBGMがよく聞こえたよ。
みんなの視線の先には、それはもう絵に描いたようなｷﾓｦﾀがいた。
ｷﾓｦﾀが店員に文句を言ってるんだろうなってのは状況的にすぐに分かった。
周りの注目も気にせずにそのｷﾓｦﾀはフーフー言いながら手に持った単行本らしきものを店員に向けて
「なんでゼロの使い魔がお薦めコーナーにあるのに、涼宮ハルヒの憂鬱は置いてないんだよ！」と。

涼宮ハルヒの憂鬱と、ゼロの使い魔。名前は知っていたよ。あのキモいアニメ。
あのｷﾓｦﾀが持っていたのは多分、ハルヒかゼロの使い魔のラノベだったんだと思う。
店員らしき男の人が申し訳ありません申し訳ありませんって謝ってたけど、ｷﾓｦﾀはその店員に向かって
何度も、「なぜ涼宮ハルヒを置かないんや。廃れるやろがっ！！」って同じ質問を何回も繰り返してる。
そんで最後には店長を呼べと。
店長が来てからはもう凄かったよ。
お前らは商売をする気があるのか、ただ売れてるものを売ってるだけだ、本当の本の価値を分かっていない・・・と。
みんなドン引き。それでもｷﾓｦﾀのラノベ講義は続く。
会計が回ってきた俺が店員に小さく「大変ですね」と言ったら、困った笑顔を作って
「はは・・お騒がせしてすみません」だって。
会計が終わってしばらくしてからｷﾓｦﾀの演説は終わった。俺は帰っても良かったんだが、『めったに見られるもんじゃねえ！』
と思ってずっと横で見物してた。てか見物人が結構いたよ。
最終的に、そのお薦めライトノベルコーナーに涼宮ハルヒを置くことでｷﾓｦﾀは納得したみたいで、文句を言うだけ言って
何も買わずに悠々と店を出て行った。
残った店内で小学生っぽい男の子が「すげー！あれが生オタクだよ！きめえええええええ！」と友達らしき子とキャイキャイ

一行目を丸ごと検索にかけるとコピペかどうか分かるなｗ

>>290
ご回答ありがとうございます。
ところでZFより弱い枠組みって例えばどんなものなんでしょうか。

http://www.salvastyle.com/images/collect/brueghel_blind00.jpg

＞「なんでゼロの使い魔がお薦めコーナーにあるのに、
＞　涼宮ハルヒの憂鬱は置いてないんだよ！」

ハルヒよりハヒル、という人は大人（ｗ

で、さすがの私も、近所のレンタルビデオ屋で
「なんで、"憂鬱"はあるのに、"消失"は置いてないの？」
とツッコム勇気はない。
もちろん、ハルヒではなくハヒルである。

>>293
Peano算術とか。

まあ表現力が弱いとか、片方がもう片方で解釈可能という意味の弱さね。

集合論ならKPなんていう体系はZFCより弱いはず。

ところで私の知り合いは
「涼宮ハルヒの父親はおそらく京大卒のサラリーマン。
　住所は阪神甲子園近く。
　で、御多分にもれず父親は猛烈なトラキチで、
　娘はそんな父親をアフォだと蔑んでいる。」
と推測しているが、こういう些細なことにこだわるのが真のヲタクだろう。

枠組みとか気にするより岩波文庫の不完全性定理の
読めるところだけでも読んでおけ

それより数学やれ
猪狩さんの実解析入門

>>300
別のスレのネタ持ち込むなよ

いやいや本質を突いたレスだと思うぞｗ

ある日反例が見つかるかもとか
下手に説明すりゃどんどん妄想を膨らませるばかりだ

不完全性定理に用いる不動点定理を眺めているのですが、内容が込み入っていて、どこか眉唾物の雰囲気を漂わせているのですが、
どこが決定的に怪しいのか、もしくは怪しくないのかわかりません

君の心理描写はいらん

不動点定理ってことはきちんと整理された現代的な本で勉強してるはずだから
分かりやすいはずなんだけどなあ。

あと第一不完全性定理のほうはrecursively enumerableとかそういう概念を使って
不動点定理を使わずに証明する方法もあるよ。

>>305
＞どこか眉唾物の雰囲気を漂わせている

まあ、気持ちはわかるよ。
不動点定理で出てくる項の意味を取ろうとしても
操作が完結しなくてできないっていうんでしょ？
でも、それを言われても困るんだよね。

>>303
ちなみに何ていう本読んでんの？

>>286
ZFからは証明できない。

あっそ

ZFからは証明できない事を証明できない事を証明できない事を示せ

ZFからは証明できない事を証明できるならば、
ZFからは証明できない事を証明できない事を証明できない事を証明できる

□¬□→□¬□¬□¬□

p→□◇p

ボレルとルベーグが一致しない理由ってなんだっけ？

掘られたくなかったからだろう……

数学基礎論って将来性ある？

これ以上分野として痩せ細ることはないだろうから
昨今のGoedelプチブームなどと考え合わせても、
あとは発展するだけじゃないかな。

998

>>317
日本での最後の輝きにならないようお互いがんばろう。

フレーゲ、ラッセルの論理主義とヒルベルトの形式主義との違いが
今一つ分かりません。どなたかご教示ください。

>>320
ちゃんとした返事はこの後わかっている人に書いてもらうとして

論理主義は集合も数もとにかく数学的対象は論理法則から全て導けるという考えから始まったもの
形式主義は数学に非構成的手法を取り入れる正当性を証明を言わば図形とか機械語の列のような無意味な形として眺めることで構文的組み合わせ的に処理し(無矛盾性証明等)示すことでそのような手法を自由に使う数学を認めようという考え
前者はタイプ理論とか今も活きているし哲学よりの論理学者は最近も新しい結果を出している
後者の公理主義の部分は数学者の標準として活きている

関連して
集合を定義するときに既に定義されている集合しか使ってはいけないとき集合の定義は可術的、そうでないような定義を非可術的という
論理主義は可術的集合のみ扱い、形式主義は非可術的集合も扱う

「可術」じゃなくて「可述」的のほうが良いんじゃないかしら。
predicativeの訳語で、predicateが叙述する、断定する、基礎を置くのような意味だから。

田中尚夫の「公理的集合論」でも「確かさを求めて」でもそうなっている。

因みにFregeとRusselの論理主義は結構違う。
FregeとRusselの論理主義について知りたかったら
「言語哲学大全　�T」や「ラッセルのパラドクス―世界を読み換える哲学」などを読むのが良い。
「フレーゲ哲学の最新像」なんていう本もある。
Hilbertの形式主義に関しては記号論理学の入門書を読むのが一番早いと思う。

>>323
すまん。いいもなにも完全な誤変換。訂正サンクス。

すいませんが、非可述的に定義された集合の簡単な例を教えていただけませんか。

実数の上限とか

上界をもつ集合の、という意味ね

なんか勘違いしてたみたいですいません。非可述的というのを
「aを定義するのに、定義されるべきaの情報を使用している」みたいなもんだと
思っていたら、調べてみると、例えば上限では「集合Sの上限aがa∈Sを満たす」
こともある（Sに最大値がある場合）わけですが、その場合、集合S全体を使って
定義されたaはSよりも型が上になるから、そもそもa∈Sと言うことを考えること
ができなくなってしまう、というのがラッセルの困ったところなんでしたっけか？

でも
「aを定義するのに、定義されるべきaの情報を使用している」みたいな話ありま
せんでしたっけ？

>>328
上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？

>>329
＞上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？
え？そうでしたっけ？aがSの上限であると言うのは、
∀x(x∈S→a≦x)∧∀b(∀x(x∈S→b≦x)→a≦b)
で表せますけど、どこら辺が「上限が定義されていないと上限は定義できない」のか教えたいただけませんか。
というか、むしろ実数の連続性が関係するのかな。

TV局の編集でそういうテツガクっぽいこと言ってるところだけ
取られちゃったんじゃないの？多分。

ごめんなさい、誤爆です

何らかの対象を、それ自身を含む集合を用いて定義することを、
非可述的に定義すると言います。
論理主義というと良く名前が出てくるのはFrege、Russel、Ramsey、Weylなどですが、
可述性がどうのということを言い出したのは多分Weylです。
彼は、著書の「連続体」(1918 因みにDoverから\2,000くらいで英訳が手に入ります）で
　自分の属するclassを用いることによってしか定義できないような実体は存在しない。
と述べて一種の悪循環原理について述べています。
この原理を採用すると、「一般の」実数の有界集合が必ず上限を持つことを保障出来ません。
従って集合論を元に解析学を展開すると、かなり早い段階で躓いてしまいます。

一方、RusselがPrincipia Mathematica (1910-1913. 2nd edn, 1925-1927)で
展開した型理論 type theory というのは、
型 0 の対象から初めて、型（及び階）の低い対象から順に、
既に定義した対象のみを使って次の対象を定義していく、ということをして
Russelの逆理を初めとする各種逆理を防ごうという壮大なプログラムです。
が、実際にPrincipia Mathematicaを通読した人は
実はほとんど居ないんじゃないのとか言われてます。

多分この二つを混同されてるんじゃないかと。

因みに現在ではFefermanらが、Dedekindの連続性の公理を少し変更して
可述的な型理論の体系Wを定義したりし、さらに自然科学に応用されているような
数学のほとんどはWのなかで展開できることを示したりしています。
Fefermanは哲学よりの研究者ではありませんが、可述性という概念も未だに研究されているということらしいです。

>>325
たとえば自らを含まない【或いは. 含む】ような集合すべての集合、とか。

>>333
ありがとうございます。

可述性がどうのということを言い出したのは1905年あたりのことでなかったかなあ。

Les mathematiques et la logique

Revue de metaphysique et de morale,14(1906)294-317

Poincare

定義可能性と計算可能性っておんなじですか?

違うと思います。

定義できるけど計算できない実数ってなんですか?

Chaitin数（Ω数）とか。
http://www.nikkei-bookdirect.com/science/page/magazine/0606/omega.html

まあそんなことしなくても、たとえば
Peano算術だとかZF集合論だとかの公理系とG¨del numberingを
適当に定義した上で、x∈[0,1]を、無限10進小数で、小数第n桁目が
nが論理式のコードでないとき0、
証明可能な論理式のコードであるとき1、
反証可能な論理式のコードであるとき2、
証明も反証も出来ない論理式のコードであるとき3と定義すれば
このxは計算可能にはならないはずです。

なるほど。そう言われればあたりまえでした。
計算できないやつを実数化すればいいですね

話は変わりますがチューリングマシンにサイコロをつければ
計算能力は上がるんでしょうか?

>>341
計算できるかできないかなら変わらない。
さいころの目が固定されているなら、単純に全ての場合を模倣できる。
（１がでて１が出た場合、１がでて２が出た場合、、、６がでて６が出た場合）
なお、計算量で違いがあるかないかはわからない、
違いのあるなしが証明できれば、賞金付きのP=NP?問題。

サイコロ振ってもでたらめな意味の無い数しか出てこないからね。
適当に振ったらなぜか何か意味がある目が出てくると仮定すれば
オラクルとして使えることになるから変わるけど。

>>341 >>342
なるほど。出た目によって幅優先で探索すればよいので
計算可能性には影響しないのですね。
そしてサイコロTMで多項式時間で解ける問題が NPに含まれてるのは明らかと。
ではサイコロの出目が無限にある場合はどうなんでしょうか?
例えばポアソン分布にしたがうとか。

違う

>>344
NDTMのDTMによるシミュレーションにexpのコストがかかるかどうかが問題になってるの、
ついでに言うと、P=NP?問題はオラクルでは決着はつかない。
連続分布のほうは知らない。

[1 0 0 1 1 0 1]
[0 1 0 1 0 1 1]
[0 0 1 0 1 1 1]

やっとゲーデルと20世紀の論理学シリーズが全部完結したねー
まだ四巻買ってないけど。

中身どうなの？

自然数上の足し算のみの体系は構文論的完全で、その定理の集合は決定可能、その補集合も決定可能、
定理の集合の任意のモデルは補集合の要素を真にしないので、濃度がNと同じなら、真にする論理式の範囲が異なることがない、
すなわち、範疇的である、と思うのですが、正しいでしょうか？ご教授お願いします。

>>350
いいんじゃない？
でも、その体系だと、「２は平方数ではない」が記述できないと思うよ。

大学一年の頃、竹内の証明論の（日本語の）本を読んでいた．Cut-elimination の定理の意味というか、
「なんでそんなことを証明したいのか」がわからなくなって放り出した．

あれから十年以上経つけど、この板にお住まいのすごい人たちに、cut-elimination の意味を
教えて欲しいです．

微分の増減表を書くとき、矢印の向きとか±とかをどうやって決めてるのかわかりません

>>353
僕はそのことが基礎論とどう関係があるのかわかりません。

>>352
cut-elimination → 算術の無矛盾性

超準モデルがあるから ω-categorical ではない。

＞Cut-elimination
証明可能なＳｅｑｕｅｎｔが、それに含まれる論理式の部分論理式だけを使って証明できるってだけでも
「へぇー、すごいなあ。」と思ったものだが。

>>357
自分のは、「わざわざややこしいCut規則を導入しておいて、それを除去して
喜んでいる」みたいな印象を受けていました．『Cut 規則がないと、色々な
証明図が長くなりすぎる傾向があるから Cut 規則を導入しておくけど、
証明体系の性質についての議論をするときに、Cut が技術的な障害になる
ので、Cut なしの証明図に書き換えてよい事を示しておく(※)』のかなあ、とか
考えましたが、独りで本を読んでいて誰にも相談できなかったので、
消化不良感だけ残りました．

やっぱり※という理解は間違ってますかね？

>>358
その理解でもいいと思います。
あとは、LKから構造規則を抜いて部分構造論理を作ったり、
□の規則を加えて様相論理を作ったりしますが、
その時にcut除去定理が成り立ったり成り立たなかったりします。
そのたびにcutを追加したり外したりするのは厄介だし本質的ではないので、
とりあえずいつもcutを入れておく、というのも１つの理由だと思います。
とりあえず入れておいて、cut除去定理が成り立つか否か、という話にしたほうが、
見通しがよくなります。

あとは、cut規則は論理学でいう三段論法に近い感じなので、
論理学の中で重要な三段論法を外せる、という意味合いもあると思います。

Aと¬Aから空シークエントを導出させて無矛盾性の証明もできたりします。

助けてください！
0.238X+9.85√X = 6000
この解き方を教えてください！お願いします。

>>360
数学基礎論と何の関係が？

>>360
>>8

Cut除去定理ってCutなしの証明図は具体的には得られないんじゃないの？
そういう記号的な操作がどうのこうのということではなくて、算術の無矛盾性とか
さらには数学そのものの無矛盾性とか、そういう雲の上の獲物たちを狙うための道具じゃないのコレって。

>>363
具体的に得る方法を与える証明もあるよ

>>364
cut除去についていうと、確かにcutは除去できるし
それによって無矛盾性は証明できるけど、
「確かに除去できる」と主張するための帰納法は、
元の体系からは証明できない。

>>359
「わざわざ導入」でいいの？あくまで、

通常の証明では三段論法はあたりまえのように使うので、形式化した推論・証明を考える際も、三段論法を表現できないとダメ。
だけどLKタイプの体系では、カット以外の推論では（単純に）三段論法を扱えないので、カットを導入する必要がある。
だだカット消去定理が成り立つので、結果的にはカットは導入しなくても証明できる論理式に違いは無いことが分かる。

では？

>>366
LKって別に普通の証明を記述するための体系ではないよ。
またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
cutの除去はあくまで無矛盾性証明のためのプロセス。
こういうことはロジシャンには常識なんだが、一般人はまず知らない

>>359, >>363
やはりcut-eliminationは技術的な詳細であって、それを使って
何をするかという事のほうが、少なくとも初学者にとっては大事だったみたいですね．
久しぶりに証明論の本を取り出して眺めてしまいました．15年前に２ちゃんがあったら
、独りで悩まずにすんだろうにな〜．

>>367
＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
え？cutを除去したら、無駄のない証明になるんでないの？

無駄がないからといって読みやすいとは限らないよ

数学の本の証明で“○○の定理により”と書いてあるところすべてに、
その○○の定理の証明が書いてあったらたまらない。

というか無駄にページ数がかさんで詐欺

何かお互いに言ってることがかみ合ってない気がする。cutのある、完全な証明図と、その証明図からcutを
取り除いた証明図を見比べたら、後者の方が無駄のない証明図になっていると思うんだけど。
>>371が言ってるのはそれとは別でしょ。

定理の適用は cut ではないと？

「無駄の無い」という言葉では曖昧だからもっと明確に表現したほうがよいかと。

＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
というのは、
（実際の数学の証明をLKで書き出すようなことは
現実的にはほとんど無いが、仮に書くとしたら）
cutありならまだ何とか読める証明も、cut無しなら重複が多くて読めたものじゃなくなる、
ということでしょ、たぶん。

定理の適用は cut だろ。
cutless の証明は, 定理を適用しない,
ものすごい冗長な証明になっているということだが。

除去されるんだから忌避される理由でもあるのでせうか
cut

>>369
>cutを除去したら、無駄のない証明になるんでないの？

間違い。曖昧なのではなく明確に間違い。

>>373

君、実際にcut除去したことないだろ。
だからそういう全くのウソを平気で喋れるんだ。
手を動かせないなら口も動かすな。

cut なしの証明については、Girard の本の前書きに少し書いてある．

cutとか、その意味での三段論法とか言うのは
要するに議論のモジュール化ということだよね。
なんか陳腐な言い方になっちゃうけど。

直観主義論理で、Sequent　Ａ⊃Ｂ⇒¬Ｂ⊃¬Ａの証明のＢに¬¬Ａを採用
すれば、三重否定からの二重否定の除去　⇒¬¬¬Ａ⊃¬Ａが得られると
聞いて素直にSequentで証明したことがある。

　　　Ａ⇒Ａ　　　　　　　　
−−−−−−−−−　　　
¬Ａ，Ａ⇒　　　　　　　　　　　　　　　　Ａ，Ａ⊃¬¬Ａ⇒¬¬Ａ
−−−−−−−−−　　　−−−−−−−−−−−−−−−−−−−
　　　Ａ⇒¬¬Ａ　　　　　　　　¬¬¬Ａ，Ａ⊃¬¬Ａ⇒¬Ａ
−−−−−−−−−　　　−−−−−−−−−−−−−−−−−−−
　　　　⇒Ａ⊃¬¬Ａ　　　　　　　　　　　　Ａ⊃¬¬Ａ⇒¬¬¬Ａ⊃¬Ａ
−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−
　　　　　　　　　　　⇒¬¬¬Ａ⊃¬Ａ

でもそれをCut除去定理の証明の方法でCutを除去していったらすごく簡単
になってびっくりしたんだよね。
　　　　　　Ａ⇒Ａ
−−−−−−−−−−−−−
　　¬Ａ，Ａ⇒
−−−−−−−−−−−−−
　　　　　　Ａ⇒¬¬Ａ
−−−−−−−−−−−−−
¬¬¬Ａ，Ａ⇒
−−−−−−−−−−−−−
　　¬¬¬Ａ⇒¬Ａ
−−−−−−−−−−−−−
　　　　　　　⇒¬¬¬Ａ⊃¬Ａ

私が言いたかったのは具体的に言うとこういうこと。

>>382
リテラル１個しかないような命題論理の証明１つだけで
「どんな証明もカット除去すれば簡単になるっ！」
と断言されてもなあ。全然論理的じゃないし。

>>383
うーむ。それはそうだなあ。しかし、今まで自分が実際にcutを除去したときはいつも簡単になったので
そう信じていた。それなら、今まで実際にcutを除去したことある人で、cutを除去したら証明が冗長に
なった例を知っている人は教えてくれないかな。というか、そういう例を探してると次第に「cut除去する
と証明って簡単になるんだな」と思えてくると思うのだが。

計算量の理論に近い人ならいろいろ知っていると思う．
cut を除去すると証明の長さが指数関数的に増大する例がありそう．

>>382
ＡＡにしかみえない

>>384
命題論理の簡単な証明なら cut 使うまでもないからなあ。

算術での例がこれの appendix にある
ttp://www.seitoku.ac.jp/~ikedak/arai.pdf
詳細は追っかけてないけど証明のサイズが論理式の double exponential になるのかな

>>384
George Boolosの論文
"Don't eliminate cut"
を読め。そういえばこれも算術での例。

>>387
算術の例というわけではないでしょ．

>>389
算術っていってるのは、自然数論のこと。
勿論、公理まで含めて記述すれば述語論理の命題になるからＯＫ

> 公理まで含めて記述すれば

はじめからそう記述しているよね。

A sequent calculus without cut-elimination is like a car without engine
Jean-Yves Girard

>>392
＞A sequent calculus without cut-elimination
cut除去なしのsequent計算がエンジンのない車のようだと言ってるの？

まあ、cut抜きだと証明図を作るときに
基本的に分解していけばいいので
アホでも出来る。

cutを使って簡潔な証明を書くには魔力が必要（ｗ

下手な分解はタマネギの無限皮むき（ｗ

場違いかもしれないんですが、
−×−＝＋
になるのはどうしてなんでしょうか？

「かもしれない」ではなく完全に場違いです。

>>395
うまくいく場合は、上手下手に関係なく剥ける。

>>398
うまくいくシーケントかどうか計算できない。

>>399
事前の計算は不必要。
うまくいく場合には、方法論に依存しないといっただけ。
もちろん、これは手数を度外視している。
手数をケチるには、オツムを使う必要がある。

一般には cut を含む証明図 P に、cut を含まない
証明図 f(P) を対応させる関数 f は、原始帰納的でつか？

>>401
P と f(P) が同じ命題の証明って条件は当然付くんだよね
考えたことないが、原始帰納では厳しいんじゃないか？

>>402

レスありがとうございます。
はい。同じ命題の証明図です。

帰納的な事は、すぐにわかるのですよ。
（二重帰納法を使いますが）
原始帰納的なことの証明を与えようとして、うまくいかなかったので。

やはり厳しいと予想されますか。

一階の述語論理の cut 除去ならば，原始帰納的。
通常の帰納法で証明できることは Gentzen の自然数論の無矛盾性の論文に
ちょろっと書いてある．
Girard の本では二重帰納法による証明の評価をまじめにやって、原始帰納的な
上限を与えている．

>>404

ありがとうございます！

(1) 大学で集合の講義をしなければならなくなった。
(2) 入門としての集合の講義なのでそんなことを授業で話す必要は
　　まるでないのだけど、教える以上は知っておかなければならないだろうと
　　ZF 等の公理論的なものや歴史を勉強しようと思った。
(3) とりあえず岩波基礎数学の集合と位相を読み、また歴史関係の本を読む。
　　学生時代、そういうことは勉強しなかったこともあり、とても面白い。
(4) ところがその後いろいろと詰めて考えみると「命題」というものが
　　良くわかってないことが判明。
(5) しょうがないので基礎論の教科書を読み出し、見事にはまる。

というわけで現在本業(微分方程式)そっちのけ状態w 質問ですが、

(a) 現在の数学基礎論は多岐にわたるそうですが、現在の研究の進展状況を
　　解説したもの (所謂 survey) はないですか？
(b) 数学基礎論ではどういう学会・研究集会があるんですか？
　　日本数学会ではあまり活動してないようなんだけど・・・。

知り合いに基礎論関係の人がいません。教えてくださいませ。

>>406

僕も日本数学会の基礎論分科会に属していますが、
入会以来、なしのつぶて。
研究集会など、何の連絡もありません。

>>407
どもども。
僕は分科会は関数方程式論にしか入ってませんが、ここは分科会の人が頑張って
メーリングリストで研究集会の連絡をしたり、り欧文論文雑誌などを作ったりなど、
それなりには活動はしてますね。
数学会の基礎論の分科会はあまり活動してないのかな。

日本にも基礎論の人が結構いるみたいだから、どこかで活動はしてるんだと
思ったんだけど、どこで頑張ってるのかなぁ。参加しやすそうな研究集会とかに
ぶらりと言って顔を出してみたかったんだけど。

基礎論の人は和気藹々と群れたりしないんだよね
専攻柄数学観を強固に持っている人が多いし、そこを侵されるのを極端に嫌う傾向が強い。

test

>>406
＞「命題」というものが良くわかってないことが判明。

具体的に、命題の何がどう分からないのでしょうか？

ところで、本当に公理的集合論についての講義が学生に必要だと
お考えならば、貴方が勉強するよりも、集合論の研究者に講義を
任せるほうがよろしいかと思いますが、いかがでしょうか？

>>409
部外者は知りもしないで口からデマカセのウソばかりいうね。

>>406
今から本屋に行って
「ゲーデルと２０世紀の論理学」を買ってきて読む
→数学基礎論サマーセミナー2007に参加する。
9/4から三日間の間静岡で行われます。8/31が締切なのでお早めに。
集合論に関する比較的入門的な内容の講義をするようです。（forcingとかBoole値モデルとか）

私は基礎論の専門家じゃないですけど、
基礎論の専門家が居る大学では、
それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。

>>413
正しくは、数学基礎論サマースクール、だね。

>>411
ちょっと書き方がわるかったようですね。
「入門としての集合の講義」というのは一年生の数学の入門としての講義です。
所謂、素朴な集合論のことですね。

ただ、ある程度しっかり話そうとするとこのテーマで話す場合 excuse を
並べることになりますね。そこをいかに話すかが、先生の腕の見せ所となるかと
思いますが、しかし知らないことを話すわけにはいかない。
あーだ、こーだと下手な考えをするまえに、現時点で数学では集合はどのように
理解されてるかをまず知っておこう、というのが勉強を始めた動機です。

> 具体的に、命題の何がどう分からないのでしょうか？

集合論で使う命題の定義がわからなくなったんですよ。

> ところで、本当に公理的集合論についての講義が学生に必要だと
> お考えならば、

普通の数学科の入門としての講義では必要ないと思ってますよ。
私自身も自分の研究では今まで（そして、おそらく今後も）なしで済ませていて、
それで困ったことがありませんから。

> 集合論の研究者に講義を任せるほうがよろしいかと思いますが、いかがでしょうか？

特論などで本当に講義をしてもらうのであれば、そのほうがいいでしょうね。
というより、そうすべきでしょうね。

>>413
どうも、どうも。四巻からなる本ですね。

サマースクールですか。
まともに出張の日と重なってしまいました。
しかし、そういう活動はされてるんですね。いいですね。

> 基礎論の専門家が居る大学では、
> それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。

なるほど。いろいろ探してみたら、比較的近くの大学で基礎論の研究グループが
あるみたいです。とりあえずはそこをホームページをウォッチしてみますね。

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

基礎論って今時、若い人でやる人いるんだろうか・・・・

数年前から独学で始めたんですが、３０代ももう終わりじゃ、若くないですか？w

何事も学び始めるのに遅すぎることはない
ただ独学は危険

>>415
いえ、書き方は悪くありません。
「入門としての集合の講義」だということは分かっていましたから
公理的集合論のことなど言い訳としても考慮する必要がないだろう
という意味で書きました。

さて
>> 具体的に、命題の何がどう分からないのでしょうか？
>集合論で使う命題の定義がわからなくなったんですよ。

集合論のどこで使う命題でしょう？
内包的記法で使う場合のことでしょうか？
それなら｛ｘ｜Ｐ（ｘ）｝と書かずに、すでに集合と分かっているａについて
｛ｘ∈ａ｜Ｐ（ｘ）｝と書いておけばラッセルパラドックスはおきません。

420で述べたことは、岩波基礎数学の「集合と位相」の冒頭にも書いてあります。

でもそういう解決法はいかにも場当たり的で、
どうして{x; φ(x)}がclassであってもsetではないのかが
学生には十分納得できないと思うけどね。

>>420
> 公理的集合論のことなど言い訳としても考慮する必要

私、何か言い訳けしましたっけ？

>集合論のどこで使う命題でしょう？

至るところで使う命題のことですよ。
失礼ですが、命題とは何かここで定義してみていただけますか？

>ラッセルパラドックスはおきません。

そうですね。だから？

>>423
>私、何か言い訳けしましたっけ？
これから、学生に対してするんでしょう？
excuseを並べるといったじゃないですか。
>>集合論のどこで使う命題でしょう？
>至るところで使う命題のことですよ。
うーん、普通の数学では気にならないのに
なぜ、集合論だと問題になるんでしょう。
メタ数学の話をするわけじゃないんでしょ？
>>ラッセルパラドックスはおきません。
>そうですね。だから？
ラッセルパラドックスが気になってるんだろうと
見当つけたんですが、もっと手前でつまづいてるんですか？

>>423 さんは、「命題の定義」がわからない
・・と言うようなことをおっしゃったので、
恐らくは、論理式の定義で、躓いているのではないですか？

>そういう解決法はいかにも場当たり的で
文句ならツェルメロにいってくれよｗ

>どうして{x; φ(x)}がclassであってもsetではないのか
古典論理や直観主義論理で考える限りにおいては、
上記のようなsetでないclassはどうしても存在せざるを得ない。

>どうして{x; φ(x)}がclassであってもsetではないのか

それこそ、集合論を BG 式に定式化して、
学生に説明する必要があると思う。

>>427
方式の問題ではないんだな。
集合であろうがなかろうが、ＶとＶ→２の間に
一対一対応なんかつけられないんだから。

煽り屋さん、いなくなりましたか？

誰が誰を指して言ってるのかによるな

>>411は当然の疑問
>>415はまだ曖昧
>>420はちょっとピントがずれてるけど煽りではない
>>423は煽り

とりあえず、{ X:文字列 | X ∈ {命題} } を日常語に近い高級言語でかきなおしてくれ。

>>432

要求の意味がわからない。

>>406,415さんは、集合論をやり始めたときは命題がわからなかったけど、>>406を書いた時点では
もう解決してるんだよ。そこんとこわかってやれよ。
だから、>>411はかなりトンチンカン。というか、相手を見下した感じがして失礼だと思う。
そもそも>>406の(2)を読めよ。公理的集合論を講義で教えるつもりはないと書いてある。そして、
なぜ、それでも公理的集合論について調べたくなったかも書いてある。
．．．つーか
ちゃんとレス嫁。

>>434

同意

>>433
ある文字列が命題であるとは？

>>436

あー、そういうことね。
確か、文字列の長さに関する帰納法で定義するんじゃなかったかな？
ここに定義を書くのは、めんどくさいけど。

で、日常語に近い高級言語って、何ですか？

>>426
Zermeloはきちんと正当化のための論文を書いて居るし
現代の数学の哲学の研究者もiterative concept of setなんてことに対して
深く考えたりしているよ

setでないclassが存在せざるを得ない、というのは古典論理や直観主義論理からの
論理的帰結でも何でもないんですけどね。

>>437
たとえばプログラミングで
機械が読むためのアセンブリは低級言語、
人が読むためのCなんかは高級言語。

命題の定義を、論理式などではなく、普通の数学の
日常的な言葉で言ってみろ

という話。

どもども。私のせいでちょっと荒れ模様になってしまったようですね。
申し分けないことです。>>411 あたりで怪しいなとは思ったのですが、
中途半端に相手にしたのが間違いだったようですね。
すいません。
もう私は相手にしないことにします。
そうそう、もう集合の授業は無事終わってますからね。大部昔の話です。
それでは、私の書き込みはこれで終わりにします。

√(411) = 21 世紀

> そうそう、もう集合の授業は無事終わってますからね。大部昔の話です。
あーそういう話だったのね。納得した。
>>406 の「はまる」ってのを「さっぱりわからん」って意味にとっちゃって、
(a)(b) とつながんなくておかしいなあって思ってた。

>>411 とは別人ですが、同じ勘違いをしたんじゃないでしょうか。

どうかんがえても、「マイブーム来ちゃった」って意味以外
取りようがなかったと思う。

まあ分かってみればそうなんだけど、不思議なもんで一度勘違いしちゃうと
そっちの解釈で頑張って理解しようとしてしまうんですよ。

俺も「さっぱりわからん」の意味だと思ってた。

マイブーム来ちゃったから研究集会とか紹介してくれ
って流れだろ、常識的に考えて。

・「命題」が良く分かってないことに気づき、「しょうがないので」基礎論の本を読み出す。
・専門は微分方程式。
・本業(微分方程式)そっちのけ状態。
この3つからは、「さっぱり分からん」の流れもまた「常識的」だろ。しかし、後半の(a)(b)とは
繋がらない。で、なぜ繋がらないのか考えようとしても、>>444のような思考のスパイラルに陥る
(このスパイラルもまた、常識的に考えてよくあること)。
すなわち、「さっぱり分からん」と解釈して首をひねる人が出るのも、常識的に考えて普通。

>>447
そんなことより、結局「命題」を定義できる奴は此処には折らんの？

>>434
＞>>406,415さんは、集合論をやり始めたときは命題がわからなかったけど、
＞>>406を書いた時点ではもう解決してるんだよ。
ウソでしょ。
>>435
＞同意
自作自演でしょ。

>>432
＞{ X:文字列 | X ∈ {命題} }

間違い。"X ∈ {命題}"なんて書き方はない。
顔洗って出直せ。

＞Zermeloはきちんと正当化のための論文を書いて居る
後からいくら言い訳したって、場当たり的でなくなるわけでもない

＞現代の数学の哲学の研究者も
＞iterative concept of setなんてこと
＞に対して深く考えたりしているよ
Boolosの反復的集合観が、classの存在を否定するわけでもない

場当たり的なのは或る面では集合論自体の性格から来ることだけど、
定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか
必要な公理を統一性もなくただ要請していくようなやり方よりは幾分かはマシだよ。
あくまでいくらかは、だけどね。

＞Boolosの反復的集合観が、classの存在を否定するわけでもない
そりゃ当たり前で、だいたい>>422に書いてあるのは、
classが必ずしも集合とは言えない、ということだけで
classが存在しないなんてことは誰も言っていない。
classが存在すると考えても新たな矛盾は起きない、それだけ。

>>406氏と同様の状況に陥った人のページ

www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/

ただしコチラは集合ではなく論理が中心だが。

＞だいたい>>422に書いてあるのは、
＞classが必ずしも集合とは言えない、ということだけで
＞classが存在しないなんてことは誰も言っていない。

>>426に書いてあるのも、集合でないclassがあるのは
通常の論理では致し方ない、ということだけだが。
少なくとも対角線論法によって矛盾を導き出せるならば
そうならざるを得ない。

＞場当たり的なのは或る面では集合論自体の性格から来ることだけど、
＞定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか
＞必要な公理を統一性もなくただ要請していくようなやり方よりは
＞幾分かはマシだよ。あくまでいくらかは、だけどね。

その言い分、まるで今井弘一の複ベクトルの正当化と同じだな。

いや私はZermeloが1930年に書いた論文とか
Boolosとかが書いたiterationに関する論文のことを言ってるんだけど。
定式化の方法が変わるだけで論理的には既存のZFCと全く同値なんだから
数学的には別に何も問題ない。
複ベクトルってのは知らないけど何か似たようなものなのかな。

Russelのantinomyから論理的にいえるのは、
∃y.∀z.(z∈y⇔φ(z))という式のφに¬z∈zという論理式を入れると
矛盾しますよ、というだけで、じゃあどういう論理式を排除するべきか、
という判断にはあまり合理的な根拠がない。
Cantorは、¬z∈zを代入するとyが「絶対無限多数」になってしまうから
いけないんだとか考えていたけど、そうではなくて¬z∈zという論理式は
型に関するルールが守られていないからだめなのだ、という考えもあり得るし、
またそれと別に、φに否定記号が入っているような論理式を認めないようにしよう、
という定式化の仕方もありうる。
http://en.wikipedia.org/wiki/Positive_set_theory
実際この集合論でもZFCや、ZFCより強いMorse-Kelleyの集合論を
解釈できる能力を持っているわけで、CantorｙやZermeloの案が採用されたのは
歴史的経緯に過ぎないよ。

いや私は「和集合公理だとか対公理だとか」を
「必要な公理を統一性もなくただ要請していく」
としか認識できない点が、ｉ＾２＝１なる元ｉ
を添加する複素数体の構成の仕方をアドホック
なものとして嫌う、能登の御隠居と全く同じ
感覚だと述べたまで。

＞Russelのantinomyから論理的にいえるのは、
＞∃y.∀z.(z∈y⇔φ(z))という式のφに¬z∈zという論理式を入れると
＞矛盾しますよ、というだけで、じゃあどういう論理式を排除するべきか、
＞という判断にはあまり合理的な根拠がない。

そもそも、「φに入る論理式を排除する」という
判断それ自体に全く論理的な根拠がない。

＞Cantorは、¬z∈zを代入すると
＞yが「絶対無限多数」になってしまうから
＞いけないんだとか考えていたけど、

それ以前に、濃度の違い云々というのが
対角線論法の成立から出てきているわけで
そもそもその対角線論法自体が成り立たない
ような論理を考えるという方策もある。

＞･･･そうではなくて¬z∈zという論理式は
＞型に関するルールが守られていないからだめなのだ、
＞という考えもあり得るし、またそれと別に、
＞φに否定記号が入っているような論理式を認めないようにしよう、
＞という定式化の仕方もありうる。
＞http://en.wikipedia.org/wiki/Positive_set_theory
＞実際この集合論でもZFCや、ZFCより強いMorse-Kelleyの集合論を
＞解釈できる能力を持っているわけで、CantorやZermeloの案が
＞採用されたのは歴史的経緯に過ぎないよ。

そもそも古典論理が採用されたのも歴史的経緯に過ぎない。

レベルの高いお話の途中すいません。最近次のような述語論理に出会いました。
公理系
F,G,Hは任意の論理式。xは任意の変数。tは任意の項として、
公理
(1)　F→(G→F)
(2)　(F→(G→H))→((F→G)→(F→H))
(3)　((¬F)→(¬G))→(G→F)
(4)　(∀x(F→G))→((∀xF)→(∀xG))
(5)　F→∀xF　ただし、変数xはFの中に現れない
(6)　¬∀x¬(x=t)　ただし、変数xはtの中に現れない
(7)　x=t→(P[x]→P[t/x])　P[x]は原子論理式
（P[t/x]は、P[x]にあるどれか1つのxに項tを代入したもの）
推論規則
(8)　FとF→GからGを導く
(9)　Fから∀xFを導く

以上です。これは「変数の自由出現に項を代入する」という表記法がないので
技術的に有利なのだそうです。しかし、以上の公理と推論規則から
(10)　∀x(x=x)
や
(11)　Fの中に自由なxがないとき、(∀x(F→G))→(F→∀xG)
を導くにはどうすればいいのでしょう？ぐぐってもそれらしいのが
見つからず、また、自分の頭ではわからず困っています。
どなたか教えていただけないでしょうか。あるいはweb上で証明してある
ところがあるなら教えていただけないでしょうか。

>>461
（１０）はexistential instantiation ruleから
（１１）はdeduction theoremから導く

>>457
でも実際Zermeloが最初に集合論の公理的取り扱いに関する論文を
発表したころは誰も見向きもしなかった。
なぜなら少なくとも当時の数学者には、Zermeloの公理系が
ただ「必要な公理を統一性もなくただ要請していく」ように見えたからね。

>>458に対しては
矛盾する命題が導かれるんだから論理的根拠はあるでしょ。
少なくともreductio ad absurdumが成り立つ限りにおいては。
古典論理が採用されたのが歴史的経緯に過ぎないという意見は
一般に認められたものでもないと思うけどね。

>>463
＞Zermeloの公理系がただ
＞「必要な公理を統一性もなくただ要請していく」
＞ように見えた

のは「当時の数学者」ではなく君だろう。
それとも君はその当時の数学者だったのか？

＞＞どういう論理式を排除するべきか、
＞＞という判断にはあまり合理的な根拠がない。
＞そもそも、「φに入る論理式を排除する」という
＞判断それ自体に全く論理的な根拠がない。
＞矛盾する命題が導かれるんだから論理的根拠はあるでしょ。

ないよ。φに入れる論理式のせいだと決め付ける論理的根拠はない。
実際、φに入れる論理式を制限せずに解決できる。
場当たり的というなら、φのせいだというのも場当たり的
場当たり対場当たりなら引き分け。

＞少なくともreductio ad absurdumが成り立つ限りにおいては。
矛盾が導けなければ背理法が認められても意味がないｗ

＞古典論理が採用されたのが歴史的経緯に過ぎないという意見は
＞一般に認められたものでもないと思うけどね。
実際には、昨今の論理の研究は、君の思い込みが
正しくないことを示しつつある。

www.math.s.chiba-u.ac.jp/~komori/jyugyou/suuriron.pdf

＞レベルの高いお話の途中すいません。
もっともレベルの低い話ですいません。命題論理です。
公理
(1)　F→(G→F)
(2)　(F→(G→H))→((F→G)→(F→H))
推論規則
　FとF→GからGを導く
ここで、以下の命題はどうやって証明できるんでしょう？
(a)　(A→(B→C))→(B→(A→C))
(b)　(A→(A→B))→(A→B)

>>464
いや当時の数学史に関して普通によく言われることなんだけど。
私の個人的意見ではないですよ。

>>465>>466>>467
古典論理もしくは直感主義論理のような背理法が使える論理を
前提に話をしてるんだけどね。
部分構造論理くらい知ってるけど、そんなの研究してるのは
大抵計算機関係の人だと思ってたけどね。
部分構造論理だとか矛盾許容論理を使って
集合論だとか解析だとかをやろうなんて話はほとんど聞いたことがない。
「昨今の論理の研究は古典論理が採用されたのは
歴史的経緯に過ぎないことを示しつつある」なんて大嘘もいい所。

大多数の数学者は古典論理は自然に受け入れた。
なぜならそれまで自分たちが使っていた論理を自然に形式化したものだったから。

>>468
(1)と(2)から証明の複雑さに関する帰納法で
演繹定理というものが導けるからそれを使えばいい。
教科書には大抵載ってます。

×直感
○直観

>>469
＞古典論理もしくは直感主義論理のような
＞背理法が使える論理を前提に話をしてるんだけどね。
直観主義論理では、背理法は無条件には使えないよ。

＞部分構造論理くらい知ってるけど、そんなの研究してるのは
＞大抵計算機関係の人だと思ってたけどね。
んなこたぁない。

＞部分構造論理だとか矛盾許容論理を使って
＞集合論だとか解析だとかをやろうなんて話は
＞ほとんど聞いたことがない。
Grisinが聞いたら嘆くだろうな。
「縁無き衆生は度し難し」
とかいって。

＞大多数の数学者は古典論理は自然に受け入れた。
＞なぜならそれまで自分たちが使っていた論理を
＞自然に形式化したものだったから。

ふーん。
じゃ聞くけど
・１２０円持ってる
・１２０円でコーラが買える
・１２０円でお茶が買える
古典論理だと、ここから
・コーラもお茶も手に入る
が導けるけど、こんなこといったら
コドモにもバカにされるぞｗ

ちゃちゃいれるのはいいとしても、何故そんなに挑発的に書く必要がある？
度量の狭さを自ら露呈することもないだろ

>>474
単に経済活動においては古典論理が成り立たないことの例を示したまで。
マルクスがこれを知っていたら、弁証法の代わりに部分構造論理を
口にしたかどうかは定かではないが。

煽りたいだけの奴はほっとけ

まあこういうのが得意な人なんだよ

>>476-477
常識でガチガチに固まってるから
簡単に煽られて炎上するんだよ。

>>468
演繹定理使えば？

>>462さっそくのレスありがとうございます。おかげで(11)は解決しました。（気が
ついてみると、(11)はとても簡単でした。お騒がせしました。）
　ところが(10)がまだわかりません。どうか、もう少しヒントなりいただけないでしょうか。

それから、証明したい論理式の型を1つ忘れていました。
(12)　∀xF→F[t/x]
（F[t/x]はFにある自由なxの全てに項tを代入したもの。ただし、代入可能な場合に限る）
これもなかなかわかりません。どうかお助けください。

あ、ちなみに>>468は私ではありません。それともそのくらい示せるかどうか試しているのでしょうか？
>>468くらいならできますが．．．。

演繹定理ですか･･･なかなか難しいですね。
いまのところ(a)について
公理２によって(A→(B→C))から((A→B)→(A→C))
公理１によってBと((A→B)→(A→C))から(A→C)
は示せましたが･･･
で、(b）のほうは、
公理２によって(A→(A→B))から((A→A)→(A→B))
で、(A→A)が導ければ(A→B)は導けるのだが･･･
ということで、追加問題
(c)　(A→A)

>>468は本当に疑問だったんですね。私も質問ばかりでは申し訳ないので、今回は
私が>>482の(c)に答えることにします。（ので、誰か私の疑問についてもどうかお願い
します。）
はっきりいえば、演繹定理証明しちゃえば>>468さんの(a),(b)はいずれも明らかで
すよ。早く何かの入門書で演繹定理を学ばれることを強く勧めます。
では>>482の(c)
(i)公理(1)より　A→(A→A)
(ii)公理(1)より　A→((A→A)→A)
(iii)公理(2)で、F,HとしてA、GとしてA→Aをとると
　　　　(A→((A→A)→A))→((A→(A→A))→(A→A))
(iv)(ii)と(iii)より　(A→(A→A))→(A→A)
(v)(i)と(iv)より(A→A)

っていうか、公理(2)は仮定Fのもとでの、「GとG→HからHを導くこと」
になってること、見えてます？そうすれば演繹定理なんて簡単なんだけど。

4=8-4

>>480
(10)はごめんなさい、勘違い
ちょっとやり直してくる

>>461-462
閉じてない論理式に対しては演繹定理成り立ってないような気がします。
(11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。

>>486
＞閉じてない論理式に対しては演繹定理成り立ってないような気がします。
generalization（>>461の推論規則(9)）が無条件で行われるので当然ではないで
しょうか。そもそも私が最初に(11)が証明できないと早合点してしまったのも
それが原因です。

＞(11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。
ええ、ですから私も>>480で(11)に関しては証明できたと申し上げました。

>演繹定理証明しちゃえば>>468さんの(a),(b)はいずれも明らかですよ。

戸田山氏の「論理学をつくる」に書いてありました。
これで勉強します_(_o_)_

だめもとと思ってぐぐってみたら、
Kalish, D. and R. Montague. On Tarski's Formalization of predicate
logic with identity, Arec. f. Math. Logik und Grundl. vol. 7(1964).
p.81-101
をネット上で見つけることができました。>>461の(10)に関しては最初の方
（p.85のLEMMA 2.）で証明されていました。後は>>480の(12)のみです。
こっちはできるかどうかわかりませんが、がんばります。また、お分かりの方
いましたら、ご教示いただけるとたすかります。では。

（ある程度昔の論文ならネット上で誰でも閲覧できる、何てふうにならないか
なあ。）

>>489訂正
（誤）Arec.→（正）Arch.

これが俗に言うMontague&Kalish型なんですか、なるほど

>>489

> をネット上で見つけることができました。>>461の(10)に関しては最初の方
> （p.85のLEMMA 2.）で証明されていました。

これの概要教えて

>>489
ならんな。泥棒猫め

>>492
を、興味を持ってくれた人がいるんですね。では概略を。命題論理関係の式変形
は省きます。
(i)公理(7)より　y=x→(y=x→x=x)
(ii)(i)より　y=x→x=x
(iii)(ii)より　¬x=x→¬y=x
(iv)推論規則(9)より　∀y(¬x=x→¬y=x)
(v)公理(4)より　∀y¬x=x→∀y¬y=x
(vi)(v)の対偶を取って　¬∀y¬y=x→¬∀y¬x=x
(vii)公理(6)より　¬∀y¬y=x
(viii)(vi)(vii)より　¬∀y¬x=x
(ix)公理(5)より　¬x=x→∀y¬x=x
(x)(ix)の対偶を取って　¬∀y¬x=x→x=x
(xi)(viii)(x)より　x=x
(xii)推論規則(9)より　∀x(x=x)

>>493
ネット上で普通に読めるのに？

煽りに反応するなよ

√(49)=7

泥棒は盗むばかり

集合論ってさ、演習やらないとわかってこないもんかな？ それとも教科書読むだけでわかってくる？

どんな分野も、自明でない例を一つ二つ考えた上で
その例で内容をなぞりつつ文献を読まないと
表面的な理解にすらも行き着かずに終わるだろうね。

集合論をテーマにしたエロゲーをつくりたい
タイトルは「プリクリ オルタネイティヴ」

ﾜﾛﾀ

>>499
結局集合算はドリルしないとだめじゃね？

俺のドリルが天を衝く

>>504
んーまあ、何をやりたいかによるんだよ。
1+1やるのに毎回毎回ペアノ算術したりλ計算する奴はあんまりいないよね？

までも一回は集合のジャングルで遭難しておいた方がいいとは思うけどね。
進めなくなって娑婆に出てこれなくなるかもだがｗ。

初心者ですみません。集合論の外延の公理は論理学で示せるのでしょうか。

>>506
へ?

>>506
高階論理、４階以上ならでてくる。

>>508
M_SHIRAISHI降臨？

地下１階の論理ってあるんですか？

そこは立ち入り禁止だから

霊界の論理

>>509
普通にtype理論を扱った教科書にはでてくるだろう。
なお、
"M_SHIRAISHI"はNGワード

>>513
君が見た本の書名と証明が書かれたページ数を記載すればいい。

それくらい自分で探せよ

>>515
そもそも
「普通にtype理論を扱った教科書」
なんて知らん

それは探す努力を全くしてないんじゃないだろうか

G,Takeui:Proof Theory だとP197以下、
P,Andrews 小川訳:数理論理学とタイプ理論　だとP161以下。

読むのメンドクセーから証明ここに書けや、ウジムシ

すみません、{ω,ω^ω,ω^(ω^ω),ω^(ω^(ω^ω)),…}のいずれよりも
大きい最小の順序数は何と書き表すのでしょうか？

数理論理学と論理学ってどう違うの？

さーなー
どこかのスレに書いてあったんじゃねーの

雨宮の定理って何ですか？

>>520が人の顔に見える

>>518
おおっ、先週「数理論理学とタイプ理論」買ってた俺、大勝利！！

直観主義をわかりよく解説した日本語の本ありますか？

教えてください。

>>520
ε_0

>>527
ありがとうございます！
ではε_1はε_0,ε_0^ω,ε_0^(ω^ω),ε_0^(ω^(ω^ω)),…ですか？

ω^(ε_0+1),ω^(ω^(ε_0+1)),...

>>526
boolean algebraとheyting algebra勉強すると直観主義論理とかわかるようになるよ

Curry-Howard isomorphism もお勧めしたい
述語論理になると急にややこしくなるが

今日の四方堂書店の新規追加本に

「数理論理学とタイプ理論　証明による真理へ」　来てます

自分が買った値段よりだいぶ安いなあ・・orz

その本確か括弧の代わりにドット使ってなかったっけ？
見た目が異様だから読む気がしないのだけど。

じゃあ読むな

logxを微分したら
1/xってどういうこと？

>>535
まあ、そうなってしまうんだから仕方がありませんな。
ていうか >>8

なんで教科書を読まないんだ厨房は

Buss "Bounded Arithmetic" って本屋で注文したら買える？
それとも、古本を探すしかない？

age

>>538
www.bibliopolis.it/
をみると、まだ入手可能じゃないかな。

この微分が解読できない。以下で式が伝わるとそもそも良いのだが・・・

積分区間[f(x),0]でg(x,u)・du
をxで微分すると
f'(x)g(x,f(x))dx+積分区間[f(x),0]でdg(x,u)・du
と論文ではなっているんだけど(というかなるはず)なんだけど
自信がない。
誰か解説してください。もう３時間くらい調べてて疲れた・・・

↑積分区間[0,f(x)]の間違い

おっともう一つ忘れていました、非積分関数の中のｘを外には出せません。

もう一つ忘れていることがあるとおもうぞ

数学基礎論って分野のことだ

・・・はっ
眠すぎてよくみてなかった、数学基礎論ね
板違い申し訳ない

聞いた相手が悪かったのでこちらに再質問。

http://science6.2ch.net/test/read.cgi/math/1193144811/20-23

＞＞第2不完全性定理に関しては、ロッサーによる上記の証明の定義を用いれば､
＞＞体系自身の無矛盾性が証明できることが､
＞クライゼル (1960) によって指摘されている｡
＞
＞…これは詰まりえーと何だと言うのだろう

つか、ロッサーのやってる所からして分かりません。

命題より弱い否定命題は無い、とは?

これらの詳解と、
これらにより不完全性定理はどう変わったのか
また、その数理哲学(と言うか単に哲学)的な意味合いの変化について
意義のご教示をお願いします。

本当にもうワケわからんちん

>>546
> 命題より弱い否定命題は無い
ってどこのこと？

> 命題の証明より小さな、否定命題の証明が存在しない
これのことなら、「小さな」はゲーデル数が小さいということじゃないの。

あと「小さな」は「命題」ではなく「証明」にかかってる

はれ？これはスイマセン。

して、結局ロッサーの不完全性定理以降、どうなったんでしょうか?

"体系自身の無矛盾性が証明できる"と言う所だけ一見すると
ゲーデルの不完全性定理にそぐわない話になりますが、
何かワケが違うんでしょうか?また、そうだとした場合は
どうワケが違うんでしょうか?

実は詳しいことはよく覚えていないのだが……

> ロッサーによる上記の証明の定義を用いれば
とあるので、証明可能の定義が違うんじゃないかな
Rosser の採用した定義のほうが強い

>>546
あのね、Wikipedia のその部分の説明は無茶苦茶だからｗ

それを読んでわからなくなっても仕方がないのであって、
もし本当に理解したいと思ってるのならば、
前原著「数学基礎論入門」あたりでもパラパラとめくってみたら？

2ch で中途半端な説明を聞くよりその方がよっぽど早くて正確。

別に問題ないじゃん、、と思ってよく読んだら吹いたｗ
以前は「論理的には」間違ってなかったんだけどなあ。
誰だ編集した奴ｗ

>>550-552
ｻﾝｸｽ、やってみる。551提示書には
クライゼルまで載ってるんかな？

>>553
載ってる。最後のほう。

ただ、前原本は第一不完全性定理はうまく書けてると思うんだけど、
第二不完全性定理のほうはちょっと読み辛く感じるかも知れないから注意。
(というか第二のほうは完全に証明を書きくだすのは大変だし。)
それでも大まかな感じを捕むためなら十分だと思うよ。

そうですか、では早速購入して勉強します。
有難う御座いました。

指数関数Exp(n)をnによらない定数回の演算で求める事は出来ますか？

>>530
>>boolean algebraとheyting algebra勉強すると直観主義論理とかわかるようになるよ

僕は、直観主義と自由選列について、日本の基礎論専門家が、どう考えているか、知りたいのです。

>>557
それだったら、例えば竹内氏の本を読めば、彼が直観主義に対してどう考えていたかは垣間見える。

今時では直観主義などはどーでもいいというのが主流。

なお、boolean algebra とか heyting algebra とか勉強しても
直観主義などわかりっこないので、騙されないように。
まさかひっかかる奴はいないと思うが、念のため。

直観主義について詳しいのは今では計算機とか哲学の方面の人じゃないかな。

今時はむしろ直観主義が再評価されてきてる感じもする
基礎論でも直観主義やってる人はそこそこいるよ

>>559
みんなでtoposやろーぜー

結局放置される >>526。 ﾐｼﾞﾒ。
でもこのスレではいつものこと。

>>526
http://science6.2ch.net/test/read.cgi/math/1072058641/905

>>563
次買う本をLogic and Structureか
Introduction to Higher-Order Categorical Logicにするか迷ってる俺がいる
λもちょっとやりたいんだよなぁ

>>564 ここのは絶版で pdf ただにゃん

http://www.amazon.co.jp/exec/obidos/ASIN/0262011255/shelarcy-22/

http://www.di.ens.fr/~longo/download.html

なんかlogic and structure読んだら
直観主義の章にforcingがどうとか書いてあったような。

連続体濃度が2番目のアレフかどうかはZFCでは決定できないと証明されているんですよね？
なら有限番目かどうかについては証明されているのでしょうか？

それどころか連続体の濃度はいくら大きくてもいい

そうなんですかー
ありがとうございました

超現実数についての質問なのですが、
X_L < y < X_R を満たす順序数yが存在するとき、
xは順序数ですか？

>>558
>今時では直観主義などはどーでもいいというのが主流。

出たよ、この半可通が。

＞今時はむしろ直観主義が再評価されてきてる感じもする
＞基礎論でも直観主義やってる人はそこそこいるよ

昔っから、直観主義論理は論理学者の主要な研究テーマの一つだが。
今時とかいうんなら、むしろ部分構造論理だろ。
哲学的にはもっとブッ飛びそうだが。

finite intersection propertyってちょ〜重要なんですね。
位相空間論からやり直してきます。

直観主義が研究対象になるのはどういう興味からなの？

>>565
超〜�dクスなんだけど、Introduction to Higher-Order Categorical Logicの方を
あぶく銭で買ってもうたぁ。

>>574
よく知らんが、計算可能性とかじゃね？

正直、直観主義などどーでもいい（笑）

正直、古典論理などどーでもいい(ﾏｼﾞ)

まあ知ってて当然だからな

まあ古典論理は物理学的に偽だからな

電波びびびびびー

寧ろ量子論理などどうでも良い

>>580
なんで？

もしかして、量子力学やってりゃ量子論理使ってることになるなんて勘違いしてるいけぬまが
いるんじゃあるまいな。

つーか、数学のいろんな分野でもそうなんだけど、
量子という言葉を安易に使いすぎなんだな。

>>585
武豊に謝れ！

量子力学以前に、古典物理学的に偽

>>まあ古典論理は物理学的に偽だからな
>なんで？

物は不変ではない。

言葉の遊びびびびびびー

>>588は古典論理を知らないだろう。

古典論理ではAとA⇒¬Aの両方が成り立つと矛盾する。
Aと¬Aの両方が成立するから。

しかし、物理においてはそのような性質は一般に保持されない。
AとA⇒¬Aから、¬Aが成り立つとき、もとのAはもはやなくなっている。

>>589
うーん、ふつう命題や述語に時間による変化なんて考えないからね。
そういうのは物理だけでやってちょうだい。

>>590
いやー物理じゃなくてたま出版とか学研とかじゃないですか？
それか現代アートの人とか。

ここは電波天文台ではありませんから

limx→0(tan3x/sin5x)
この極限が求めれないです・・・
誰か教えてください

すみません。質問スレ間違えました

>>592
だから電波に気が付かないんじゃないの？

>>590
時間軸ぶん一次元増やせば無問題

一世一代のネタ振りのつもりらしいが覚えたのが>>589だけじゃ情けない。
思考遊戯だけじゃなく真面目に勉強して欲しいと思う。

>>596
それは単に辻褄あわせにしか過ぎない。
>>597
マジメに勉強してもネタ一つ触れない君なんて
情けないというよりもどうしようもない。

物は不変でないとか、なんか電波っぽい人が出没してるな、、

古典論理は何も、物は不変だとかそんなことは主張しちゃ居ない。
一応、時相論理なんて論理も考案されちゃいるけど、
別に古典論理が間違っているというわけじゃないと思うけどね。

>>589
こういう人に限って計算問題は全滅だったりするからなｗ

まぁ量子論理のことでもいいたいんだろうけど、
なんで1階述語論理の文法使うかな
measureとかframeとかの方が親和性いいんじゃないの？

不完全性定理によると真とも偽とも証明できない命題が存在するんですよね？
ではどの命題も少なくとも真か偽か真とも偽とも証明できないかのいずれかは証明できるのでしょうか？
それともそれさえも証明できない命題が存在するのでしょうか？

ここは国語のスレッドではありません

分かりにくくてすみません＞＜
真か偽か独立かは必ず証明できるの？って聞きたかったんです

>>604
> 真か偽か独立か

不完全性定理についてもういちど学習しなおしてください。

>>604
No!

すいません。どなたかわかる方教えていただけないでしょうか。
命題論理で、
公理系１
（１−１）A→(B→A)
（１−２）[A→(B→C)]→[(A→B)→(A→C)]
（１−３）[(¬B)→(¬A)]→(A→B)
と
公理系２
（２−１）(A→B)→[(B→C)→(A→C)]
（２−２）[(¬A)→A]→A
（２−３）A→((¬A)→B)
が同値であることがなかなか示せません。推論規則はいずれも
（MP）AとA→BからBを導く
のみです。
公理系１はいろいろな入門書で説明されているので、公理系１から公理系２
の公理を導くのはできたのですが、逆がうまくいきません。Churchの
「Introduction to Mathematical Logic」にそれが載っているという情報から
実際に見てみると、結局はExerciseになっていて解答が載ってなく、今現在
そこで挫折中です。

どなたか、親切な方お教えいただけると助かります。

>>605
独立の部分がまずかったんでしょうか＞＜
詳しくお願いします＞＜

>>608
だから答えを書いてやってるだろ　ＮＯ

>>606>>609
ありがとうございます！！
では、どの命題についても
真と証明できるか、偽と証明できるか、独立と証明できるか、どれもできないと証明できるか、
のいずれかはできるのでしょうか？

>>605
不完全性定理を学習したって>>604には答えられんだろ
答えられるとしたらCHの独立性証明って何なんだよって話になるだろうが

>>610
延々とやってろ馬鹿

>>610
できません！！

>>612-613
ひょっとしてこの過程を延々やってもいずれも証明できない命題が存在しますか？

>>614
それも No！

>>615
ということはどの命題も延々やったらいつかはいずれかが証明できるけれど
それがいつ来るかは分からないということですか？

>>616
No, no, no！

もはや単純に場合分けだけの問題だから >>610 に戻って良く考えてみよう。
>>614 みたいな横着はしないように。

>>607
ウカシェヴィチの本の邦訳が出ているはず。

>>602
＞不完全性定理によると真とも偽とも証明できない命題が存在するんですよね？

正確にいえば、
「証明できない命題が存在するとすれば、
　その命題が証明できないことは証明できない。」

特に
「矛盾が証明できない（つまり無矛盾）とすれば、
　そのこともまた証明できない」

独立性の証明は、絶対的なものではない。
なんらかの前提を必要とする。

例えば集合論におけるある命題の独立性を示す場合
集合論における無矛盾性を前提するものである。

>>611
>>602の疑問はは ↓ ここからスタートしているので
> 不完全性定理によると真とも偽とも証明できない命題が存在するんですよね？

不完全性定理についてきちんと学習すれば、そもそもの疑問が間違いだと気付く。

＞CHの独立性証明って何なんだよ

もちろんZFCの無矛盾性を前提している。
ZFCが矛盾していればCHもその否定も証明できるから。

集合論の勉強を始めたのですが，壁にぶつかった為質問させて頂きます．
一般の合併集合と共通部分についてですが，
空集合でない集合Iの元をパラメータとする集合の集合{A_i;i∈I}の合併集合と共通部分についての
一般分配律の証明が略されているのですが，Venn図を用いるのでしょうか？それ以外の証明の仕方があれば教えて下さい．
よろしくお願いします．

ネタはよそでやってくれ

>>622
無矛盾性は前提というより定理の前件だと思うが
まあどっちでもいいな

Venn図で証明ってどんだけゆとりなんだよ

いやまあこの際ゆとり教育とかは関係ないでしょ。
なんかあまり基礎論と関係ないけど、他には汎用の質問スレしかないな。
まあそっちで聞いたほうが良いかも知れないけど。

>>623
x∈B∩(∪_{i∈I} A_i)
⇔x∈Bかつ、或るi∈Iに対してx∈A_i
⇔或るi∈Iに対してx∈B∩A_i
とかそんな感じで、或る〜に対して〜（〜となるような〜が存在する）
とか任意の〜に対して〜とか、そういう言い換えをして示す。

>>627
なんで日本語の集合論の本って、
quantifierの説明を最初にもってこないのかなって思うけどね。
∃とか∀で部分分配律な場合があるとかね。

日本語どっぷりだとなかなか意識しない部分だと思うんだけど。
書いてる人には自明すぎる話だからかな。

元の質問してる人とは違うんだけど、好意的に解釈すれば、
T:再帰的に公理化可能で自然数論を解釈出来るような無矛盾な理論として、

Tからφも¬φも示せないようなφが存在するってのが第一不完全性定理だけど、
じゃあφも¬φも¬Prov(φ)∧¬Prov(¬φ) も示せないようなφは存在するの？
φも¬φも¬Prov(φ)∧¬Prov(¬φ)も¬Prov(φ)∧¬Prov(¬φ)∧¬Prov((¬Prov(φ)∧¬Prov(¬φ))
も示せないようなφは存在するの？と聞いてるんだと思う。
なんか安易にそうだとか答えてるレスがあるけどそんな強いこと言えるんだっけ？
不完全性定理の拡張を簡単に示しちゃったことになるけど。

>>602
φを証明する、というのと、φが真であることを証明するというのは
ちょっと意味が違うので、二つを使い分けられるようになるまで
勉強してからまた考えてみては、ということかと。。

>>629
T=PA のときは、様相論理 GL を使って
Solovay の completeness theorem から出てきそうに思える。

なんかprovablity logicとか使えば
少なくとも近いことは出来そうな気はするよね。

>>629
ψが何であっても、¬(Prov(ψ)) から Con(T) が出てくるので、
φ と ¬φ さえ証明できなければ、その他の条件はあってもなくても同じ。

ああ、そうか。

¬Prov(ψ)じゃなくてCon(T)→¬Prov(ψ)にしないと絶対示せないよね。

そゆことよ

>>618
レスありがとうございます。さっそく探してみます。
ところで
>>607の公理系２からみなさんならどんなトートロジーを示せますか？私はいまだに
A→Aくらいしか示せません。他にどなたか有用なトートロジーを示せる方がいましたら
教えていただけないでしょうか。

>>635
公理系 1 と公理系 2 は同値なんだろ？

＞Tからφも¬φも示せないようなφが存在する
＞ってのが第一不完全性定理だけど、

誤り。φ⇔¬Prov(φ)なるφを具体的に構成したのが第一不完全性定理。
¬Prov(φ)なるφの存在を証明したわけではない。

>>637
いわずもがなだが、
φ⇔¬Prov(φ)⇔¬Prov(¬Prov(φ))⇔¬Prov(¬Prov(¬Prov(φ)))⇔･･･

> φ⇔¬Prov(φ)なる

NでとかTでとか指定せずにそんなこと言っても意味ないよ

>>636
だから、公理系２から公理系１の公理を導く仕方がわからないので、いきなり公理系１の公理を導くのを目標に
するのではなく、とにかくまず何が導けるかいろいろ試してみようと思い、そこら辺についてみなさんのご意見を
伺いたいと思ったわけです。

>>639
>NでとかTでとか指定せずにそんなこと言っても意味ないよ

NでとかTでとか指定するだけでは大して意味ないが。
要は対角線論法による自己言及技法の問題であって
それを可能とする体系であれば何でもよいし、
逆に技法について述べられない奴が体系の名前だけ
したり顔で語ってみても意味がない。

こちらの論理学スレにも遊びに来てちょ
http://academy6.2ch.net/test/read.cgi/philo/1194155261/l50

>>641
あんたがよくわかってないことはわかった

>>643
あんたが体系の名前を覚えただけで
判ったつもりになれるおめでたい人
だということはわかった。

馬鹿は数学板には必要ない。

まともに不完全性定理勉強したことがあれば
よりにもよってNを体系の名前とは思わんよね
馬鹿は必要ないからどっか行ってね半可通さん

松本信号点灯中

>>645
>>639が半可通か。マツシン以下の馬鹿だな。

またまたかまかけにひっかかっとるなマツシン

>>648
マツシン病患者を収容隔離しまつ

存在を示したわけじゃないってのもいくらなんでもまた言い過ぎでしょ。
そりゃ存在だけならTarskiの定理からすぐに出てくるけど
だからって当時Godel以外の誰かがそれに気づいていたわけでも無いし。

本によってはN（\mathbbとか\mathfrakじゃなくて普通のN）を
公理系の名前として使ってたような気がするけどまああまり一般的ではないかな。

>>639
いまTをT'にしてT'で¬Prov_T(φ)を示すとかそういう
複数の理論にまたがった話をしてるわけじゃなくて
特定のTを固定して話してるんだから、
取り敢えずは議論に関係ない添字を省略するのは別に何の不都合もないと思うけど。
こういう省略って結構数学ではやるでしょ。

>>650
T |- ¬Prov(φ) なるφの存在を・・・
と
N |= ¬Prov(φ) なるφの存在を・・・
とじゃ全然違うけどね

>>650も見当違い

Tarskiの定理は任意のφに対してφ⇔True(φ)となる
述語Trueが算術的に表せないことを示すもの。

一方でProv(φ)が算術的に表せることはすぐに分かるから、
ProvとTrueが一致してないことはすぐに分かるでしょ。
Godelは最初にこの弱い形の不完全性定理を発見して、
それから対角線論法によるφの構成を発見したといわれている。

だから別に見当違いじゃないし、「存在を示した」というのは
論文に発表された結果よりも少し弱いだけであって間違っていない。

test

>>653
「(¬Prov(φ)なるφの)存在を示した」
というのは明確に間違ってるよ。

>「存在を示した」というのは
>論文に発表された結果よりも少し弱いだけ

君、読み間違っちゃったね。

確かにゲーデルは、φ⇔¬Prov(φ)なるφについては
具体的に構成したわけだから単にその存在を示すよりも
強い結果を出したといっていい。

しかし、φ⇔¬Prov(φ)なるφを構成したところで、
それが即¬Prov(φ)だといえるわけではない。
前提が必要だ。例えばω無矛盾性とかあるいは健全性とか。

Implicational(Implicative?) Propositional calculusについて解説してあるサイト（英語でも可）
ご存知の方いましたら、教えていただけないでしょうか？特に従来の古典命題論理の公理が
証明されるところをきちんと述べてくれてると嬉しいのですが。

あるいは何かよい書籍あったら教えていただけないでしょうか。

>>656
もしそれがimplicational fragment of propositional logicのことだったら
substractural logicsの文献調べればいいんじゃね？

wikipediaにも或る程度は載ってるようだね

>>657
すいません。implicational fragment of propositional logicってなんでしょうか。わからんです。

>>658
はい。wikiはざっと目を通したのですが、私が知りたいのは、
http://eom.springer.de/I/i050300.htm
にある2つの公理系の、上のほうから下のほうを導くところなのです。wikiに書いてあるのはどちらかというと
下のほうから上を導いているのではないでしょうか。

実は私は>>607なのです。いろいろ調べているうちにこうなつてしまつたのだ。誰か助けて著。

>>659
657だけど、同じことだとおもう
substructural logicsの文献見ると参考になる
（答えが見つかるかどうかは別だけど
an introduction to substructural logicsに
近いことが書いてあったような

>>660
＞an introduction to substructural logicsに
その本ってGreg Restall著のですか？だとしたら、今月末までそれ手に入んないなあ。
ちくしょー。
っていうか、情報には本当に感謝してます。どっかのsiteに書いてないかなあ。

>>602-655の話って結局決着が付いたの？

>>618さん改めてありがとうございます。今日、
＞ウカシェヴィチの本の邦訳
が手元に届きましたので、ざっと目を通したところ、まさに>>607の公理系２が公理として採用されていて、
そこからいろいろなトートロジーが導かれていました。公理系１の論理式もその中に含まれています。
これから解読します。本当にありがとうございました。
ちなみに、本は
ヤン・ウカシェーヴィチ著　高松鶴吉訳「数理論理学原論」（文化書房博文社）
です。

>>662
>>655にレスなしだから推して知るべし

r=√(x^2+y^2+z^2)のとき
grad rを求めよ。
わかりません教えてください。

>>665
基礎論と何の関係が？

「質問」スレがいくつもあるから迷った挙句
「基礎」という文字に吸い寄せられたんだろう

>>665はマルチしてるからそれはねーな

>>665
>>8

>>655
あのさあ、そりゃあ理論が再帰的に公理化可能だとか
そういう前提条件は仮定しているけれども、
不完全性定理の話なんだから629あたりの条件は当然満足するとして話してるんでしょ。

じゃなきゃφ⇔¬Prov(φ)自体が証明できない。

だいたい、メタなレベルでの理論の無矛盾性を
暗黙のうちに仮定して話をするのはそうおかしなことじゃないでしょ。
矛盾してるときには全てが自明なんだから。
例えばBolyaiとLobachevskyは平行線の公理が証明不可能なことを示した、
とか言うとき、これは本当は嘘で、「Euclid幾何が無矛盾ならば」とか
そういう前提条件が付くのが正しいわけだけど、そんなこと普通はわざわざ断らない。

メタじゃなくてオブジェクトレベルで、
¬Prov(φ)とCon(T)⇒¬Prov(φ)を混同するなというのはその通りだけどね。

>>669
>不完全性定理の話なんだから629あたりの条件は
>当然満足するとして話してるんでしょ。

「629あたりの条件」といってるのはズバリ"無矛盾"かな？

>じゃなきゃφ⇔¬Prov(φ)自体が証明できない。

証明するだけなら無矛盾性を前提する必要はないよ。
矛盾する体系なら何でも証明できるわけだし。

>だいたい、メタなレベルでの理論の無矛盾性を
>暗黙のうちに仮定して話をするのはそうおかしなことじゃないでしょ。

おかしいな。ゲーデルは暗黙の仮定なんて置いてないが。

>>669
>例えばBolyaiとLobachevskyは平行線の公理が証明不可能なことを示した、
>とか言うとき、これは本当は嘘で、「Euclid幾何が無矛盾ならば」とか
>そういう前提条件が付くのが正しいわけだけど、そんなこと普通はわざわざ断らない。

まあ、２ｃｈって普通間違ってるけどな。

>>670
「再帰的に公理化可能」じゃないとそもそもProv(φ)という
述語が実際に論理式で表せないし、
「自然数論が解釈できる」体系じゃなければGodel numberingが行えないから
やはり一般には、証明可能性を体系内で扱えない。
この二つの条件が成り立って、さらに「無矛盾」なときには、
φも¬φも示せないような文φが存在する。

これが不完全性定理の内容で、大体みんなこの三つのカギ括弧内の
前提条件が成り立つと仮定してレスをしている。

一方であなたはそういうレスに対して無矛盾じゃないとφは存在しないとか、
レス毎に前提条件を二度も三度もいちいち書け、とか言ってるわけ。
たぶんあなたの基準じゃ、最初の二つは前のレスを受けた仮定として
断らなくて良いけど、「無矛盾だ」という条件だけは強調すべし、みたいなルールなのかな。
どうみても阿呆なこと言ってるのはあなたでしょ。

629と637を良く読めば最初の話が
>前提が必要だ。例えばω無矛盾性とかあるいは健全性とか。
こういう話じゃないのは一目瞭然でしょ。

具体的にはRobinsonのQを解釈できる理論じゃないと
φ⇔¬Prov(φ)は証明できないよね。

>>673
>「再帰的に公理化可能」じゃないとそもそもProv(φ)という
>述語が実際に論理式で表せないし、

そこは論点ではないからいうだけ無駄である。

>「自然数論が解釈できる」体系じゃなければ
>Godel numberingが行えないから
>やはり一般には、証明可能性を体系内で扱えない。

そこも論点ではないからいうだけ無駄である。

>この二つの条件が成り立って、さらに「無矛盾」なときには、
>φも¬φも示せないような文φが存在する。

そこが論点。

>あなたは…無矛盾じゃないとφは存在しないとか、

間違い。私はこう書いている

「¬Prov(φ)なるφの存在を証明したわけではない。 」

これはこういう意味だ。

「(φ⇔¬Prov(φ)なる)ゲーデル命題φを構成したとして、
　¬Prov（φ）がもとの体系から証明されたわけではない」

>レス毎に前提条件を二度も三度もいちいち書け、とか

これは大嘘。そのような事実はない。

私が云っているのは以下の事柄
「ゲーデル命題はあくまでφ⇔¬Prov(φ)となる命題φ。
　¬Prov(φ)は元の体系からは導けない。
　¬Prov(φ)を導くには元の体系以外の前提が必要になる。
　例えば分かりやすい例では任意のψについて
　Prov(ψ)⇒ψが成り立つとする健全性等」

>たぶんあなたの基準じゃ、最初の二つは前のレスを受けた仮定として
>断らなくて良いけど、「無矛盾だ」という条件だけは強調すべし、
>みたいなルールなのかな。

ルールの問題だと思ったことが、根本的な誤りだな。
頭を冷やせ。

いや私は

Tは再帰的に公理化可能で自然数論を解釈出来るような無矛盾な理論とするとき、
Tにはφも¬φも証明出来ないような文φが存在する……(*)

ことをGodelは示した、と言っただけで
T |- ¬Prov(φ)となるようなφが存在するなんて誰も言ってないんだけど…
敢えて言うなら>>655が一人で言ってるだけ。
>>653は(*)はTarskiの定理からすぐに出る、と言ってるだけだし、
>>650は或る体系の無矛盾性を「別の体系から」導出するような話
（例えばZFC + XでZFCのモデルを作って（ZFCが無矛盾ならば）
ZFCより真に強いことを示すとかそういう話）は今の話題ではない、と言ってるだけ。

もしかして、T |- φでない、ということとT |- ¬Prov(φ)ということを
単にあなたが混同してるだけじゃない？

> T:再帰的に公理化可能で自然数論を解釈出来るような無矛盾な理論として、
> Tからφも¬φも示せないようなφが存在するってのが第一不完全性定理だけど、

第一不完全性定理ではなくて Rosser の不完全性定理でないと正しくない。

ええと、メタなレベルの議論を出来るだけ認めたくない人なのかな？
（これこれの仮定の下）Tにはφも¬φも証明出来ない文φが存在する
じゃ不満でT |- Con(T) → ¬Prov(φ)と言わないと気が済まないとか。

うーん、謎だ。。

>>680
そらそうだけどｗ
それ現在の論点と全然違うでしょｗ
あなたも言ってるけど。ただの揚げ足取りにしか思えない。

というかただの呼び方の問題であって、
Rosserの不完全性定理のほうが単純に強いのだから
これを第一不完全性定理（の強いver.）と呼んだって
Rosserの先取権を尊重すべきだとかそういう問題を除けば別に大した問題はない。

Rosser の不完全性定理のことを「第一」不完全性定理と
呼んでいる本が一冊でもありますか？

妖怪・揚げ足取り

「第一不完全性定理」を「T |- φ⇔¬Prov(φ)となるようなφが存在する」
という主張を表すのに使って、Godelがω無矛盾のときに、Rosserが無矛盾のときに示した、
という書き方をすることはいくらでもあると思うけど。

例えば英語版wikipediaはそういう書き方。
本だと例えばcomputability & logicの第五版のp.223には
17.7 Theorem(Godel's first incompleteness theorem)
There is no consistent, complete, axiomatizable extension of Q.
となってる。ほかにも図書館で探せば結構あると思う。私はそこまではしないけど。

というか呼び方なんてどうでも良いと思うんだけどね…

他の分野じゃ、明らかにAbelやRiemannの時代には定式化されてない概念を
使って述べた定理を、彼らの名前を冠して呼んだりするんだから。

「ブーロス氏の証明した定理は私の知る不完全性定理ではない」
と書いた先生がいたのを思い出した。

>>679
>T |- ¬Prov(φ)となるようなφが存在するなんて誰も言ってないんだけど
>>650で冒頭にそう断言するべきだったね。

>もしかして、T |- φでない、ということと
>T |- ¬Prov(φ)ということを
>単にあなたが混同してるだけじゃない？

否、君が明確にステートメントを述べる能力を持っていないだけだ。

>メタなレベルの議論を出来るだけ認めたくない人なのかな？

メタの問題だと思ったことが、根本的な誤りだな。
頭を冷やせ。

言いがかりを付けたいだけの論議には飽きたんでこのへんで撤退する。

http://ja.wikipedia.org/wiki/%E9%81%B8%E6%8A%9E%E5%85%AC%E7%90%86
「選択公理よりも『弱い』公理として」とあるけれど正しいのでしょうか？
連続の定義の場合　各点連続＞一様連続＞リプシッツ連続
連結の定義なら　　　連結＞弧状連結
と右の方が強い、条件が厳しくなっていく。だったと思います。

可算選択公理というものが「選択公理の成立する範囲を可算濃度以下に限定したもの」であるなら、
選択公理よりも強い、条件が厳しいと言えるので
この場合は「強い公理」と言うののが正しいのではないのでしょうか？
それとも公理の場合は定義の場合の強い、弱いという考えとは逆になるとか、
あるいは上の連続の時とかの自分の理解が間違ってるからオカシク感じたのでしょうか？

「可算濃度以下で成立する」ことを要求するのと
「すべての濃度で成立する」ことを要求するのとどっちが厳しいか

「だったと思います」じゃ困るなー
そっちに自信ないという方が気になるぞｗ

どうもありがと。

少し慣れてきたけれど強いとか弱いとか結構混乱するもので…。

>>691
一様連続　ならば　各点連続
選択公理　ならば　可算選択公理

一般にpならばq（「not pまたはq」と同値）は、
仮定のpが強いほど、弱い命題になる。
pの前にnotが来るから反転してそうなると理解して良いと思う。

「選択公理の成立する範囲を可算濃度以下に限定したもの」じゃなくて
「少なくとも可算濃度以下のときは選択公理が成り立つ
（そうでないときに関しては何も言っていない。
成り立つのかもしれないし成り立たないのかも知れない）」でしょ。

高校あたりで教科書すっ飛ばしてるのかもね

マツシンうざすぎ

またマツシン妄想か。
どんだけマツシンに精神強＊されたんだ？

>>695
ま、「成立を仮定・要請する範囲を」なら制限・限定でいいんだけどな。

うわ
ホントにコピペどおりの習性だな>>698

---
160 名前： １３２人目の素数さん [sage] 投稿日： 2007/03/09(金) 20:50:49
マツシンという奴（か“それと同レベルの奴”）が
基礎論関係のスレには永遠に住み着いていて
こいつ（ら）と言い争いになったらスルーが基本。
マツシン（かそれと同レベルの奴）が誤りを認めることは
基本的にありえない。人工無能のように必ずレスを返して
いつまでも食い下がっては鸚鵡返しで煽り、はぐらかす。
無理に調伏しようとするとスレがぐだぐだに荒れる。

「お前マツシン並だな」と言われたときに
普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
何故か「お前はマツシン以下だな」と返す、などの習性がある。
---

>>672みたいなのはだいたいコイツのレスだってわけだ

>700
マツシン病患者が誤りを認めることは基本的にありえない。
啓蒙書しか読めず、それゆえ、啓蒙書が絶対だと信じて突っ張る。
究極の馬鹿。

>「お前マツシン並だな」と言われたときに
>普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
>何故か「お前はマツシン以下だな」と返す、などの習性がある。

マツシン並ならガマンできるところを「以下」ということで
ファビョらせることができる。実に簡単。

以下でも並でも大して変わらんよーな

意味はぜんぜん変わらんよな

誤：以下
正：未満

マツシンってのが既にバカとかゴキブリの類義語なのだから
それを基準に並だの以下など言ったところで

>>705
　マツシン：マツシン病患者
＝ゴキブリ：黴菌
といった感じか。

test

>>672は特徴的だよね
基礎論のスレでこの手の変な逃げ（書いた本人は切り返しだと思ってる？）は
昔からよく目にする
他のスレと違って独特

マツシンタンは変わんないでつね

>>708は特徴的だよね
完全に切られた首で変な強がりを口にするのは
昔からよく目にする
他の人と違っていかにも狂ってる

すまんが、誰か、Combinator Logicsの初歩がわかりやすく書いてあるサイト（英語または日本語）
教えてくれんか。たのむ。

間が空いてしまってすみません！
なんかいつの間にやら話が進んでしまっているようで申し訳ないです。

>>629
＞φを証明するとφが真であることを証明するの違い
うーん、難しいです。
どちらも　公理系→φ　ということとは違うのでしょうか…

Matsushin 痰（こと松本真吾＠鉄道総総合研究所
http://www.rtri.or.jp/index_J.html）に告ぐ

今からでも、決して、遅くはない。

投降せよ。（御大 宛に E-mail（宛先：[email protected]）で詫び状を送れ！）
さもなくば、酷い目に逢うぞぁ〜〜〜〜！！！！。

これは冗談ではないぞぉ〜〜〜〜！

俺からも恩大に頼んでやる。

お前の身を案じて、こんなことを書いてるんだぞ！！！！

元賊軍兵士（いち早く、官軍に投降すますたＷ）

お前は卑劣奸だ！！！　そんな者に誰がついてくる門下！

お前は、「NewYork_Academy_of_Sciencesなど、金さえ払えば誰でも
入れる」とかなんとか言って、恩大ならびに NewYork_Academy_of_Sciences
の名誉を著しく毀損しただろう。　違うか？！！！！！！！！！

恩大の場合はだな、先方（＝NewYork_Academy_of_Sciences）のほうから
是非会員になって下さいとの丁重な案内状が届いたのでそうされたのだゾ。

何でそんなことを知っているのか聞きたいか？　教えてやろう、恩大に
メールを送って俺は尋ねたのだ。

ここはどろどろした論理のｽﾚですね

>>713
今のヒトは、御大なんて知らんだろ。

それはともかくニューヨーク科学アカデミーは
ホームページでも会員募集の宣伝してるんだが。

ttp://www.nyas.org/membership/main.asp

質問来てるんだからコテ談義なんてしてないで答えてやれよw

>>712
＞＞φを証明するとφが真であることを証明するの違い
＞うーん、難しいです。
＞どちらも　公理系→φ　ということとは違うのでしょうか…

違います。
全ての意味づけでφが真であること
公理系からφが証明できること
それぞれが別のことです。

完全性定理が成立する場合は結果的には同値だけどまあ同じじゃないよね。

ありがとうございます。
>>717
うーん……φが真であることを証明できるは公理系を充足するようなモデルを作ってみて
どんな風に作ってもそのモデルでφに相当する式は真になっているということで、
φが証明できるは単純に公理系→φが示せるということ……ですか？
>>718
ということは普通の論理を使っている限りは気にしなくていいということでしょうか？

test

‖-とか｜=ってどういう意味ですか？

forceとmodels

過疎だな

集合論では
>x1 ∋ x2 ∋ x3 ∋ ...... ∋ xn ∋ ....... なる無限列が存在する
モデルがあるそうですが、
http://www.iis.it-hiroshima.ac.jp/~ohkawa/math/math_problem_all.htm#101
これはどうなんでしょうか？

すみません、>>719はあってますか？

それは 無限列 だけど *無限列 ではないということはわかる？

超積理論は兎も角、モデルである事には間違いないよね。

＞φが真であることを証明できるは公理系を充足するようなモデルを作ってみて
＞どんな風に作ってもそのモデルでφに相当する式は真になっているということで、

間違ってます。
思いつき口にせず、自分で勉強してください。

>>728
後半はあってますか？

>>728
まず、専門書を読んで確認してください。
専門書が読めないなら諦めなさい。

>>728

だから、失業率の問題を議論させないための目くらましだったと考えるとスッキリしないか？ 
俺なら教科書（「団結」ってタイトル）の28ページを熟読するけどな。 

>>719
きちんと「φが真」の定義を勉強しないと簡単に間違いますよ。
その例が>>724の問題とかSkolemの逆理とかだと思う。

>>724
compact性定理使ってもすぐに出るけどね。
モデルの中の概念と外の概念を区別しないといけないってのが大事だと思う。

しかしそのページの著者の人はなんか集合論とかきちんとした論理学は全然知らないみたいな書き方だね。
多分超準解析の本を読んだことがあるとかそういうことだろうね。

＞通常の集合論（例えば有限集合論）では　 x1 ∋ x2 ∋ x3 ∋ ...... ∋ xn 　なる有限列は取れる。
通常の集合論（例えば有限集合論）って何のことなんだろう……？

＞しかしこれは矛盾ではない。（中略）
＞上記事実は、第２階、或いは階数を超えた「人間の全ての思考」のレベルで述べられた物だからである。
とかまるでDedekindの時代の数学者みたいな物言いだし。

＞だから可算無限濃度と連続体の濃度の中間の濃度が見つかっても、何らこれまでの数学に矛盾する物ではない。
とか……
これはもしかして連続体仮説の否定が真となるモデルが存在しても
矛盾じゃないって言いたいんだろうか？とてもそうは取れないけど。

>まるでDedekindの時代の数学者みたいな物言いだし。
数学は専門分化し、沢山の高度な結果が得られたが、
基礎的な考え方はDedekindの時代からどの程度進化したのだろうか？

本を読めよ

問いかけのつもりで教えて君になってしまっている

ここでいいのかよくわからないんだけど、
Dedekind流の無限定義とPeano流の無限定義ってどう違うの？

授業の課題が全く太刀打ちできずお手上げなので、アドバイスください

二次元射影空間RP2から小さな開円板Dを除くとメービウスの帯になることを説明せよ

あと、当方数学科の初年級なんですが、幾何の分野は今から学んでおくべきですか？

>>738
それ基礎論じゃないよ

>>739
スレチですか。すいませんでした。
どのスレが適当ですか？

>>740
わからない問題スレとかでいいんじゃないの？

>>741
�dクスです
いってみます

他分野専攻の人ならともかく数学専攻なら基礎論くらいは知ってるものじゃないのか？
これがゆとり教育の産物なのか…

俺は基礎論の存在を知ったのは大学二年の時だな

>>744　
健全だ（ｗ

漏れは中３のころに「数学から超数学へ」という本を
うっかり読んでしまってから、ダークサイドに堕ちたｗ

>>737
Dedekind流の有限定義はPeano流の有限定義と同値だがDedekind有限の定義とは異なる

>>746は選出公理が無いとき

>>747
選択公理を否定すれば同値でない事が示されるのか？

>>748
もち

有限の定義ってどんなのあったっけ？
i) 整列且つ、逆整列な全順序が存在する。
ii) 空集合であるか、または自分自身の真部分集合と対等でない・・・

「空でない任意の真部分集合Aに対しf(A)がAの部分集合にならない」ような自身への写像fがある。

俺は32歳
最近ゲーデルやチューリングに興味を持った
これから基礎論に取り組む
よろしく

こちらこそよろしく

物理屋ですが数学もぼちぼち勉強してます。

「ブルバキとグロタンディーク」日経ＢＰ社　を読んだら、数学の基礎はいまや集合ではなく
圏論というものであり、ブルバキも集合論ではなく圏論を基礎にして書き直すべきだった
みたく書いてあります。ところが同じ本で圏論は集合論や代数、位相幾何などの
上部構造（下部ではなく）とあり、混乱しました。
圏論ってのは集合みたく高校教科書に載せる事ができるような基本的概念なんでしょうか。

物理屋なら集合論なんて勉強しないほうがいいよ。
物理ができなくなるよ。

勉強といってもリーマン多様体や線形Lie群程度です。基礎論は趣味で一般向けの本を読む程度。
ただ、多様体も群も集合を基礎にしてるんで集合よりも基礎的（？）な圏論てなものがあると
聞いて驚いたんで聞いてみました。

>>756
圏論は構造を調べるときの視点をちょっと変えて、見通しをよくしてるんだよ。
要素中心で行くか、射中心でいくかみたいな。

>>746-747
thx.
Axiom of Choice by Horst Herrlichでも買ってきて、ちょっと違いを考えてみます。

チューリングマシンもピンと来ない。
「有限回で終了する」なる概念の厳密な定義がない。

>>757
視点の変更は重要だ。
存在論を取っ払ったわけだから。

「ブルバキとグロタンディーク」では圏論は物理での相対論に比肩するほど革新的で
有用なアイデアとのことだったので、jp.wikipedia.orgを読んでみたのですが、
えらく抽象的な感じでどう有用なのかさっぱりでした。準同型みたいな写像に
注目するのかな、てな程度で。
（特殊相対論は高校程度の知識で理解できるのでちょっと期待したのですが）

文献として「圏論の基礎」という本を挙げてありましたが、やはり代数幾何とかの
ある程度高度な数学的知識がないと理解できないと思ったほうがよいでしょうか。

>>760
「取っ払った」わけじゃないでしょ。有用ではあるだろうけどね。
実際に集合の概念無しで例えば実解析とかが展開できるわけじゃないでしょ。
集合論的な構成為しで代数的閉包の存在だとかが仮定できたりするわけでもない。

或る程度知識が無いと理解しづらいだろうけど、例えば情報科学でも
圏論は利用されたりしてるので、別に「代数幾何とかのある程度
高度な数学的知識」が必要なわけでもないかと。

で、大学一円程度の線形代数とかでいいの？

>>762
>例えば情報科学でも圏論は利用されたりしてるので

検索したらこういう本もありました。図書館で見てみます。
ありがとうございました。

Basic Category Theory for Computer Scientists (Foundations of Computing) Benjamin C. Pierce (ペーパーバック - 1991/8/7)

圏論による論理学―高階論理とトポス 清水 義夫

昨日書店に行ったら清水氏の圏本が数学のコーナーじゃなく思想のコーナーに置いてあった

>>764
algol N作ってたYonedaせんせのlemmaは圏論の本に出まくりでそ
ttp://www.chimaira.org/img/yoneda-nobuo.gif

>>761
そんなに心配なら、F. W. Lawvereの"Conceputual Mathematics: A first introduction to categories"。
小学生でも読破可。

>>759
Hoare logicはやったのか？

>>762
キミがしがみついてるだけ。
例えば実解析が集合論なしに展開されていないのは
実解析の理論が後進的だから。他についても同じ。

存在は無用だ。

カテゴリーを数学の基礎付けに使おうとするのは、歴史的には
全く無理。可能だというだけで、もともと集合概念の方が、
論理とのつながりがよいのだから、カテゴリーは基礎付けなど
に使わないで、数学のなかで使うのがまともだ。

>>769
＞実解析の理論が後進的だから。
そうじゃなくて、圏論がそもそも（少なくとも現時点では）
数学全体の基礎付けに充分ではないということじゃないの。

集合論的な独立命題に影響を受けやすい分野を「後進的」と呼んでいるようだけど
そういう分野はいくら発展しようと分野の特性上「後進的」のままになってしまう。
先進的とか後進的という進歩に関する言葉を使うのは明らかに間違い。

函数解析だとか確率論だとかそういう分野を全て無用、後進的という言葉のもとに
捨て去るような態度がまともなわけがない。個人的な嗜好の問題に留めておくべき。

＞集合論的な独立命題に影響を受けやすい分野を
＞「後進的」と呼んでいるようだけど

そうではないよ。
集合論以外の枠組みについて考えてない点が「後進的」ってことさ。
日本語が読めないと数学も学べないよ。

独自定義で悦に入って日本語も何もない

>>773
そもそも「後進的」という用語は数学用語ではないがｗ
いずれにしても771が文章を読めなかったという事実だけが残る。

>>774
一般用語として解釈して、独自用語だと言われているのに気付かない
「日本語が理解できてない」なんてお前が言っても説得力皆無

法学じゃないんだから、数学で歴史的由来を持ち出すのは無理があるなあ。
論理とのつながりでいえば、集合もToposもどっちもどっち。
どちらかといえば、集合が古典論理よりでToposが直観主義論理よりなだけ。
実解析関連に関しては、直観主義的な実数（実様体だっけ）の問題で、
直観主義的集合論でやっても難しさは変わらないと思う。

おいおい、まさか772は
代数的位相幾何などでは圏論が有用
（これも別に集合論無しで展開出来る、という意味ではない）なのは
集合論以外の枠組みについて（位相幾何学者が）ちゃんと考えたからだ、
実解析学なんかで圏論が役に立たないのは解析学者が
集合論以外の枠組みについて考えなかったからだ、と言いたいわけ？

今日、本屋に行ったらこれを見つけた　ノ

http://www.amazon.co.jp/dp/4535783829/

「数学基礎論へのいざない」(倉田令二朗著)は、基礎論をゼロから学ぶのに適しているのでしょうか？
演繹定理を"すぐわかる"と流しているあたり、個人的にはあまりやさしくないように思います。
集合と位相は履修した学部生です。

それなりに良い本だと思いますよ。ただ「いざない」は、
たった160頁で不完全性定理と連続体仮説の独立性の話を紹介しようという
かなり「欲張った」本だから証明をちょっと省略したりしてるのは仕方の無いことかと。

私は最初にこの本で勉強しました。
本棚探しても無いので図書館で借りて読んだんでしょうけど。

ちなみに「数学基礎論講義」の演繹定理の証明も述語論理の場合に
「命題論理の場合と同様」とか言って一部流してたりします。

「いざない」と同じシリーズの「入門数学基礎論」のほうは、きちんと書いてあります。
演繹定理もきちんと命題論理の場合と述語論理の場合に分けて三、四頁は使って証明してあるし、
LKとHilbert styleの公理系が等価であることをわざわざ両方向の証明を書き下したりと
ものすごくガチガチに書いてあります。カット除去定理の証明とかも載っている。

細部は飛ばして全体の感じを掴みたいなら「いざない」、
隙間の無いガチガチな書き方が好きなら「入門数学基礎論」を読むと良いと思う。
まあ別の本でも良いんですけどね。

>>780
丁寧なお返事ありがとうございます。
0巻と称していたのはそれが理由なんですね。
全体をつかんでから、1巻に入りたいと思います。

倉田（故人）

このシリーズなかなか手に入らないんだよね・・
（今、本屋で買えるのは「モデルの理論」と「逆数学と２階算術」だけ）

自分の読んでる奴は、明○館で見つけてきた奴だ

自然数のみを含む集合の存在を示すためには、BGの公理のうち、最低どれだけの公理が必要ですか？

例えば{0,1,2,3}なんてのは自然数のみを含む集合だけど、
そうじゃなくてωのことを言ってるんだよね、たぶん。

定式化の仕方にも拠るだろうけど、
無限公理と分出公理あたりがあれば大体大丈夫じゃない？
外延性公理を使ってるかどうかは微妙。自分で確かめて。

ゲーデルの原論文が文庫で読めるってすごいことだと思うんですが
基礎論は知らないけど、数学は学部レベルは理解してる人がその文庫だけ
読んで理解することは可能でしょうか？

どの文庫でどの原論文のことか不明なことには答えようがない

岩波から出てるやつじゃないか？
いきなりあれを読んでも、理解したつもりってくらいにしかなれないと思う
あれを読む前に一階述語論理の初歩を勉強したほうがいい

日本語の文庫で出てるGodelの原論文は多分一つしかないと思うけどね。
文庫でなければ邦訳のある論文とか講演はいくつかあるけど。

あの岩波文庫の原論文だけ読んでも理解は難しいと思うけど
後ろに解説がついてるから、一応の大雑把な内容は解説を読んで理解できるとは思う。
寧ろHilbert計画と不変式論の関わりとかに重点を置いて書かれた本なので、
歴史的経緯にあまり興味が無くて不完全性定理本体の数学的内容の理解がしたいのならお勧めしません。
というかそもそもPrincipia Mathematicaの公理系の説明とかきちんと書いてなかったような。
code化はきちんとやってるからそこから類推は出来るかもしれないけど。

本体の内容を日本語で理解するには何を読めばいいですか？

現代的なのは「数学基礎論講義」（絶版）とか
ゲーデルと20世紀の論理学の第三巻とか。
洋書で良いならComputability & Logicとか
SmullyanのG&omul;del's Incompleteness Theoremsとか。
但しゲーデルと20世紀の論理学の三巻とSmullyanは
一階の述語論理について或る程度分かっていることが前提。

前原昭二の数学基礎論入門は古い本で、
ほぼ原論文に沿った形で型理論に対して不完全性定理を証明している。

G&omul;del's→ö

洋書の数理論理学の入門書なら結構不完全性定理についてきちんと書いてあるのが多いよ。

友人が行っている文系院の部屋を訪ねた際、そこの教授（考古学・歴史学）に
「数学基礎論やガロア理論、フェルマーの定理を理解するにはまず何をするべきだろうか」
と聞かれた。当人はどうもベクトルや複素数のことを前提知識と考えているようでちょっと回答に窮した。
その教授は歴史上の学者に関しての論文を今まとめているらしいが、数学や物理の難解理論が分からんから人物の凄さも分からんとのこと。
来週もまた尋ねるんだが、おまいらなら何と答えますよ？教授は高校数学(�VC)までは理解している。

>>793
ブルバキ一式持っていってぶつけてやったら？

なんだそりゃ
どこの星の考古学・歴史学だよ

ガロア理論はアルティンでいいのでは？
数学基礎論はゲーデルと２０世紀で分かりそうなところを
読んでもらって、フェルマーは諦めてもらうのが手頃では。

ところで（私は基礎論に素人の数学専攻ですが）、ゲーデルと２０世紀は
どの巻も二つ目がよく書けてる気がするのは気のせいでしょうか？

某巻の三つ目に、あまりにひどいミスぷりがあるのは私の本だけ
なのだろうか。幾ら何でも素人編集者でも気付くべきだと思ったのですが。

>>791
ありがとうございます。
Computability and Logic/ Boolos, Burgess, Jeffrey (Paperback)
$29.99
が名著とされているようですね。値段も安いです。

無作為抽出法の計算で

起点数が10
信頼水準（1-α)＝0.99（信頼係数2.58）
N=10000
抽出誤差5％

コレの調査対象の数を求める計算が判らん

計画数理って強化なんだが
スレチだったらスマン

「数学や物理の難解理論が分からんから人物の凄さも分からん」
ってのは素直で良いと思うけどな。

理論をまともに理解しようと思ったら、
相当な時間が根気が必要だということをまず伝えないといけない。

ロジックの部分に限って言うなら、他の分野の知識が無くてもあまり困らないので
入門書をいくらか読んで研究の歴史的動機を他の本で勉強すればどうにかなるかも。
実際に哲学専攻の一部の人は基礎論には滅茶苦茶詳しかったりすることもある。
取り敢えず「歴史上の人物」が誰かによって少々違うけどゲーデルなら
廣瀬・横田の「ゲーデルの世界」とか「確かさを求めて」とか。
あとFrom Frege to Godelとかが歴史的な研究という観点からは良い本。

FLTを「その証明まで」理解するには数論とか代数幾何専攻の大学院生と
ほぼ同等の勉強が必要になるから常識的に考えて無理だというしかない。
おそらく通俗的な解説本を読んでお茶を濁すことになる。
歴史的経緯ということなら「フェルマーの最終定理13講」とかが良いのかな。
ただ、コラッツやゴールドバッハが偉大な数学者とは言われないのと同じ理由で
FLTを予想したということは別にフェルマーの主要な業績じゃないと思うけどね。

スレタイを変えたら変えたで「基礎論」という呼び方しか知らない人が迷うわけか……

「二つ目」ってのは序論を除いて第二部のことかな？
一巻は田中尚夫の第一部も結構面白いことが書いてある。
他の巻は、第一部が基礎の解説、第二部が発展的事項の紹介、
第三部が哲学の話というのが基本っぽいので
第二部をありがたく感じるってことじゃないかな。

＞某巻の三つ目に、あまりにひどいミスぷりがある
ってのは何のことかな。まあ記述集合論を可述的集合論と訳すような
ものすごいミスじゃない限り無問題かとｗ

>>798
質問スレか統計のスレへgo

質問です

基礎論の人の論文は、他の数学分野の論文に比べる平均的に
短い傾向にあるように思われるのですが、なぜなんでしょうか？

二巻に、うつらうつらとして打ってしまったんじゃないかと
おぼしきランダムな文字列があるな。

色々ありがとう。上で挙げてくれたのや図書館にある分を持っていくわ。
まあ本の虫でかつ研究職だけあって研究心は異常なんで、教えれるところは教えたい。

しかし国立大学の図書館はいいな。蔵書数のケタが違う。

記号くらい分かっててくれないと「この定理ってどういうことなの？」なんて言われてもねえ・・・
野球を知らない人にイチローのプレーの凄さを説くようなもんだ。

文系ってやっぱり数学科なんかが何やってるのか意味不明らしいな。
幾何学とか面体とか名前からして。

へー

Fermat予想 1・2と、これを読むのに必要な予備知識を纏めた本を
全部リストアップして持ってくってのもネタとしては良いかも。
ブルバキ一式持ってくより余程インパクトがあるかとｗ

分野が違うとはいえ、研究者ならそういう説明の困難さは想像がつかないもんかね
こっちが>>793から勝手に想像してしまってるのかもしれんが

>>807
前提知識を知りたがってるのにいきなりそれはどうなんだｗ

>>808
説明を聞いても何を読んでも分からんだろうから、何をすべきだろう的な感じだった。
大学教授なんて知ったかの塊なんで、ずいぶんと真摯な態度だな、とか偉そうに思ってしまった。

俺の知ってるうちでは大学教授に
知ったかの塊みたいな人ってあんまいないんだけど

>>793
小野孝の数論序説と足立恒雄のフェルマーの大定理
廣瀬・横田の「ゲーデルの世界」とりあえずこの三冊をもっていったら？

廣瀬・横田の「ゲーデルの世界」って古い本だから
内容に細かいミスがあったり、うまくストーリーが
繋がらないところとかがあったりするから短所の無い本、というわけではないけどね。

ゲーデル（不完全性定理）に興味があるけど本を買うのはちょっとという人は
以下のサイトをみてみるといい。
下のほうで述語論理を学んで、上のほうでゲーデルも含めて一階論理が
扱われている。

http://www.phil.gu.se/posters/first-order-logic.pdf#search='first%20order%20logic'
http://research.nii.ac.jp/~terui/mita06.pdf

でもまぁ、不完全性定理は証明を理解するのはさほど難しくないのに
解説書や解説サイトは山のようにあるよね。

いろいろ見て回ったけど、結局やっぱり原論文だけでいいやってなってしまった。
シンプル、かつ厳密、やや冗長のきらいはあるがそのぶん誤解を生みにくい。

不完全性定理は照井先生のページにそれだけを書いたpdfが公開されてるね。
Simpsonのホームページにある論理学の講義ノートとかも良さげ。

再帰関数とか決定不可能問題の話を勉強したいのですが、
おすすめがあれば教えて下さい。

今月の日経サイエンスの記事(2008年4月-多世界から生まれた計算機)に衝撃を受けたんですが、誰か噛み砕いて優しく書いて本にしてもらえないですか？

１．計算は物理操作である、紙の上に書いても脳で行っても、記号操作は、物理操作と表裏一体
２．物理操作の基本は量子力学にあるに違いない
３．チューリングマシンは古典力学に基づいて作られている
４．量子コンピュータを考えると量子チューリングマシンも考えられる
５．量子チューリングマシンの基本操作でできる事は、チューリングマシンを拡張している

チューリングマシンは拡張可能→数学も拡張される？

>>817
情報板池

>>818
それを認めたら数学基礎論なんて数学じゃないし、板違いになる。

>>816
何も知らないなら一冊目にはこれがおすすめ
大学の一回生でも絶対に最後まで読める

ttp://www.amazon.co.jp/dp/4316376209/

で、同じ著者のこの本は評判が良いので（この間復刊された本）
次にこれを読むのはどうだろう

ttp://www.amazon.co.jp/dp/4254116608/

> 本にしてもらえないですか？

／(＾o＾)＼

>>819
いやいや、どんな偏見を持ってるのか知らんけど集合論もモデル理論も数学だろ。
量子計算機の話題は普通は数学よりも物理よりの話題ってことになってると思うけど。

>>816
そっち方面の定番として良く知られてる洋書の専門書はいくつかあるみたいだけど
最初はもっと軽めの本で始めたほうが良いだろうなあ。

「計算論入門」渡辺 治、米崎 直樹
が参考文献に挙げられてるのを見たことがある。まともに読んだことないので中身は知りません。
あと「帰納的関数と述語」篠田寿一とかかな。もう本屋には売ってないけど。

数学基礎論の先には何もないんやろかねー

なんだかつかみどころのないレスが増えたな

>>820
でも広瀬 健ってめんどくさい証明はすぐ省略する癖があるよねえ。

>>817
量子計算可能=計算可能
だったはずだが

どうもありがとうございます。

英語の定番の本も良ければ教えて頂ければ参考にしたいです。

現在持っている予備知識は「ゲーデルと２０世紀」の三巻
不完全生定理の章と竹内外史「語の問題」の２章までです。

>>822
たぶん「情報板」が変だって言いたいなんだと思うよ
実際基礎論って情報系の学部に追い出されてない？

情報系の方が基礎論に出せる資金を持ってるだけだろ。

>>826
肝心なところは、計算可能とかそんな所じゃなくて、数学は物理から分離独立できないと思われるところだと思った。

右手座標系と左手座標系がある時、左手右手を同時に考えずに右手座標系を定義してみろってぐらいに、物理と数学は分離できないに違いないと思う。

下手な例えだな

なんでもカンデモ量子つければ売れると思っている文屋がいるな？
量子構造の定義からちゃんとやってくれよ。

>>793とかで思い出したが、
Wikipedia - 数学
http://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6
とかの項目にあるようなのが一体何物なのかをを素人にすら分かるように解説した本ってなかったっけ？

>>796
連続体「仮設」のこと?
帯までそうなっていたね。

continuum hypothesisのことを連続体「仮設」という風に書くのは
単なる誤字、誤訳である場合が多いけど、
例えば志賀浩二なんかは、「集合への30講」とか「無限への飛翔」
なんかで連続体「仮設」という言葉を意図的に使っているみたい。

個人的にはあくまでもhypothesisのほうが良いんじゃないかと思うけどね。

>>833
でもね、最近基礎論が実は近似なんじゃないか(<-なんじゃそりゃと思われるかもしれないが)という気もしなくもない

基礎論は言葉の遊びではござらぬ

「仮設」のこと？

>>837
近似にきまってんじゃねーの？それとも永久不変の真実だって？

２巻の１２４ページのことじゃない？

>>793
＞「数学基礎論やガロア理論、フェルマーの定理を理解するにはまず何をするべきだろうか」

大学の理学部数学科に入って卒業するまで４年間勉強すること。

＞数学や物理の難解理論が分からんから人物の凄さも分からん

成果は凄いが、別に人物は凄くない。
まあ、理解できないのなら、
「数学者や物理学者なんてただのワケワカラン奴だ」
と書いていただいて構わない。
数学や物理が理解できない人に口先だけ褒められても不愉快だ。
だいたい人に褒められたがる奴は精神をわずらってるから入院すべき。

sub(add(x,1),1)=恒等関数(f(x)とする)・・・※　sub(x,y):x-y ,add(x,y):x+y
※を示すためには、どうすればいいですか？
∀x∈R,(sub(add(x,1),1)=f(x))・・・�@
(sub(add(x,1),1)の定義域)=(f(x)の定義域)・・・�A
�@∧�Aを示さずに※を示す方法はありますか？

>>843
どういう体系での証明を考えてるのかよくわからないんだけど。

＞「数学基礎論やガロア理論、フェルマーの定理を理解するにはまず何をするべきだろうか」

＞大学の理学部数学科に入って卒業するまで４年間勉強すること。

そしてそれでもFLTの証明は後姿すら見えないほど遠い位置にいることを
わからせること。

>>843
λ式でやってみたら？

てかstandard L_Ω structureの話かな？

>>793
どうしてまともな質問よりこのような話にレスが多くつくのだろうか・・・。

まともな質問は一度は誰もが通る道なので、
じっくり悩んだほうがいいという場合が多いから
だと思われる。
あるいは内容によっては一言で済むってことも。

>>846
すみません、教えてもらえないでしょうか？

>>850
SUCC := λ n f x. f (n f x)
PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)

reductionをやって
(PRED)(SUCC)=λ x. x
になるのを確かめれば良い。

ttp://www.mscs.dal.ca/~selinger/papers.html#lambdanotes
これみてがんばれ。

>>851
(1/2)(x+1)^2-xの導関数を求めよ、という問題なんですが
D{λx.(1/2)(x+1)^2-x}=(x+1)-1=xとなりますよね。
この変形は、別の証明方法があるということは、
∀x∈R,(sub(add(x,1),1)=f(x))
(sub(add(x,1),1)の定義域)=(f(x)の定義域)
などを省略しているというわけではないということですか？

>>852
あ、ごめん。
自然数の演算の話かと思ったよ。
普通に微分してxでいいんじゃね？
dom, codomが気になるの？
ちなみにuntyped lambdaだから域なんて考えてないよ。

>>853
はい、定義域や値域(始域や終域)が一致してるかどうかを無視しているのが
きになって。関数を等号で結んでいるのに、域を無視していいのでしょうか？

>>854
でも（高校数学っぽい）微分とか言ってるから、暗黙に実関数の話なんでしょ？
関数のequalityが気になるのなら、関数をbinary relationに置き換えてみて、
R^2の部分集合として同じになるのをチェックしてみたら？

>>855
始域終域定義域値域が全てＲであるということを前提としているということですか？
では、サイコロをn回振って1が１回以上出る確率をp(n)を求める時
p(n)=1-(1/6)^n=(6^n-1)/(6^n)という変形における関数のequalityでは
始域終域定義域値域全てＮであることを前提とするんですかね？

>>856
だから、論理展開している前提条件(context)によるんじゃないの？

>>856
あとね、855で集合的に考えてみたらって書いたのは、
域とか関係なしで、外延性公理でもつかって、納得したらってのもあったんだけどね。

>>857
この問題を解くとき、どのような論理展開をするのが一般的でしょうか？
域を全てＮとして関数のequaliyで攻めるのか、全称記号を使って数値のequality
で攻めるのか
>>858
グラフの一致は外延性公理でいけますが、
関数の一致には、グラフの一致＋域の域の一致を考慮に入れる必要があるような気がして。。

んー、頭痛くなって来た。
だれかバトンタッチpls.
ｵﾚは遁走する。

もっと文脈がわからんとどんな説明が欲しいんだか想像しにくいなあ

どうせ最近あちこちのスレを荒らしてる電波くんだろ、
もまいらスルーしる

>>861
856の確率の問題を立てるとき、
λn.p(n)=λn.1-(1/6)^n∧λn.p(n)=λn.(6^n-1)/(6^n)と関数のequalityか
∀n.p(n)=1-(1/6)^n∧∀n.p(n)=(6^n-1)/(6^n)と数値のequalityか
どちらの論理展開をすればよいかが分かりません。前者の場合は、域を
考慮に入れないといけない分、後者に比べて無駄なことをしてる気がするのですが。