数学基礎論の質問スレッド その３
レス数が1000を超えています。これ以上書き込みはできません。
0001１３２人目の素数さん
2007/02/04(日) 19:22:390002にょにょ ◆yxpks8XH5Y
2007/02/04(日) 19:24:46今だ！2ｹﾞｯﾄｫｵ
￣￣￣￣￣∨￣￣￣ (´´
∧∧ ) (´⌒(´
⊂（ﾟДﾟ⊂⌒｀つ≡≡≡(´⌒;;;≡≡≡
￣￣ (´⌒(´⌒;;
ｽﾞｻﾞｰｰｰｰｰｯ
0003１３２人目の素数さん
2007/02/04(日) 19:59:49濃度の比較可能定理⇔AC
0004１３２人目の素数さん
2007/02/04(日) 20:07:54こんなスレを立ててくれたんだからな。
スペイン語で数字の「５」のことを「Cinco」って言うんだ。
OK、あぁ、わかってる。
お前のことだからとりあえずチンコを連想しただろ？
読み方をカタカナで表すとシンコって感じなんだが、
まぁ、今はそんなことどうだっていいんだ。
いいか、よく聞け。
これからは２ゲットの時代じゃなく、５に Cinco って書くことが流行る。
そう、５に合わせてただ Cinco とだけ書くんだ。
読み方のわからない厨房はチンコを連想するだろ？
まさにそれが狙いなんだ。
頭のいいお前には「５」ってことがわかるが、厨房には「チンコ」だ。
わかるか？それがお前と厨房の差なんだ。
これからはそうやって５をゲットすることでお前のすごさを見せ付けてほしい。
↓さぁ！
0005にょにょ ◆yxpks8XH5Y
2007/02/04(日) 20:10:510006１３２人目の素数さん
2007/02/04(日) 20:11:100007１３２人目の素数さん
2007/02/04(日) 20:38:560008１３２人目の素数さん
2007/02/04(日) 22:51:30116 名前：１３２人目の素数さん[sage] 投稿日：2006/05/12(金) 12:15:28
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野で、
非古典論理、証明論、構成的数学、モデル論や意味論、集合論、計算論
などの分野群の総称です
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何（Hrushovskらiによる研究）などを含み、多岐にわたります
（cf. 数学セミナー98年6月号、「数学基礎論の学び方」）
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります
他のスレで御質問なさるようにお願いします
0009１３２人目の素数さん
2007/02/05(月) 00:14:12前スレ958で修正されてたバージョンの方が良かったのでは
0011１３２人目の素数さん
2007/02/05(月) 21:03:22数学基礎論の質問スレッド その２
http://science5.2ch.net/test/read.cgi/math/1143943264/
数学基礎論の質問スレッド
http://science4.2ch.net/test/read.cgi/math/1097659610/
0012１３２人目の素数さん
2007/02/07(水) 21:55:430013（ ^ω^）
2007/02/08(木) 23:35:00これから読むお（ ^ω^）
0014１３２人目の素数さん
2007/02/09(金) 00:13:51一緒に読も
0015１３２人目の素数さん
2007/02/11(日) 10:08:240016１３２人目の素数さん
2007/02/11(日) 23:15:540017１３２人目の素数さん
2007/02/12(月) 06:46:40独語ではGrundlagen der Mathematikで、同名のHilbertとBernaysによる著書が
1939年に出版されていて、日本語の抄訳がSpringerから「数学の基礎」の題名で出ている。
いつ誰が分野名として「Grundlagen der Mathematik」という言葉を使ったのが最初か、
誰が「数学基礎論」と命名したのかはちょっと謎。
上のHilbert/Bernaysが起源となっている可能性も高いと思うけど、
きちんと調べて見ないと自信持って答えられないんじゃないかな。
「キソロン」みたいな語感は日本に特有だと思う。
英語名だともっと「数学の基礎（付け）」って感じじゃないかな。
分野名としても使われてる言葉だとは思うけど。
0018１３２人目の素数さん
2007/02/14(水) 14:54:090019１３２人目の素数さん
2007/02/15(木) 09:56:480020１３２人目の素数さん
2007/02/15(木) 10:57:460021１３２人目の素数さん
2007/02/15(木) 11:17:52具体的に論文とかありますかね
0022１３２人目の素数さん
2007/02/15(木) 19:44:420023１３２人目の素数さん
2007/02/15(木) 20:37:160024１３２人目の素数さん
2007/02/15(木) 20:41:420025１３２人目の素数さん
2007/02/15(木) 21:27:58ありがとうございます。さがしてみます
0026１３２人目の素数さん
2007/02/15(木) 21:49:050027１３２人目の素数さん
2007/02/16(金) 18:09:560028１３２人目の素数さん
2007/02/16(金) 21:14:360029１３２人目の素数さん
2007/02/17(土) 20:42:040030１３２人目の素数さん
2007/02/18(日) 10:15:45ある物体oに曜日の設定を１つしたい場合
week(o) = {mon, tue, wen, thu, fri, sat, sun}
とすると７つとも設定すると言う意味でしょうか？
∨などを曜日の略記の間に挟んだりしなければならないのですか？
宜しくお願いします。
0031１３２人目の素数さん
2007/02/18(日) 10:41:010032１３２人目の素数さん
2007/02/18(日) 10:53:01week関数に曜日を設定する定義式の書き方です。
weekは・・・ああー自決しました。頭悪かったです。
失礼しました。
0033１３２人目の素数さん
2007/02/18(日) 11:09:430034１３２人目の素数さん
2007/02/18(日) 15:59:05あげくに首つったか腹掻っ捌いたか知らんが自決とは……
何、いまどきの日本人ってこんなに低レベルなんだっけ？
0035１３２人目の素数さん
2007/02/18(日) 18:03:58重要かつ興味深い結果って何か出てるんですか？
0036１３２人目の素数さん
2007/02/18(日) 19:58:280037１３２人目の素数さん
2007/02/18(日) 20:21:060038１３２人目の素数さん
2007/02/18(日) 22:42:45Lowenheim-Skolemの定理（実数論の可算モデルを作ったり出来る）とか、
証明論ならcut除去定理とか、集合論を含めるならCohenのforcingとか。
それにプログラミングが好きならCurry-Howardとかも興味深いだろうし
さらに人によっては自然数論とか「解析」の無矛盾性証明が興味深くて重要かもしれないし。
>>36>>37にだいたい同意。
不完全性定理のインパクトの強さは人による。
完全性定理に匹敵する結果が無いって事はないんじゃないかなあ。
0039１３２人目の素数さん
2007/02/18(日) 23:06:53証明論だと巨大基数類似可算順序数を利用した数学の無矛盾性プログラムなんてのもある。
0040１３２人目の素数さん
2007/02/19(月) 00:17:52病院にいる花京院の魂を賭けるぜ
0041１３２人目の素数さん
2007/02/19(月) 00:46:320042１３２人目の素数さん
2007/02/19(月) 03:49:01人によって違うのはそうだけど、基礎論に与えた影響という意味で重要性を測るとしたら、
不完全性定理に比べたら、cut除去定理とか自然数論の無矛盾性とかかなり見劣りするように思う。
0043１３２人目の素数さん
2007/02/19(月) 08:10:36だけど「証明や反証できるのはラッキーな場合だけで、いつもそんなにうまくいくはずがない」と思ってる人とか、更には「そもそも命題が真か偽かどちらかだという考えがおかしい。」という直観主義者にとっては不完全性定理なんて「ふうん。当たり前じゃん」で終わり。
0044１３２人目の素数さん
2007/02/19(月) 09:39:39やっぱり感嘆の対象になるでしょう。不完全性定理はそういう結果だと思う。
あんな証明方法思いつくところがすごい。
0045１３２人目の素数さん
2007/02/19(月) 11:08:440046１３２人目の素数さん
2007/02/19(月) 13:30:31こういう常識的感覚を生んだのが不完全性定理だから
ちょっとアレだけどね。
>>42
それは証明論の基礎論での位置をどのくらい重要だと評価するかの問題が大きいと思う
0047１３２人目の素数さん
2007/02/20(火) 05:12:460048１３２人目の素数さん
2007/02/20(火) 05:39:29abcde-fghi=33333
abcdefghiは1から9までのいずれかの数字が入り。同じ数字は使えない。
よろしくお願いします
0049１３２人目の素数さん
2007/02/20(火) 06:10:01質問
というキーワードが含まれているからだなｗ
0050１３２人目の素数さん
2007/02/20(火) 07:33:44=33 mod 100
=333 mod 1000
=3333 mod 10000
=33333 mod 100000
0051１３２人目の素数さん
2007/02/20(火) 14:00:0019世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
0052１３２人目の素数さん
2007/02/21(水) 09:18:33＞ヒルベルトの「幾何学基礎論」は、そのまま中学の教科書に使えるのではないかというぐらい平易で、
＞「本物に教えてもらう」快感を「ふつうの人」でも存分に味わうことができる。
↑こういうことを言う人のブログが日本で9番目に多く読まれてるらしいです（・・
0053１３２人目の素数さん
2007/02/21(水) 09:29:330054１３２人目の素数さん
2007/02/21(水) 10:23:16おとなしくスクリプトでも書いてりゃいいのに
0055１３２人目の素数さん
2007/02/21(水) 10:31:18扱われているのでしょうか。amazon.comのページを見る限り、
Boole代数、無限組み合わせ論や巨大基数について触れられてるのは分かるのですけど、
例えば強制法などについては載っているのでしょうか。
友隣社やマテマティカなどにも置いてないようで、ちょっと内容が分からないのでご存知の方いらっしゃったら教えて下さい。
0056ビギナー
2007/02/21(水) 23:59:00「数学の楽しみ」２００６秋「ゲーデルと現代ロジック」で、p.47脚注13に、
「矛盾する命題が一つ証明できれば、それからすべての命題が証明されてしま
うので、体系が無矛盾であることは、ある命題がその体系から証明できない
ことと同値である」との記述があります。
「ある命題」には、「体系が無矛盾であること」も含まれるのでしょうか。
そうであれば、第二不完全性定理から、（初等数論の体系を含む）公理系は、
自身の無矛盾性を証明できないので、そのことは、体系が無矛盾であることと
同値であるということになり、結局、体系が無矛盾であることを示していると
なりそうなのですが、どこが間違っているのでしょうか。
0057１３２人目の素数さん
2007/02/22(木) 00:20:06「無矛盾ならば」自身の無矛盾性を証明できないので、
が正しい。
0058１３２人目の素数さん
2007/02/22(木) 00:56:32例えていえば微分積分の理論が無矛盾であることを微分方程式や級数なんかを使って
命題で表現しろというわけですからtrivialからは程遠いでしょう？
その条件が「（初等数論の体系を含む）」となってるわけですが。
あと無矛盾性は、具体的に証明のどこで使ってるんですか？と言われると
きちんと勉強してないと答えるのが難しいね。
0059１３２人目の素数さん
2007/02/22(木) 01:37:46> うので、体系が無矛盾であることは、ある命題がその体系から証明できない
> ことと同値である」との記述があります。
これの意味はおｋ？なにか誤解してそうなんだけど
0060１３２人目の素数さん
2007/02/22(木) 09:13:05modelの話は扱わないという方針。
だから、forcingも出てこない。
006155
2007/02/22(木) 17:47:56強制法の載っている教科書はやっぱり高いなあ…
0062１３２人目の素数さん
2007/02/22(木) 17:54:210063１３２人目の素数さん
2007/02/22(木) 23:21:11その存在証明に真に選択公理を必要とするものがありますか？
0064１３２人目の素数さん
2007/02/26(月) 09:52:560065１３２人目の素数さん
2007/02/26(月) 10:47:220066１３２人目の素数さん
2007/02/26(月) 10:54:130067１３２人目の素数さん
2007/02/26(月) 11:12:120068１３２人目の素数さん
2007/02/26(月) 11:13:34洋書嫁。最近の和書は絶版か品切ればかり。
0069１３２人目の素数さん
2007/02/27(火) 16:40:52＞基礎論で、ゲーデル達の完全性／不完全性定理以降、
＞それに匹敵するくらい重要かつ興味深い結果って
＞何か出てるんですか？
コーエンのフォーシングと、これを用いた選択公理・連続体仮説の独立性
0070１３２人目の素数さん
2007/02/27(火) 16:45:21＞Lowenheim-Skolemの定理とか
これ、ゲーデルの完全性/不完全性定理より古いんじゃなかった？
＞Curry-Howardとか
これも、結構古い。もともとはCurryがλ計算と
論理との関連を研究していて見つけたもの。
0071１３２人目の素数さん
2007/02/27(火) 16:56:35「数学と論理」に挙がってるこの本っておすすめですか？
Stephen G. Simpson : Subsystems of second order arithmetic
Springer 1991
0072１３２人目の素数さん
2007/02/27(火) 16:58:20＞「体系が無矛盾であること」をその体系で表現できるか
残念ながらできません。
0073１３２人目の素数さん
2007/02/27(火) 18:34:55それは二階算術の部分体系を用いて、代数・解析・幾何などをやろうっていう本なので、
基礎論の基本的な勉強をしたいというときに使う本ではないぞ
0074１３２人目の素数さん
2007/02/27(火) 18:48:51あらら、逆数学というのを勉強したら、数学基礎論で使う証明の形式の
枠組みが（弱い体系限定かもしれませんが）きちんと理解できるのかと
思ってたんですが、必ずしもそういう印象ではないのですか？
0075１３２人目の素数さん
2007/02/27(火) 20:15:15まず基礎論で使う基本的な枠組みは理解してから取り組むものだと思う
というか、そういう類の本は、
読者が基礎論のそれなりの知識を既に持ってることを前提として書いてあるもんだが
0076１３２人目の素数さん
2007/02/27(火) 20:35:430077１３２人目の素数さん
2007/02/28(水) 12:12:24「ゲーデルと２０世紀の論理学」の３巻が出ることになってて
それに「逆数学と２階算術」の章があるみたいだぞ
0078１３２人目の素数さん
2007/02/28(水) 13:01:49自分の意見を言ってみたら、逆数学はその定義に当てはまらなかった。
0079１３２人目の素数さん
2007/02/28(水) 19:20:360080１３２人目の素数さん
2007/03/01(木) 01:51:090081１３２人目の素数さん
2007/03/02(金) 05:19:55Vがxの近傍というのは、x∈U⊂Vを満たす開集合Uが存在するということですけど、Vの開核が存在すればそれはUになりえるので、必然的にVは近傍になっちゃうと思うのですがどうなんですか？
0082１３２人目の素数さん
2007/03/02(金) 05:27:310083１３２人目の素数さん
2007/03/02(金) 06:18:30ご教授お願いします。。。。。。
0084１３２人目の素数さん
2007/03/02(金) 09:09:29>>51
http://science6.2ch.net/test/read.cgi/math/1149259755/330
にちょっとレスしました
0085１３２人目の素数さん
2007/03/02(金) 21:05:00LKでψが証明可能である⇒入力￢ψに対してタブローが停止する
はどうやって証明したらよいのでしょうか
0086１３２人目の素数さん
2007/03/02(金) 21:16:00完全性定理を使えば自明
0087１３２人目の素数さん
2007/03/02(金) 21:41:560088１３２人目の素数さん
2007/03/02(金) 23:23:07林晋の数理論理学（コロナ社）にのっていたと思う。証明長いからここじゃ無理。
0089１３２人目の素数さん
2007/03/02(金) 23:24:00廣瀬健の「帰納的関数」（共立出版）に次のように有りました。
（＊）「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)なんかはどうやって作るんでしょう？
どなたか偉い方お願いします。
0090１３２人目の素数さん
2007/03/03(土) 00:05:24昔全く同じところで悩んだ記憶があるよ
J をうまく使えばできるはず
0091１３２人目の素数さん
2007/03/03(土) 02:37:100092１３２人目の素数さん
2007/03/03(土) 07:44:05私も良く知らないんですが、（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のプログラムの部分的実現となっているという喧伝。
0093その壱
2007/03/03(土) 07:46:16Stanford 哲学百科事典 のHilbertのプログラムの記事から必要そうなところだけごく一部引用。
文献番号省略。finitary standpointとfinitist point of view、
有限の立場と有限主義はほぼ同義語として使われているような感じです。
1. Hilbeltのプログラムの歴史的発展
1.3 有限主義と無矛盾性証明の探求
Hilbertによると、内容的な算術という「具体的記号に関する純粋に直観的な基礎にのみ依拠する」
特別な数学の分野があり、その対象は「全ての思考に先立って直観的に直接経験として存在する」、
「それらの対象の存在、それらの差異、それらの並びは
（それらの対象自身と同じように）何か別のものに還元できない」
これらは記号列は意味を持たず、つまり抽象的な対象を表さず、然しながら演算を受け
（例えば連結され）比較される。これらの性質や関係の知識は直観的で論理的推論を介さない。
Hilbertによると、このようにして展開された内容的な算術は確実であり、
内容的数論の命題には論理的な構造がないのであるから、いかなる矛盾も起きない。
3. 形式主義、還元主義、道具主義
理念的な手法によって証明される実在的命題が「正しい」こと、
つまり有限の計算によって直接的に確かめられることが求められる。
これをSmorynskiが、実在的数学に理念的数学を付け加えて保存拡大になること、
と言い換えていることが4. HilbertのプログラムとGoedelの不完全性定理に述べられている。
0094その弐
2007/03/03(土) 07:46:51この方法論的な立場は、数学的思考を「全ての思考に先立ち直観的に直接経験として存在」
するような対象、またそのような対象に関する抽象的概念の導入を必要とせず、特に、
完結した無限の総体に訴えることをしないような、演算と推論の方法に制限することより成っている。
2.1 有限的な対象と有限主義者の認識論
・Hilbertが数項（numeral、数字とも訳す）をどれくらい正確に理解していたか？
Bernaysの提示した最も円熟した有限主義においては、有限主義の対象は
繰り返しの過程によって再帰的に生成される形式的な対象として特徴付けられる。
・有限主義における対象の認識論的な意義についてどう考えていたか？
・当時までの学者達のHilbert及びBernaysへの影響。
2.2 有限的に意味のある命題と有限的な推論
・特性函数が再帰的に、典型的には原始再帰法によって定義されるような関係は受け入れられる。
・このような関係から論理積∧、論理和∨、否定￢、限定量化によって出来た命題。
「任意のnに対してn+1=1+nとなる」のような数項に関する一般的事実を述べる命題は
問題のある有限的命題である。「どうしたって全ての数について試すわけにはいかない。」
有限的な一般命題は無限な連言∧_{x} φ(x)としてではなく、
「ただ、一つ数項が任意に与えられたときに何かを主張するような仮言的判断φ(x)として」
理解されねばならない。
このように一般的有限的命題に問題があるとしても、この種の命題は特に重要である。
0095その参
2007/03/03(土) 07:47:30・どのような演算、どのような原理が有限の立場で許されるのか、という問題は決定的に重要である。
Hilbertは一般的な説明を与えず、ただ許容される内容的算術の演算と推論方法の例を与えただけ。
Hilbertは直観的な思考は「再帰法と有限主義的に存在する総体に対する直観的帰納法」を含むと述べて
累乗法（冪）を例に挙げ、Bernaysは累乗法が如何にして数項に関する有限的演算と理解されるかを述べた。
・彼らが述べたことによれば原始再帰法により定義された演算と、
（仮言的）帰納法による証明が許されることになる。
・これらは原始再帰法による函数定義と量化記号なしの論理式の上の帰納法を認める
原始再帰算術（primitive recursive arithmetic; PRA）として形式化できる。
・しかしHilbertもBernaysも原始再帰法「しか」有限的だと見做されないと主張したわけではないし、
実際彼らは原始再帰的でない方法を用いて、表面的には有限的な無矛盾性証明を既に1923年に得ている。
（ε計算を使うらしいから「数学の基礎」に載ってるやつか？）
0096その四
2007/03/03(土) 07:48:00Parsons(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
0097１３２人目の素数さん
2007/03/03(土) 08:59:57有限の立場が
「有限の具体的図形に関する具体的な性質云々」
は全然違うと思うけど……。
0098１３２人目の素数さん
2007/03/03(土) 09:11:06PAはPRAかな
>>97
神話としてはいいんじゃない？現代的な解釈はともかく
0099１３２人目の素数さん
2007/03/03(土) 09:18:060100１３２人目の素数さん
2007/03/03(土) 10:38:180101１３２人目の素数さん
2007/03/03(土) 15:41:100102１３２人目の素数さん
2007/03/03(土) 17:51:09基礎論での「直観」などというのはKant的な意味合いが大きいみたいです。
そもそも有限の立場での絶対的な無矛盾性の証明は実現不可能なんだから
体系を限定することに昔ほど大きな重要性はないんのではないでしょうか。
>>98
Hilbertたちはどう考えていたか、というあくまで「Hilbert（学派）の有限の立場」の話なので。
最後の項には竹内外史の仕事だとか逆数学だとかも書いてありましたけど
直接的に関係がないので省略しました。
>>97
でも>>92の照井一成先生のpdfではそういう説明がされてるし、
大雑把に一言で説明するならこういう説明になりそうな気がするのですが
どういうところがおかしいですか？
「図形」というのは証明図のような
「有限個の記号から作られた有限的なもの」程度の意味です。
（↓「ゲーデルの世界」廣瀬健、横田一正より）
すなわちこの立場は，直観的に確かめられうる対象とそれらに対する
有限の操作の過程というものに方法を限定したものであった．
（↓岩波文庫「不完全性定理」の「内容的な数学」の説明）
ポイントは、これらの表現が全て有限個の記号から構成された有限的存在であり，
また，それに関する議論も有限的であるという事実である．内容的な数学とは，
本質的に有限的な数学なのである．そして，そこには直観的な議論があるだけで，
過程すべき公理も論理法則もないのである．（中略）
これが後に有限の立場と呼ばれるようになるものの原型である．
0103１３２人目の素数さん
2007/03/03(土) 18:03:03そもそも
「有限の具体的図形に関する
具体的な性質、具体的な操作、
および具体的な推論」
の全体を有限個の文字で記述
しつくすことは不可能。
つまり「有限の立場」は有限ではない。
0104１３２人目の素数さん
2007/03/03(土) 18:09:41誰も許される推論全体が有限だとか全て書き尽くせるだとか
そういうことは言ってないけど…
finitary「有限個のものに関するような、有限的な」と
finite「有限個の」じゃだいぶ意味が違うような
0105１３２人目の素数さん
2007/03/03(土) 18:40:59有限の立場ってのは、
個々の証明について、必ず具体的な有限の操作で行うってことじゃないのか
0107１３２人目の素数さん
2007/03/04(日) 10:32:11（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出来ている。
0108１３２人目の素数さん
2007/03/04(日) 14:36:51h'の定義が
h(0):=f(0),h(x+1):=g(h(x))
と一致していないような
011089
2007/03/04(日) 16:29:01やっぱり原始帰納的定義のところが、どーしてもわかりましぇん。例えばH(z):=L(z)+R(z)
なんてどうやって構成すればいいのやら。おばかですみません。もう少しヒントを。
0111１３２人目の素数さん
2007/03/05(月) 02:38:08「証明論等のメタ数学では、自然数論の範囲を超えた方法は使わない」
っていうような感じに捉えてたんだけど。
例えば、cut除去定理を証明する場合に、数学的帰納法は使ってもいいが、
超限帰納法は使っちゃダメ、みたいな。
ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、
まさにこれを実践するためでしょ？
0112１３２人目の素数さん
2007/03/05(月) 12:47:22＞誰も許される推論全体が有限だとか
＞全て書き尽くせるだとか
＞そういうことは言ってないけど…
本来、有限の立場とは、何が推論として許されるかが
有限個の文字数で書き表せ、有限ステップの操作で
検査可能である、という主張。
したがって、>>92のような立場は、有限の立場から逸脱している。
なお、専門家の中にも、この手の誤りをおかす者は少なくない。
0113１３２人目の素数さん
2007/03/05(月) 15:59:01さすがドクトル
0114１３２人目の素数さん
2007/03/05(月) 16:02:240115１３２人目の素数さん
2007/03/05(月) 21:26:47「本来」ってのはどの文献にそういうことが載ってるの？
Hilbertがどこでそういうことを言ったんですか？
011689
2007/03/06(火) 09:23:24Raphael 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」を今解読中ですが、どうも私の疑問を解決しては
くれなさそうな．．．。（英語も苦手なんで、四苦八苦中）
おやさしい方、どうかご教示ください。
0117１３２人目の素数さん
2007/03/06(火) 11:51:40￢（A→B）を仮定して、￢（A→B）からどう動けばよいのか、別に何を仮定したらよいかがわかりません
よろしくおねがいします。
0118１３２人目の素数さん
2007/03/06(火) 14:22:49￢(A→B), ￢A |- （矛盾）
だから ￢(A→B) |- ￢￢A、あとはNKの二重否定除去を使う。
NJでは出来なさそうな気がする。
B |- A→Bだから￢(A→B), B |- （矛盾）
だから￢(A→B) |- ￢B、こっちは楽ー
0119１３２人目の素数さん
2007/03/06(火) 18:20:14HilbertはGoedelの不完全性定理の証明の後
表向き「有限の立場」だといいつつ、実際には
かつて主張していた「有限の立場」を完全に
否定する論文を書いた。
Goedelはこれをみて
「よくもまあこんなものが書けたものだ」
といったそうだ。
0120１３２人目の素数さん
2007/03/06(火) 19:14:51Grattan-Guinnessに書いてあるだとか、
Ewaldに載ってただとかそういうのでも構いません。
その不完全性定理後にHilbertによって修正された立脚点のことを
「本来の有限の立場」と言ってるのだとしたら苦しすぎないですか？
Königsbergの会議が1930年7月だから
せいぜい30年の年内くらいまでのHilbertの有限主義が「本来の有限の立場」だと思いますが。
0121１３２人目の素数さん
2007/03/06(火) 22:30:19> 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
0122１３２人目の素数さん
2007/03/06(火) 23:30:31それってシーケント計算じゃない？
0123１３２人目の素数さん
2007/03/06(火) 23:45:19単にNKの公理を一段メタな立場から書いたつもりだったんだけど。
ちょうど今「完全性定理とモデル理論」
のLKのカット除去のとこ読んでたからそれが影響したのかねｗ
こんな感じ↓
[B]1
------
A→B, ￢(A→B)
---------------1
￢B
012489
2007/03/07(水) 00:36:42ありがとう。でも一般人が大学から資料もらえるのかな？（もちろんコピーだけど）電話で聞けばいいのかな？
でもここから大学まで車で片道2時間。日曜日って大学やってないよね？
0125１３２人目の素数さん
2007/03/07(水) 01:00:14休日やってるとこもあるよ。
web で簡単な利用案内があると思うから、確認してみては。
あるいは、公立の図書館通じてコピーを送ってもらうとか。
どこでも対応してくれるわけじゃなさそうだけど、運がよければ。
0126１３２人目の素数さん
2007/03/07(水) 05:05:23>>119はその通り「修正前が本来」と
言ってるように思ったけどな
0127１３２人目の素数さん
2007/03/07(水) 16:42:57漏れもそう思う。>>119は日本語が読めてない。
北朝鮮に帰れ。
0128１３２人目の素数さん
2007/03/07(水) 17:55:30修正された有限の立場、もしくは修正後流布した俗説が>>92ってこと？
でも>>119の主張を裏付ける（可能性がある）ものは
具体的にどの論文か良く分からないが
「Hilbertが不完全性定理の発見後に書いたらしいかつての立場を放棄する論文」しかない。
一方でStanford 哲学百科 はHilbertが書いたものだけでも20くらいの文章、本から
翻訳引用して、彼はここではこういっているし別のこれでもこういうことを言っている。
だから当時のHilbertの考えはこういうことなのだろう、というふうに推測している。
そのうち"Grundlagen der Mathematik" 1 & 2以外は全て不完全性定理発見前の文献。
Stanford 哲学百科の記事が正しいのだとしたらそれを大雑把に
（Kantに馴染みの薄い現代の日本の読者に対しても意味があるように）
要約したものとしては>>92の説明で間違っているとはいえないような気がするけどなあ。
「有限の立場」の>>112みたいな説明はここ以外で読んだことない。
>>103は「具体的」というものが何を意味するのかわからないから駄目だ、
とか言っているのかもしれないし、曖昧であることは確かで、実際は
Hilbertは例えば |、||、||| みたいな棒を並べたものを「具体的図形」の例として提示して
たとえば||と|||の連結は|||は||に等しい、というのが2 + 3 = 3 + 2の意味だ、とか言っている。
「具体的」というのがきちんとformalに表現できて、
「有限的にある推論が許されるかどうかが、有限的に確かめられる」為にはそもそも
超数学自体が形式化されないといけないような気もするけど、
「直接経験」だとか「直観により論理を介さず」とか言ってたHilbertが
そういうことを考えてたとは思わないけどなあ。
ジャキントの本（田中一之 監訳）読んでからレスしたかったけど、まあとりあえず。
0129１３２人目の素数さん
2007/03/07(水) 17:57:40○||と|||の連結は|||と||の連結に等しい
連結はconcatenationの訳です
0130１３２人目の素数さん
2007/03/08(木) 16:26:44＞でも>>119の主張を裏付ける（可能性がある）ものは
119のいう「不完全性定理証明後の変節論文」は
115の問いの答えではなくて、問い自体の
ナンセンスさを指摘するものかと。
＞「有限の立場」の>>112みたいな説明はここ以外で読んだことない。
いったいどこでどんな説明を読んだの？
君こそ今までに読んだ文献を全て挙げてごらんよ。
0131１３２人目の素数さん
2007/03/08(木) 16:29:53＞「具体的」というのがきちんとformalに表現できて、
＞「有限的にある推論が許されるかどうかが、有限的に確かめられる」為には
＞そもそも超数学自体が形式化されないといけないような気もするけど、
安易にformalとか形式化とかいってるけど、
君はその意味を説明できるかい？
その説明は112の主張を否定するものかい？
0132１３２人目の素数さん
2007/03/08(木) 16:32:490133１３２人目の素数さん
2007/03/08(木) 16:49:270134128
2007/03/09(金) 01:09:28私が特に間違いだと思っているのは>>119ではなくて、>>112の「有限の立場」の説明に関してです。
>>112はHilbertたちの本来の「有限の立場」がこうだ、という主張なのですから、
Hilbertや周りの人たちの書いたり述べたりしたものが根拠に無ければなりません。
その一次資料が何か（或いは、それは何という二次資料を読めば分かるか）を教えてくれ、
という問いはナンセンスではない有意味な質問だと思いますが。
少なくとも「Hilbertはひっきりなしに態度を変えていて一貫していなかったから、
本来の立場と呼べるものなど無いのだ」などの主張は>>112のレスと両立しません。
Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など
ある種の具体性を要求しています。
それが有限の文字数で書き表せるかどうかというのは別問題です
（いやもちろん、曖昧な説明でも良いなら、Hilbertの著作中に現れる文字数は
明らかに有限なのだからこの条件は自明に満たされることになりますが。。）
それに対して
＞何が推論として許されるかが有限個の文字数で書き表せ」
というような、「許される推論の説明に要する文字数」について
Hilbeltや周囲の人間が何か要求していたというのは聞いたことがありません。
＞君こそ今までに読んだ文献を全て挙げてごらんよ。
私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから
このスレ以外に>>112のような説明が決して無いことは立証出来ません。
そもそも、今までに読んだ文献を「全て」挙げろ、というのは
幾らなんでも無茶な主張じゃないですか？あなたは出来ますか？
私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを2ch以外で
「少なくとも一つ」教えてくれ、といっているだけなので、出来て当然だと思いますが。
0135128
2007/03/09(金) 01:14:54Hilbelt→Hilbert
0136１３２人目の素数さん
2007/03/09(金) 11:49:13＞>>112はHilbertたちの本来の「有限の立場」がこうだ、
＞という主張なのですから
112にはHilbertの名前は出てこないよ。
128が勝手に「有限の立場はHilbertが言い出したんだから
Hilbertの言葉がなければ根拠にならない」とわめいてるだけ。
しかも128は当のHilbertの論文を理解できていない可能性大。
だから馬鹿にされるんだよ。
0137１３２人目の素数さん
2007/03/09(金) 11:53:44＞Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など
＞ある種の具体性を要求しています。
＞それが有限の文字数で書き表せるかどうかというのは別問題です
やっぱり数学が判らずに、言葉だけで勝手な憶測しちゃってるな。
＞＞何が推論として許されるかが有限個の文字数で書き表せ」
＞というような、「許される推論の説明に要する文字数」について
＞Hilbeltや周囲の人間が何か要求していたというのは
＞聞いたことがありません。
ほら、君、やっぱりHilbertの論文読めてないよ。
0138１３２人目の素数さん
2007/03/09(金) 12:06:23＞私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから
もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。
＞ そもそも、今までに読んだ文献を「全て」挙げろ、というのは
＞幾らなんでも無茶な主張じゃないですか？
一つも挙げられないのは、いくらなんでもヒドイんじゃないか？ｗ
＞私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを
＞2ch以外で「少なくとも一つ」教えてくれ、といっているだけなので、
＞出来て当然だと思いますが。
そもそも112は、Hilbertが言ったとはいっていないのだが。
むしろ、Hilbertが言ってることとは違うというなら、
君がHilbertの言葉を引用すべきであって、112にそれを
求めるのは間違ってる。
0139１３２人目の素数さん
2007/03/09(金) 12:07:50思わせぶりじゃなくちゃんと書いたらどうだ？
0140１３２人目の素数さん
2007/03/09(金) 12:09:060141１３２人目の素数さん
2007/03/09(金) 12:11:05なに、泣きわめいてるんだ。この馬鹿ｗ
貴様は三歳のガキか。
0142１３２人目の素数さん
2007/03/09(金) 12:13:30自分でHilbert読め。馬鹿がｗ
0143１３２人目の素数さん
2007/03/09(金) 12:25:36そういう書き方しかできないのならトンデモ扱いされても仕方ないだろう
最初から具体的に書けばすむことなのになあ
0144１３２人目の素数さん
2007/03/09(金) 12:46:38＞最初から具体的に書けばすむことなのになあ
ほんとだよ115=128=143君ｗ
自己矛盾はマツシン以下の馬鹿だよｗ
0145１３２人目の素数さん
2007/03/09(金) 12:48:20ガキって自分にモノを教えてくれないと、
拗ねて相手をトンデモ呼ばわりするよねｗ
0146１３２人目の素数さん
2007/03/09(金) 13:33:02以後は気をつけな
0147１３２人目の素数さん
2007/03/09(金) 14:21:210148１３２人目の素数さん
2007/03/09(金) 14:54:240149１３２人目の素数さん
2007/03/09(金) 14:57:03マツシンマニアってキモイ
0150１３２人目の素数さん
2007/03/09(金) 14:58:16トンデモの便臭を漂わすなよ（ｗ
0151１３２人目の素数さん
2007/03/09(金) 15:00:00君は全然不可通だけどな（ｗ
0152１３２人目の素数さん
2007/03/09(金) 15:21:00Scott位相とか領域理論について丁寧に書いてある本ありますか？
読書のスピードからいくと、できれば和書がいいのですが、
無いということであれば洋書でも大丈夫です
0153１３２人目の素数さん
2007/03/09(金) 15:47:23自分で探せ
0154１３２人目の素数さん
2007/03/09(金) 16:10:37おすすめがなければ、こいつに突撃かと思ってるんですけど
高いしごっつそうだし、もう少し何か無いものかと・・
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
0155128
2007/03/09(金) 19:32:42いやHilbertじゃなくてBernaysでもAckermannでもNeumannでも良いですよ。
「有限の立場」というのは彼らGoettingenの公理論者の
主義主張を指す言葉だから彼らがそういう主張をしていた、ということでしょう。
一次文献かせめて二次文献くらいの根拠はあるものだと思いましたが。
もう啓蒙書とかブルーバックスとかでも構いませんけど。
竹内外史なんかは多少違った主張をしますけど、
彼の主張はどちらかというと異端的ですし、歴史的にみて明らかに後発で
彼を持って先行者を「本来の立場」ではなかったとすることは出来ません。
「当のHilbertの論文」とは具体的にどれですか？と言ってるのに
それに答えられないで読めてないなあ誤解してるなあばかり連発されても困ります。
Hilbertのどの論文を読めてないのかもわかりません。
その論文には表題は付いてなかったんですか？
>>138
＞もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。
「全て」と言われているのにニ、三冊だけ挙げても答えになっていないし
それだけしか読んでないのか、なんて言って莫迦にする人も居るかもしれませんしね。
「たとえばニ三冊挙げるなら」Stanford哲学百科とか岩波文庫の「不完全性定理」とか
（きちんと全部読んでないけど）Heijenoortとかまだ一部しか読んでないけどジャキントとかですけど。
あなたが読まれたHilbert計画に関する文献を全部挙げて下さい。
0156128
2007/03/09(金) 19:33:28「全ての思考に先立ち直観的に直接経験として存在」
「どうしたって全ての数について試すわけにはいかない。」だとか
「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか
全部Hilbertたちが書いたものそのままの引用なんですよ。
「許される推論の説明に要する文字数」について
Hilbertや周囲の人間が何か要求していたことを示す文献は無いと言っているんですが。
112が「本来の有限の立場」とは違うというなら、
112が「本来の有限の立場」を示す分権を引用するべきだと思いますけど
「本来の有限の立場」と言えばHilbertの周囲の者、
もしくはHilbert自身の立場だとみなすのはごく当たり前かと。
それに>>92にも（Hilbertの）有限の立場だとことわってあります。
>>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、
というのにたいして、それは違う、と言ってるのが>>112でしょ。
で、そういう文献は知られていない、というレスに対して
0157128
2007/03/09(金) 19:35:05>>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、
というのにたいして、それは違う、本来はこうだ、と言ってるのが>>112でしょ。
で、そういう文献は知られていない、というレスに対して、
じゃあ>>112を否定する文献を挙げろ、と求めてるのがレスの流れ。
どうして>>112は根拠を挙げなくて良いんですかね。
0158１３２人目の素数さん
2007/03/09(金) 19:40:45基礎論スレの初心者？
0159128
2007/03/09(金) 20:30:130160１３２人目の素数さん
2007/03/09(金) 20:50:49基礎論関係のスレには永遠に住み着いていて
こいつ（ら）と言い争いになったらスルーが基本。
マツシン（かそれと同レベルの奴）が誤りを認めることは
基本的にありえない。人工無能のように必ずレスを返して
いつまでも食い下がっては鸚鵡返しで煽り、はぐらかす。
無理に調伏しようとするとスレがぐだぐだに荒れる。
「お前マツシン並だな」と言われたときに
普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
何故か「お前はマツシン以下だな」と返す、などの習性がある。
0161１３２人目の素数さん
2007/03/10(土) 00:22:53横レスですが、大変勉強になりました。ありがとうございます
0162１３２人目の素数さん
2007/03/10(土) 01:01:420163１３２人目の素数さん
2007/03/10(土) 10:54:24112は誰の名前も出していないよ。
「「有限の立場」はHilbertとその仲間のものだ」
という128こそ一次文献でも二次文献でも啓蒙書でも
ブルーバックスでもいいから文献名と引用文で
示せばいいが、ドイツ語どころか漢字も読めないかい？
0164１３２人目の素数さん
2007/03/10(土) 11:06:25＞竹内外史なんかは多少違った主張をしますけど、
＞彼の主張はどちらかというと異端的ですし、
＞歴史的にみて明らかに後発で
＞彼を持って先行者を「本来の立場」ではなかった
＞とすることは出来ません。
>>92のほうが碍子っぽいけどな。
そういえば>>120でも
＞不完全性定理後にHilbertによって修正された立脚点のことを
＞「本来の有限の立場」と言ってるのだとしたら
なんて真逆な誤読してるヤシがいたけど、マジで日本語読めないのか？
0165１３２人目の素数さん
2007/03/10(土) 11:14:02＞「たとえばニ三冊挙げるなら」
＞Stanford哲学百科とか
＞岩波文庫の「不完全性定理」とか
＞（きちんと全部読んでないけど）Heijenoortとか
＞まだ一部しか読んでないけどジャキントとかですけど。
じゃ、それぞれの中で君が読んだという箇所を上げてごらん。
岩波文庫もハイエノールトもジャキントもここにあるから
君が読んだかどうかは確認できるよ。さあ、やってごらん。
0166128
2007/03/10(土) 11:16:55誰もHilbertたちの占有物だ、とは言ってませんよ。
「「有限の立場」はHilbertとその仲間の提唱したものだ」と同じ意味にとって良いんですかね。
これくらい基礎論では常識だと思ったんですが。
0167１３２人目の素数さん
2007/03/10(土) 11:21:08＞「全ての思考に先立ち直観的に直接経験として存在」
＞「どうしたって全ての数について試すわけにはいかない。」だとか
＞「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか
＞全部Hilbertたちが書いたものそのままの引用なんですよ。
ふーん、つまらない文章を引用するね。
まず、はじめの文章は何も述べていないに等しい。
次の文章はあまりにも自明で、引用するだけ無駄。
問題は最後の文章で、再帰法や直観的帰納法として
どこまで考えているかってこと。
0168１３２人目の素数さん
2007/03/10(土) 11:24:55＞「許される推論の説明に要する文字数」について
＞Hilbertや周囲の人間が何か要求していたことを
＞示す文献は無いと言っているんですが。
だから無限に書き続けていいというのが
「不完全性定理後に修正された立脚点」
であって、ゲーデルにバカにされたこと
なんだがな。
0169128
2007/03/10(土) 11:45:22＞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/
これで満足？
0170128
2007/03/10(土) 11:59:45別にその文章で「有限の立場」がどういうものか完璧に分かるって言ってんじゃないですよ。
Hilbertの別の著作から普通に解釈すれば原始再帰算術になるって何十年か昔から言われてるし、
その解釈に対する議論も為されてるじゃないですか。それで何が問題が？
>>92の「有限の立場」の大雑把な説明は上から五番目のpdfから
ほぼそのまま取ってきたものですけど、著者はPRAくらい当然知ってて
その大雑把な説明を与えているんだと思いますけど。
誰もあれが完璧な説明だなんて思ってないでしょう。
>>112だと超数学のレベルでどんな抽象的でよく訳の分からないidealな対象でも
使って良いことになりますよね。例えば自然数の任意の部分集合とか。
証明が正しいことは有限的に判定できますから。
一方で超数学における推論の説明には普通一般に言われてるよりもきつい条件を貸すことになる。
どんなに具体的でrealで、誰もがよく知っているようなものでも、
よく説明出来ないものは使っちゃいけないことになる。
そんなことHilbertが言っていましたか？
無限に続けるってのは、多分、何が許される推論か、Hilbertが無限に説明を続けるんじゃなくて
「有限ステップの操作で検査可能である」の方に反するんじゃないですか？
具体的にどの文献のどこのなんと言う文言か教えてくれるつもりがないようなので確かめようが無いんだけど。
0171１３２人目の素数さん
2007/03/10(土) 15:02:57＞>>112だと超数学のレベルでどんな抽象的でよく訳の分からない
＞idealな対象でも使って良いことになりますよね。
112にはそんなことは全く書いてないが。
＞例えば自然数の任意の部分集合とか。
＞証明が正しいことは有限的に判定できますから。
やっぱり日本語がまったく読めない人なんだな。
自然数の任意の部分集合全体なんて、
有限個の文字数で書き表わせないが。
ああ「有限個の文字数で書き表わす」と言う場合の
有限個は文字の種類数ではなく、例えば「２００字以内で書け」
という意味の純然たる字数のことである。
0172１３２人目の素数さん
2007/03/10(土) 15:05:15＞無限に続けるってのは、多分、何が許される推論か、
＞Hilbertが無限に説明を続けるんじゃなくて
＞「有限ステップの操作で検査可能である」の方に
＞反するんじゃないですか？
見苦しい言い訳だな。バカなんじゃないのか？
0173１３２人目の素数さん
2007/03/10(土) 15:08:02＞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.
これが「有限の立場」がどういうものか完璧に分かる文章なのかい？
バカなんじゃないのか？
0174１３２人目の素数さん
2007/03/10(土) 15:18:18＞誤りを認めることは基本的にありえない。
＞人工無能のように必ずレスを返して
＞いつまでも食い下がっては鸚鵡返しで煽り、
＞はぐらかす。
128だな。二言目には文献とわめき
サルでもできる検索の結果をどうだと
ばかりにひけらかす。まったく恥かしい。
＞無理に調伏しようとするとスレがぐだぐだに荒れる。
「調伏」なんて聞いたことがないので、
もしかして朝鮮語かと思って検索したら、
「加持や祈祷を用いて、悪霊や物の怪を屈服させること。」
なんて奇怪な意味の言葉らしい。
やっぱり数学よりも妖怪に詳しいオカシナ奴らしいな。
0175１３２人目の素数さん
2007/03/10(土) 15:27:28＞超数学における推論の説明には普通一般に言われてるよりも
＞きつい条件を貸すことになる。
＞どんなに具体的でrealで、誰もがよく知っているようなものでも、
＞よく説明出来ないものは使っちゃいけないことになる。
なんかまったく見当違いなことをいってるな。
半可通を笑う四半可通、といったところか。
もちろん、1/2よりも1/4のほうが小さい。
0176１３２人目の素数さん
2007/03/10(土) 15:51:10＞>>92の「有限の立場」の大雑把な説明は
＞上から五番目のpdfからほぼそのまま
＞取ってきたものですけど、
>>102では「照井一成先生のpdf」と自慢げに名前を出してたがｗ
で、しかも、>>92を見ると
＞ぐぐって出て来たので一部ちょっとだけ参考にさせて貰いました。
なんて臆面もなく書いてるね。
上記のpdfを拝見したが、そもそも碍子チックな臭いが
プンプンするわけで、92の説明もそういう立場を理解した
上で読まないと間違う。
０を正当化するのに１、１を正当化するのに２・・・
とつづけていって、１も２も・・・も全部有限だからＯＫ
みたいな屁理屈は、体系の強さの順序付けとかいう後から
出てきた御利益を除けば、本来の無矛盾性証明の目的を
全く達成していない点で無意味。
0177１３２人目の素数さん
2007/03/10(土) 16:10:53幻惑されてるように思える。
カット消去は数学的には興味深いが、哲学的な基礎付けの問題を
解決するようなものではない。
岡田光弘氏も現代思想の「ゲーデル」特集号の中で、
ゲーデルの不完全性定理から考えてカット消去は
正しいとしても体系内では証明できないことが
明らかであり、竹内外史は竹内予想を提出する際
この点について”楽観的”だったのではないか
と指摘している。
0178128
2007/03/10(土) 22:05:48使っていけない、と書いてない以上>>112の条件さえ満たされたら
使って良いと考えるのはごく当然だと思うけど。
＞自然数の任意の部分集合全体なんて、
＞有限個の文字数で書き表わせないが。
「書き表せる」ってのは何のことを言ってるんですかね。
一つ変数を用いれば自然数の任意の部分集合なんて
いくらでも表記のしようがあると思いますが。
例えば「偶数全体の集合」（七文字）だとか円周率だとかは
有限の文字数で書き表せるの？そうじゃないの？
「偶数全体」は書き表せないから、「偶数」という概念は使っちゃ駄目ってことなんですか？
>>173
>>163で「有限の立場」がHilbertやその周囲の人物の提唱した立場であることを
示せとか言い出すから根拠を書いたんですが。
本当はこんなこと常識以外の何ものでもないと思うけど。
「有限の立場がHilbertのものだとは言ってない」とやたら強調されてたけど
Hilbert以外の誰が提唱したとおっしゃるんですかね。
＞どうだとばかりにひけらかす。
自分で文献を挙げろと言っておいてそりゃないだろう。自分が何言ったか覚えてないのか？
＞もちろん、1/2よりも1/4のほうが小さい。
はあ？
0179１３２人目の素数さん
2007/03/10(土) 22:36:56http://www.chunichi.co.jp/flash/2007031001000102.html
0180１３２人目の素数さん
2007/03/11(日) 06:18:400181１３２人目の素数さん
2007/03/11(日) 09:32:45それと基礎論と何の関係が?
0182１３２人目の素数さん
2007/03/11(日) 10:41:10120までは普通の流れなのに
なんで文献名が出ないんだ？
0183１３２人目の素数さん
2007/03/11(日) 10:42:01どこの板にもいるものだ。「基礎」とか書いてあるしｗ
0184１３２人目の素数さん
2007/03/11(日) 13:43:50文献文献と＊＊の一つ覚えで騒ぐ＊違いか
0185１３２人目の素数さん
2007/03/11(日) 13:52:46128は形式化が全く理解できていない四半可通
0186１３２人目の素数さん
2007/03/11(日) 14:21:480187１３２人目の素数さん
2007/03/11(日) 15:15:53>本来､有限の立場とは、何が推論として許されるかが
>有限個の文字数で書き表せ、有限ステップの操作で
>検査可能である、という主張。
これって本当なの？
一連の流れは
「本来」って書いてるぐらいだから有限の立場を唱えていた学者のうちの誰かがそれを唱えてたんでしょ？
それは誰よ？
って質問なんじゃないの？
0188１３２人目の素数さん
2007/03/11(日) 16:41:42自分の主張を逸脱といわれて逆上し
＊＊の一つ覚えを繰り返す＊違い
0189１３２人目の素数さん
2007/03/11(日) 17:03:15＞ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、
ヒルベルトの弟子であるアッカーマンが実質的に
PRA（原始帰納的算術）を有限の立場と考え、
その無矛盾性を「証明」していたから。
（「不完全性定理」岩波文庫ｐ229）
ただし上記の文献にもあるように、上の「証明」は
実際には超限帰納法を用いている。
実際、不完全性定理から明らかなように、
PRA自身の無矛盾性はPRAでは証明できない。
0190128
2007/03/11(日) 21:22:19と思ってぐぐったら出来るっぽいですね。
しかし文献を示せというから言われた通り示したら
「どうだとばかりにひけらかす」とか言われてビックリしたよ
何かの罠みたいなもんだったのかなー
自然数の無矛盾性証明なんて別にGentzenに限らず
多くの人が行っていて、何通りもある。
ただ「有限の立場」はHilbertの書きものを素直に読めばPRAとほぼ同一視でき、
全ての証明はPRAを逸脱した立場で行なわれているから
Hilbert計画の達成とは見做されない、それだけの話なのにね。
>>112は多分そういうことを知らないんだろうけど、
Gentzenの自然数論の無矛盾性証明を
「有限の立場で認められる無矛盾性証明」から排除するために
「本来の有限の立場」なんてのを後付けでデッチアゲてしまっているんだろう。
それでいて後から主張を翻したHilbertを批判してるんだから御目出度いものだ。
だからHilbert学派がそういうことを述べていたソースを出せ、と言われても
答えられないし、挙句の果てには「有限の立場」はHilbertたちのものじゃない、
などと馬鹿げたことを言い出す。
きっと「本来の有限の立場」なるものは「オレ流・真・有限の立場」な感じで
>>112の脳内のなかにしかないんでしょ。
0192１３２人目の素数さん
2007/03/11(日) 21:55:030193１３２人目の素数さん
2007/03/12(月) 01:15:110194１３２人目の素数さん
2007/03/12(月) 08:04:03＞>>112の脳内のなかにしかないんでしょ。
なるほど納得
>>112も始めから「『俺が思うに』有限の立場とは本来こういうものなんだよ！」
て書けばいいのに
0195１３２人目の素数さん
2007/03/12(月) 09:42:11＞自然数の無矛盾性証明なんて別にGentzenに限らず
＞多くの人が行っていて、何通りもある。
＞ただ「有限の立場」はHilbertの書きものを素直に読めば
＞PRAとほぼ同一視でき、全ての証明はPRAを逸脱した立場で
＞行なわれているからHilbert計画の達成とは見做されない、
＞それだけの話なのにね。
やっぱり肝心なことがわかってないな。
超数学で元の体系より強いものを使ったらダメなんだが。
有限の立場は「内容的な数学」だとかいうのは、
不完全性定理以後では、そういう無茶を押し通すための
強弁に成り下がってしまった。
0196１３２人目の素数さん
2007/03/12(月) 09:50:24＞Gentzenの自然数論の無矛盾性証明を
＞「有限の立場で認められる無矛盾性証明」から排除するために
＞「本来の有限の立場」なんてのを後付けでデッチアゲて
＞しまっているんだろう。
Gentzenの「証明」の問題点は、有限の立場とかいう以前に
対象理論では定義してないことを、後だしジャンケンのように
超数学の理論で持ち出していることにある。
「超限帰納法だって定義できるからいいだろう」というかも
しれないが、そうやって、後だしジャンケンを無限につづければ
いいという発想で、全体をなし崩しに正当化するのは、結局有限の
立場自体を否定するものである。
0197１３２人目の素数さん
2007/03/14(水) 12:12:28なんか重い空気のなかすみません
自然演繹で
∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である
（ただし、∃ｘA（ｘ）はaを含んではいけない）、というのは、
例えば、
∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか
∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから、きっと、ｓ０と０は別物で、ｓ０は入れていいのだ、と勝手な判断をして導出を続けていったら、
いろいろなものがでてきて、ちょっと今、困ってます
0198１３２人目の素数さん
2007/03/14(水) 14:19:05> ∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか
これ自体は正しいけど、その前の部分とこのことをあなたがどうやって関係付けたのかわからない
> ∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから
よくないよ
もしかして∃と∀を混同してない？
0199１３２人目の素数さん
2007/03/14(水) 14:22:07> ∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら
ここの a は変数？
0200１３２人目の素数さん
2007/03/14(水) 15:47:09書き方が良くなかったです
前のはなかったことにして、
定項（数項）０、１、２、・・・があって
関数記号ｓがなし、
関数記号＋があって、
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメですか？
ということでした
0201１３２人目の素数さん
2007/03/14(水) 16:21:19普通の自然演繹の体系ならダメ
0202１３２人目の素数さん
2007/03/14(水) 17:27:00例えば、
＝除去規則
ｓx＝ｓxとx＝０＋xが導出可能であるならばｓ（０＋x）＝ｓxが導出可能である、というような代入のしかたはOKでしょうか
0203１３２人目の素数さん
2007/03/14(水) 18:27:17導出自体は問題ないと思うけど、
1. = の除去規則
2. その規則をどう使ったら sx=sx, x=0+x から s(0+x)=sx が出るのか
を正確に書ける？
0204１３２人目の素数さん
2007/03/14(水) 18:52:59１＝除去規則
A（a）とa＝bが導出可能であるならばA（ｂ）が導出可能である、（A(ｂ）はA（a）のaのところを（全部でなくてよい）ｂにおきかえたもの
よって２
としたのではまずいでしょうか
0205１３２人目の素数さん
2007/03/14(水) 20:48:03よさそうだけど一応確認を。
2 で A(a) に対応する論理式と b に対応する項は？
0206１３２人目の素数さん
2007/03/14(水) 23:05:31ところで
>>201
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ
ということなので
>>１９７
の、
>（ただし、∃ｘA（ｘ）はaを含んではいけない）
は（ただし、∃ｘA（ｘ）はaに含まれる項を含んではいけない
のようなことになるのでしょうか
0207１３２人目の素数さん
2007/03/14(水) 23:20:38どこでおかしくなってるのか分かったような気がする。
あなたの知っている∃除去規則を正確に述べてみてください。
0208１３２人目の素数さん
2007/03/15(木) 20:10:17等号に関する公理（equality axiom）というのがあります。
教科書などの、この公理に関する記述を参照。
あと∃の除去則（∃-elimination）のところも要復習。
要は>>207さんの言う事を良く聞きましょう、という事で。
0209ご迷惑をおかけしました
2007/03/16(金) 09:14:00∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である
（ただし、∃ｘA（ｘ）はaを含んではいけない）
aは新しい定数
∃ｘ（０＋ｘ＝ｘ）が導出可能で
０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ
０＋１は定数ではなくて項だからダメ
でした。
0210１３２人目の素数さん
2007/03/16(金) 13:11:05もしかしてそこらへんにわかってない原因があるんじゃないの？ちなみに
＞０＋１は定数ではなくて項だからダメ
これはとてもとんちんかんに感じる。
0211１３２人目の素数さん
2007/03/17(土) 15:52:05まあ良いや
0212１３２人目の素数さん
2007/03/19(月) 16:38:34読むべし、読むべし
集合の本？ ボコボコにしてやんよ
∧＿∧
( ･ω･)＝つ≡つ
(っ ≡つ＝つ
/ ) ﾊﾞﾊﾞﾊﾞﾊﾞ
( /￣∪
http://2ch-news.net/up/up50539.jpg
0213１３２人目の素数さん
2007/03/19(月) 17:05:29よく手に入ったね
しかし田中をこれから読むのにカナモリさんも一緒に買うとはなかなか
0214１３２人目の素数さん
2007/03/19(月) 20:06:50こういうのは手に入るときに手に入れておこう
0215１３２人目の素数さん
2007/03/19(月) 20:08:120216１３２人目の素数さん
2007/03/19(月) 20:51:140217１３２人目の素数さん
2007/03/19(月) 21:31:45（邦訳は初版）
KunenとかJechがまだ訳書出てないのに意味無いよね、はっきり言って
0218１３２人目の素数さん
2007/03/19(月) 23:37:080219１３２人目の素数さん
2007/03/20(火) 16:05:220220１３２人目の素数さん
2007/03/20(火) 17:14:110221１３２人目の素数さん
2007/03/21(水) 17:02:090222１３２人目の素数さん
2007/03/21(水) 21:24:430223１３２人目の素数さん
2007/03/21(水) 22:13:460224１３２人目の素数さん
2007/03/22(木) 10:11:39集合論研究者のいう世間とは、同業者の集まりことらしい
0225１３２人目の素数さん
2007/03/22(木) 12:10:230226KingOfUniverse ◆667la1PjK2
2007/03/22(木) 12:19:150227１３２人目の素数さん
2007/03/22(木) 23:17:330228１３２人目の素数さん
2007/03/23(金) 01:14:070229１３２人目の素数さん
2007/03/23(金) 10:59:27どんな本？
0230１３２人目の素数さん
2007/03/23(金) 12:07:46わしも聞きたい
0231１３２人目の素数さん
2007/03/23(金) 13:40:280232１３２人目の素数さん
2007/03/26(月) 14:37:28どちらかというと読み物風というスタイルな気がする。
0233１３２人目の素数さん
2007/03/26(月) 16:07:18とはいえ、”４分冊”で思いつくのは>>77だけ。
228にはゴツいんだろう。他にどんな本を読んだか知らないけど
0234１３２人目の素数さん
2007/03/27(火) 10:00:15もちろんそうすると辞書みたいに分厚くなるだろうし、洋書しかないんでしょうけど、どなたか
わかるかた、教えて著。
0235１３２人目の素数さん
2007/03/29(木) 19:00:140236１３２人目の素数さん
2007/03/30(金) 15:40:47「公理的集合論」とか「公理論的集合論」とか「公理論的集合論」とか
「証明論入門」とか「現代集合論入門」とか
0237１３２人目の素数さん
2007/03/31(土) 01:01:53数理論理学も4種類上あるみたいだけどね
0238１３２人目の素数さん
2007/03/31(土) 19:45:120239１３２人目の素数さん
2007/03/31(土) 22:16:14それとも「数理論理学」かな。
たぶん復刊されたというから前者だと思うけど
数学基礎論入門は少なくとも数年前には単行本化されてたし
今でも手に入ると思うけどね
>>234
「20世紀の論理学」には割ときちんと証明が載ってる気がするけど
0240１３２人目の素数さん
2007/04/01(日) 00:05:13カテゴリーがどうのこうのとか書いてあるけど
最初読んだときは良く意味が分からなかった。
最近哲学系の本を読んでやっとcategorial grammerとか
型理論とかと関係があるんだろうなあ、と想像がつくようになった。
モダン過ぎて初学者には全然意味が分からないと思うんだけどなあ、あの書き方じゃ。
0241１３２人目の素数さん
2007/04/01(日) 04:32:001975年当時はもっとモダンに見えただろうなあ、
難波さんの翻訳した本か何かにそれについての論考があったと思うので、
気が向いたら探してみて。
0242１３２人目の素数さん
2007/04/01(日) 04:59:34数学セミナー増刊「数学基礎論の応用」とか
0243１３２人目の素数さん
2007/04/01(日) 14:22:07「代数幾何学」（ハーツホーン）とかはやっぱりデフォなの？
0244１３２人目の素数さん
2007/04/02(月) 02:48:49おお、なんかどうもありがとうございます。
今度図書館に行ったときにでも読んでみます。
0245１３２人目の素数さん
2007/04/03(火) 18:42:00「 { }は空集合である または { }は無限集合である 」
を証明することは可能ですか？
0246１３２人目の素数さん
2007/04/03(火) 20:15:13どういう論理体系でやるのかをはっきりさせないと答えようがないような
0247１３２人目の素数さん
2007/04/03(火) 20:19:27http://www.technobahn.com/cgi-bin/news/read2?f=200704031617&ref=rss
0248１３２人目の素数さん
2007/04/03(火) 20:58:42とか思ってたら連続体仮説を「証明」かｗ
0249１３２人目の素数さん
2007/04/03(火) 21:18:42記事へのリンクがあった
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
0250１３２人目の素数さん
2007/04/03(火) 21:40:14{ }を特徴付ける公理が何もないなら、ほとんど何も証明できないんでないの？（恒真式なら証明できるけど
そんなの意味ないでしょ。）
0251１３２人目の素数さん
2007/04/03(火) 23:20:02空集合の公理は、実は無限下降列の非存在（と他のいくつかの公理）から引き出せる
空集合の存在を認めるのと、無限下降列の存在を認めないのと、どちらがいいのかは哲学
0252１３２人目の素数さん
2007/04/03(火) 23:47:44どういう風に定義されてるに拠るんじゃないの。
何か{_}に関する性質が前もって与えられてないと証明できるわけ無いじゃん。
定数記号cが∀x￢x∈cを満たすことを
cに関する論理式を使わないで証明できるわけが無いのと全く同じで。
naiveな集合論しか知らない人にはそういう見通しが立たないのかもしれないけど。
0253１３２人目の素数さん
2007/04/03(火) 23:56:54特にロジックの非専門家や一般人にとってはね。
連続体仮説を解決じゃなくて証明とか書いてるのは
記者がわかってないんだろうなあ。
連続体仮説はZFCから証明出来ないことを証明した、と書けば良いのに。
0254１３２人目の素数さん
2007/04/04(水) 00:29:200255１３２人目の素数さん
2007/04/04(水) 00:44:000256１３２人目の素数さん
2007/04/04(水) 07:44:07やっぱりそうですよね。ありがとうございます。
もう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」を示すことは可能でしょうか？
0257１３２人目の素数さん
2007/04/04(水) 09:43:41だとしたら～を使わずに、というのは意味不明なんだけど。
何が言いたいの？
0258１３２人目の素数さん
2007/04/04(水) 10:20:040259１３２人目の素数さん
2007/04/04(水) 10:31:25久しぶりに「アメリカの数学者たち」を部屋の奥から掘り出した俺
0260１３２人目の素数さん
2007/04/04(水) 17:04:13うーん、何と説明したらいいんだろう…
と考えていたら、自分でも質問の意味が分からなくなってきました。
>>256は取り下げます。
0261１３２人目の素数さん
2007/04/04(水) 18:25:20ちゃんとした先生にちゃんとした授業で教えを受けること。
まだ大学に行ける年齢でないならそれまで我慢すること。
0262１３２人目の素数さん
2007/04/04(水) 18:41:550263１３２人目の素数さん
2007/04/04(水) 22:21:23それだけだけどｗ
0264１３２人目の素数さん
2007/04/04(水) 22:57:450265１３２人目の素数さん
2007/04/05(木) 09:29:53全頁和訳してdvi/ps/pdfでくれ
0266１３２人目の素数さん
2007/04/05(木) 10:57:230267１３２人目の素数さん
2007/04/05(木) 15:22:43>{ }が空集合である･･･ことを用いずに、
>「 { }は空集合である または { }は無限集合である 」
>を証明することは可能ですか？
{ }が無限集合である可能性なんてあるのか？（ｗ
0268１３２人目の素数さん
2007/04/05(木) 23:46:02持ってるのこれの昔の版↓だよ
Set Theory and the Continuum Hypothesis (Paperback)
たぶん国会図書館や大学図書館で閲覧可能でしょう
0269１３２人目の素数さん
2007/04/05(木) 23:52:15国会図書館には洋書の専門書ってあまり無い気がするよ。
大学図書館にはあるだろうけど（原論文もあるだろう）。
訳書のほうは国会図書館にもあるだろうね。
0270１３２人目の素数さん
2007/04/06(金) 02:35:250271１３２人目の素数さん
2007/04/07(土) 18:30:530272１３２人目の素数さん
2007/04/07(土) 21:00:25http://ja.wikipedia.org/wiki/%C3%96
0273１３２人目の素数さん
2007/04/12(木) 21:02:31古本屋で 8000円出して買った私は少し悲しい・・
0274１３２人目の素数さん
2007/04/15(日) 15:11:440275１３２人目の素数さん
2007/04/15(日) 17:44:080276１３２人目の素数さん
2007/04/24(火) 15:22:120277１３２人目の素数さん
2007/05/06(日) 21:57:220278１３２人目の素数さん
2007/05/11(金) 11:09:01>巨大基数の集合論 販売価格 ： \8,000
>
>著者名 ： カナモリ，A．著 淵野昌訳
>出版社 ： シュプリンガー・フェアラーク東京
>発行年度 ： 1998年
0279１３２人目の素数さん
2007/05/11(金) 17:12:06むむ、今確認したらもう無くなってる
漏れの書き込みは役にたったんだろうか？？
0280１３２人目の素数さん
2007/05/11(金) 19:38:19欲しかった……。
0281１３２人目の素数さん
2007/05/11(金) 23:18:15ありがとう
0282１３２人目の素数さん
2007/05/12(土) 08:36:33もしかして買った人？ なら、書いて良かった ノ
（自分の分のときも結構探したので・・）
0284１３２人目の素数さん
2007/05/26(土) 21:08:100285１３２人目の素数さん
2007/05/26(土) 22:18:560286１３２人目の素数さん
2007/05/28(月) 18:21:14ボレル非可測なルベーグ可測集合の例を
ttp://www-an.acs.i.kyoto-u.ac.jp/~kigami/analysis1-9.pdf
で読んだのですが、ルベーグ非可測集合を使って構成しています。しかし、
ルベーグ非可測集合を作るには選択公理が必須だと聞いたことがあります。
0287１３２人目の素数さん
2007/05/31(木) 01:49:37Fermatの最終定理って解決しましたよね。
でもあれっていわゆる集合論の枠組みの中での証明な訳ですよね。
ってことは、コツコツ計算していったら
ある日Fermatの最終定理の反例が見つかる
(系として集合論が無矛盾でないことが分かる)という可能性は
残っている訳なんですか？
0288１３２人目の素数さん
2007/05/31(木) 04:04:07って何？
先生がいいと言うまで廊下に立ってなさい。
0289１３２人目の素数さん
2007/05/31(木) 19:57:040290１３２人目の素数さん
2007/05/31(木) 21:02:00まあ残ってますけど、でもZFより弱い枠組みで証明できるはずですよ。
初等整数論の定理はZFCから証明できる場合は選択公理を使わないで証明できる、
とか、どうやらそういう種類の定理があるようで。（数学セミナー増刊号に載ってた）
>>289
まあネットだし2chだし。
0291１３２人目の素数さん
2007/05/31(木) 21:13:12でも、んなもんに興味のない俺は、特に気にすることもなく目当てのものを探して、レジで並んでた。
次は俺の会計だな、と思ってたら後ろから怒号が飛んできて、近くにいた人が一斉にそっちに向いたわけ。
一瞬、誰もしゃべらない状態になって、店内に流れるBGMがよく聞こえたよ。
みんなの視線の先には、それはもう絵に描いたようなｷﾓｦﾀがいた。
ｷﾓｦﾀが店員に文句を言ってるんだろうなってのは状況的にすぐに分かった。
周りの注目も気にせずにそのｷﾓｦﾀはフーフー言いながら手に持った単行本らしきものを店員に向けて
「なんでゼロの使い魔がお薦めコーナーにあるのに、涼宮ハルヒの憂鬱は置いてないんだよ！」と。
涼宮ハルヒの憂鬱と、ゼロの使い魔。名前は知っていたよ。あのキモいアニメ。
あのｷﾓｦﾀが持っていたのは多分、ハルヒかゼロの使い魔のラノベだったんだと思う。
店員らしき男の人が申し訳ありません申し訳ありませんって謝ってたけど、ｷﾓｦﾀはその店員に向かって
何度も、「なぜ涼宮ハルヒを置かないんや。廃れるやろがっ！！」って同じ質問を何回も繰り返してる。
そんで最後には店長を呼べと。
店長が来てからはもう凄かったよ。
お前らは商売をする気があるのか、ただ売れてるものを売ってるだけだ、本当の本の価値を分かっていない・・・と。
みんなドン引き。それでもｷﾓｦﾀのラノベ講義は続く。
会計が回ってきた俺が店員に小さく「大変ですね」と言ったら、困った笑顔を作って
「はは・・お騒がせしてすみません」だって。
会計が終わってしばらくしてからｷﾓｦﾀの演説は終わった。俺は帰っても良かったんだが、『めったに見られるもんじゃねえ！』
と思ってずっと横で見物してた。てか見物人が結構いたよ。
最終的に、そのお薦めライトノベルコーナーに涼宮ハルヒを置くことでｷﾓｦﾀは納得したみたいで、文句を言うだけ言って
何も買わずに悠々と店を出て行った。
残った店内で小学生っぽい男の子が「すげー！あれが生オタクだよ！きめえええええええ！」と友達らしき子とキャイキャイ
0292１３２人目の素数さん
2007/06/01(金) 00:28:410294１３２人目の素数さん
2007/06/01(金) 04:28:430295１３２人目の素数さん
2007/06/01(金) 11:00:14＞ 涼宮ハルヒの憂鬱は置いてないんだよ！」
ハルヒよりハヒル、という人は大人（ｗ
0296１３２人目の素数さん
2007/06/01(金) 11:13:12「なんで、"憂鬱"はあるのに、"消失"は置いてないの？」
とツッコム勇気はない。
もちろん、ハルヒではなくハヒルである。
0297１３２人目の素数さん
2007/06/01(金) 11:20:44Peano算術とか。
まあ表現力が弱いとか、片方がもう片方で解釈可能という意味の弱さね。
集合論ならKPなんていう体系はZFCより弱いはず。
0298１３２人目の素数さん
2007/06/01(金) 11:28:57「涼宮ハルヒの父親はおそらく京大卒のサラリーマン。
住所は阪神甲子園近く。
で、御多分にもれず父親は猛烈なトラキチで、
娘はそんな父親をアフォだと蔑んでいる。」
と推測しているが、こういう些細なことにこだわるのが真のヲタクだろう。
0299１３２人目の素数さん
2007/06/01(金) 13:53:45読めるところだけでも読んでおけ
0300１３２人目の素数さん
2007/06/01(金) 13:58:18猪狩さんの実解析入門
0301１３２人目の素数さん
2007/06/01(金) 15:06:38別のスレのネタ持ち込むなよ
0302１３２人目の素数さん
2007/06/01(金) 17:31:32ある日反例が見つかるかもとか
下手に説明すりゃどんどん妄想を膨らませるばかりだ
0303１３２人目の素数さん
2007/06/06(水) 10:44:40どこが決定的に怪しいのか、もしくは怪しくないのかわかりません
0304１３２人目の素数さん
2007/06/06(水) 15:51:180305１３２人目の素数さん
2007/06/07(木) 10:13:19分かりやすいはずなんだけどなあ。
あと第一不完全性定理のほうはrecursively enumerableとかそういう概念を使って
不動点定理を使わずに証明する方法もあるよ。
0306１３２人目の素数さん
2007/06/07(木) 11:39:06＞どこか眉唾物の雰囲気を漂わせている
まあ、気持ちはわかるよ。
不動点定理で出てくる項の意味を取ろうとしても
操作が完結しなくてできないっていうんでしょ？
でも、それを言われても困るんだよね。
0307１３２人目の素数さん
2007/06/07(木) 16:41:51ちなみに何ていう本読んでんの？
0308１３２人目の素数さん
2007/06/10(日) 12:32:59ZFからは証明できない。
0309１３２人目の素数さん
2007/06/10(日) 12:44:220310１３２人目の素数さん
2007/06/10(日) 12:46:530311１３２人目の素数さん
2007/06/10(日) 14:46:19ZFからは証明できない事を証明できない事を証明できない事を証明できる
0312１３２人目の素数さん
2007/06/10(日) 15:01:000313１３２人目の素数さん
2007/06/10(日) 15:02:560314１３２人目の素数さん
2007/06/11(月) 21:11:580315１３２人目の素数さん
2007/06/11(月) 21:37:300316１３２人目の素数さん
2007/06/12(火) 01:54:120317１３２人目の素数さん
2007/06/13(水) 11:32:05昨今のGoedelプチブームなどと考え合わせても、
あとは発展するだけじゃないかな。
0318１３２人目の素数さん
2007/06/25(月) 14:14:560319１３２人目の素数さん
2007/07/15(日) 08:03:42日本での最後の輝きにならないようお互いがんばろう。
0320１３２人目の素数さん
2007/07/15(日) 22:56:42今一つ分かりません。どなたかご教示ください。
0321１３２人目の素数さん
2007/07/16(月) 02:27:59ちゃんとした返事はこの後わかっている人に書いてもらうとして
論理主義は集合も数もとにかく数学的対象は論理法則から全て導けるという考えから始まったもの
形式主義は数学に非構成的手法を取り入れる正当性を証明を言わば図形とか機械語の列のような無意味な形として眺めることで構文的組み合わせ的に処理し(無矛盾性証明等)示すことでそのような手法を自由に使う数学を認めようという考え
前者はタイプ理論とか今も活きているし哲学よりの論理学者は最近も新しい結果を出している
後者の公理主義の部分は数学者の標準として活きている
0322１３２人目の素数さん
2007/07/19(木) 01:42:11集合を定義するときに既に定義されている集合しか使ってはいけないとき集合の定義は可術的、そうでないような定義を非可術的という
論理主義は可術的集合のみ扱い、形式主義は非可術的集合も扱う
0323辰宮鵺星守影踏丸
2007/07/19(木) 10:52:22predicativeの訳語で、predicateが叙述する、断定する、基礎を置くのような意味だから。
田中尚夫の「公理的集合論」でも「確かさを求めて」でもそうなっている。
因みにFregeとRusselの論理主義は結構違う。
FregeとRusselの論理主義について知りたかったら
「言語哲学大全 Ⅰ」や「ラッセルのパラドクス―世界を読み換える哲学」などを読むのが良い。
「フレーゲ哲学の最新像」なんていう本もある。
Hilbertの形式主義に関しては記号論理学の入門書を読むのが一番早いと思う。
0324１３２人目の素数さん
2007/07/19(木) 11:22:10すまん。いいもなにも完全な誤変換。訂正サンクス。
0325１３２人目の素数さん
2007/07/19(木) 21:11:010326１３２人目の素数さん
2007/07/19(木) 21:51:110327１３２人目の素数さん
2007/07/19(木) 22:05:280328325
2007/07/19(木) 23:35:54「aを定義するのに、定義されるべきaの情報を使用している」みたいなもんだと
思っていたら、調べてみると、例えば上限では「集合Sの上限aがa∈Sを満たす」
こともある（Sに最大値がある場合）わけですが、その場合、集合S全体を使って
定義されたaはSよりも型が上になるから、そもそもa∈Sと言うことを考えること
ができなくなってしまう、というのがラッセルの困ったところなんでしたっけか？
でも
「aを定義するのに、定義されるべきaの情報を使用している」みたいな話ありま
せんでしたっけ？
0329１３２人目の素数さん
2007/07/19(木) 23:44:24上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？
0330１３２人目の素数さん
2007/07/20(金) 10:14:58＞上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？
え？そうでしたっけ？aがSの上限であると言うのは、
∀x(x∈S→a≦x)∧∀b(∀x(x∈S→b≦x)→a≦b)
で表せますけど、どこら辺が「上限が定義されていないと上限は定義できない」のか教えたいただけませんか。
というか、むしろ実数の連続性が関係するのかな。
0331辰宮鵺星守影踏丸
2007/07/20(金) 10:39:15取られちゃったんじゃないの？多分。
0332辰宮鵺星守影踏丸
2007/07/20(金) 10:39:570333辰宮鵺星守影踏丸
2007/07/20(金) 13:06:45非可述的に定義すると言います。
論理主義というと良く名前が出てくるのは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
たとえば自らを含まない【或いは. 含む】ような集合すべての集合、とか。
0335１３２人目の素数さん
2007/07/21(土) 07:31:440336１３２人目の素数さん
2007/07/22(日) 05:00:57Revue de metaphysique et de morale,14(1906)294-317
Poincare
0337１３２人目の素数さん
2007/07/24(火) 22:25:190338１３２人目の素数さん
2007/07/25(水) 09:25:380339１３２人目の素数さん
2007/07/25(水) 09:29:140340１３２人目の素数さん
2007/07/25(水) 09:38:48http://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は計算可能にはならないはずです。
0341１３２人目の素数さん
2007/07/25(水) 10:08:00計算できないやつを実数化すればいいですね
話は変わりますがチューリングマシンにサイコロをつければ
計算能力は上がるんでしょうか?
0342１３２人目の素数さん
2007/07/25(水) 11:05:35計算できるかできないかなら変わらない。
さいころの目が固定されているなら、単純に全ての場合を模倣できる。
（１がでて１が出た場合、１がでて２が出た場合、、、６がでて６が出た場合）
なお、計算量で違いがあるかないかはわからない、
違いのあるなしが証明できれば、賞金付きのP=NP?問題。
0343１３２人目の素数さん
2007/07/25(水) 17:27:09適当に振ったらなぜか何か意味がある目が出てくると仮定すれば
オラクルとして使えることになるから変わるけど。
0344１３２人目の素数さん
2007/07/25(水) 20:03:00なるほど。出た目によって幅優先で探索すればよいので
計算可能性には影響しないのですね。
そしてサイコロTMで多項式時間で解ける問題が NPに含まれてるのは明らかと。
ではサイコロの出目が無限にある場合はどうなんでしょうか?
例えばポアソン分布にしたがうとか。
0345１３２人目の素数さん
2007/07/25(水) 21:44:220346１３２人目の素数さん
2007/07/26(木) 11:43:51NDTMのDTMによるシミュレーションにexpのコストがかかるかどうかが問題になってるの、
ついでに言うと、P=NP?問題はオラクルでは決着はつかない。
連続分布のほうは知らない。
0347１３２人目の素数さん
2007/07/26(木) 22:23:38[0 1 0 1 0 1 1]
[0 0 1 0 1 1 1]
0348１３２人目の素数さん
2007/07/27(金) 10:51:57まだ四巻買ってないけど。
0349１３２人目の素数さん
2007/07/27(金) 18:54:530350１３２人目の素数さん
2007/07/31(火) 11:40:51定理の集合の任意のモデルは補集合の要素を真にしないので、濃度がNと同じなら、真にする論理式の範囲が異なることがない、
すなわち、範疇的である、と思うのですが、正しいでしょうか？ご教授お願いします。
0351１３２人目の素数さん
2007/08/01(水) 11:44:53いいんじゃない？
でも、その体系だと、「２は平方数ではない」が記述できないと思うよ。
0352１３２人目の素数さん
2007/08/02(木) 00:23:51「なんでそんなことを証明したいのか」がわからなくなって放り出した．
あれから十年以上経つけど、この板にお住まいのすごい人たちに、cut-elimination の意味を
教えて欲しいです．
0353１３２人目の素数さん
2007/08/02(木) 00:33:440354１３２人目の素数さん
2007/08/02(木) 00:56:44僕はそのことが基礎論とどう関係があるのかわかりません。
0355１３２人目の素数さん
2007/08/02(木) 01:59:58cut-elimination → 算術の無矛盾性
0356１３２人目の素数さん
2007/08/02(木) 13:41:230357１３２人目の素数さん
2007/08/02(木) 21:15:11証明可能なＳｅｑｕｅｎｔが、それに含まれる論理式の部分論理式だけを使って証明できるってだけでも
「へぇー、すごいなあ。」と思ったものだが。
0358１３２人目の素数さん
2007/08/03(金) 01:52:04自分のは、「わざわざややこしいCut規則を導入しておいて、それを除去して
喜んでいる」みたいな印象を受けていました．『Cut 規則がないと、色々な
証明図が長くなりすぎる傾向があるから Cut 規則を導入しておくけど、
証明体系の性質についての議論をするときに、Cut が技術的な障害になる
ので、Cut なしの証明図に書き換えてよい事を示しておく(※)』のかなあ、とか
考えましたが、独りで本を読んでいて誰にも相談できなかったので、
消化不良感だけ残りました．
やっぱり※という理解は間違ってますかね？
0359１３２人目の素数さん
2007/08/03(金) 06:27:38その理解でもいいと思います。
あとは、LKから構造規則を抜いて部分構造論理を作ったり、
□の規則を加えて様相論理を作ったりしますが、
その時にcut除去定理が成り立ったり成り立たなかったりします。
そのたびにcutを追加したり外したりするのは厄介だし本質的ではないので、
とりあえずいつもcutを入れておく、というのも１つの理由だと思います。
とりあえず入れておいて、cut除去定理が成り立つか否か、という話にしたほうが、
見通しがよくなります。
あとは、cut規則は論理学でいう三段論法に近い感じなので、
論理学の中で重要な三段論法を外せる、という意味合いもあると思います。
Aと￢Aから空シークエントを導出させて無矛盾性の証明もできたりします。
0360１３２人目の素数さん
2007/08/03(金) 09:09:010.238X+9.85√X = 6000
この解き方を教えてください！お願いします。
0361１３２人目の素数さん
2007/08/03(金) 09:14:27数学基礎論と何の関係が？
0362１３２人目の素数さん
2007/08/03(金) 09:14:35>>8
0363１３２人目の素数さん
2007/08/03(金) 11:58:04そういう記号的な操作がどうのこうのということではなくて、算術の無矛盾性とか
さらには数学そのものの無矛盾性とか、そういう雲の上の獲物たちを狙うための道具じゃないのコレって。
0364１３２人目の素数さん
2007/08/03(金) 12:36:06具体的に得る方法を与える証明もあるよ
0365１３２人目の素数さん
2007/08/03(金) 14:55:31cut除去についていうと、確かにcutは除去できるし
それによって無矛盾性は証明できるけど、
「確かに除去できる」と主張するための帰納法は、
元の体系からは証明できない。
0366１３２人目の素数さん
2007/08/03(金) 15:24:35「わざわざ導入」でいいの？あくまで、
通常の証明では三段論法はあたりまえのように使うので、形式化した推論・証明を考える際も、三段論法を表現できないとダメ。
だけどLKタイプの体系では、カット以外の推論では（単純に）三段論法を扱えないので、カットを導入する必要がある。
だだカット消去定理が成り立つので、結果的にはカットは導入しなくても証明できる論理式に違いは無いことが分かる。
では？
0367１３２人目の素数さん
2007/08/03(金) 16:37:07LKって別に普通の証明を記述するための体系ではないよ。
またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
cutの除去はあくまで無矛盾性証明のためのプロセス。
こういうことはロジシャンには常識なんだが、一般人はまず知らない
0368352=358
2007/08/03(金) 21:13:54やはりcut-eliminationは技術的な詳細であって、それを使って
何をするかという事のほうが、少なくとも初学者にとっては大事だったみたいですね．
久しぶりに証明論の本を取り出して眺めてしまいました．15年前に２ちゃんがあったら
、独りで悩まずにすんだろうにな～．
0369１３２人目の素数さん
2007/08/03(金) 21:20:21＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
え？cutを除去したら、無駄のない証明になるんでないの？
0370１３２人目の素数さん
2007/08/03(金) 22:35:420371１３２人目の素数さん
2007/08/04(土) 06:32:14その○○の定理の証明が書いてあったらたまらない。
0372１３２人目の素数さん
2007/08/04(土) 09:04:480373369
2007/08/04(土) 09:18:31取り除いた証明図を見比べたら、後者の方が無駄のない証明図になっていると思うんだけど。
>>371が言ってるのはそれとは別でしょ。
0374１３２人目の素数さん
2007/08/04(土) 09:24:050375１３２人目の素数さん
2007/08/04(土) 13:17:38＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。
というのは、
（実際の数学の証明をLKで書き出すようなことは
現実的にはほとんど無いが、仮に書くとしたら）
cutありならまだ何とか読める証明も、cut無しなら重複が多くて読めたものじゃなくなる、
ということでしょ、たぶん。
0376１３２人目の素数さん
2007/08/04(土) 13:19:54cutless の証明は, 定理を適用しない,
ものすごい冗長な証明になっているということだが。
0377１３２人目の素数さん
2007/08/04(土) 13:29:05cut
0378１３２人目の素数さん
2007/08/04(土) 14:29:05>cutを除去したら、無駄のない証明になるんでないの？
間違い。曖昧なのではなく明確に間違い。
0379１３２人目の素数さん
2007/08/04(土) 14:30:45君、実際にcut除去したことないだろ。
だからそういう全くのウソを平気で喋れるんだ。
手を動かせないなら口も動かすな。
0380１３２人目の素数さん
2007/08/04(土) 16:40:140381１３２人目の素数さん
2007/08/04(土) 21:45:09要するに議論のモジュール化ということだよね。
なんか陳腐な言い方になっちゃうけど。
0382369
2007/08/05(日) 12:58:02すれば、三重否定からの二重否定の除去 ⇒￢￢￢Ａ⊃￢Ａが得られると
聞いて素直にSequentで証明したことがある。
Ａ⇒Ａ
－－－－－－－－－
￢Ａ，Ａ⇒ Ａ，Ａ⊃￢￢Ａ⇒￢￢Ａ
－－－－－－－－－ －－－－－－－－－－－－－－－－－－－
Ａ⇒￢￢Ａ ￢￢￢Ａ，Ａ⊃￢￢Ａ⇒￢Ａ
－－－－－－－－－ －－－－－－－－－－－－－－－－－－－
⇒Ａ⊃￢￢Ａ Ａ⊃￢￢Ａ⇒￢￢￢Ａ⊃￢Ａ
－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－
⇒￢￢￢Ａ⊃￢Ａ
でもそれをCut除去定理の証明の方法でCutを除去していったらすごく簡単
になってびっくりしたんだよね。
Ａ⇒Ａ
－－－－－－－－－－－－－
￢Ａ，Ａ⇒
－－－－－－－－－－－－－
Ａ⇒￢￢Ａ
－－－－－－－－－－－－－
￢￢￢Ａ，Ａ⇒
－－－－－－－－－－－－－
￢￢￢Ａ⇒￢Ａ
－－－－－－－－－－－－－
⇒￢￢￢Ａ⊃￢Ａ
私が言いたかったのは具体的に言うとこういうこと。
0383１３２人目の素数さん
2007/08/05(日) 15:48:06リテラル１個しかないような命題論理の証明１つだけで
「どんな証明もカット除去すれば簡単になるっ！」
と断言されてもなあ。全然論理的じゃないし。
0384369
2007/08/05(日) 16:30:30うーむ。それはそうだなあ。しかし、今まで自分が実際にcutを除去したときはいつも簡単になったので
そう信じていた。それなら、今まで実際にcutを除去したことある人で、cutを除去したら証明が冗長に
なった例を知っている人は教えてくれないかな。というか、そういう例を探してると次第に「cut除去する
と証明って簡単になるんだな」と思えてくると思うのだが。
0385１３２人目の素数さん
2007/08/05(日) 17:46:08cut を除去すると証明の長さが指数関数的に増大する例がありそう．
0386１３２人目の素数さん
2007/08/05(日) 19:52:07ＡＡにしかみえない
0387１３２人目の素数さん
2007/08/05(日) 20:42:51命題論理の簡単な証明なら cut 使うまでもないからなあ。
算術での例がこれの appendix にある
ttp://www.seitoku.ac.jp/~ikedak/arai.pdf
詳細は追っかけてないけど証明のサイズが論理式の double exponential になるのかな
0388１３２人目の素数さん
2007/08/06(月) 09:06:50George Boolosの論文
"Don't eliminate cut"
を読め。そういえばこれも算術での例。
0389１３２人目の素数さん
2007/08/06(月) 14:17:46算術の例というわけではないでしょ．
0390１３２人目の素数さん
2007/08/06(月) 14:35:10算術っていってるのは、自然数論のこと。
勿論、公理まで含めて記述すれば述語論理の命題になるからＯＫ
0391１３２人目の素数さん
2007/08/06(月) 14:45:01はじめからそう記述しているよね。
0392１３２人目の素数さん
2007/08/08(水) 01:39:02Jean-Yves Girard
0393１３２人目の素数さん
2007/08/08(水) 10:59:50＞A sequent calculus without cut-elimination
cut除去なしのsequent計算がエンジンのない車のようだと言ってるの？
0394１３２人目の素数さん
2007/08/08(水) 11:19:20基本的に分解していけばいいので
アホでも出来る。
cutを使って簡潔な証明を書くには魔力が必要（ｗ
0395１３２人目の素数さん
2007/08/15(水) 00:03:490396１３２人目の素数さん
2007/08/16(木) 00:31:37－×－＝＋
になるのはどうしてなんでしょうか？
0397１３２人目の素数さん
2007/08/16(木) 00:38:120398１３２人目の素数さん
2007/08/18(土) 09:47:47うまくいく場合は、上手下手に関係なく剥ける。
0399１３２人目の素数さん
2007/08/19(日) 12:52:01うまくいくシーケントかどうか計算できない。
0400１３２人目の素数さん
2007/08/20(月) 07:36:08事前の計算は不必要。
うまくいく場合には、方法論に依存しないといっただけ。
もちろん、これは手数を度外視している。
手数をケチるには、オツムを使う必要がある。
0401１３２人目の素数さん
2007/08/24(金) 15:24:36証明図 f(P) を対応させる関数 f は、原始帰納的でつか？
0402１３２人目の素数さん
2007/08/24(金) 15:30:37P と f(P) が同じ命題の証明って条件は当然付くんだよね
考えたことないが、原始帰納では厳しいんじゃないか？
0403１３２人目の素数さん
2007/08/24(金) 17:05:49レスありがとうございます。
はい。同じ命題の証明図です。
帰納的な事は、すぐにわかるのですよ。
（二重帰納法を使いますが）
原始帰納的なことの証明を与えようとして、うまくいかなかったので。
やはり厳しいと予想されますか。
0404１３２人目の素数さん
2007/08/25(土) 01:20:38通常の帰納法で証明できることは Gentzen の自然数論の無矛盾性の論文に
ちょろっと書いてある．
Girard の本では二重帰納法による証明の評価をまじめにやって、原始帰納的な
上限を与えている．
0405１３２人目の素数さん
2007/08/25(土) 20:07:06ありがとうございます！
0406１３２人目の素数さん
2007/08/26(日) 12:10:54(2) 入門としての集合の講義なのでそんなことを授業で話す必要は
まるでないのだけど、教える以上は知っておかなければならないだろうと
ZF 等の公理論的なものや歴史を勉強しようと思った。
(3) とりあえず岩波基礎数学の集合と位相を読み、また歴史関係の本を読む。
学生時代、そういうことは勉強しなかったこともあり、とても面白い。
(4) ところがその後いろいろと詰めて考えみると「命題」というものが
良くわかってないことが判明。
(5) しょうがないので基礎論の教科書を読み出し、見事にはまる。
というわけで現在本業(微分方程式)そっちのけ状態w 質問ですが、
(a) 現在の数学基礎論は多岐にわたるそうですが、現在の研究の進展状況を
解説したもの (所謂 survey) はないですか？
(b) 数学基礎論ではどういう学会・研究集会があるんですか？
日本数学会ではあまり活動してないようなんだけど・・・。
知り合いに基礎論関係の人がいません。教えてくださいませ。
0407１３２人目の素数さん
2007/08/26(日) 12:44:31僕も日本数学会の基礎論分科会に属していますが、
入会以来、なしのつぶて。
研究集会など、何の連絡もありません。
0408406
2007/08/26(日) 12:55:02どもども。
僕は分科会は関数方程式論にしか入ってませんが、ここは分科会の人が頑張って
メーリングリストで研究集会の連絡をしたり、り欧文論文雑誌などを作ったりなど、
それなりには活動はしてますね。
数学会の基礎論の分科会はあまり活動してないのかな。
日本にも基礎論の人が結構いるみたいだから、どこかで活動はしてるんだと
思ったんだけど、どこで頑張ってるのかなぁ。参加しやすそうな研究集会とかに
ぶらりと言って顔を出してみたかったんだけど。
0409１３２人目の素数さん
2007/08/26(日) 14:14:30専攻柄数学観を強固に持っている人が多いし、そこを侵されるのを極端に嫌う傾向が強い。
0410γ ◆WqqSMT0LS6
2007/08/26(日) 16:51:430411１３２人目の素数さん
2007/08/26(日) 17:20:40＞「命題」というものが良くわかってないことが判明。
具体的に、命題の何がどう分からないのでしょうか？
ところで、本当に公理的集合論についての講義が学生に必要だと
お考えならば、貴方が勉強するよりも、集合論の研究者に講義を
任せるほうがよろしいかと思いますが、いかがでしょうか？
0412１３２人目の素数さん
2007/08/26(日) 17:22:14部外者は知りもしないで口からデマカセのウソばかりいうね。
0413１３２人目の素数さん
2007/08/26(日) 20:42:23今から本屋に行って
「ゲーデルと２０世紀の論理学」を買ってきて読む
→数学基礎論サマーセミナー2007に参加する。
9/4から三日間の間静岡で行われます。8/31が締切なのでお早めに。
集合論に関する比較的入門的な内容の講義をするようです。（forcingとかBoole値モデルとか）
私は基礎論の専門家じゃないですけど、
基礎論の専門家が居る大学では、
それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。
0414１３２人目の素数さん
2007/08/26(日) 22:45:28正しくは、数学基礎論サマースクール、だね。
0415１３２人目の素数さん
2007/08/26(日) 22:56:21ちょっと書き方がわるかったようですね。
「入門としての集合の講義」というのは一年生の数学の入門としての講義です。
所謂、素朴な集合論のことですね。
ただ、ある程度しっかり話そうとするとこのテーマで話す場合 excuse を
並べることになりますね。そこをいかに話すかが、先生の腕の見せ所となるかと
思いますが、しかし知らないことを話すわけにはいかない。
あーだ、こーだと下手な考えをするまえに、現時点で数学では集合はどのように
理解されてるかをまず知っておこう、というのが勉強を始めた動機です。
> 具体的に、命題の何がどう分からないのでしょうか？
集合論で使う命題の定義がわからなくなったんですよ。
> ところで、本当に公理的集合論についての講義が学生に必要だと
> お考えならば、
普通の数学科の入門としての講義では必要ないと思ってますよ。
私自身も自分の研究では今まで（そして、おそらく今後も）なしで済ませていて、
それで困ったことがありませんから。
> 集合論の研究者に講義を任せるほうがよろしいかと思いますが、いかがでしょうか？
特論などで本当に講義をしてもらうのであれば、そのほうがいいでしょうね。
というより、そうすべきでしょうね。
0416406=415
2007/08/26(日) 23:06:41どうも、どうも。四巻からなる本ですね。
サマースクールですか。
まともに出張の日と重なってしまいました。
しかし、そういう活動はされてるんですね。いいですね。
> 基礎論の専門家が居る大学では、
> それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。
なるほど。いろいろ探してみたら、比較的近くの大学で基礎論の研究グループが
あるみたいです。とりあえずはそこをホームページをウォッチしてみますね。
どうもありがとうございました。
0417（´・ω・`）
2007/08/27(月) 00:05:150418１３２人目の素数さん
2007/08/27(月) 00:56:100419１３２人目の素数さん
2007/08/27(月) 01:09:59ただ独学は危険
0420１３２人目の素数さん
2007/08/27(月) 11:32:14いえ、書き方は悪くありません。
「入門としての集合の講義」だということは分かっていましたから
公理的集合論のことなど言い訳としても考慮する必要がないだろう
という意味で書きました。
さて
>> 具体的に、命題の何がどう分からないのでしょうか？
>集合論で使う命題の定義がわからなくなったんですよ。
集合論のどこで使う命題でしょう？
内包的記法で使う場合のことでしょうか？
それなら｛ｘ｜Ｐ（ｘ）｝と書かずに、すでに集合と分かっているａについて
｛ｘ∈ａ｜Ｐ（ｘ）｝と書いておけばラッセルパラドックスはおきません。
0421１３２人目の素数さん
2007/08/27(月) 11:46:330422１３２人目の素数さん
2007/08/27(月) 12:15:54どうして{x; φ(x)}がclassであってもsetではないのかが
学生には十分納得できないと思うけどね。
0423１３２人目の素数さん
2007/08/27(月) 12:19:46> 公理的集合論のことなど言い訳としても考慮する必要
私、何か言い訳けしましたっけ？
>集合論のどこで使う命題でしょう？
至るところで使う命題のことですよ。
失礼ですが、命題とは何かここで定義してみていただけますか？
>ラッセルパラドックスはおきません。
そうですね。だから？
0424１３２人目の素数さん
2007/08/27(月) 14:44:00>私、何か言い訳けしましたっけ？
これから、学生に対してするんでしょう？
excuseを並べるといったじゃないですか。
>>集合論のどこで使う命題でしょう？
>至るところで使う命題のことですよ。
うーん、普通の数学では気にならないのに
なぜ、集合論だと問題になるんでしょう。
メタ数学の話をするわけじゃないんでしょ？
>>ラッセルパラドックスはおきません。
>そうですね。だから？
ラッセルパラドックスが気になってるんだろうと
見当つけたんですが、もっと手前でつまづいてるんですか？
0425１３２人目の素数さん
2007/08/27(月) 14:49:16・・と言うようなことをおっしゃったので、
恐らくは、論理式の定義で、躓いているのではないですか？
0426１３２人目の素数さん
2007/08/27(月) 14:50:39文句ならツェルメロにいってくれよｗ
>どうして{x; φ(x)}がclassであってもsetではないのか
古典論理や直観主義論理で考える限りにおいては、
上記のようなsetでないclassはどうしても存在せざるを得ない。
0427１３２人目の素数さん
2007/08/27(月) 15:03:16それこそ、集合論を BG 式に定式化して、
学生に説明する必要があると思う。
0428１３２人目の素数さん
2007/08/27(月) 15:39:49方式の問題ではないんだな。
集合であろうがなかろうが、ＶとＶ→２の間に
一対一対応なんかつけられないんだから。
0429１３２人目の素数さん
2007/08/27(月) 19:51:370430１３２人目の素数さん
2007/08/27(月) 19:58:140431１３２人目の素数さん
2007/08/27(月) 20:09:33>>415はまだ曖昧
>>420はちょっとピントがずれてるけど煽りではない
>>423は煽り
0432１３２人目の素数さん
2007/08/27(月) 20:15:080433１３２人目の素数さん
2007/08/27(月) 20:26:22要求の意味がわからない。
0434１３２人目の素数さん
2007/08/27(月) 20:43:01もう解決してるんだよ。そこんとこわかってやれよ。
だから、>>411はかなりトンチンカン。というか、相手を見下した感じがして失礼だと思う。
そもそも>>406の(2)を読めよ。公理的集合論を講義で教えるつもりはないと書いてある。そして、
なぜ、それでも公理的集合論について調べたくなったかも書いてある。
．．．つーか
ちゃんとレス嫁。
0435１３２人目の素数さん
2007/08/27(月) 20:46:58同意
0436１３２人目の素数さん
2007/08/27(月) 21:03:13ある文字列が命題であるとは？
0437433
2007/08/27(月) 21:12:27あー、そういうことね。
確か、文字列の長さに関する帰納法で定義するんじゃなかったかな？
ここに定義を書くのは、めんどくさいけど。
で、日常語に近い高級言語って、何ですか？
0438１３２人目の素数さん
2007/08/27(月) 21:19:18Zermeloはきちんと正当化のための論文を書いて居るし
現代の数学の哲学の研究者もiterative concept of setなんてことに対して
深く考えたりしているよ
setでないclassが存在せざるを得ない、というのは古典論理や直観主義論理からの
論理的帰結でも何でもないんですけどね。
0439１３２人目の素数さん
2007/08/27(月) 21:38:36たとえばプログラミングで
機械が読むためのアセンブリは低級言語、
人が読むためのCなんかは高級言語。
命題の定義を、論理式などではなく、普通の数学の
日常的な言葉で言ってみろ
という話。
0440406, 415, 423
2007/08/27(月) 21:45:10申し分けないことです。>>411 あたりで怪しいなとは思ったのですが、
中途半端に相手にしたのが間違いだったようですね。
すいません。
もう私は相手にしないことにします。
そうそう、もう集合の授業は無事終わってますからね。大部昔の話です。
それでは、私の書き込みはこれで終わりにします。
0441441
2007/08/27(月) 21:55:420442１３２人目の素数さん
2007/08/27(月) 22:49:27あーそういう話だったのね。納得した。
>>406 の「はまる」ってのを「さっぱりわからん」って意味にとっちゃって、
(a)(b) とつながんなくておかしいなあって思ってた。
>>411 とは別人ですが、同じ勘違いをしたんじゃないでしょうか。
0443１３２人目の素数さん
2007/08/27(月) 23:19:04取りようがなかったと思う。
0444１３２人目の素数さん
2007/08/27(月) 23:44:54そっちの解釈で頑張って理解しようとしてしまうんですよ。
0445１３２人目の素数さん
2007/08/28(火) 01:17:370446１３２人目の素数さん
2007/08/28(火) 02:01:52って流れだろ、常識的に考えて。
0447１３２人目の素数さん
2007/08/28(火) 02:13:36・専門は微分方程式。
・本業(微分方程式)そっちのけ状態。
この3つからは、「さっぱり分からん」の流れもまた「常識的」だろ。しかし、後半の(a)(b)とは
繋がらない。で、なぜ繋がらないのか考えようとしても、>>444のような思考のスパイラルに陥る
(このスパイラルもまた、常識的に考えてよくあること)。
すなわち、「さっぱり分からん」と解釈して首をひねる人が出るのも、常識的に考えて普通。
0448１３２人目の素数さん
2007/08/28(火) 02:15:28そんなことより、結局「命題」を定義できる奴は此処には折らんの？
0449１３２人目の素数さん
2007/08/28(火) 07:37:25＞>>406,415さんは、集合論をやり始めたときは命題がわからなかったけど、
＞>>406を書いた時点ではもう解決してるんだよ。
ウソでしょ。
>>435
＞同意
自作自演でしょ。
0450１３２人目の素数さん
2007/08/28(火) 07:39:06＞{ X:文字列 | X ∈ {命題} }
間違い。"X ∈ {命題}"なんて書き方はない。
顔洗って出直せ。
0451１３２人目の素数さん
2007/08/28(火) 07:45:40後からいくら言い訳したって、場当たり的でなくなるわけでもない
＞現代の数学の哲学の研究者も
＞iterative concept of setなんてこと
＞に対して深く考えたりしているよ
Boolosの反復的集合観が、classの存在を否定するわけでもない
0452１３２人目の素数さん
2007/08/28(火) 08:05:20定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか
必要な公理を統一性もなくただ要請していくようなやり方よりは幾分かはマシだよ。
あくまでいくらかは、だけどね。
＞Boolosの反復的集合観が、classの存在を否定するわけでもない
そりゃ当たり前で、だいたい>>422に書いてあるのは、
classが必ずしも集合とは言えない、ということだけで
classが存在しないなんてことは誰も言っていない。
classが存在すると考えても新たな矛盾は起きない、それだけ。
0453１３２人目の素数さん
2007/08/28(火) 08:11:54www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/
ただしコチラは集合ではなく論理が中心だが。
0454１３２人目の素数さん
2007/08/28(火) 08:17:17＞classが必ずしも集合とは言えない、ということだけで
＞classが存在しないなんてことは誰も言っていない。
>>426に書いてあるのも、集合でないclassがあるのは
通常の論理では致し方ない、ということだけだが。
少なくとも対角線論法によって矛盾を導き出せるならば
そうならざるを得ない。
0455１３２人目の素数さん
2007/08/28(火) 08:19:52＞定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか
＞必要な公理を統一性もなくただ要請していくようなやり方よりは
＞幾分かはマシだよ。あくまでいくらかは、だけどね。
その言い分、まるで今井弘一の複ベクトルの正当化と同じだな。
0456１３２人目の素数さん
2007/08/28(火) 11:05:17Boolosとかが書いた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の案が採用されたのは
歴史的経緯に過ぎないよ。
0457１３２人目の素数さん
2007/08/28(火) 12:02:39「必要な公理を統一性もなくただ要請していく」
としか認識できない点が、ｉ＾２＝１なる元ｉ
を添加する複素数体の構成の仕方をアドホック
なものとして嫌う、能登の御隠居と全く同じ
感覚だと述べたまで。
0458１３２人目の素数さん
2007/08/28(火) 12:12:35＞∃y.∀z.(z∈y⇔φ(z))という式のφに￢z∈zという論理式を入れると
＞矛盾しますよ、というだけで、じゃあどういう論理式を排除するべきか、
＞という判断にはあまり合理的な根拠がない。
そもそも、「φに入る論理式を排除する」という
判断それ自体に全く論理的な根拠がない。
0459１３２人目の素数さん
2007/08/28(火) 12:17:11＞yが「絶対無限多数」になってしまうから
＞いけないんだとか考えていたけど、
それ以前に、濃度の違い云々というのが
対角線論法の成立から出てきているわけで
そもそもその対角線論法自体が成り立たない
ような論理を考えるという方策もある。
0460１３２人目の素数さん
2007/08/28(火) 12:24:15＞型に関するルールが守られていないからだめなのだ、
＞という考えもあり得るし、またそれと別に、
＞φに否定記号が入っているような論理式を認めないようにしよう、
＞という定式化の仕方もありうる。
＞http://en.wikipedia.org/wiki/Positive_set_theory
＞実際この集合論でもZFCや、ZFCより強いMorse-Kelleyの集合論を
＞解釈できる能力を持っているわけで、CantorやZermeloの案が
＞採用されたのは歴史的経緯に過ぎないよ。
そもそも古典論理が採用されたのも歴史的経緯に過ぎない。
0461１３２人目の素数さん
2007/08/28(火) 14:15:57公理系
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上で証明してある
ところがあるなら教えていただけないでしょうか。
0462１３２人目の素数さん
2007/08/28(火) 14:26:20（１０）はexistential instantiation ruleから
（１１）はdeduction theoremから導く
0463１３２人目の素数さん
2007/08/28(火) 14:37:51でも実際Zermeloが最初に集合論の公理的取り扱いに関する論文を
発表したころは誰も見向きもしなかった。
なぜなら少なくとも当時の数学者には、Zermeloの公理系が
ただ「必要な公理を統一性もなくただ要請していく」ように見えたからね。
>>458に対しては
矛盾する命題が導かれるんだから論理的根拠はあるでしょ。
少なくともreductio ad absurdumが成り立つ限りにおいては。
古典論理が採用されたのが歴史的経緯に過ぎないという意見は
一般に認められたものでもないと思うけどね。
0464１３２人目の素数さん
2007/08/28(火) 14:45:19＞Zermeloの公理系がただ
＞「必要な公理を統一性もなくただ要請していく」
＞ように見えた
のは「当時の数学者」ではなく君だろう。
それとも君はその当時の数学者だったのか？
0465１３２人目の素数さん
2007/08/28(火) 14:48:28＞＞という判断にはあまり合理的な根拠がない。
＞そもそも、「φに入る論理式を排除する」という
＞判断それ自体に全く論理的な根拠がない。
＞矛盾する命題が導かれるんだから論理的根拠はあるでしょ。
ないよ。φに入れる論理式のせいだと決め付ける論理的根拠はない。
実際、φに入れる論理式を制限せずに解決できる。
場当たり的というなら、φのせいだというのも場当たり的
場当たり対場当たりなら引き分け。
0466１３２人目の素数さん
2007/08/28(火) 14:57:45矛盾が導けなければ背理法が認められても意味がないｗ
＞古典論理が採用されたのが歴史的経緯に過ぎないという意見は
＞一般に認められたものでもないと思うけどね。
実際には、昨今の論理の研究は、君の思い込みが
正しくないことを示しつつある。
0467１３２人目の素数さん
2007/08/28(火) 15:07:450468１３２人目の素数さん
2007/08/28(火) 15:19:54もっともレベルの低い話ですいません。命題論理です。
公理
(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)
0469１３２人目の素数さん
2007/08/28(火) 15:22:28いや当時の数学史に関して普通によく言われることなんだけど。
私の個人的意見ではないですよ。
>>465>>466>>467
古典論理もしくは直感主義論理のような背理法が使える論理を
前提に話をしてるんだけどね。
部分構造論理くらい知ってるけど、そんなの研究してるのは
大抵計算機関係の人だと思ってたけどね。
部分構造論理だとか矛盾許容論理を使って
集合論だとか解析だとかをやろうなんて話はほとんど聞いたことがない。
「昨今の論理の研究は古典論理が採用されたのは
歴史的経緯に過ぎないことを示しつつある」なんて大嘘もいい所。
大多数の数学者は古典論理は自然に受け入れた。
なぜならそれまで自分たちが使っていた論理を自然に形式化したものだったから。
0470１３２人目の素数さん
2007/08/28(火) 15:24:09(1)と(2)から証明の複雑さに関する帰納法で
演繹定理というものが導けるからそれを使えばいい。
教科書には大抵載ってます。
0471１３２人目の素数さん
2007/08/28(火) 15:25:55○直観
0472１３２人目の素数さん
2007/08/28(火) 16:02:51＞古典論理もしくは直感主義論理のような
＞背理法が使える論理を前提に話をしてるんだけどね。
直観主義論理では、背理法は無条件には使えないよ。
＞部分構造論理くらい知ってるけど、そんなの研究してるのは
＞大抵計算機関係の人だと思ってたけどね。
んなこたぁない。
＞部分構造論理だとか矛盾許容論理を使って
＞集合論だとか解析だとかをやろうなんて話は
＞ほとんど聞いたことがない。
Grisinが聞いたら嘆くだろうな。
「縁無き衆生は度し難し」
とかいって。
0473１３２人目の素数さん
2007/08/28(火) 16:08:05＞なぜならそれまで自分たちが使っていた論理を
＞自然に形式化したものだったから。
ふーん。
じゃ聞くけど
・１２０円持ってる
・１２０円でコーラが買える
・１２０円でお茶が買える
古典論理だと、ここから
・コーラもお茶も手に入る
が導けるけど、こんなこといったら
コドモにもバカにされるぞｗ
0474１３２人目の素数さん
2007/08/28(火) 16:20:16度量の狭さを自ら露呈することもないだろ
0475１３２人目の素数さん
2007/08/28(火) 16:30:17単に経済活動においては古典論理が成り立たないことの例を示したまで。
マルクスがこれを知っていたら、弁証法の代わりに部分構造論理を
口にしたかどうかは定かではないが。
0476１３２人目の素数さん
2007/08/28(火) 16:33:410477１３２人目の素数さん
2007/08/28(火) 16:35:530478１３２人目の素数さん
2007/08/28(火) 16:49:34常識でガチガチに固まってるから
簡単に煽られて炎上するんだよ。
0479１３２人目の素数さん
2007/08/28(火) 17:09:32演繹定理使えば？
0480461
2007/08/28(火) 17:10:08ついてみると、(11)はとても簡単でした。お騒がせしました。）
ところが(10)がまだわかりません。どうか、もう少しヒントなりいただけないでしょうか。
それから、証明したい論理式の型を1つ忘れていました。
(12) ∀xF→F[t/x]
（F[t/x]はFにある自由なxの全てに項tを代入したもの。ただし、代入可能な場合に限る）
これもなかなかわかりません。どうかお助けください。
0482468
2007/08/28(火) 17:29:47いまのところ(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)
0483461
2007/08/28(火) 21:08:46私が>>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を導くこと」
になってること、見えてます？そうすれば演繹定理なんて簡単なんだけど。
0484484
2007/08/28(火) 22:16:430485１３２人目の素数さん
2007/08/28(火) 23:10:48(10)はごめんなさい、勘違い
ちょっとやり直してくる
0486１３２人目の素数さん
2007/08/29(水) 00:11:08閉じてない論理式に対しては演繹定理成り立ってないような気がします。
(11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。
0487461
2007/08/29(水) 09:09:51＞閉じてない論理式に対しては演繹定理成り立ってないような気がします。
generalization（>>461の推論規則(9)）が無条件で行われるので当然ではないで
しょうか。そもそも私が最初に(11)が証明できないと早合点してしまったのも
それが原因です。
＞(11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。
ええ、ですから私も>>480で(11)に関しては証明できたと申し上げました。
0488468
2007/08/29(水) 09:26:08戸田山氏の「論理学をつくる」に書いてありました。
これで勉強します_(_o_)_
0489461
2007/08/29(水) 13:07:56Kalish, 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)のみです。
こっちはできるかどうかわかりませんが、がんばります。また、お分かりの方
いましたら、ご教示いただけるとたすかります。では。
（ある程度昔の論文ならネット上で誰でも閲覧できる、何てふうにならないか
なあ。）
0491１３２人目の素数さん
2007/08/29(水) 15:27:190492１３２人目の素数さん
2007/08/29(水) 16:42:03> をネット上で見つけることができました。>>461の(10)に関しては最初の方
> （p.85のLEMMA 2.）で証明されていました。
これの概要教えて
0493１３２人目の素数さん
2007/08/29(水) 17:01:39ならんな。泥棒猫め
0494461
2007/08/29(水) 17:07:50を、興味を持ってくれた人がいるんですね。では概略を。命題論理関係の式変形
は省きます。
(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)
0496１３２人目の素数さん
2007/08/29(水) 17:10:130497497
2007/08/29(水) 22:40:280498１３２人目の素数さん
2007/08/30(木) 07:41:370499１３２人目の素数さん
2007/09/02(日) 16:02:310500１３２人目の素数さん
2007/09/02(日) 22:46:41その例で内容をなぞりつつ文献を読まないと
表面的な理解にすらも行き着かずに終わるだろうね。
0501１３２人目の素数さん
2007/09/03(月) 18:17:18タイトルは「プリクリ オルタネイティヴ」
0502１３２人目の素数さん
2007/09/04(火) 10:22:130503１３２人目の素数さん
2007/09/22(土) 01:11:45結局集合算はドリルしないとだめじゃね？
0504１３２人目の素数さん
2007/09/25(火) 20:21:090505１３２人目の素数さん
2007/09/25(火) 21:51:22んーまあ、何をやりたいかによるんだよ。
1+1やるのに毎回毎回ペアノ算術したりλ計算する奴はあんまりいないよね？
までも一回は集合のジャングルで遭難しておいた方がいいとは思うけどね。
進めなくなって娑婆に出てこれなくなるかもだがｗ。
0506１３２人目の素数さん
2007/09/28(金) 00:24:210507１３２人目の素数さん
2007/09/28(金) 00:28:56へ?
0508１３２人目の素数さん
2007/09/28(金) 03:23:07高階論理、４階以上ならでてくる。
0509１３２人目の素数さん
2007/10/01(月) 11:41:28M_SHIRAISHI降臨？
0510１３２人目の素数さん
2007/10/01(月) 20:29:240511１３２人目の素数さん
2007/10/01(月) 20:30:260512１３２人目の素数さん
2007/10/01(月) 22:10:100513１３２人目の素数さん
2007/10/03(水) 04:53:03普通にtype理論を扱った教科書にはでてくるだろう。
なお、
"M_SHIRAISHI"はNGワード
0514１３２人目の素数さん
2007/10/04(木) 12:02:08君が見た本の書名と証明が書かれたページ数を記載すればいい。
0515１３２人目の素数さん
2007/10/04(木) 16:54:560516１３２人目の素数さん
2007/10/05(金) 09:51:02そもそも
「普通にtype理論を扱った教科書」
なんて知らん
0517１３２人目の素数さん
2007/10/06(土) 01:07:220518１３２人目の素数さん
2007/10/06(土) 03:23:09P,Andrews 小川訳:数理論理学とタイプ理論 だとP161以下。
0519１３２人目の素数さん
2007/10/06(土) 04:50:160520１３２人目の素数さん
2007/10/06(土) 19:15:28大きい最小の順序数は何と書き表すのでしょうか？
0521１３２人目の素数さん
2007/10/06(土) 19:16:300522１３２人目の素数さん
2007/10/06(土) 19:19:38どこかのスレに書いてあったんじゃねーの
0523１３２人目の素数さん
2007/10/06(土) 22:33:030524１３２人目の素数さん
2007/10/07(日) 03:30:040525１３２人目の素数さん
2007/10/07(日) 14:44:21おおっ、先週「数理論理学とタイプ理論」買ってた俺、大勝利！！
0526１３２人目の素数さん
2007/10/07(日) 16:42:46教えてください。
0527１３２人目の素数さん
2007/10/07(日) 19:18:49ε_0
0528１３２人目の素数さん
2007/10/07(日) 21:55:16ありがとうございます！
ではε_1はε_0,ε_0^ω,ε_0^(ω^ω),ε_0^(ω^(ω^ω)),…ですか？
0529１３２人目の素数さん
2007/10/08(月) 02:18:320530１３２人目の素数さん
2007/10/15(月) 00:51:12boolean algebraとheyting algebra勉強すると直観主義論理とかわかるようになるよ
0531１３２人目の素数さん
2007/10/15(月) 08:41:18述語論理になると急にややこしくなるが
0532１３２人目の素数さん
2007/10/16(火) 06:51:19「数理論理学とタイプ理論 証明による真理へ」 来てます
自分が買った値段よりだいぶ安いなあ・・orz
0533１３２人目の素数さん
2007/10/16(火) 14:40:35見た目が異様だから読む気がしないのだけど。
0534１３２人目の素数さん
2007/10/16(火) 14:45:280535１３２人目の素数さん
2007/10/25(木) 15:15:181/xってどういうこと？
0536１３２人目の素数さん
2007/10/26(金) 08:27:30まあ、そうなってしまうんだから仕方がありませんな。
ていうか >>8
0537１３２人目の素数さん
2007/10/26(金) 10:33:130538１３２人目の素数さん
2007/10/27(土) 21:19:33それとも、古本を探すしかない？
0539１３２人目の素数さん
2007/10/28(日) 05:23:370540１３２人目の素数さん
2007/10/29(月) 00:46:03www.bibliopolis.it/
をみると、まだ入手可能じゃないかな。
0541１３２人目の素数さん
2007/10/29(月) 01:26:16積分区間[f(x),0]でg(x,u)・du
をxで微分すると
f'(x)g(x,f(x))dx+積分区間[f(x),0]でdg(x,u)・du
と論文ではなっているんだけど(というかなるはず)なんだけど
自信がない。
誰か解説してください。もう３時間くらい調べてて疲れた・・・
0542１３２人目の素数さん
2007/10/29(月) 01:27:100543１３２人目の素数さん
2007/10/29(月) 01:29:220544１３２人目の素数さん
2007/10/29(月) 01:33:41数学基礎論って分野のことだ
0545１３２人目の素数さん
2007/10/29(月) 01:36:42眠すぎてよくみてなかった、数学基礎論ね
板違い申し訳ない
0546１３２人目の素数さん
2007/11/03(土) 05:27:42http://science6.2ch.net/test/read.cgi/math/1193144811/20-23
＞＞第2不完全性定理に関しては、ロッサーによる上記の証明の定義を用いれば､
＞＞体系自身の無矛盾性が証明できることが､
＞クライゼル (1960) によって指摘されている｡
＞
＞…これは詰まりえーと何だと言うのだろう
つか、ロッサーのやってる所からして分かりません。
命題より弱い否定命題は無い、とは?
これらの詳解と、
これらにより不完全性定理はどう変わったのか
また、その数理哲学(と言うか単に哲学)的な意味合いの変化について
意義のご教示をお願いします。
本当にもうワケわからんちん
0547１３２人目の素数さん
2007/11/03(土) 20:28:12> 命題より弱い否定命題は無い
ってどこのこと？
> 命題の証明より小さな、否定命題の証明が存在しない
これのことなら、「小さな」はゲーデル数が小さいということじゃないの。
0548１３２人目の素数さん
2007/11/03(土) 20:29:140549１３２人目の素数さん
2007/11/03(土) 21:23:08して、結局ロッサーの不完全性定理以降、どうなったんでしょうか?
"体系自身の無矛盾性が証明できる"と言う所だけ一見すると
ゲーデルの不完全性定理にそぐわない話になりますが、
何かワケが違うんでしょうか?また、そうだとした場合は
どうワケが違うんでしょうか?
0550１３２人目の素数さん
2007/11/03(土) 21:44:07> ロッサーによる上記の証明の定義を用いれば
とあるので、証明可能の定義が違うんじゃないかな
Rosser の採用した定義のほうが強い
0551１３２人目の素数さん
2007/11/03(土) 21:54:17あのね、Wikipedia のその部分の説明は無茶苦茶だからｗ
それを読んでわからなくなっても仕方がないのであって、
もし本当に理解したいと思ってるのならば、
前原著「数学基礎論入門」あたりでもパラパラとめくってみたら？
2ch で中途半端な説明を聞くよりその方がよっぽど早くて正確。
0552１３２人目の素数さん
2007/11/03(土) 22:01:01以前は「論理的には」間違ってなかったんだけどなあ。
誰だ編集した奴ｗ
0553１３２人目の素数さん
2007/11/03(土) 23:24:28ｻﾝｸｽ、やってみる。551提示書には
クライゼルまで載ってるんかな？
0554１３２人目の素数さん
2007/11/04(日) 00:02:46載ってる。最後のほう。
ただ、前原本は第一不完全性定理はうまく書けてると思うんだけど、
第二不完全性定理のほうはちょっと読み辛く感じるかも知れないから注意。
(というか第二のほうは完全に証明を書きくだすのは大変だし。)
それでも大まかな感じを捕むためなら十分だと思うよ。
0555１３２人目の素数さん
2007/11/04(日) 10:53:09有難う御座いました。
0556１３２人目の素数さん
2007/11/08(木) 21:22:150557１３２人目の素数さん
2007/11/10(土) 09:18:16>>boolean algebraとheyting algebra勉強すると直観主義論理とかわかるようになるよ
僕は、直観主義と自由選列について、日本の基礎論専門家が、どう考えているか、知りたいのです。
0558１３２人目の素数さん
2007/11/10(土) 21:35:58それだったら、例えば竹内氏の本を読めば、彼が直観主義に対してどう考えていたかは垣間見える。
今時では直観主義などはどーでもいいというのが主流。
なお、boolean algebra とか heyting algebra とか勉強しても
直観主義などわかりっこないので、騙されないように。
まさかひっかかる奴はいないと思うが、念のため。
0559１３２人目の素数さん
2007/11/10(土) 22:07:540560１３２人目の素数さん
2007/11/11(日) 00:39:41基礎論でも直観主義やってる人はそこそこいるよ
0561１３２人目の素数さん
2007/11/11(日) 01:04:08みんなでtoposやろーぜー
0562１３２人目の素数さん
2007/11/11(日) 10:49:11でもこのスレではいつものこと。
0563１３２人目の素数さん
2007/11/11(日) 16:17:56http://science6.2ch.net/test/read.cgi/math/1072058641/905
0564１３２人目の素数さん
2007/11/11(日) 20:04:08次買う本をLogic and Structureか
Introduction to Higher-Order Categorical Logicにするか迷ってる俺がいる
λもちょっとやりたいんだよなぁ
0565１３２人目の素数さん
2007/11/11(日) 23:22:14http://www.amazon.co.jp/exec/obidos/ASIN/0262011255/shelarcy-22/
http://www.di.ens.fr/~longo/download.html
0566１３２人目の素数さん
2007/11/12(月) 00:29:03直観主義の章にforcingがどうとか書いてあったような。
0567１３２人目の素数さん
2007/11/12(月) 19:46:36なら有限番目かどうかについては証明されているのでしょうか？
0568１３２人目の素数さん
2007/11/12(月) 20:02:060569１３２人目の素数さん
2007/11/13(火) 11:58:07ありがとうございました
0570１３２人目の素数さん
2007/11/13(火) 12:08:13X_L < y < X_R を満たす順序数yが存在するとき、
xは順序数ですか？
0571１３２人目の素数さん
2007/11/19(月) 17:23:03>今時では直観主義などはどーでもいいというのが主流。
出たよ、この半可通が。
0572１３２人目の素数さん
2007/11/19(月) 17:29:28＞基礎論でも直観主義やってる人はそこそこいるよ
昔っから、直観主義論理は論理学者の主要な研究テーマの一つだが。
今時とかいうんなら、むしろ部分構造論理だろ。
哲学的にはもっとブッ飛びそうだが。
0573１３２人目の素数さん
2007/11/19(月) 22:54:39位相空間論からやり直してきます。
0574１３２人目の素数さん
2007/11/19(月) 22:56:040575１３２人目の素数さん
2007/11/19(月) 22:56:47超～㌧クスなんだけど、Introduction to Higher-Order Categorical Logicの方を
あぶく銭で買ってもうたぁ。
0576１３２人目の素数さん
2007/11/19(月) 23:41:53よく知らんが、計算可能性とかじゃね？
0577１３２人目の素数さん
2007/11/20(火) 00:13:400578１３２人目の素数さん
2007/11/20(火) 14:31:300579１３２人目の素数さん
2007/11/20(火) 17:06:250580１３２人目の素数さん
2007/11/21(水) 15:01:040581１３２人目の素数さん
2007/11/21(水) 16:23:550582１３２人目の素数さん
2007/11/25(日) 21:06:270583１３２人目の素数さん
2007/11/26(月) 15:31:39なんで？
0584１３２人目の素数さん
2007/11/26(月) 21:48:23いるんじゃあるまいな。
0585１３２人目の素数さん
2007/11/26(月) 21:49:54量子という言葉を安易に使いすぎなんだな。
0586１３２人目の素数さん
2007/11/27(火) 14:45:51武豊に謝れ！
0587１３２人目の素数さん
2007/11/28(水) 13:37:29>>まあ古典論理は物理学的に偽だからな
>なんで？
物は不変ではない。
0588１３２人目の素数さん
2007/11/28(水) 13:59:590589１３２人目の素数さん
2007/11/28(水) 14:22:51古典論理ではAとA⇒￢Aの両方が成り立つと矛盾する。
Aと￢Aの両方が成立するから。
しかし、物理においてはそのような性質は一般に保持されない。
AとA⇒￢Aから、￢Aが成り立つとき、もとのAはもはやなくなっている。
0590１３２人目の素数さん
2007/11/28(水) 14:32:55うーん、ふつう命題や述語に時間による変化なんて考えないからね。
そういうのは物理だけでやってちょうだい。
0591１３２人目の素数さん
2007/11/28(水) 15:51:27いやー物理じゃなくてたま出版とか学研とかじゃないですか？
それか現代アートの人とか。
0592１３２人目の素数さん
2007/11/28(水) 16:03:140593１３２人目の素数さん
2007/11/28(水) 19:53:36この極限が求めれないです・・・
誰か教えてください
0594１３２人目の素数さん
2007/11/28(水) 19:54:380595１３２人目の素数さん
2007/11/28(水) 20:28:17だから電波に気が付かないんじゃないの？
0596１３２人目の素数さん
2007/11/28(水) 20:29:03時間軸ぶん一次元増やせば無問題
0597１３２人目の素数さん
2007/11/28(水) 21:58:21思考遊戯だけじゃなく真面目に勉強して欲しいと思う。
0598１３２人目の素数さん
2007/11/29(木) 12:30:33それは単に辻褄あわせにしか過ぎない。
>>597
マジメに勉強してもネタ一つ触れない君なんて
情けないというよりもどうしようもない。
0599１３２人目の素数さん
2007/11/29(木) 14:02:03古典論理は何も、物は不変だとかそんなことは主張しちゃ居ない。
一応、時相論理なんて論理も考案されちゃいるけど、
別に古典論理が間違っているというわけじゃないと思うけどね。
0600１３２人目の素数さん
2007/11/30(金) 16:54:08こういう人に限って計算問題は全滅だったりするからなｗ
0601１３２人目の素数さん
2007/11/30(金) 23:41:27なんで1階述語論理の文法使うかな
measureとかframeとかの方が親和性いいんじゃないの？
0602１３２人目の素数さん
2007/12/01(土) 13:55:56ではどの命題も少なくとも真か偽か真とも偽とも証明できないかのいずれかは証明できるのでしょうか？
それともそれさえも証明できない命題が存在するのでしょうか？
0603１３２人目の素数さん
2007/12/01(土) 14:26:260604１３２人目の素数さん
2007/12/01(土) 20:11:53真か偽か独立かは必ず証明できるの？って聞きたかったんです
0605１３２人目の素数さん
2007/12/02(日) 07:32:35> 真か偽か独立か
不完全性定理についてもういちど学習しなおしてください。
0606１３２人目の素数さん
2007/12/02(日) 11:09:33No!
0607１３２人目の素数さん
2007/12/02(日) 15:31:49命題論理で、
公理系１
（１－１）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になっていて解答が載ってなく、今現在
そこで挫折中です。
どなたか、親切な方お教えいただけると助かります。
0608１３２人目の素数さん
2007/12/02(日) 15:54:13独立の部分がまずかったんでしょうか＞＜
詳しくお願いします＞＜
0609１３２人目の素数さん
2007/12/02(日) 15:55:56だから答えを書いてやってるだろ ＮＯ
0610１３２人目の素数さん
2007/12/02(日) 16:07:04ありがとうございます！！
では、どの命題についても
真と証明できるか、偽と証明できるか、独立と証明できるか、どれもできないと証明できるか、
のいずれかはできるのでしょうか？
0611１３２人目の素数さん
2007/12/02(日) 16:20:59不完全性定理を学習したって>>604には答えられんだろ
答えられるとしたらCHの独立性証明って何なんだよって話になるだろうが
0612１３２人目の素数さん
2007/12/02(日) 16:25:42延々とやってろ馬鹿
0613１３２人目の素数さん
2007/12/02(日) 17:27:44できません！！
0614１３２人目の素数さん
2007/12/02(日) 17:40:10ひょっとしてこの過程を延々やってもいずれも証明できない命題が存在しますか？
0615１３２人目の素数さん
2007/12/02(日) 17:54:27それも No！
0616１３２人目の素数さん
2007/12/02(日) 18:00:04ということはどの命題も延々やったらいつかはいずれかが証明できるけれど
それがいつ来るかは分からないということですか？
0617１３２人目の素数さん
2007/12/02(日) 18:13:41No, no, no！
もはや単純に場合分けだけの問題だから >>610 に戻って良く考えてみよう。
>>614 みたいな横着はしないように。
0618１３２人目の素数さん
2007/12/03(月) 12:07:59ウカシェヴィチの本の邦訳が出ているはず。
0619１３２人目の素数さん
2007/12/03(月) 13:05:43＞不完全性定理によると真とも偽とも証明できない命題が存在するんですよね？
正確にいえば、
「証明できない命題が存在するとすれば、
その命題が証明できないことは証明できない。」
特に
「矛盾が証明できない（つまり無矛盾）とすれば、
そのこともまた証明できない」
0620１３２人目の素数さん
2007/12/03(月) 13:15:56なんらかの前提を必要とする。
例えば集合論におけるある命題の独立性を示す場合
集合論における無矛盾性を前提するものである。
0621１３２人目の素数さん
2007/12/03(月) 15:10:00>>602の疑問はは ↓ ここからスタートしているので
> 不完全性定理によると真とも偽とも証明できない命題が存在するんですよね？
不完全性定理についてきちんと学習すれば、そもそもの疑問が間違いだと気付く。
0622１３２人目の素数さん
2007/12/03(月) 15:32:11もちろんZFCの無矛盾性を前提している。
ZFCが矛盾していればCHもその否定も証明できるから。
0623１３２人目の素数さん
2007/12/03(月) 17:28:17一般の合併集合と共通部分についてですが，
空集合でない集合Iの元をパラメータとする集合の集合{A_i;i∈I}の合併集合と共通部分についての
一般分配律の証明が略されているのですが，Venn図を用いるのでしょうか？それ以外の証明の仕方があれば教えて下さい．
よろしくお願いします．
0624１３２人目の素数さん
2007/12/03(月) 17:41:100625１３２人目の素数さん
2007/12/03(月) 21:14:30無矛盾性は前提というより定理の前件だと思うが
まあどっちでもいいな
0626１３２人目の素数さん
2007/12/03(月) 21:35:380627１３２人目の素数さん
2007/12/04(火) 00:07:40なんかあまり基礎論と関係ないけど、他には汎用の質問スレしかないな。
まあそっちで聞いたほうが良いかも知れないけど。
>>623
x∈B∩(∪_{i∈I} A_i)
⇔x∈Bかつ、或るi∈Iに対してx∈A_i
⇔或るi∈Iに対してx∈B∩A_i
とかそんな感じで、或る～に対して～（～となるような～が存在する）
とか任意の～に対して～とか、そういう言い換えをして示す。
0628１３２人目の素数さん
2007/12/04(火) 00:17:28なんで日本語の集合論の本って、
quantifierの説明を最初にもってこないのかなって思うけどね。
∃とか∀で部分分配律な場合があるとかね。
日本語どっぷりだとなかなか意識しない部分だと思うんだけど。
書いてる人には自明すぎる話だからかな。
0629１３２人目の素数さん
2007/12/04(火) 00:45:54T:再帰的に公理化可能で自然数論を解釈出来るような無矛盾な理論として、
Tからφも￢φも示せないようなφが存在するってのが第一不完全性定理だけど、
じゃあφも￢φも￢Prov(φ)∧￢Prov(￢φ) も示せないようなφは存在するの？
φも￢φも￢Prov(φ)∧￢Prov(￢φ)も￢Prov(φ)∧￢Prov(￢φ)∧￢Prov((￢Prov(φ)∧￢Prov(￢φ))
も示せないようなφは存在するの？と聞いてるんだと思う。
なんか安易にそうだとか答えてるレスがあるけどそんな強いこと言えるんだっけ？
不完全性定理の拡張を簡単に示しちゃったことになるけど。
>>602
φを証明する、というのと、φが真であることを証明するというのは
ちょっと意味が違うので、二つを使い分けられるようになるまで
勉強してからまた考えてみては、ということかと。。
0630１３２人目の素数さん
2007/12/04(火) 02:15:57T=PA のときは、様相論理 GL を使って
Solovay の completeness theorem から出てきそうに思える。
0631１３２人目の素数さん
2007/12/04(火) 08:00:30少なくとも近いことは出来そうな気はするよね。
0632１３２人目の素数さん
2007/12/04(火) 10:26:26ψが何であっても、￢(Prov(ψ)) から Con(T) が出てくるので、
φ と ￢φ さえ証明できなければ、その他の条件はあってもなくても同じ。
0633１３２人目の素数さん
2007/12/04(火) 17:34:58￢Prov(ψ)じゃなくてCon(T)→￢Prov(ψ)にしないと絶対示せないよね。
0634625
2007/12/04(火) 17:45:190635607
2007/12/04(火) 22:23:18レスありがとうございます。さっそく探してみます。
ところで
>>607の公理系２からみなさんならどんなトートロジーを示せますか？私はいまだに
A→Aくらいしか示せません。他にどなたか有用なトートロジーを示せる方がいましたら
教えていただけないでしょうか。
0636１３２人目の素数さん
2007/12/04(火) 23:35:10公理系 1 と公理系 2 は同値なんだろ？
0637１３２人目の素数さん
2007/12/05(水) 16:39:22＞ってのが第一不完全性定理だけど、
誤り。φ⇔￢Prov(φ)なるφを具体的に構成したのが第一不完全性定理。
￢Prov(φ)なるφの存在を証明したわけではない。
0638１３２人目の素数さん
2007/12/05(水) 16:53:47いわずもがなだが、
φ⇔￢Prov(φ)⇔￢Prov(￢Prov(φ))⇔￢Prov(￢Prov(￢Prov(φ)))⇔･･･
0639１３２人目の素数さん
2007/12/05(水) 16:57:36NでとかTでとか指定せずにそんなこと言っても意味ないよ
0640607
2007/12/05(水) 17:00:07だから、公理系２から公理系１の公理を導く仕方がわからないので、いきなり公理系１の公理を導くのを目標に
するのではなく、とにかくまず何が導けるかいろいろ試してみようと思い、そこら辺についてみなさんのご意見を
伺いたいと思ったわけです。
0641１３２人目の素数さん
2007/12/05(水) 17:19:32>NでとかTでとか指定せずにそんなこと言っても意味ないよ
NでとかTでとか指定するだけでは大して意味ないが。
要は対角線論法による自己言及技法の問題であって
それを可能とする体系であれば何でもよいし、
逆に技法について述べられない奴が体系の名前だけ
したり顔で語ってみても意味がない。
0642１３２人目の素数さん
2007/12/05(水) 17:46:40http://academy6.2ch.net/test/read.cgi/philo/1194155261/l50
0643１３２人目の素数さん
2007/12/05(水) 17:58:43あんたがよくわかってないことはわかった
0644１３２人目の素数さん
2007/12/05(水) 18:13:03あんたが体系の名前を覚えただけで
判ったつもりになれるおめでたい人
だということはわかった。
馬鹿は数学板には必要ない。
0645１３２人目の素数さん
2007/12/05(水) 18:17:02よりにもよってNを体系の名前とは思わんよね
馬鹿は必要ないからどっか行ってね半可通さん
0646１３２人目の素数さん
2007/12/05(水) 18:27:100647１３２人目の素数さん
2007/12/06(木) 10:10:26>>639が半可通か。マツシン以下の馬鹿だな。
0648１３２人目の素数さん
2007/12/06(木) 10:23:510649１３２人目の素数さん
2007/12/06(木) 12:42:10マツシン病患者を収容隔離しまつ
0650１３２人目の素数さん
2007/12/07(金) 00:47:49そりゃ存在だけならTarskiの定理からすぐに出てくるけど
だからって当時Godel以外の誰かがそれに気づいていたわけでも無いし。
本によってはN（\mathbbとか\mathfrakじゃなくて普通のN）を
公理系の名前として使ってたような気がするけどまああまり一般的ではないかな。
>>639
いまTをT'にしてT'で￢Prov_T(φ)を示すとかそういう
複数の理論にまたがった話をしてるわけじゃなくて
特定のTを固定して話してるんだから、
取り敢えずは議論に関係ない添字を省略するのは別に何の不都合もないと思うけど。
こういう省略って結構数学ではやるでしょ。
0651１３２人目の素数さん
2007/12/07(金) 08:57:42T |- ￢Prov(φ) なるφの存在を・・・
と
N |= ￢Prov(φ) なるφの存在を・・・
とじゃ全然違うけどね
0652１３２人目の素数さん
2007/12/07(金) 09:27:44Tarskiの定理は任意のφに対してφ⇔True(φ)となる
述語Trueが算術的に表せないことを示すもの。
0653１３２人目の素数さん
2007/12/07(金) 12:30:47ProvとTrueが一致してないことはすぐに分かるでしょ。
Godelは最初にこの弱い形の不完全性定理を発見して、
それから対角線論法によるφの構成を発見したといわれている。
だから別に見当違いじゃないし、「存在を示した」というのは
論文に発表された結果よりも少し弱いだけであって間違っていない。
0654１３２人目の素数さん
2007/12/08(土) 11:58:280655１３２人目の素数さん
2007/12/08(土) 16:23:06「(￢Prov(φ)なるφの)存在を示した」
というのは明確に間違ってるよ。
>「存在を示した」というのは
>論文に発表された結果よりも少し弱いだけ
君、読み間違っちゃったね。
確かにゲーデルは、φ⇔￢Prov(φ)なるφについては
具体的に構成したわけだから単にその存在を示すよりも
強い結果を出したといっていい。
しかし、φ⇔￢Prov(φ)なるφを構成したところで、
それが即￢Prov(φ)だといえるわけではない。
前提が必要だ。例えばω無矛盾性とかあるいは健全性とか。
0656１３２人目の素数さん
2007/12/08(土) 16:58:55ご存知の方いましたら、教えていただけないでしょうか？特に従来の古典命題論理の公理が
証明されるところをきちんと述べてくれてると嬉しいのですが。
あるいは何かよい書籍あったら教えていただけないでしょうか。
0657１３２人目の素数さん
2007/12/08(土) 19:58:02もしそれがimplicational fragment of propositional logicのことだったら
substractural logicsの文献調べればいいんじゃね？
0658１３２人目の素数さん
2007/12/09(日) 00:04:330659656
2007/12/09(日) 15:00:47すいません。implicational fragment of propositional logicってなんでしょうか。わからんです。
>>658
はい。wikiはざっと目を通したのですが、私が知りたいのは、
http://eom.springer.de/I/i050300.htm
にある2つの公理系の、上のほうから下のほうを導くところなのです。wikiに書いてあるのはどちらかというと
下のほうから上を導いているのではないでしょうか。
実は私は>>607なのです。いろいろ調べているうちにこうなつてしまつたのだ。誰か助けて著。
0660１３２人目の素数さん
2007/12/09(日) 19:41:42657だけど、同じことだとおもう
substructural logicsの文献見ると参考になる
（答えが見つかるかどうかは別だけど
an introduction to substructural logicsに
近いことが書いてあったような
0661656
2007/12/09(日) 21:52:32＞an introduction to substructural logicsに
その本ってGreg Restall著のですか？だとしたら、今月末までそれ手に入んないなあ。
ちくしょー。
っていうか、情報には本当に感謝してます。どっかのsiteに書いてないかなあ。
0662１３２人目の素数さん
2007/12/14(金) 17:28:320663607
2007/12/14(金) 21:55:24＞ウカシェヴィチの本の邦訳
が手元に届きましたので、ざっと目を通したところ、まさに>>607の公理系２が公理として採用されていて、
そこからいろいろなトートロジーが導かれていました。公理系１の論理式もその中に含まれています。
これから解読します。本当にありがとうございました。
ちなみに、本は
ヤン・ウカシェーヴィチ著 高松鶴吉訳「数理論理学原論」（文化書房博文社）
です。
0664１３２人目の素数さん
2007/12/15(土) 11:21:27>>655にレスなしだから推して知るべし
0665１３２人目の素数さん
2007/12/15(土) 22:50:46grad rを求めよ。
わかりません教えてください。
0666１３２人目の素数さん
2007/12/16(日) 00:29:14基礎論と何の関係が？
0667１３２人目の素数さん
2007/12/16(日) 01:37:54「基礎」という文字に吸い寄せられたんだろう
0668１３２人目の素数さん
2007/12/16(日) 06:08:590669１３２人目の素数さん
2007/12/16(日) 23:28:54>>8
>>655
あのさあ、そりゃあ理論が再帰的に公理化可能だとか
そういう前提条件は仮定しているけれども、
不完全性定理の話なんだから629あたりの条件は当然満足するとして話してるんでしょ。
じゃなきゃφ⇔￢Prov(φ)自体が証明できない。
だいたい、メタなレベルでの理論の無矛盾性を
暗黙のうちに仮定して話をするのはそうおかしなことじゃないでしょ。
矛盾してるときには全てが自明なんだから。
例えばBolyaiとLobachevskyは平行線の公理が証明不可能なことを示した、
とか言うとき、これは本当は嘘で、「Euclid幾何が無矛盾ならば」とか
そういう前提条件が付くのが正しいわけだけど、そんなこと普通はわざわざ断らない。
メタじゃなくてオブジェクトレベルで、
￢Prov(φ)とCon(T)⇒￢Prov(φ)を混同するなというのはその通りだけどね。
0670１３２人目の素数さん
2007/12/17(月) 12:01:33>不完全性定理の話なんだから629あたりの条件は
>当然満足するとして話してるんでしょ。
「629あたりの条件」といってるのはズバリ"無矛盾"かな？
>じゃなきゃφ⇔￢Prov(φ)自体が証明できない。
証明するだけなら無矛盾性を前提する必要はないよ。
矛盾する体系なら何でも証明できるわけだし。
0671１３２人目の素数さん
2007/12/17(月) 12:17:17>暗黙のうちに仮定して話をするのはそうおかしなことじゃないでしょ。
おかしいな。ゲーデルは暗黙の仮定なんて置いてないが。
0672１３２人目の素数さん
2007/12/17(月) 12:25:01>例えばBolyaiとLobachevskyは平行線の公理が証明不可能なことを示した、
>とか言うとき、これは本当は嘘で、「Euclid幾何が無矛盾ならば」とか
>そういう前提条件が付くのが正しいわけだけど、そんなこと普通はわざわざ断らない。
まあ、２ｃｈって普通間違ってるけどな。
0673１３２人目の素数さん
2007/12/17(月) 14:46:59「再帰的に公理化可能」じゃないとそもそもProv(φ)という
述語が実際に論理式で表せないし、
「自然数論が解釈できる」体系じゃなければGodel numberingが行えないから
やはり一般には、証明可能性を体系内で扱えない。
この二つの条件が成り立って、さらに「無矛盾」なときには、
φも￢φも示せないような文φが存在する。
これが不完全性定理の内容で、大体みんなこの三つのカギ括弧内の
前提条件が成り立つと仮定してレスをしている。
一方であなたはそういうレスに対して無矛盾じゃないとφは存在しないとか、
レス毎に前提条件を二度も三度もいちいち書け、とか言ってるわけ。
たぶんあなたの基準じゃ、最初の二つは前のレスを受けた仮定として
断らなくて良いけど、「無矛盾だ」という条件だけは強調すべし、みたいなルールなのかな。
どうみても阿呆なこと言ってるのはあなたでしょ。
629と637を良く読めば最初の話が
>前提が必要だ。例えばω無矛盾性とかあるいは健全性とか。
こういう話じゃないのは一目瞭然でしょ。
0674１３２人目の素数さん
2007/12/17(月) 14:49:25φ⇔￢Prov(φ)は証明できないよね。
0675１３２人目の素数さん
2007/12/17(月) 15:20:39>「再帰的に公理化可能」じゃないとそもそもProv(φ)という
>述語が実際に論理式で表せないし、
そこは論点ではないからいうだけ無駄である。
>「自然数論が解釈できる」体系じゃなければ
>Godel numberingが行えないから
>やはり一般には、証明可能性を体系内で扱えない。
そこも論点ではないからいうだけ無駄である。
0676１３２人目の素数さん
2007/12/17(月) 15:37:51>φも￢φも示せないような文φが存在する。
そこが論点。
>あなたは…無矛盾じゃないとφは存在しないとか、
間違い。私はこう書いている
「￢Prov(φ)なるφの存在を証明したわけではない。 」
これはこういう意味だ。
「(φ⇔￢Prov(φ)なる)ゲーデル命題φを構成したとして、
￢Prov（φ）がもとの体系から証明されたわけではない」
0677１３２人目の素数さん
2007/12/17(月) 15:46:32これは大嘘。そのような事実はない。
私が云っているのは以下の事柄
「ゲーデル命題はあくまでφ⇔￢Prov(φ)となる命題φ。
￢Prov(φ)は元の体系からは導けない。
￢Prov(φ)を導くには元の体系以外の前提が必要になる。
例えば分かりやすい例では任意のψについて
Prov(ψ)⇒ψが成り立つとする健全性等」
0678１３２人目の素数さん
2007/12/17(月) 15:48:46>断らなくて良いけど、「無矛盾だ」という条件だけは強調すべし、
>みたいなルールなのかな。
ルールの問題だと思ったことが、根本的な誤りだな。
頭を冷やせ。
0679１３２人目の素数さん
2007/12/17(月) 18:24:16Tは再帰的に公理化可能で自然数論を解釈出来るような無矛盾な理論とするとき、
Tにはφも￢φも証明出来ないような文φが存在する……(*)
ことをGodelは示した、と言っただけで
T |- ￢Prov(φ)となるようなφが存在するなんて誰も言ってないんだけど…
敢えて言うなら>>655が一人で言ってるだけ。
>>653は(*)はTarskiの定理からすぐに出る、と言ってるだけだし、
>>650は或る体系の無矛盾性を「別の体系から」導出するような話
（例えばZFC + XでZFCのモデルを作って（ZFCが無矛盾ならば）
ZFCより真に強いことを示すとかそういう話）は今の話題ではない、と言ってるだけ。
もしかして、T |- φでない、ということとT |- ￢Prov(φ)ということを
単にあなたが混同してるだけじゃない？
0680１３２人目の素数さん
2007/12/17(月) 18:34:45> Tからφも￢φも示せないようなφが存在するってのが第一不完全性定理だけど、
第一不完全性定理ではなくて Rosser の不完全性定理でないと正しくない。
0681１３２人目の素数さん
2007/12/17(月) 18:41:00（これこれの仮定の下）Tにはφも￢φも証明出来ない文φが存在する
じゃ不満でT |- Con(T) → ￢Prov(φ)と言わないと気が済まないとか。
うーん、謎だ。。
0682１３２人目の素数さん
2007/12/17(月) 18:48:07そらそうだけどｗ
それ現在の論点と全然違うでしょｗ
あなたも言ってるけど。ただの揚げ足取りにしか思えない。
というかただの呼び方の問題であって、
Rosserの不完全性定理のほうが単純に強いのだから
これを第一不完全性定理（の強いver.）と呼んだって
Rosserの先取権を尊重すべきだとかそういう問題を除けば別に大した問題はない。
0683１３２人目の素数さん
2007/12/17(月) 19:21:20呼んでいる本が一冊でもありますか？
0684１３２人目の素数さん
2007/12/17(月) 21:48:150685１３２人目の素数さん
2007/12/17(月) 22:16:52という主張を表すのに使って、Godelがω無矛盾のときに、Rosserが無矛盾のときに示した、
という書き方をすることはいくらでもあると思うけど。
例えば英語版wikipediaはそういう書き方。
本だと例えばcomputability & logicの第五版のp.223には
17.7 Theorem(Godel's first incompleteness theorem)
There is no consistent, complete, axiomatizable extension of Q.
となってる。ほかにも図書館で探せば結構あると思う。私はそこまではしないけど。
0686１３２人目の素数さん
2007/12/17(月) 22:26:37他の分野じゃ、明らかにAbelやRiemannの時代には定式化されてない概念を
使って述べた定理を、彼らの名前を冠して呼んだりするんだから。
0687１３２人目の素数さん
2007/12/18(火) 03:44:14と書いた先生がいたのを思い出した。
0688１３２人目の素数さん
2007/12/18(火) 07:44:53>T |- ￢Prov(φ)となるようなφが存在するなんて誰も言ってないんだけど
>>650で冒頭にそう断言するべきだったね。
>もしかして、T |- φでない、ということと
>T |- ￢Prov(φ)ということを
>単にあなたが混同してるだけじゃない？
否、君が明確にステートメントを述べる能力を持っていないだけだ。
0689１３２人目の素数さん
2007/12/18(火) 07:50:18メタの問題だと思ったことが、根本的な誤りだな。
頭を冷やせ。
0690１３２人目の素数さん
2007/12/18(火) 12:30:320691１３２人目の素数さん
2007/12/18(火) 15:29:12「選択公理よりも『弱い』公理として」とあるけれど正しいのでしょうか？
連続の定義の場合 各点連続＞一様連続＞リプシッツ連続
連結の定義なら 連結＞弧状連結
と右の方が強い、条件が厳しくなっていく。だったと思います。
可算選択公理というものが「選択公理の成立する範囲を可算濃度以下に限定したもの」であるなら、
選択公理よりも強い、条件が厳しいと言えるので
この場合は「強い公理」と言うののが正しいのではないのでしょうか？
それとも公理の場合は定義の場合の強い、弱いという考えとは逆になるとか、
あるいは上の連続の時とかの自分の理解が間違ってるからオカシク感じたのでしょうか？
0692１３２人目の素数さん
2007/12/18(火) 15:34:27「すべての濃度で成立する」ことを要求するのとどっちが厳しいか
「だったと思います」じゃ困るなー
そっちに自信ないという方が気になるぞｗ
0693１３２人目の素数さん
2007/12/18(火) 16:07:21少し慣れてきたけれど強いとか弱いとか結構混乱するもので…。
0694１３２人目の素数さん
2007/12/18(火) 21:44:50一様連続 ならば 各点連続
選択公理 ならば 可算選択公理
0695１３２人目の素数さん
2007/12/20(木) 19:44:03仮定のpが強いほど、弱い命題になる。
pの前にnotが来るから反転してそうなると理解して良いと思う。
「選択公理の成立する範囲を可算濃度以下に限定したもの」じゃなくて
「少なくとも可算濃度以下のときは選択公理が成り立つ
（そうでないときに関しては何も言っていない。
成り立つのかもしれないし成り立たないのかも知れない）」でしょ。
0696１３２人目の素数さん
2007/12/20(木) 19:57:390697１３２人目の素数さん
2007/12/22(土) 04:23:120698１３２人目の素数さん
2007/12/22(土) 15:33:41どんだけマツシンに精神強＊されたんだ？
0699１３２人目の素数さん
2007/12/22(土) 19:16:23ま、「成立を仮定・要請する範囲を」なら制限・限定でいいんだけどな。
0700１３２人目の素数さん
2007/12/24(月) 06:35:40ホントにコピペどおりの習性だな>>698
---
160 名前： １３２人目の素数さん [sage] 投稿日： 2007/03/09(金) 20:50:49
マツシンという奴（か“それと同レベルの奴”）が
基礎論関係のスレには永遠に住み着いていて
こいつ（ら）と言い争いになったらスルーが基本。
マツシン（かそれと同レベルの奴）が誤りを認めることは
基本的にありえない。人工無能のように必ずレスを返して
いつまでも食い下がっては鸚鵡返しで煽り、はぐらかす。
無理に調伏しようとするとスレがぐだぐだに荒れる。
「お前マツシン並だな」と言われたときに
普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
何故か「お前はマツシン以下だな」と返す、などの習性がある。
---
>>672みたいなのはだいたいコイツのレスだってわけだ
0701１３２人目の素数さん
2007/12/25(火) 15:15:03マツシン病患者が誤りを認めることは基本的にありえない。
啓蒙書しか読めず、それゆえ、啓蒙書が絶対だと信じて突っ張る。
究極の馬鹿。
>「お前マツシン並だな」と言われたときに
>普通人なら「マツシン並なのはお前のほうだ」と言い返すところを
>何故か「お前はマツシン以下だな」と返す、などの習性がある。
マツシン並ならガマンできるところを「以下」ということで
ファビョらせることができる。実に簡単。
0702１３２人目の素数さん
2007/12/25(火) 20:37:080703１３２人目の素数さん
2007/12/25(火) 20:59:040704１３２人目の素数さん
2007/12/26(水) 08:17:31正：未満
0705１３２人目の素数さん
2007/12/26(水) 11:06:15それを基準に並だの以下など言ったところで
0706１３２人目の素数さん
2007/12/26(水) 18:13:16マツシン：マツシン病患者
＝ゴキブリ：黴菌
といった感じか。
0707１３２人目の素数さん
2007/12/27(木) 22:49:250708１３２人目の素数さん
2007/12/29(土) 12:59:09基礎論のスレでこの手の変な逃げ（書いた本人は切り返しだと思ってる？）は
昔からよく目にする
他のスレと違って独特
0709１３２人目の素数さん
2007/12/29(土) 13:43:380710１３２人目の素数さん
2007/12/29(土) 17:05:09完全に切られた首で変な強がりを口にするのは
昔からよく目にする
他の人と違っていかにも狂ってる
0711１３２人目の素数さん
2008/01/03(木) 15:38:43教えてくれんか。たのむ。
0712１３２人目の素数さん
2008/01/06(日) 00:03:53なんかいつの間にやら話が進んでしまっているようで申し訳ないです。
>>629
＞φを証明するとφが真であることを証明するの違い
うーん、難しいです。
どちらも 公理系→φ ということとは違うのでしょうか…
0713１３２人目の素数さん
2008/01/06(日) 00:57:09http://www.rtri.or.jp/index_J.html）に告ぐ
今からでも、決して、遅くはない。
投降せよ。（御大 宛に E-mail（宛先：[email protected]）で詫び状を送れ！）
さもなくば、酷い目に逢うぞぁ～～～～！！！！。
これは冗談ではないぞぉ～～～～！
俺からも恩大に頼んでやる。
お前の身を案じて、こんなことを書いてるんだぞ！！！！
元賊軍兵士（いち早く、官軍に投降すますたＷ）
お前は卑劣奸だ！！！ そんな者に誰がついてくる門下！
お前は、「NewYork_Academy_of_Sciencesなど、金さえ払えば誰でも
入れる」とかなんとか言って、恩大ならびに NewYork_Academy_of_Sciences
の名誉を著しく毀損しただろう。 違うか？！！！！！！！！！
恩大の場合はだな、先方（＝NewYork_Academy_of_Sciences）のほうから
是非会員になって下さいとの丁重な案内状が届いたのでそうされたのだゾ。
何でそんなことを知っているのか聞きたいか？ 教えてやろう、恩大に
メールを送って俺は尋ねたのだ。
0714１３２人目の素数さん
2008/01/06(日) 02:12:370715１３２人目の素数さん
2008/01/06(日) 16:40:34今のヒトは、御大なんて知らんだろ。
それはともかくニューヨーク科学アカデミーは
ホームページでも会員募集の宣伝してるんだが。
ttp://www.nyas.org/membership/main.asp
0716１３２人目の素数さん
2008/01/06(日) 22:42:480717１３２人目の素数さん
2008/01/07(月) 03:22:57＞＞φを証明するとφが真であることを証明するの違い
＞うーん、難しいです。
＞どちらも 公理系→φ ということとは違うのでしょうか…
違います。
全ての意味づけでφが真であること
公理系からφが証明できること
それぞれが別のことです。
0718１３２人目の素数さん
2008/01/07(月) 11:34:000719１３２人目の素数さん
2008/01/07(月) 17:04:02>>717
うーん……φが真であることを証明できるは公理系を充足するようなモデルを作ってみて
どんな風に作ってもそのモデルでφに相当する式は真になっているということで、
φが証明できるは単純に公理系→φが示せるということ……ですか？
>>718
ということは普通の論理を使っている限りは気にしなくていいということでしょうか？
0720１３２人目の素数さん
2008/01/08(火) 15:54:250721１３２人目の素数さん
2008/01/09(水) 22:52:020722１３２人目の素数さん
2008/01/09(水) 22:55:280723１３２人目の素数さん
2008/01/12(土) 01:42:090724１３２人目の素数さん
2008/01/12(土) 05:22:42>x1 ∋ x2 ∋ x3 ∋ ...... ∋ xn ∋ ....... なる無限列が存在する
モデルがあるそうですが、
http://www.iis.it-hiroshima.ac.jp/~ohkawa/math/math_problem_all.htm#101
これはどうなんでしょうか？
0725１３２人目の素数さん
2008/01/12(土) 20:45:000726１３２人目の素数さん
2008/01/12(土) 21:01:510727１３２人目の素数さん
2008/01/12(土) 21:24:170728１３２人目の素数さん
2008/01/13(日) 10:26:17＞どんな風に作ってもそのモデルでφに相当する式は真になっているということで、
間違ってます。
思いつき口にせず、自分で勉強してください。
0729１３２人目の素数さん
2008/01/13(日) 15:21:36後半はあってますか？
0730１３２人目の素数さん
2008/01/13(日) 15:26:14まず、専門書を読んで確認してください。
専門書が読めないなら諦めなさい。
0731１３２人目の素数さん
2008/01/13(日) 18:54:020732１３２人目の素数さん
2008/01/14(月) 00:45:58俺なら教科書（「団結」ってタイトル）の28ページを熟読するけどな。
0733１３２人目の素数さん
2008/01/15(火) 12:23:18きちんと「φが真」の定義を勉強しないと簡単に間違いますよ。
その例が>>724の問題とかSkolemの逆理とかだと思う。
>>724
compact性定理使ってもすぐに出るけどね。
モデルの中の概念と外の概念を区別しないといけないってのが大事だと思う。
しかしそのページの著者の人はなんか集合論とかきちんとした論理学は全然知らないみたいな書き方だね。
多分超準解析の本を読んだことがあるとかそういうことだろうね。
＞通常の集合論（例えば有限集合論）では x1 ∋ x2 ∋ x3 ∋ ...... ∋ xn なる有限列は取れる。
通常の集合論（例えば有限集合論）って何のことなんだろう……？
＞しかしこれは矛盾ではない。（中略）
＞上記事実は、第２階、或いは階数を超えた「人間の全ての思考」のレベルで述べられた物だからである。
とかまるでDedekindの時代の数学者みたいな物言いだし。
＞だから可算無限濃度と連続体の濃度の中間の濃度が見つかっても、何らこれまでの数学に矛盾する物ではない。
とか……
これはもしかして連続体仮説の否定が真となるモデルが存在しても
矛盾じゃないって言いたいんだろうか？とてもそうは取れないけど。
0734１３２人目の素数さん
2008/01/18(金) 20:31:31数学は専門分化し、沢山の高度な結果が得られたが、
基礎的な考え方はDedekindの時代からどの程度進化したのだろうか？
0735１３２人目の素数さん
2008/01/18(金) 21:08:540736１３２人目の素数さん
2008/01/18(金) 21:39:480737１３２人目の素数さん
2008/01/18(金) 22:28:51Dedekind流の無限定義とPeano流の無限定義ってどう違うの？
0738１３２人目の素数さん
2008/01/19(土) 00:04:57二次元射影空間RP2から小さな開円板Dを除くとメービウスの帯になることを説明せよ
あと、当方数学科の初年級なんですが、幾何の分野は今から学んでおくべきですか？
0739１３２人目の素数さん
2008/01/19(土) 00:06:27それ基礎論じゃないよ
0740１３２人目の素数さん
2008/01/19(土) 00:09:32スレチですか。すいませんでした。
どのスレが適当ですか？
0741１３２人目の素数さん
2008/01/19(土) 00:11:26わからない問題スレとかでいいんじゃないの？
0742１３２人目の素数さん
2008/01/19(土) 00:13:33㌧クスです
いってみます
0743１３２人目の素数さん
2008/01/19(土) 00:23:18これがゆとり教育の産物なのか…
0744１３２人目の素数さん
2008/01/19(土) 00:45:240745１３２人目の素数さん
2008/01/19(土) 10:59:58健全だ（ｗ
漏れは中３のころに「数学から超数学へ」という本を
うっかり読んでしまってから、ダークサイドに堕ちたｗ
0746１３２人目の素数さん
2008/01/19(土) 14:35:37Dedekind流の有限定義はPeano流の有限定義と同値だがDedekind有限の定義とは異なる
0747１３２人目の素数さん
2008/01/19(土) 14:53:340748１３２人目の素数さん
2008/01/19(土) 22:52:35選択公理を否定すれば同値でない事が示されるのか？
0749１３２人目の素数さん
2008/01/20(日) 00:24:46もち
0750１３２人目の素数さん
2008/01/20(日) 01:00:09i) 整列且つ、逆整列な全順序が存在する。
ii) 空集合であるか、または自分自身の真部分集合と対等でない・・・
0751１３２人目の素数さん
2008/01/20(日) 01:46:470752１３２人目の素数さん
2008/01/20(日) 17:55:39最近ゲーデルやチューリングに興味を持った
これから基礎論に取り組む
よろしく
0753１３２人目の素数さん
2008/01/20(日) 18:53:080754１３２人目の素数さん
2008/01/20(日) 20:14:32「ブルバキとグロタンディーク」日経ＢＰ社 を読んだら、数学の基礎はいまや集合ではなく
圏論というものであり、ブルバキも集合論ではなく圏論を基礎にして書き直すべきだった
みたく書いてあります。ところが同じ本で圏論は集合論や代数、位相幾何などの
上部構造（下部ではなく）とあり、混乱しました。
圏論ってのは集合みたく高校教科書に載せる事ができるような基本的概念なんでしょうか。
0755１３２人目の素数さん
2008/01/20(日) 20:42:05物理ができなくなるよ。
0756754
2008/01/20(日) 20:51:45ただ、多様体も群も集合を基礎にしてるんで集合よりも基礎的（？）な圏論てなものがあると
聞いて驚いたんで聞いてみました。
0757１３２人目の素数さん
2008/01/20(日) 21:35:19圏論は構造を調べるときの視点をちょっと変えて、見通しをよくしてるんだよ。
要素中心で行くか、射中心でいくかみたいな。
0758１３２人目の素数さん
2008/01/20(日) 21:37:43thx.
Axiom of Choice by Horst Herrlichでも買ってきて、ちょっと違いを考えてみます。
0759１３２人目の素数さん
2008/01/20(日) 22:50:05「有限回で終了する」なる概念の厳密な定義がない。
0760１３２人目の素数さん
2008/01/21(月) 17:40:33視点の変更は重要だ。
存在論を取っ払ったわけだから。
0761754
2008/01/22(火) 12:53:33有用なアイデアとのことだったので、jp.wikipedia.orgを読んでみたのですが、
えらく抽象的な感じでどう有用なのかさっぱりでした。準同型みたいな写像に
注目するのかな、てな程度で。
（特殊相対論は高校程度の知識で理解できるのでちょっと期待したのですが）
文献として「圏論の基礎」という本を挙げてありましたが、やはり代数幾何とかの
ある程度高度な数学的知識がないと理解できないと思ったほうがよいでしょうか。
0762１３２人目の素数さん
2008/01/22(火) 17:57:20「取っ払った」わけじゃないでしょ。有用ではあるだろうけどね。
実際に集合の概念無しで例えば実解析とかが展開できるわけじゃないでしょ。
集合論的な構成為しで代数的閉包の存在だとかが仮定できたりするわけでもない。
或る程度知識が無いと理解しづらいだろうけど、例えば情報科学でも
圏論は利用されたりしてるので、別に「代数幾何とかのある程度
高度な数学的知識」が必要なわけでもないかと。
0763１３２人目の素数さん
2008/01/22(火) 18:29:250764１３２人目の素数さん
2008/01/23(水) 08:27:51>例えば情報科学でも圏論は利用されたりしてるので
検索したらこういう本もありました。図書館で見てみます。
ありがとうございました。
Basic Category Theory for Computer Scientists (Foundations of Computing) Benjamin C. Pierce (ペーパーバック - 1991/8/7)
圏論による論理学―高階論理とトポス 清水 義夫
0765１３２人目の素数さん
2008/01/27(日) 06:01:460766１３２人目の素数さん
2008/01/27(日) 11:55:29algol N作ってたYonedaせんせのlemmaは圏論の本に出まくりでそ
ttp://www.chimaira.org/img/yoneda-nobuo.gif
0767１３２人目の素数さん
2008/01/27(日) 11:58:49そんなに心配なら、F. W. Lawvereの"Conceputual Mathematics: A first introduction to categories"。
小学生でも読破可。
0768１３２人目の素数さん
2008/01/27(日) 12:02:59Hoare logicはやったのか？
0769１３２人目の素数さん
2008/01/27(日) 16:56:17キミがしがみついてるだけ。
例えば実解析が集合論なしに展開されていないのは
実解析の理論が後進的だから。他についても同じ。
存在は無用だ。
0770１３２人目の素数さん
2008/01/27(日) 19:28:03全く無理。可能だというだけで、もともと集合概念の方が、
論理とのつながりがよいのだから、カテゴリーは基礎付けなど
に使わないで、数学のなかで使うのがまともだ。
0771１３２人目の素数さん
2008/01/28(月) 13:40:10＞実解析の理論が後進的だから。
そうじゃなくて、圏論がそもそも（少なくとも現時点では）
数学全体の基礎付けに充分ではないということじゃないの。
集合論的な独立命題に影響を受けやすい分野を「後進的」と呼んでいるようだけど
そういう分野はいくら発展しようと分野の特性上「後進的」のままになってしまう。
先進的とか後進的という進歩に関する言葉を使うのは明らかに間違い。
函数解析だとか確率論だとかそういう分野を全て無用、後進的という言葉のもとに
捨て去るような態度がまともなわけがない。個人的な嗜好の問題に留めておくべき。
0772１３２人目の素数さん
2008/01/30(水) 11:51:53＞「後進的」と呼んでいるようだけど
そうではないよ。
集合論以外の枠組みについて考えてない点が「後進的」ってことさ。
日本語が読めないと数学も学べないよ。
0773１３２人目の素数さん
2008/01/30(水) 12:13:240774１３２人目の素数さん
2008/01/30(水) 12:59:36そもそも「後進的」という用語は数学用語ではないがｗ
いずれにしても771が文章を読めなかったという事実だけが残る。
0775１３２人目の素数さん
2008/01/30(水) 13:05:25一般用語として解釈して、独自用語だと言われているのに気付かない
「日本語が理解できてない」なんてお前が言っても説得力皆無
論理とのつながりでいえば、集合もToposもどっちもどっち。
どちらかといえば、集合が古典論理よりでToposが直観主義論理よりなだけ。
実解析関連に関しては、直観主義的な実数（実様体だっけ）の問題で、
直観主義的集合論でやっても難しさは変わらないと思う。
0777１３２人目の素数さん
2008/01/31(木) 15:29:15代数的位相幾何などでは圏論が有用
（これも別に集合論無しで展開出来る、という意味ではない）なのは
集合論以外の枠組みについて（位相幾何学者が）ちゃんと考えたからだ、
実解析学なんかで圏論が役に立たないのは解析学者が
集合論以外の枠組みについて考えなかったからだ、と言いたいわけ？
0778２人目の素数さん
2008/02/10(日) 15:38:49http://www.amazon.co.jp/dp/4535783829/
0779１３２人目の素数さん
2008/02/16(土) 22:59:42演繹定理を"すぐわかる"と流しているあたり、個人的にはあまりやさしくないように思います。
集合と位相は履修した学部生です。
0780１３２人目の素数さん
2008/02/16(土) 23:56:26たった160頁で不完全性定理と連続体仮説の独立性の話を紹介しようという
かなり「欲張った」本だから証明をちょっと省略したりしてるのは仕方の無いことかと。
私は最初にこの本で勉強しました。
本棚探しても無いので図書館で借りて読んだんでしょうけど。
ちなみに「数学基礎論講義」の演繹定理の証明も述語論理の場合に
「命題論理の場合と同様」とか言って一部流してたりします。
「いざない」と同じシリーズの「入門数学基礎論」のほうは、きちんと書いてあります。
演繹定理もきちんと命題論理の場合と述語論理の場合に分けて三、四頁は使って証明してあるし、
LKとHilbert styleの公理系が等価であることをわざわざ両方向の証明を書き下したりと
ものすごくガチガチに書いてあります。カット除去定理の証明とかも載っている。
細部は飛ばして全体の感じを掴みたいなら「いざない」、
隙間の無いガチガチな書き方が好きなら「入門数学基礎論」を読むと良いと思う。
まあ別の本でも良いんですけどね。
0781１３２人目の素数さん
2008/02/17(日) 00:12:50丁寧なお返事ありがとうございます。
0巻と称していたのはそれが理由なんですね。
全体をつかんでから、1巻に入りたいと思います。
0782１３２人目の素数さん
2008/02/17(日) 00:33:000783１３２人目の素数さん
2008/02/18(月) 13:09:11（今、本屋で買えるのは「モデルの理論」と「逆数学と２階算術」だけ）
自分の読んでる奴は、明○館で見つけてきた奴だ
0784１３２人目の素数さん
2008/02/20(水) 13:27:260785１３２人目の素数さん
2008/02/20(水) 21:03:46そうじゃなくてωのことを言ってるんだよね、たぶん。
定式化の仕方にも拠るだろうけど、
無限公理と分出公理あたりがあれば大体大丈夫じゃない？
外延性公理を使ってるかどうかは微妙。自分で確かめて。
0786１３２人目の素数さん
2008/02/25(月) 00:27:54基礎論は知らないけど、数学は学部レベルは理解してる人がその文庫だけ
読んで理解することは可能でしょうか？
0787１３２人目の素数さん
2008/02/25(月) 10:30:420788１３２人目の素数さん
2008/02/25(月) 13:10:25いきなりあれを読んでも、理解したつもりってくらいにしかなれないと思う
あれを読む前に一階述語論理の初歩を勉強したほうがいい
0789１３２人目の素数さん
2008/02/25(月) 18:23:20文庫でなければ邦訳のある論文とか講演はいくつかあるけど。
あの岩波文庫の原論文だけ読んでも理解は難しいと思うけど
後ろに解説がついてるから、一応の大雑把な内容は解説を読んで理解できるとは思う。
寧ろHilbert計画と不変式論の関わりとかに重点を置いて書かれた本なので、
歴史的経緯にあまり興味が無くて不完全性定理本体の数学的内容の理解がしたいのならお勧めしません。
というかそもそもPrincipia Mathematicaの公理系の説明とかきちんと書いてなかったような。
code化はきちんとやってるからそこから類推は出来るかもしれないけど。
0790１３２人目の素数さん
2008/02/25(月) 20:04:050791１３２人目の素数さん
2008/02/25(月) 20:18:46ゲーデルと20世紀の論理学の第三巻とか。
洋書で良いならComputability & Logicとか
SmullyanのG&omul;del's Incompleteness Theoremsとか。
但しゲーデルと20世紀の論理学の三巻とSmullyanは
一階の述語論理について或る程度分かっていることが前提。
前原昭二の数学基礎論入門は古い本で、
ほぼ原論文に沿った形で型理論に対して不完全性定理を証明している。
0792１３２人目の素数さん
2008/02/25(月) 20:21:41洋書の数理論理学の入門書なら結構不完全性定理についてきちんと書いてあるのが多いよ。
0793１３２人目の素数さん
2008/02/25(月) 23:14:58「数学基礎論やガロア理論、フェルマーの定理を理解するにはまず何をするべきだろうか」
と聞かれた。当人はどうもベクトルや複素数のことを前提知識と考えているようでちょっと回答に窮した。
その教授は歴史上の学者に関しての論文を今まとめているらしいが、数学や物理の難解理論が分からんから人物の凄さも分からんとのこと。
来週もまた尋ねるんだが、おまいらなら何と答えますよ？教授は高校数学(ⅢC)までは理解している。
0794１３２人目の素数さん
2008/02/25(月) 23:20:52ブルバキ一式持っていってぶつけてやったら？
0795１３２人目の素数さん
2008/02/25(月) 23:26:08どこの星の考古学・歴史学だよ
0796１３２人目の素数さん
2008/02/25(月) 23:32:35数学基礎論はゲーデルと２０世紀で分かりそうなところを
読んでもらって、フェルマーは諦めてもらうのが手頃では。
ところで（私は基礎論に素人の数学専攻ですが）、ゲーデルと２０世紀は
どの巻も二つ目がよく書けてる気がするのは気のせいでしょうか？
某巻の三つ目に、あまりにひどいミスぷりがあるのは私の本だけ
なのだろうか。幾ら何でも素人編集者でも気付くべきだと思ったのですが。
0797１３２人目の素数さん
2008/02/25(月) 23:58:56ありがとうございます。
Computability and Logic/ Boolos, Burgess, Jeffrey (Paperback)
$29.99
が名著とされているようですね。値段も安いです。
0798１３２人目の素数さん
2008/02/26(火) 00:04:45起点数が10
信頼水準（1-α)＝0.99（信頼係数2.58）
N=10000
抽出誤差5％
コレの調査対象の数を求める計算が判らん
計画数理って強化なんだが
スレチだったらスマン
0799１３２人目の素数さん
2008/02/26(火) 00:16:22ってのは素直で良いと思うけどな。
理論をまともに理解しようと思ったら、
相当な時間が根気が必要だということをまず伝えないといけない。
ロジックの部分に限って言うなら、他の分野の知識が無くてもあまり困らないので
入門書をいくらか読んで研究の歴史的動機を他の本で勉強すればどうにかなるかも。
実際に哲学専攻の一部の人は基礎論には滅茶苦茶詳しかったりすることもある。
取り敢えず「歴史上の人物」が誰かによって少々違うけどゲーデルなら
廣瀬・横田の「ゲーデルの世界」とか「確かさを求めて」とか。
あとFrom Frege to Godelとかが歴史的な研究という観点からは良い本。
FLTを「その証明まで」理解するには数論とか代数幾何専攻の大学院生と
ほぼ同等の勉強が必要になるから常識的に考えて無理だというしかない。
おそらく通俗的な解説本を読んでお茶を濁すことになる。
歴史的経緯ということなら「フェルマーの最終定理13講」とかが良いのかな。
ただ、コラッツやゴールドバッハが偉大な数学者とは言われないのと同じ理由で
FLTを予想したということは別にフェルマーの主要な業績じゃないと思うけどね。
0800１３２人目の素数さん
2008/02/26(火) 00:26:270801１３２人目の素数さん
2008/02/26(火) 00:32:50一巻は田中尚夫の第一部も結構面白いことが書いてある。
他の巻は、第一部が基礎の解説、第二部が発展的事項の紹介、
第三部が哲学の話というのが基本っぽいので
第二部をありがたく感じるってことじゃないかな。
＞某巻の三つ目に、あまりにひどいミスぷりがある
ってのは何のことかな。まあ記述集合論を可述的集合論と訳すような
ものすごいミスじゃない限り無問題かとｗ
>>798
質問スレか統計のスレへgo
0802１３２人目の素数さん
2008/02/26(火) 00:39:57基礎論の人の論文は、他の数学分野の論文に比べる平均的に
短い傾向にあるように思われるのですが、なぜなんでしょうか？
0803１３２人目の素数さん
2008/02/26(火) 00:46:39おぼしきランダムな文字列があるな。
0804793
2008/02/26(火) 00:58:48まあ本の虫でかつ研究職だけあって研究心は異常なんで、教えれるところは教えたい。
しかし国立大学の図書館はいいな。蔵書数のケタが違う。
0805１３２人目の素数さん
2008/02/26(火) 01:09:24野球を知らない人にイチローのプレーの凄さを説くようなもんだ。
文系ってやっぱり数学科なんかが何やってるのか意味不明らしいな。
幾何学とか面体とか名前からして。
0806１３２人目の素数さん
2008/02/26(火) 01:27:370807１３２人目の素数さん
2008/02/26(火) 01:29:01全部リストアップして持ってくってのもネタとしては良いかも。
ブルバキ一式持ってくより余程インパクトがあるかとｗ
0808１３２人目の素数さん
2008/02/26(火) 01:32:49こっちが>>793から勝手に想像してしまってるのかもしれんが
0809１３２人目の素数さん
2008/02/26(火) 03:41:59前提知識を知りたがってるのにいきなりそれはどうなんだｗ
>>808
説明を聞いても何を読んでも分からんだろうから、何をすべきだろう的な感じだった。
大学教授なんて知ったかの塊なんで、ずいぶんと真摯な態度だな、とか偉そうに思ってしまった。
0810１３２人目の素数さん
2008/02/26(火) 04:18:07知ったかの塊みたいな人ってあんまいないんだけど
0811１３２人目の素数さん
2008/02/26(火) 11:08:01小野孝の数論序説と足立恒雄のフェルマーの大定理
廣瀬・横田の「ゲーデルの世界」とりあえずこの三冊をもっていったら？
0812１３２人目の素数さん
2008/02/26(火) 20:23:33内容に細かいミスがあったり、うまくストーリーが
繋がらないところとかがあったりするから短所の無い本、というわけではないけどね。
0813１３２人目の素数さん
2008/02/26(火) 22:24:09以下のサイトをみてみるといい。
下のほうで述語論理を学んで、上のほうでゲーデルも含めて一階論理が
扱われている。
http://www.phil.gu.se/posters/first-order-logic.pdf#search='first%20order%20logic'
http://research.nii.ac.jp/~terui/mita06.pdf
0814１３２人目の素数さん
2008/02/26(火) 22:36:54解説書や解説サイトは山のようにあるよね。
いろいろ見て回ったけど、結局やっぱり原論文だけでいいやってなってしまった。
シンプル、かつ厳密、やや冗長のきらいはあるがそのぶん誤解を生みにくい。
0815１３２人目の素数さん
2008/02/26(火) 22:45:43Simpsonのホームページにある論理学の講義ノートとかも良さげ。
0816１３２人目の素数さん
2008/02/27(水) 00:46:40おすすめがあれば教えて下さい。
0817１３２人目の素数さん
2008/02/27(水) 16:23:57１．計算は物理操作である、紙の上に書いても脳で行っても、記号操作は、物理操作と表裏一体
２．物理操作の基本は量子力学にあるに違いない
３．チューリングマシンは古典力学に基づいて作られている
４．量子コンピュータを考えると量子チューリングマシンも考えられる
５．量子チューリングマシンの基本操作でできる事は、チューリングマシンを拡張している
チューリングマシンは拡張可能→数学も拡張される？
0818１３２人目の素数さん
2008/02/27(水) 16:35:31情報板池
0819１３２人目の素数さん
2008/02/27(水) 16:38:50それを認めたら数学基礎論なんて数学じゃないし、板違いになる。
0820１３２人目の素数さん
2008/02/27(水) 16:57:13何も知らないなら一冊目にはこれがおすすめ
大学の一回生でも絶対に最後まで読める
ttp://www.amazon.co.jp/dp/4316376209/
で、同じ著者のこの本は評判が良いので（この間復刊された本）
次にこれを読むのはどうだろう
ttp://www.amazon.co.jp/dp/4254116608/
0821１３２人目の素数さん
2008/02/27(水) 17:00:25／(＾o＾)＼
0822１３２人目の素数さん
2008/02/27(水) 18:57:46いやいや、どんな偏見を持ってるのか知らんけど集合論もモデル理論も数学だろ。
量子計算機の話題は普通は数学よりも物理よりの話題ってことになってると思うけど。
>>816
そっち方面の定番として良く知られてる洋書の専門書はいくつかあるみたいだけど
最初はもっと軽めの本で始めたほうが良いだろうなあ。
「計算論入門」渡辺 治、米崎 直樹
が参考文献に挙げられてるのを見たことがある。まともに読んだことないので中身は知りません。
あと「帰納的関数と述語」篠田寿一とかかな。もう本屋には売ってないけど。
0823１３２人目の素数さん
2008/02/27(水) 19:47:480824１３２人目の素数さん
2008/02/27(水) 21:18:060825１３２人目の素数さん
2008/02/27(水) 21:42:39でも広瀬 健ってめんどくさい証明はすぐ省略する癖があるよねえ。
0826１３２人目の素数さん
2008/02/27(水) 21:57:20量子計算可能=計算可能
だったはずだが
0827816
2008/02/27(水) 22:08:28英語の定番の本も良ければ教えて頂ければ参考にしたいです。
現在持っている予備知識は「ゲーデルと２０世紀」の三巻
不完全生定理の章と竹内外史「語の問題」の２章までです。
0828１３２人目の素数さん
2008/02/28(木) 02:06:54たぶん「情報板」が変だって言いたいなんだと思うよ
実際基礎論って情報系の学部に追い出されてない？
0829１３２人目の素数さん
2008/02/28(木) 02:16:080830１３２人目の素数さん
2008/02/28(木) 04:19:36肝心なところは、計算可能とかそんな所じゃなくて、数学は物理から分離独立できないと思われるところだと思った。
0831１３２人目の素数さん
2008/02/28(木) 04:30:590832１３２人目の素数さん
2008/02/28(木) 04:33:210833１３２人目の素数さん
2008/02/28(木) 04:33:46量子構造の定義からちゃんとやってくれよ。
0834１３２人目の素数さん
2008/02/28(木) 05:25:58Wikipedia - 数学
http://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6
とかの項目にあるようなのが一体何物なのかをを素人にすら分かるように解説した本ってなかったっけ？
0835１３２人目の素数さん
2008/02/28(木) 17:19:51連続体「仮設」のこと?
帯までそうなっていたね。
0836１３２人目の素数さん
2008/02/29(金) 00:22:48単なる誤字、誤訳である場合が多いけど、
例えば志賀浩二なんかは、「集合への30講」とか「無限への飛翔」
なんかで連続体「仮設」という言葉を意図的に使っているみたい。
個人的にはあくまでもhypothesisのほうが良いんじゃないかと思うけどね。
0837１３２人目の素数さん
2008/02/29(金) 11:23:35でもね、最近基礎論が実は近似なんじゃないか(<-なんじゃそりゃと思われるかもしれないが)という気もしなくもない
0838１３２人目の素数さん
2008/02/29(金) 11:28:590839１３２人目の素数さん
2008/02/29(金) 21:09:490840１３２人目の素数さん
2008/02/29(金) 21:54:42近似にきまってんじゃねーの？それとも永久不変の真実だって？
0841１３２人目の素数さん
2008/02/29(金) 23:36:590842１３２人目の素数さん
2008/03/01(土) 15:17:31＞「数学基礎論やガロア理論、フェルマーの定理を理解するにはまず何をするべきだろうか」
大学の理学部数学科に入って卒業するまで４年間勉強すること。
＞数学や物理の難解理論が分からんから人物の凄さも分からん
成果は凄いが、別に人物は凄くない。
まあ、理解できないのなら、
「数学者や物理学者なんてただのワケワカラン奴だ」
と書いていただいて構わない。
数学や物理が理解できない人に口先だけ褒められても不愉快だ。
だいたい人に褒められたがる奴は精神をわずらってるから入院すべき。
0843１３２人目の素数さん
2008/03/01(土) 15:31:22※を示すためには、どうすればいいですか？
∀x∈R,(sub(add(x,1),1)=f(x))・・・①
(sub(add(x,1),1)の定義域)=(f(x)の定義域)・・・②
①∧②を示さずに※を示す方法はありますか？
0844１３２人目の素数さん
2008/03/01(土) 18:19:11どういう体系での証明を考えてるのかよくわからないんだけど。
0845１３２人目の素数さん
2008/03/01(土) 21:11:21＞大学の理学部数学科に入って卒業するまで４年間勉強すること。
そしてそれでもFLTの証明は後姿すら見えないほど遠い位置にいることを
わからせること。
0846１３２人目の素数さん
2008/03/01(土) 21:38:16λ式でやってみたら？
0847１３２人目の素数さん
2008/03/01(土) 21:42:320848１３２人目の素数さん
2008/03/01(土) 22:08:52どうしてまともな質問よりこのような話にレスが多くつくのだろうか・・・。
0849１３２人目の素数さん
2008/03/01(土) 22:22:01じっくり悩んだほうがいいという場合が多いから
だと思われる。
あるいは内容によっては一言で済むってことも。
0850１３２人目の素数さん
2008/03/02(日) 07:42:50すみません、教えてもらえないでしょうか？
0851１３２人目の素数さん
2008/03/02(日) 08:31:03SUCC := λ 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
これみてがんばれ。
0852１３２人目の素数さん
2008/03/02(日) 08:49:27(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)の定義域)
などを省略しているというわけではないということですか？
0853１３２人目の素数さん
2008/03/02(日) 09:01:49あ、ごめん。
自然数の演算の話かと思ったよ。
普通に微分してxでいいんじゃね？
dom, codomが気になるの？
ちなみにuntyped lambdaだから域なんて考えてないよ。
0854１３２人目の素数さん
2008/03/02(日) 09:15:46はい、定義域や値域(始域や終域)が一致してるかどうかを無視しているのが
きになって。関数を等号で結んでいるのに、域を無視していいのでしょうか？
0855１３２人目の素数さん
2008/03/02(日) 09:30:49でも（高校数学っぽい）微分とか言ってるから、暗黙に実関数の話なんでしょ？
関数のequalityが気になるのなら、関数をbinary relationに置き換えてみて、
R^2の部分集合として同じになるのをチェックしてみたら？
0856１３２人目の素数さん
2008/03/02(日) 09:42:12始域終域定義域値域が全てＲであるということを前提としているということですか？
では、サイコロをn回振って1が１回以上出る確率をp(n)を求める時
p(n)=1-(1/6)^n=(6^n-1)/(6^n)という変形における関数のequalityでは
始域終域定義域値域全てＮであることを前提とするんですかね？
0857１３２人目の素数さん
2008/03/02(日) 10:04:41だから、論理展開している前提条件(context)によるんじゃないの？
0858１３２人目の素数さん
2008/03/02(日) 10:11:11あとね、855で集合的に考えてみたらって書いたのは、
域とか関係なしで、外延性公理でもつかって、納得したらってのもあったんだけどね。
0859１３２人目の素数さん
2008/03/02(日) 10:26:22この問題を解くとき、どのような論理展開をするのが一般的でしょうか？
域を全てＮとして関数のequaliyで攻めるのか、全称記号を使って数値のequality
で攻めるのか
>>858
グラフの一致は外延性公理でいけますが、
関数の一致には、グラフの一致＋域の域の一致を考慮に入れる必要があるような気がして。。
0860１３２人目の素数さん
2008/03/02(日) 10:33:48だれかバトンタッチpls.
ｵﾚは遁走する。
0861１３２人目の素数さん
2008/03/02(日) 10:45:400862１３２人目の素数さん
2008/03/02(日) 11:33:09もまいらスルーしる
0863１３２人目の素数さん
2008/03/02(日) 13:06:26856の確率の問題を立てるとき、
λ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か
どちらの論理展開をすればよいかが分かりません。前者の場合は、域を
考慮に入れないといけない分、後者に比べて無駄なことをしてる気がするのですが。
0864１３２人目の素数さん
2008/03/02(日) 13:19:03リンク先のpdf全然読んでねーな？
0865１３２人目の素数さん
2008/03/02(日) 13:43:190866１３２人目の素数さん
2008/03/02(日) 17:20:450867１３２人目の素数さん
2008/03/02(日) 18:08:07濃度が分数な集合が定義できる体系のことです。
0868１３２人目の素数さん
2008/03/02(日) 18:38:07英語がよめないのですが、その方法をとると
∀x∈R,(sub(add(x,1),1)=f(x))を示さずに
関数が一致することを示せるのでしょうか？
0869１３２人目の素数さん
2008/03/02(日) 19:19:210870１３２人目の素数さん
2008/03/02(日) 19:21:580871１３２人目の素数さん
2008/03/02(日) 20:31:37κ/λならそれは常にκとか、無意味な定義で。
なので、分数濃度としてどういう性質を要求したいかが分からないとどうしようもない。
0872１３２人目の素数さん
2008/03/02(日) 20:49:12まあやるとしたらcardinal arithmeticが閉じたものになるようにするあたり？
cartesian productに対応する逆概念がなんなのかよくわからんが。
0873１３２人目の素数さん
2008/03/02(日) 20:55:49つか書いた直後であれだが、片方の濃度が1じゃなければ、
primeな濃度のproduct setなんて存在しないから、意味ないな。orz
0874１３２人目の素数さん
2008/03/02(日) 21:16:28と思いつきで書いてみる
0875１３２人目の素数さん
2008/03/02(日) 22:22:440876１３２人目の素数さん
2008/03/02(日) 23:46:280877１３２人目の素数さん
2008/03/02(日) 23:52:240878１３２人目の素数さん
2008/03/02(日) 23:53:100879１３２人目の素数さん
2008/03/02(日) 23:55:230880１３２人目の素数さん
2008/03/02(日) 23:56:510881１３２人目の素数さん
2008/03/03(月) 00:10:22説明できない人が言ったとしたら只の馬鹿だよ
0882１３２人目の素数さん
2008/03/03(月) 15:19:26何でもそうだが、何らかの結果にいたらないうちは、「意味がない」
とされるべきだ。そうでなければ、語呂合わせをするごとに、意味が
あるかないか判断する必要が生じる。そんなバカなことはする必要
がない。
0883１３２人目の素数さん
2008/03/03(月) 15:37:46どっちか判断しかねるときは「分からない」と宣言する。
そうすれば、必ずしも意味があるかないか判断しなくてよい。
そのかわり、「くだらない」と宣言したら、なぜくだらないのか説明する必要が生じ、
「くだらなくない」と宣言したら、どこが有用なのか説明する必要が生じる。
0884１３２人目の素数さん
2008/03/04(火) 11:50:380885１３２人目の素数さん
2008/03/04(火) 14:46:280886１３２人目の素数さん
2008/03/04(火) 15:56:21"fractional cardinality"で検索すると結構引っ掛かるけどその辺は違うの？
0887１３２人目の素数さん
2008/03/04(火) 18:49:59ラムダでやったらぁ～って書いた人だけど、哲板には行った事無いよw
873-もｵﾚのレスじゃないし。
0888１３２人目の素数さん
2008/03/04(火) 18:58:00・ 数学と哲学
・ 数学を理解できない馬鹿が、哲学に逃げる
・ モチーフの哲学と志村多様体
記号言語としてしか興味ないのでw。
0889１３２人目の素数さん
2008/03/04(火) 19:08:10哲学とかどうでもいいけど、もう数学板にも来なくていいからｗ
0890１３２人目の素数さん
2008/03/04(火) 19:11:02ラムダでやったらぁって提案しただけで、(x+1)-1=xがどうのこうのとか、
分数濃度ってあるの？とか、くだらないのうんぬんって、ｵﾚとは別人だから。
冤罪はご免だw
0891１３２人目の素数さん
2008/03/04(火) 21:52:04これだから意味不明はスルーしろってあれほど…
0892１３２人目の素数さん
2008/03/04(火) 23:17:39誰が誰で誰と話してるんだ
0893１３２人目の素数さん
2008/03/05(水) 01:02:400894１３２人目の素数さん
2008/03/05(水) 10:01:26うん。おまえはよくやった！
ただ余計な事まで書いちまったようだ
0895１３２人目の素数さん
2008/03/05(水) 10:13:370896１３２人目の素数さん
2008/03/05(水) 12:19:080897１３２人目の素数さん
2008/03/05(水) 23:42:250898１３２人目の素数さん
2008/03/05(水) 23:52:200899１３２人目の素数さん
2008/03/06(木) 00:29:330900１３２人目の素数さん
2008/03/06(木) 00:37:26ラムダ式の人はともかく分数濃度の普通の質問じゃね？
こっちの場合はどちらかというと知らないのに無理に答えようとして紛糾した感じだが
0901１３２人目の素数さん
2008/03/06(木) 00:41:490902１３２人目の素数さん
2008/03/06(木) 11:33:470903１３２人目の素数さん
2008/03/06(木) 14:21:33普通の質問なら普通の答えが返ってくるよ
0904１３２人目の素数さん
2008/03/08(土) 14:52:34これとか？ なんかあまり集合という感じはしないけど。
ttp://math.ucr.edu/home/baez/week147.html
0905１３２人目の素数さん
2008/03/15(土) 19:12:05ソーカル
0906１３２人目の素数さん
2008/03/21(金) 11:19:20自然数の数が加算有限ならば、私の思ったことは間違ってるはずなのです。
任意の自然数nを0<x<1に変換する全単射な関数f(n)を定義する。
たとえばf(n)は、
f(1)=0.1 (=0.1000000000000000・・・・)
f(23)=0.32 (=0.320000000000000・・・・)
のように、自然数の10^mのけたをそれぞれ、10^(-m-1)に変換する関数。
ここで、
f(1)=0.100000000000000000000000・・・・
f(2)=0.200000000000000000000000・・・・
・・・・
のようにならべて、あとは対角線論法と同様の方法を使えば、
並べたなかにはない小数rが存在することがわかり、
fの逆関数をgとすると、並べたなかにはない自然数g(r)が存在し、
自然数は不加算であることがわかる。
自然数が加算であり、対角線論法に間違いがないと認めるなら、
何が間違っているでしょうか？
0907１３２人目の素数さん
2008/03/21(金) 11:27:58この議論がまずいのは、一つには０が連続する小数と９が連続する小数の区別が暗黙に前提されていること
（たとえば0.100000…と0.09999999…）、もうひとつにはその前提を無視して対角線論法を適用した
「つもり」になっていること。
「実際に」対角線論法を使ってみれば、これが間違えなのがすぐわかる。
0908１３２人目の素数さん
2008/03/21(金) 11:39:48数字のずらし方によるのでそれはあまり関係ない。
>>906
fは全射ではないので、その逆関数gの定義域は区間全体にはならない。
rは定義域に含まれないので、g(r)存在しない。
0909906
2008/03/21(金) 11:46:02つまり、
・０が連続する小数と９が連続する小数は区別できないので、例に出したf(n)は単射ではない
・条件を満たすf(n)はそもそも存在しない
(存在を仮定した時点で、自然数が実数と同じ濃度と仮定しているのと同じ)
ということでしょうか。
0910906
2008/03/21(金) 11:51:19>>908
全射じゃない？どのような小数でも、自然数に戻せるのでは。
（桁数が無限なら、戻すのに無限の操作は必要ですが）
0911１３２人目の素数さん
2008/03/21(金) 11:57:02仮定も何も、そのfってのが10進表記の数字の並びを逆にして小数点以下にくっつける関数のことを言ってるんだとしたら
全然全射になってないっていうか、1/3とか1/√2とか対応できてない数字が幾らでもあるでしょ。
0912写楽ほーすけ
2008/03/21(金) 12:11:49無限階正則連続写像対象Ｇはシュワルツ超関数Ｃ（無限）Ｇ⇒無限回可微分Ｇ
0913906
2008/03/21(金) 12:20:33g(1/3)は33333333333333333・・・・だし、
g(1/√2)は・・・・187601707だし、対応できるのでは？
無限小数だろうがなんだろうが、
ひとつひとつの数字を見ると加算無限個の0～9の整数の並びなのだから、
変換自体はできるはず。
0914１３２人目の素数さん
2008/03/21(金) 12:24:12えっと……自然数の定義分かってるよね？
0915906
2008/03/21(金) 12:42:360916写楽ほーすけ
2008/03/21(金) 12:44:04（ｇ～：ａ） ∩ ｛Ｇ∩∋⊃ａ｝
なので、元群表記は ｇ⇒ａ になるはずなんですが？
それと、カントール型無限連続体論ですか？
>>914 よく解りません。教えて下さい！
ドラやき
0917１３２人目の素数さん
2008/03/21(金) 12:51:39全射である必要に、なぜ1/3や1/√2が関係してくるんだ？
0918917
2008/03/21(金) 12:53:270919１３２人目の素数さん
2008/03/21(金) 13:14:07０に「１を足す」をという操作を有限回繰り返して得られる数ね（あんまり正確じゃないけど）。
「１を足す」という操作を有限回繰り返しても333333…なんて数は出てこないでしょ？
0920906
2008/03/21(金) 13:48:130921１３２人目の素数さん
2008/03/21(金) 13:58:08本気で自然数が有限しか無いって言ってるのか？
0922１３２人目の素数さん
2008/03/21(金) 14:15:29桁数が無限大の自然数というのは存在しますか？
0923906
2008/03/21(金) 14:16:25足す回数が有限でなければ、有限じゃなくなるけど。
0924１３２人目の素数さん
2008/03/21(金) 14:17:47いや多分>>920が言いたいのは、
有限回数の「１を足す」操作で到達できるものだけを整数と言うのであれば
整数は有限個しかないことになってしまうが、実際は整数は可算無限個ある
ゆえに、整数には「１を足す」操作を無限回繰り返した物も含まれる
ってことなんじゃね？
こういう、
「有限回の操作」の有限回をどこまでも大きくできるという話に、
不用意に「無限回」という意味不明の概念を持ち込んでしまう輩の脳内から、
混乱した「無限」の概念を引きはがすには、どうしたらよいのだろう。
0925１３２人目の素数さん
2008/03/21(金) 14:20:50というよりそもそもきちんと定義されてない。
「 0 に +1 をという操作を有限回繰り返して得られる数」
の全体は可算無限個でしょ。個々の自然数は有限の大きさ。
自然数は全部で無限個あるというのと、大きさが有限でない自然数が在るというのは区別しないと。
0926１３２人目の素数さん
2008/03/21(金) 15:00:11昨夜の「◆ わからない問題はここに書いてね ２３９ ◆」スレの656と
よく似てるね。
数学好きの中学生？高校生？
0927１３２人目の素数さん
2008/03/21(金) 15:01:410928906
2008/03/21(金) 15:02:35有限回足すだけですべての自然数ができるって定義になるはずです。
0929906
2008/03/21(金) 15:03:39昨夜は来てないです。
数学が苦手な大学生です。
0930１３２人目の素数さん
2008/03/21(金) 15:05:36まずは、一階述語論理とペアノ算術でもやったほうがいいんじゃないの？
0931１３２人目の素数さん
2008/03/21(金) 15:09:37そんなレベルではないような気がするが
0932１３２人目の素数さん
2008/03/21(金) 15:13:14そこが分かっていれば、>>906のfが全射でないことも分かるだろう。
0933１３２人目の素数さん
2008/03/21(金) 15:21:52そうなのか。てっきりオッサンかと思った。
似たようなことサイト開いて書いてるオッサンがいたから。
0934１３２人目の素数さん
2008/03/21(金) 15:51:480935１３２人目の素数さん
2008/03/21(金) 15:55:050936１３２人目の素数さん
2008/03/21(金) 16:02:14RichardやBerryの逆理との区別が付かない数学者は
たくさん居たからね。
ZermeloとWittgensteinは良く分かってなかったはず。
Russelも表層的な理解しかしていなかったような感じ。
0937１３２人目の素数さん
2008/03/21(金) 16:05:040938１３２人目の素数さん
2008/03/21(金) 16:49:390939１３２人目の素数さん
2008/03/21(金) 16:59:160940１３２人目の素数さん
2008/03/21(金) 16:59:450941１３２人目の素数さん
2008/03/21(金) 17:06:40死ねばいいのに
0942１３２人目の素数さん
2008/03/21(金) 17:18:52これは集合に関する記法を全く知らない人の疑問だけど、
基礎論を勉強し始めると
「要素として含まれる、というのはどういう意味か？」
という疑問が湧いてくることがあって、
そして今度は A と ∈ と B という三つの記号が並んでいるだけ、
と答えざるを得ないことになる。
別に940が単なる皮肉を言っているわけではないよ。
ただの記号列だと見做すというのは基礎論でよくやるやり方。
まあ906にせよ940にせよ基礎論の質問じゃないんだけどね、、
まあ数学科でも人によってはこんなのが
基礎論なんだと信じて疑わない人も居るんだろうね。
0943１３２人目の素数さん
2008/03/21(金) 17:24:50知ったか乙ｗ
Ａ∈ＢはＡは集合Ｂに属するって意味だ
お前が言ってるのはＡ⊂Ｂ←こっちの話し
0944１３２人目の素数さん
2008/03/21(金) 17:36:44A ∈ B というのは A が B の要素である ということ。
要素として含まれる、も、元となってはいり込んでるも
要素として潜り込んでる、も、みんな同じ、要素である と同じ。
言葉のニュアンスなんか問題にしてはいけない。
0945１３２人目の素数さん
2008/03/21(金) 17:43:580946１３２人目の素数さん
2008/03/21(金) 17:44:19記号の羅列に対する変形規則として数学を定義するとどうなるかというような
議論を想定して言ってるんじゃねーか。
それこそが基礎論なんだと信じて疑わない人なのだろう。
0947写楽ほーすけ
2008/03/21(金) 17:47:59∩（Ｇ）∋｜｛Ａ｝ ∈∩ ｛Ｂ｝
この様な記述法もある。
0948１３２人目の素数さん
2008/03/21(金) 17:50:01含まれる は両方の意味に使われることがある。
だからあまり好ましい言葉遣いではないというのは確かにそうなんだけどね。
>>946
いや基礎論の一部でしょ。それが全てだとは誰も言ってない。
0949写楽ほーすけ
2008/03/21(金) 17:53:57［ｍｏｄ～（Ｇ）∋⊇（ａ）］
～∩（Ｇ）∋｜｛Ａ｝⊆∈｛Ｂ｝
の書き方もある。
、
0950１３２人目の素数さん
2008/03/21(金) 18:00:59どこかでアホの放生会でもやったのか
0951１３２人目の素数さん
2008/03/21(金) 18:52:57X*(Y_L) + (X_L)*Y - (X_L)*(Y_L) って、
{ X*y + x*Y - x*y | x∈(X_L), y∈(Y_L)} って意味ですか？ それとも、
{ X*(y_1) + (x_1)*Y - (x_2)*(y_2) | (x_1),(x_2)∈(X_L), (y_1),(y_2)∈(Y_L)} って意味ですか？
0952１３２人目の素数さん
2008/03/22(土) 13:09:280953１３２人目の素数さん
2008/03/23(日) 17:40:200954１３２人目の素数さん
2008/03/26(水) 21:19:440955１３２人目の素数さん
2008/03/27(木) 19:14:30この集合に属する全ての座標データの分布について
別のパラメータで表す方法ってどのようなものがあるのでしょうか？
0956955
2008/03/27(木) 19:17:54「なるべく分布の特徴を失わずに別のパラメータで表す方法」
です
よろしくお願いします
0957１３２人目の素数さん
2008/03/28(金) 08:21:36全部束縛変数ではいけないのでしょうか…
0958１３２人目の素数さん
2008/03/28(金) 10:13:200959１３２人目の素数さん
2008/03/28(金) 11:28:500960１３２人目の素数さん
2008/03/28(金) 16:14:14ああ、たしかにtureな文だね。
0961１３２人目の素数さん
2008/03/28(金) 16:15:35というか、最初にfreeじゃないとbindもできないんじゃないの？
0963１３２人目の素数さん
2008/03/28(金) 17:33:55￢∀x(P(x)) ⇔ ∃x(￢P(x)) はどうやったら証明できますか？
0964１３２人目の素数さん
2008/03/28(金) 18:19:34閉じた式だけでいいんじゃないか
ということだな
0965１３２人目の素数さん
2008/03/29(土) 19:40:360966１３２人目の素数さん
2008/04/01(火) 06:34:30R^(1/2)の意味は？
0967１３２人目の素数さん
2008/04/01(火) 09:07:101/2からRへの写像全体
0968１３２人目の素数さん
2008/04/01(火) 09:32:070969１３２人目の素数さん
2008/04/02(水) 00:59:081/2を集合とする限りは意味無し。
1/2が空集合のときはR^{1/2}＝R^{φ}＝φとなって意味無し。
1/2が1元集合のときはR^{1/2}＝R^1 となって、やはり意味無し。
：
：
0970１３２人目の素数さん
2008/04/02(水) 02:25:37ありがとうございます。
他の定義の仕方でも駄目ですか？
0971１３２人目の素数さん
2008/04/04(金) 02:16:00ファジーって真偽値を実数の区間[0,1]にとるものだろ、
だったら直観主義論理の部分系となるわけで、集合論的には不思議なものはでてこないのでは。
確か、竹内外史のお弟子さんの本があったような。
0972１３２人目の素数さん
2008/04/04(金) 02:26:59でも真偽値集合の濃度が非可算無限になるのでandの演算がなんか変になりそう。
というか旧来の論理からはみ出そう。
0973１３２人目の素数さん
2008/04/04(金) 04:43:08今までにどこかで誰かがやっている
おもしろ特許じゃないんだから
0974１３２人目の素数さん
2008/04/04(金) 04:54:07どうにか面白くしてくださいって感じ？
0975１３２人目の素数さん
2008/04/04(金) 06:59:12おまいら寝ろよ。ろくなアイディアも出なくなるぞｗｗｗ。
0976１３２人目の素数さん
2008/04/04(金) 10:22:310977１３２人目の素数さん
2008/04/04(金) 23:37:05普通にブール値使うとか（この場合はH値か）と同じ程度にははみ出すけれど、それ以上は？
0978１３２人目の素数さん
2008/04/05(土) 00:14:39こういう式ってどういう意味ですか？
どういうキーワードでぐぐったらこういうのの解説でてきますかね？
0979１３２人目の素数さん
2008/04/05(土) 00:28:09もしあったらどんなものかを考えて見当つけるのは探す上で普通のことだろ？
明らかにありそうに無いなら探しても無駄なんだから。
0980１３２人目の素数さん
2008/04/05(土) 00:31:04取り敢えず変なものを作ってみよう、
というので大したものって無いような気がするなあ
>>978
「関数」でぐぐったら。
というかこのスレは基礎的な数学のスレじゃなくて
数理論理学とか公理的集合論とかのスレだからね。
誤解無きよう。
0981１３２人目の素数さん
2008/04/05(土) 00:49:57というか人によって質問者のこと言ってたり回答者のこと言ってたりで話が錯綜してる気がする。
0982１３２人目の素数さん
2008/04/05(土) 01:19:13ありがとうございます
わかりました
0983１３２人目の素数さん
2008/04/05(土) 19:22:390984１３２人目の素数さん
2008/04/06(日) 08:25:12数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
0985１３２人目の素数さん
2008/04/07(月) 07:22:390986１３２人目の素数さん
2008/04/07(月) 20:45:45Heyting算術にω規則を加えたら完全になりますか？
0987１３２人目の素数さん
2008/04/07(月) 20:59:300988１３２人目の素数さん
2008/04/08(火) 19:22:390989１３２人目の素数さん
2008/04/09(水) 19:22:410990986
2008/04/09(水) 20:05:48以下同様にΠi完全ならば存在量化によって(i+1)完全。ω規則によってΠ(i+1)完全。
よってΔ0完全であることを示せば良い。とここまであってますでしょうか？
0991１３２人目の素数さん
2008/04/10(木) 19:23:180992１３２人目の素数さん
2008/04/10(木) 23:08:470993１３２人目の素数さん
2008/04/11(金) 08:34:470994１３２人目の素数さん
2008/04/11(金) 16:48:05数学基礎論の質問スレッド その4
http://science6.2ch.net/test/read.cgi/math/1207899938/
0995１３２人目の素数さん
2008/04/11(金) 19:22:390996１３２人目の素数さん
2008/04/12(土) 09:52:080997１３２人目の素数さん
2008/04/12(土) 09:52:540998１３２人目の素数さん
2008/04/12(土) 10:03:150999１３２人目の素数さん
2008/04/12(土) 10:03:361000小倉優子 ◆YUKOH0W58Q
2008/04/12(土) 10:03:571001１００１
Over 1000Threadもう書けないので、新しいスレッドを立ててくださいです。。。
レス数が1000を超えています。これ以上書き込みはできません。