105 :
132人目の素数さん :
2011/07/04(月) 23:28:23.63 基礎論屋(=馬鹿どもw)に質問しま〜〜〜すw 1:形式的証明が与えられることは大事なことである 2:(ゲーデルの第一)不完全性定理は重要な定理である これらの意見については、どう思います。というか、2番の意見は正しいけど、 1番の意見は全くのデタラメでしょwww
106 :
132人目の素数さん :2011/07/04(月) 23:31:31.17
>>105 :
ということで。基礎論屋(=馬鹿どもw)の考え方によれば
不完全性定理に形式的証明を与えることは重要である
ってことになるよな。じゃ、もう誰かさんがやったのかな?
重要だとすれば、その業績はちょー有名なんだよなあwww
もし未だだったら、それをやったら、重要な業績として高く
評価されるんだよねwwwそれなら、頑張って形式的証明に
挑戦してる人も沢山いるんだよねえw
107 :
132人目の素数さん :2011/07/04(月) 23:38:13.90
>>95 自らの数学への理解にあいまいなものが多く含まれることに
ほとんどの人が気付いていない。
積み木を積み上げていくように数学はできない。
そもそも数学を1から構成する以前に数学とは何かをみな理解していない。
>>102 > そして成り立つかどうかを問題にするものは論理式に対するイメージだろう。
これはちょっとかみ合ってませんね。
「論理式に対するイメージ」って意味論のことを言ってるように聞こえます。
形式論を問題にしてますよ。
>>104 いつか
109 :
おさーん ◆xKQl9rTMwao4 :2011/07/04(月) 23:47:50.04
>>108 つまり式の集合とか可算無限個の項だとかという言い方が
正当(定義可能)なのかどうかってことですよね。
計算理論や不完全性定理の正確な証明を勉強すれば、
その疑問が解消するでしょう。
>>109 ホントですか?!?!
って書こうとしてよく見たら「定義可能」なのかどうか、ってことですか...
定義は可能でしょうとも。
正当性と真偽の違い、とでも言ったらいいんでしょうかね。
111 :
いんでぃ ◆ZnBI2EKkq. :2011/07/04(月) 23:56:30.43
いんでぃ
112 :
かえる ◆JnXWn8istY :2011/07/04(月) 23:56:49.87
かえる
113 :
おさーん ◆xKQl9rTMwao4 :2011/07/05(火) 00:03:01.88
>>110 あなたの持っているイメージは、
具体的に書かれた式とか論理式とか無機質な文字の羅列が、
いきなり集合論的な世界の対象のように
論理式の集合とか、別の論理式を加えた和集合みたいな扱いを
されていることへの違和感ではないだろうか?
それを解消したいならやはり、
計算可能性や不完全性定理の証明過程の議論が回答になると思う。
114 :
132人目の素数さん :2011/07/05(火) 00:27:38.40
・ゲーデルの不完全性定理の形式的証明はすでに与えられている(勿論読むに耐えない) ・医師に依る死亡確認が大切なのと、どの医師が死亡確認をしたのかは副次的な事なのとは両立する。
115 :
132人目の素数さん :2011/07/05(火) 01:29:12.69
>>114 :
真実:
定理の証明が重要であることと、その定理の形式的証明が大して意味がないことは普通に両立する
116 :
132人目の素数さん :2011/07/05(火) 01:34:50.98
117 :
132人目の素数さん :2011/07/05(火) 01:44:58.83
真実: 定理(形式的証明に関する定理を含む)の証明は重要であるが、 定理の形式的証明には大して意味がない。
118 :
132人目の素数さん :2011/07/05(火) 02:10:47.76
重要な定理が普通に証明されるよりも前に、形式的証明が与えられれば、 大したものなんだがなあ
119 :
132人目の素数さん :2011/07/05(火) 03:00:40.92
ある重要な定理が証明されたあと、 実はそれ以前に実質的に証明されていた、ということはあるな ゲーデルの不完全定理がまさにその例だ
>>106 >
>>105 :
> ということで。基礎論屋(=馬鹿どもw)の考え方によれば
>
> 不完全性定理に形式的証明を与えることは重要である
>
> ってことになるよな。じゃ、もう誰かさんがやったのかな?
> 重要だとすれば、その業績はちょー有名なんだよなあwww
>
> もし未だだったら、それをやったら、重要な業績として高く
> 評価されるんだよねwwwそれなら、頑張って形式的証明に
> 挑戦してる人も沢山いるんだよねえw
やってる研究者は実際にいる
もちろんコンピュータの助けを借りてだが
その不完全性定理の機械的証明、つまり証明の形式化は確か未完成の時点ではあったが
ちゃんとした本としてCambridge University Pressから出版されているよ
今の時点でその証明の形式化が完成しているか否かは知らないが、草を生やす前にその程度の事は調べたまえ
その程度もチェックせずに草を生やすとは、己の無知蒙昧、不勉強を曝け出しているだけだな
証明を形式化しようとしまいと定理そのものの興味深さは変わらないが
証明を形式化して初めて発見される証明そのものに関する興味深い事実も世の中にはあるんだよ
Girardのパラドックスの形式化をしたケースとかね
121 :
132人目の素数さん :2011/07/05(火) 12:10:24.39
>証明を形式化して初めて発見される証明そのものに関する興味深い事実も世の中にはある たまには意味がある、ということね。逆に言えば、普通は形式的証明にあまり意味はない。 もちろん、そのたまにあることをやったときには、まあ評価はされる。
122 :
132人目の素数さん :2011/07/05(火) 12:16:49.82
>今の時点でその証明の形式化が完成しているか否かは知らない ってことは、その程度にしか注目してない、ということだな そして、「調べがすぐにつかない」ってことは大して意味がないことだから もしも形式的証明が重要であれば、大いに注目を受けていて然るべきだろう
123 :
132人目の素数さん :2011/07/05(火) 12:29:04.31
定理の形式的証明が本当に重要なら、 1:既に形式的証明がついているか?どうか?を気にする 2:まだ形式的証明がついていないのなら、できれば形式的証明を付けたいと思う 君は、どっちも満たしていないみたいだね。つまり、嘘吐き、ということだ。 「本当は大して重要でないこと」を「自分が関わっていることに近いこと(つまり、基礎論の研究)」だから、 重要性を主張しているだけだろう。
124 :
132人目の素数さん :2011/07/05(火) 12:31:50.19
形式的証明に全く意味がない、と言っている訳ではない 動かしがたい事実:「(証明)>>>…>>>(形式的証明)」 だ、ということだ
125 :
132人目の素数さん :2011/07/05(火) 13:46:47.98
完全な証明をつけるのが重要になっているプロジェクトといえば有限単純群の分類 証明完了宣言が出た後、原田耕一郎先生が講演で「実はギャップがたくさんあるんですけどね」と言ったそうだ。 私がその話を聞いたのが1993年で、実際そのあとギャップが発見された(すぐ埋められたが) 完全に形式的な証明をつけることはこの手の小さなギャップを発見するのには役立つかも知れない。
なるほど。 猫
>>120 Shankarのは完成しているよ。対象はZ2。
他に構成主義的な形式的証明もある。
128 :
132人目の素数さん :2011/07/05(火) 16:03:02.55
大定理に初めて形式的証明が与えられても、 大してニュースにもならない件について…。
WKLが唐突に思える人は、スコーレム先生やエルブラン先生の やってたこともちゃんと理解できてないだろ。 かなり初歩的なことなのに。 コンパクト定理、レーベンハイム・スコーレムの定理なんて もう全く理解できないだろうし。
別に形式的に証明を遂行すること自体に価値があるんじゃなくて、 原理的にそうできることで証明自身が数学的対象とみなせたり ある証明が正しいかどうかについて万人の意見が一致したりといった 御利益があるから大事なだけなんだけどね 何かそのあたりから既に勘違いして藁人形を攻撃してるように見える
131 :
132人目の素数さん :2011/07/05(火) 20:39:29.63
>原理的にそうできることで ある数学的な命題が証明できたならば、必ず形式的証明がある って定理でもあるのか?
>>131 その証明が正しければ、
ほとんど機械的に形式的証明に変換できるんじゃないの?
133 :
132人目の素数さん :2011/07/05(火) 20:49:23.92
> 形式的に証明を遂行すること自体に価値があるんじゃなくて ここは同意だが。 > 証明自身が数学的対象とみなせたり > ある証明が正しいかどうかについて万人の意見が一致したり 証明と形式的証明は別物だろ。 「その形式化で偽な命題が形式的証明されないことの証明」+「形式的証明」で証明になることは否定しないが、 形式的証明だけでは証明にはならん。
134 :
132人目の素数さん :2011/07/05(火) 20:57:51.78
>その証明が正しければ、ほとんど機械的に形式的証明に変換できる んじゃ、なぜ、例えば、不完全性定理の形式的証明にてこづった…? もしも証明が正しければ、機械的に形式的証明ができると言うのなら 任意の正しい証明をコンピュータに読み込ませればその定理の正しい 形式的証明を作ってくれるアルゴリズムが存在でもするのか?
135 :
132人目の素数さん :2011/07/05(火) 21:08:46.35
証明は意味論で、形式的証明は統語論。 少なくとも、そういう意味で全くの別物だろう。 1階述語論理までなら、この2つは同じだけど 数学一般になると(既に1階算術のレベルで)、 この2つが乖離すんじゃないのか?
第2不完全性って、第1不完全性定理を形式化して証明するんじゃ なかったっけ?
137 :
132人目の素数さん :2011/07/05(火) 21:22:29.17
第2不完全は「無矛盾である」という命題を形式化する。 しかし、「無矛盾である」という命題の形式化は他にも あって、それは証明できる。結局のところ、形式化には 任意性がある。林晋のページを参照
138 :
132人目の素数さん :2011/07/05(火) 21:25:15.61
例えば、不完全性定理の証明は算術に関する真なる直観を利用して それが正しい、ということを確認した訳だ。真なる直観はもちろん 形式的なものではない
139 :
132人目の素数さん :2011/07/05(火) 21:32:21.91
140 :
132人目の素数さん :2011/07/05(火) 22:03:44.22
完全性定理は、形式的証明できることと恒真(あらゆるモデルで真)が 同じということ ところが、数学は特定のモデルを想定する。そして、形式的証明できる ことと特定のモデルで真であることは乖離する。証明は、想定している 特定のモデルで真であることの確認…
141 :
132人目の素数さん :2011/07/05(火) 22:11:57.46
証明は想定している特定のモデルで真であることの確認。 その特定のモデルを離れて、形式系だけに注目をすれば、 もしその形式系が無矛盾ならば、その命題を公理として 追加しても、新たに矛盾するようなことはない、という こと
142 :
132人目の素数さん :2011/07/05(火) 22:18:49.06
ゲーデルにとって,集合論の対象とする宇宙は唯一つの絶対存在であり,
集合論の各命題は,その宇宙において,真か偽かの確定した値をとる.
ゲーデルは,連続体仮説を成り立たせる人工的宇宙を構成してみせる一方で,
本物の宇宙では連続体仮説は成り立っていないと予想した.
そして,それを示す方法論として,つぎつぎと巨大基数公理を強化して
集合論の公理系を拡大していく所謂「ゲーデルのプログラム」を提唱した.
http://www.utp.or.jp/series/godel.html
基礎付けにこだわってる人に、ブルバキ数学言論「集合論1」の序文から次の引用を贈ろう。 ↓ ・・・しかしすぐに任意の整数と数学的帰納法とを主として用いる典型的な数学的外観を 持つ論証の例に出会うことになる。 ・・・ここでは不当前提の虚偽に関する危険性を否定し去ることはもはや不可能である。 というのは、なかんずく基礎的な事項の説明をしようとしている際に、はじめから算術の 手段の全てを用いているように思われるからである。 ・・・よって、数学者の常識とでも言うべきものに信頼を置かざるを得ない;その信頼とは、 会計係や技術者がペアノの公理の存在を夢想をだにせず公式や数表を承認している ときの信頼と同種のものであり、最終的には事実によって未だかつて否認されたことは なかったという、そのことに基礎を置いているものなのである。 ↑結局は「信頼」して進め、ということだよ。
144 :
132人目の素数さん :2011/07/05(火) 23:05:03.89
今の形式化が気に入らないのなら 全く新しい別世界を創造せよ。
数学言論w
真理表におけるp⇒qだと、その真理値はpとqの真理値のみによるから、 必要条件・十分条件を言うことは出来ないよな?
147 :
132人目の素数さん :2011/07/06(水) 03:38:19.65
数学原論の理念と数学基礎論は違うし 前者は整理と統一的記述 後者は点検とメタ的言及
形式的証明だけでは証明にならないってのは無茶で、 ペアノ算術での7+8=15にの証明は、ただ7+8を計算すればいいのであって ε0までの超限帰納法とかそんなもんを要求するのは狂気の沙汰。 だいたい非形式的であれば無矛盾性の証明は必要無いとでも言いたげなのがわからない。 形式的だろうがそうでなかろうが、ラッセルのパラドックスみたいなのはありうる訳で、 形式的証明には無矛盾性の証明が必要だというのなら非形式的証明だってそうじゃないとおかしい。 不完全性定理は、それがペアノ算術とかで証明できること自体は 早くから分かってたんだけど、その計算機上での実現が遅かったのは、 そもそもまともな演算能力を持つ計算機の実現が遅かったってのもあるし、 既に証明された定理を形式的に表現するのは手間がかかるだけで それ自体にあまり意味が無いからやろうとする人が少なかったという事もある。
"METAMATHEMATICS, MACHINES, AND GOEDEL'S PROOF" N.Shankar SRI International で、ゲーデルの不完全性定理をLispで書いてるけど、ってことは形式化されてる ってことだよね。
150 :
132人目の素数さん :2011/07/06(水) 13:13:16.70
>ペアノ算術での7+8=15にの証明 ってのは形式的証明のことだろ。それから形式化が正しいというのは、 無矛盾ってこと(だけ)ではないが。今、想定している特定の数学的 対象がその形式系のモデルになっているということだ。
151 :
132人目の素数さん :2011/07/06(水) 18:44:59.22
> 「その形式化で偽な命題が形式的証明されないことの証明」+「形式的証明」で証明になることは否定しないが > 形式的証明だけでは証明にはならん。 「その形式化で偽な命題が形式的証明されないことの証明」っていうのは「(正しい)形式化であることの証明」、 同じことだが、「想定している特定の数学的対象がその形式系のモデルになっていることの証明」と言い換えても よい
証明が正しいことの証明とか言い出したらキリ無いよ
キリはあるよ、形而下にあるものを形而上で評価する話なのだから
154 :
132人目の素数さん :2011/07/06(水) 22:18:38.87
>>142 > つぎつぎと巨大基数公理を強化して集合論の公理系を拡大していく
公理系を拡大していく際に、その拡大した結果が集合論の記述として
正しいということが必要であり、これは形式的な無矛盾性の問題ではない。
155 :
132人目の素数さん :2011/07/06(水) 22:22:45.55
>>142 > 集合論の対象とする宇宙は唯一つの絶対存在であり,
> 集合論の各命題は,その宇宙において,真か偽かの確定した値をとる
集合論の形式化は、この真偽値と整合的でなければならず、この整合性が
形式的に証明された定理の正しさを保証する。この整合性の確認は定理の
形式的な証明とは別途に行われる必要がある。
156 :
132人目の素数さん :2011/07/06(水) 22:29:01.89
整合性の確認とは、つまり、集合論がその形式系のモデル (の一つ)であることを確認するということ。
>>136 第二は形式的なものどころか、
省略なしの証明が殆ど無い。
ゲーデル先生も約束しといて放置。
>>149 LispじゃなくてNQTHM。
>>132 > その証明が正しければ、
> ほとんど機械的に形式的証明に変換できるんじゃないの?
無理です。人間は飛躍した証明を好みます。
飛躍してない証明はほとんどの数学者が読むに耐えません。
そんなことはないという人は、
http://r6.ca/Goedel/goedel1.html から
形式的証明をダウンロードして読んでみてください。
5万行弱ありますよ。wellFormed.vだけで1000行を超えるのです。
まあちょっとしたプログラムは直ぐに何万行になるからね
160 :
132人目の素数さん :2011/07/07(木) 20:27:09.10
定理ごとにモジュール化してもダメなの?
>>147 数学原論の理念と数学基礎論の理念はそりゃ違うんだろうけど、
メタレベルに対する算術の適用に関しては結局のところ「信じてる」で同じでは?
後者の理念が「点検」というのなら「信じる」じゃダメでしょ。
信じるなんてスタンスあるわけないだろ。
>>160 モジュール化したものを検証せずに、
正しいと信じて形式的証明に使うのであれば、
それは
>>158 の言う「飛躍した証明」でしょう。
相対的な形式性は確保しているとはいえ。
164 :
132人目の素数さん :2011/07/08(金) 02:46:05.64
繰り返すが、形式証明が証明でもあるための条件は、その形式系が「考察の対象に指定した数学的対象」の形式化になっていること。 例えば、ペアノ公理からの決定不能命題(独立命題)のひとつをAとする。 <1>:ペアノ公理に命題Aをさらに公理として追加した形式系 <2>:ペアノ公理に命題Aの否定をさらに公理として追加した形式系 このうち、どちらか一方は算術の形式化であるが、他方は算術の形式化ではない。 実際(当たり前のことだが)形式系1では命題Aが形式証明できて、形式系2では命題Aの否定が形式証明できる。
165 :
132人目の素数さん :2011/07/08(金) 11:16:18.18
>>163 証明の定義通りだと、いったん証明した定理を再適用するときもまた証明しなおさないといけないでしょ。
一旦証明した定理を公理として使ってよければ証明は短縮できる。
だいぶ意味合いはズレるけどハノイの塔の手順は一つ一つの板の移動を記述したら膨大になるけど、
上のn-1枚の板を第3の棒に移して、一番下の板を目的地の棒に移して、第3の棒のn-1枚の板を目的地の棒に移す
という風に短く書けるでしょ
>>165 > 一旦証明した定理を公理として使ってよければ証明は短縮できる。
何が言いたいのかわからん。短縮したらどうだっての?
ハノイについては帰納法のパワーが直接問題を解いているのであって、
今の問題とは全然関係ない。帰納法自体を理解できてない発言としか思えない。
167 :
132人目の素数さん :2011/07/08(金) 12:35:16.46
藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。 藤原先生は虚偽申請をやりました。藤原先生は虚偽申請をやりました。
168 :
132人目の素数さん :2011/07/08(金) 12:41:09.13
>>166 形式的証明が何万行もあって読むに耐えないけど、それを定理をモジュール化することで短縮できれば何とか読めるんじゃないかということ。
証明の論理式の列に再帰的な構造があればこれによって大幅に短縮できる。
読むに耐えない理由は大抵、各ステップに新たなアイデアが必要だからじゃなくて、「同様に」で済むところを一々書いているから。
169 :
132人目の素数さん :2011/07/08(金) 12:56:35.92
>公理として使ってよければ証明は短縮できる 公理でないものを、公理に追加したら、それは別の形式系だ。 もちろん、定理を公理に加えた場合は、同値な形式系だが…。 例えば、ペアノ公理系に「ペアノ公理系のすべての定理」を 公理として加えた形式系はもとの形式系と(意味論的には) 同値ではあるが、形式的な性質について(=統語論的に)は 大きく異なる部分がある。
170 :
132人目の素数さん :2011/07/08(金) 13:03:01.87
>>169 そのようなことをした場合は、確かに、新たな系では形式証明は不要になる。
しかし、元の形式系で形式証明が簡単化される訳では(当然ながら、)ない。
171 :
132人目の素数さん :2011/07/08(金) 13:08:42.99
藤原一宏先生はえらそうにしているだけで虚偽論文の訂正論文が全く書けません。 コレ常識ナ。 猫
藤原なんぞどうでもいいが さすがに痴漢に言われる筋合いはないだろ
>>172 では誰になら何を言われる筋合いがアルのでしょうか?
猫
175 :
ゆ ◆KkNV/VOqcw :2011/07/08(金) 16:42:31.91
なるほど。
>>172 何故『痴漢に言われる筋合いはない』のかに関する理由を記述して下さい。
猫
177 :
ゆ ◆KkNV/VOqcw :2011/07/08(金) 17:07:37.70
それは難しい。
>>168 そんな素朴なアイデアで短く出来るわけもないことは明らか。
> 読むに耐えない理由は大抵、各ステップに新たなアイデアが必要だからじゃなくて、
> 「同様に」で済むところを一々書いているから。
形式的証明にあまりにも無知。
>>177 幾ら難しくても何とかしなければならない問題が存在します。
猫
180 :
ゆ ◆KkNV/VOqcw :2011/07/08(金) 18:52:34.46
ソレは「面白い」のではなくて『当たり前』だと思いますが。 猫
182 :
ゆ ◆KkNV/VOqcw :2011/07/08(金) 18:55:38.33
なるほど。
難しい問題には少なくとも次の三つのケースがあります。 何とかスルべき事:2ちゃんの数学板に湧く馬鹿を全部撲滅 どうでもエエ事:数学科の学生や院生が限りなくダサい事 どうにもならない事:数学科の学生や院生が全然モテない事 例えばこういう話ですね。 猫
184 :
132人目の素数さん :2011/07/08(金) 19:19:21.00
>>178 そりゃゲーデルの論文以上に短くなるとは思わんけれど、少なくとも何万行もある証明にはならんでしょ
185 :
超越論的数学天使 ◆xKQl9rTMwao4 :2011/07/08(金) 20:17:40.35
形式的証明のモジュール化などはできない。 形式的証明は基本的にはLKとかHKとかの証明図を書いていくという原理だから。 これが実際はロビンソン系とかで行われる。 C言語とかの数学関数のモジュールとかとは無関係の議論。
モジュール化の定義によると思うが
187 :
ゆ ◆KkNV/VOqcw :2011/07/08(金) 22:02:20.51
うん。
>>104 遅レスだが、チューリングマシンって方眼用紙の上で平面幾何学を検証してるような感じだよね。
>>174 もうちょっと早めに重版すれば良かったのに。
十年前と違って今だと、数あるロジックの本の一つ、という感じだと思う。
モジュール化ってのは、定理1.14.3より〜〜とか、 そういう風な省略をきちんと形式的にやる仕組みを作るってことでしょ。 www.shayashi.jp/HistoryOfFOM/Books/books.htmlの >ゲーデルの論文では、定義とは、省略記号なのだということで通してあります。 しかし、さすがゲーデルというか、そういう定義を完全に展開してしまうと 扱っている論理式が非常に大きくなるだろうとか、Principia Mathematica のよう、 定義のメカニズムが入っていれば、短くなるが、などの証明工学的な話もちゃんと議論しています。 みたいな話だと思う。LKとかにはそういうシステムは無い。 まあせいぜい定数倍程度の話なので、一万行くらいにはなっても、 これが一兆行とかになることは無いと思うよ
ちょっとすみません、話をぶった切ってしまいますが…… 写像と関係の違いについて、クドいぐらいに説明している本とかってありますか? あるいはどの分野を調べれば良いか教えて頂けると助かります。 Prologを知って興味が出て来たんですけど、何を調べればいいか判らなくて。
194 :
超越論的数学天使 ◆xKQl9rTMwao4 :2011/07/10(日) 07:28:34.62
>>192 写像は関数。
関係は述語。
両者は述語論理。
まずは新井の数学基礎論をはじめなさい。
>194 サンクスです。述語論理から当ってみます。
マジレスすると 齋藤正彦「数学の基礎」とかの方が良いと思います 数学基礎論の難しいことは一切必要無い
197 :
超越論的数学天使 ◆xKQl9rTMwao4 :2011/07/10(日) 18:37:45.95
プログラミングの事は詳しくないけど Prologって基本的には1階論理の命題の真偽の再帰的な 演繹をプログラムと捉えている(いわゆる導出)と読んだことがある。 論理プログラミングって本がコロナ社から出てるけど、 その前に新井の数学基礎論で論理の練習をした方が良い。 もちろんそのさらに前に斎藤の数学の基礎の位相以外を知っておいた方が良い。
198 :
超越論的数学天使 ◆xKQl9rTMwao4 :2011/07/10(日) 18:45:29.41
嘘吐きました。 コロナ社の数理論理学って本に 論理プログラミングの章があるってことでした。 関数・述語は集合論からも計算機からもアプローチした方が理解が深まります。 また関数と述語の関係として、 関数除去定理というものがあることが、 上江州の述語論理入門に掲載されています。
「数学基礎論」には位相空間もちょくちょく出て来るから 位相の知識もあった方が良いよ あと初学者に「数学基礎論」で論理の練習をしようとか言うのはちょっと無理過ぎる Shoenfieldよりちょっと難しいくらいだと思っといた方が良い
ホーン節、ロビンソンの導出原理を扱っていればPrologまで到達できる。 小野寛晰「情報科学における論理」 萩谷昌己,西崎真也「論理と計算のしくみ」 あたりが良書かと。どっちもそれなりに手強いけども。
紹介ありがとうございます。 まずは「数学の基礎」あたりを探してきます。 「数学基礎論」はなぜか手許にあるので、そのあとにでも読んでみます。 「論理と計算のしくみ」も一階述語論理とλ計算のところを摘み読みしただけなので、 ヒマを見て通しで読んでみることにします。 本棚を見ると論理系の本がかなり積んであります……一度整理しようかな
数学者の権威にすがるあたりはかわいい
>>201 持ってるのなら一章の内容くらい理解しろよw
理解できてないならつまみ読みしても意味ねえよ。
あの本だと関数は(二項)関係の特殊な例だって、 初学者はちょっとわかりづらいかもね。
ある数学者の教科書には「こういうことは哲学的問題になってしまいます。哲学は嫌いなのでこれ以上追究しません」 他の数学者の本には「適当の専門家がいないから、しょうがなく哲学者に聞いたところ、いい答えは返ってこなかった」 とある
最近自称釣り師がダイレクトで自分の本音を攻撃されて「釣れた!」とか 言ってるの多いよね。 って感じ。 間違いを認めないにしても大人の対応するなら大したことにはならんのに >実は、昨日の数学パラドックスを寓話化するのに、数学者と10時間以上の議論を重ねて、 >どのようなパラドックスにし、どのような哲学を語るかを準備した。 とか >いやはや、数学者の方々に感謝感謝!! とか間違いを論われて火病ってから「種明かし」とか言うから底の浅さが知れる。
ていうか校長先生のつまらない話みたいだな。 単に、練れてない。
>>209 最近は自分自身をエサにするイタい釣り師が多いよねw
>>211 ❶東大
❷R
❸BHG
❹ラミ
❺バーチャ
❻センター
❼JEL
❶東大 ❷R ❸BHG ❹ラミ ❺バーチャ ❻センター ❼JEL
214 :
132人目の素数さん :2011/07/17(日) 18:40:07.21
ドメインを「実数すべての集合」とするとき、次の命題の真偽値を判定せよ。 (∀x)(∃y)(x+y=0) だれか教えてくれ。 俺の頭では全然わからん。
>214 宿題スレにでも投げろや。 「証明しろ」とは言っていないから、まずはx+y=0が実数すべての集合でどうなるか想像したら?
>>214 何が分からないのかまったく説明していませんが、
ドメイン(問題領域)や∀(全称記号)や∃(存在記号)の意味を教えてという事でしょうか?
ドメインを「実数すべての集合」とする : xやyなどの自由変数は実数である
∀x : 全てのxについて
∃y : yが存在する
x+y=0 : xとyを足すと0
つまり、次の命題が正しいか間違っているか判定しろという事です。
ドメインを「実数すべての集合」とするとき、(∀x)(∃y)(x+y=0) :
全ての実数xについて、実数xと実数yを足すと0となる実数yが存在する
❶東大 ❷R ❸BHG ❹ラミ ❺バーチャ ❻センター
>>189 ここまで(in)completenessに焦点絞った本は今でも珍しいよ。
220 :
132人目の素数さん :2011/07/25(月) 21:27:57.94
すいませんが 集合論で1論理式の具体例を教えてください。
断る
0論理式 は1論理式である。0論理式をもとに、帰納的に定義される ものが1論理式となる(証明は本を勉強すること)。 例は、自然数(順序数)の足し算を a+b=c とした3変数論理式。
223 :
132人目の素数さん :2011/07/28(木) 00:03:40.90
この最初の方で出た話題と同じことがもっとしょぼいことかもしれないが、 述語論理の言語を定義した後に、論理式は一意的に読めるという 基本的な定理の証明にも数学的帰納法を使ってるが、数学的帰納法 自体はどうやって正当化されるの?循環してるように見えてしまうけど。 というかここでの証明で使ってよい言葉とか論理ってのは何? 日常の言葉と論理にしか思えないけど。というか言語の定義の 段階で「任意」や「ならば」という言葉が使われてる。 いかに形式化をしてもそれをするための言葉や論理が前提されてる と考えていいの?
いや論理式としての数学的帰納法の公理の方はただの 記号の有限列の変形規則に過ぎないので循環してないよ 妥当かどうか分からなかった帰納法を正当化したいという訳じゃないので まあ別に循環してても良いんだけど。
特に断りなく「数学的帰納法」って言うと、 自然数など、対象となるドメイン上の帰納法のこと。 論理式の定義に使ってるのは帰納的定義だよ。 構造は似てる(帰納構造)けど全然別のもの。 帰納的定義を認めないということだと、 自然数の式、例えば1 + 2 * 3なんかも、 いちいち列挙するなどしないと、自然数の式として認められないことになる。 それこそ真の数学だと思う人はそういうのを追求してみればいいんじゃない? ほとんど全ての人はそう思わないし、豊かな数学を展開できないと思えるから 帰納的定義を認めているわけだけど。 公理論的かつ形式的な証明論は、 自然数の公理に従った自然数論と一緒で、数学の一種なんです。 ルールに基づいて記号的操作で行う数学的対象と構造の研究です。
>>223 公理主義をよく理解できてないからそういう疑問が出るんだと思う。
∃、∀の意味は公理によって定められている。
意味論上、公理と推論規則以外のものは、全く必要ない。
モデル論をちゃんと勉強すれば、その種の疑問は∀解決する。
というかもっとストイックに、 「成り立ってないかもしれない」とか考えてるんじゃないの?
数学ガールで言う所の知らないふりゲームか。。。
知らんがなw
230 :
132人目の素数さん :2011/07/28(木) 22:44:02.05
1階論理の論理式の定義などに使われる帰納的定義も 1階論理をメタ理論に埋め込むことで証明体系として形式化できる。 例:Pは定義する論理式、QはPと素な論理式、 tは項、nは任意自然数とした推論規則 P(t1) P(t2) ...P(tn) Q(u) ____________________________ P(t') あと数学的帰納法はACを仮定すれば、 定理として得られる超限帰納法を自然数に適用して証明できる。 逆数学では帰納法のない体系がたくさん登場する。
231 :
132人目の素数さん :2011/07/29(金) 00:31:47.28
>>224 なるほど。公理として認めておくし、有限回の操作の規則か。
>>226 俺が言いたいのは公理を定めるための言葉はどうなってるのってこと。
言語だとか推論規則を記述している言葉って何なのっていう。「任意の」とか
「ならば」とかっていう言葉を使って書かれてるでしょ。公理系を定めようとしてもその
公理系自身を書くための言葉と理解するための論理って何のかなと。
具体的には、推論規則に則って「正しく」式を導出するための論理というか。
232 :
132人目の素数さん :2011/07/29(金) 00:44:07.52
>>226 念のため追加しておくと、"∀"を「任意」と解釈
したわけではない。「任意の式A,Bについて、A∧Bは論理式である」
とかっていう言語の定義における「任意の」という文字列、
その意味を問題にしてます。
自然言語
234 :
132人目の素数さん :2011/07/29(金) 01:25:53.17
2次平面において、関数pを原点からの距離で定義する。p(x,y)=√x^2+y^2。 pの勾配▽pが、原点からの距離に関係なく原点から外向きに向いた方向に向いていることを示せ。 おねがいします(><)
>>234 どのへんが基礎論的に意義のある内容なのですか?
236 :
132人目の素数さん :2011/07/29(金) 01:42:52.00
どこに質問すればいいか分からなかったのでちょっとぽいとおもって質問してしまいました。 関係のない質問をしてしまってすいませんでした。
夏ちゃん出現
>>231 それは普段我々が使ってる日常言語とか論理とか形式化されていない自然数論
(そこでは数学的帰納法が正しい推論の法則として認められている)
とかでいいんじゃないの?
上でも誰かが言ってたけど、形式化って
「論理というものがまったく存在しないところに、ゼロから論理のしくみやはたらきを発生させる」
ためのものではないでしょ
239 :
132人目の素数さん :2011/07/29(金) 07:03:14.70
いずれにしろペアノの公準だけでも 数学的帰納法は証明可能。 超限帰納法は整礎的順序から証明できる。 メタ理論の超限帰納法によって再帰的定義が正当化される。 ただしメタ理論は少なくとも2階論理でなければならばい。
>>235 「数学」の「基礎」的な問題だから「数学」「基礎」論スレが妥当だということだろ。
こうやって我々は自然言語を交えて基礎論について議論している その自然言語を使った議論の妥当性は何によって正当化されるのか 自然言語による議論も全て形式化できるのか
242 :
132人目の素数さん :2011/07/29(金) 08:00:20.85
できるってw 自然言語は略記。
243 :
132人目の素数さん :2011/07/29(金) 08:05:44.91
上江洲の述語論理に 自然言語→証明体系(NJ)の 仮定が詳述されてる。
知らない振りゲームってのは結構難しくて 偉い学者でも、直観的に明らかだから、当然 公理系から証明できる事だろうと思ってたら 実は証明できなかったりとかね
>>241 > 自然言語による議論も全て形式化できるのか
出来る。
HOLやCoqのサイトでも見て、形式的証明を読んでみれば?
ただHOLやCoqを理解するには、証明論や計算論の基本的な知識は必要だよ。
ちょっと勉強してからじゃないと歯が立たないと思う。
>>243 一章で証明図やって、
また途中で証明図の書き換えについて詳しくやってるよね。
計算論の人はλ式の昔からこういうことも詳しくやるんだけども。
β変換が計算に本質的な役割をするので。
上江洲の述語論理入門は数理論理学初めの1冊としてはかなりの良書。 なぜか話題に上らないが・・・。
ただし 自然言語による議論を全て形式化できる ≠ 自然言語をなくせる だけどな
>>248 そういう観点だと現代数理論理学序説もいいね。
コンビネータベースだから書き換えもシンプルだし。
>>238 そうか。気が楽になったw
このスレの最初のほうに書いてあるけど述語論理の定義には
ZFCが使われてるわけ?確かにアルファベットが可算無限個
あるっていう言語の定義があるよね。集合の言語を定義する前なのに。
それに、証明論の発想ですごいと思ったのは意味と構文を分けて、
言語ってのは目の間にある単なる文字列、物体みたいなものと
認識する考え方なのにそれが無限個あるっていうのは分からない。
目の前に転がってる文字とそれを使った有限回の操作っていうので
客観性を担保したと思ったら無限個を持ち出されたら一貫性がないというか。
俺一人が質問の嵐wで申し訳ない。質問できる人いないんだよね。
>>252 その一番最初の残ってしまうところは、形式化してもしようがない部分です。
「目の間にある単なる文字列」がどういう性質を持っているかは、「検証」すべきことだと思ってるんですか?
254 :
238 :2011/07/30(土) 08:35:56.30
>>252 俺も独学で勉強してる最中なんで、あんまりしゃべるとすぐにボロが出るけど
述語論理の定義にはZFCは使われてないと思ってた.
>アルファベットが可算無限個あるっていう言語の定義
そこにZFCを持ち出さないといけないとすると
集合論の公理系だって、言語の自由変数や束縛変数の記号が
可算無限個あるという定義だから
「ZFCの定義にはZFCが必要だ」ということになってしまうんじゃ・・・
255 :
238 :2011/07/30(土) 08:48:50.44
というかこの学問は根本的に独学に向いてないような気がする
初心者ですが、 述語論理の定義における「集合」は 公理的集合論における「集合」という意味じゃなくて 単なる「記号の集まり」という意味じゃないの? 「集まり」って何か、とか言い出すと じゃあそもそも「記号」って何か、 とかそういうのと同じレベルの話になってしまうかと。 「可算無限個」というのも集合論での定義とは無関係で、 単に「記号はいくらでも沢山作ることが出来る」 ということを表してるだけなんじゃ。
記号列の連結とかパターンマッチングとかのちょっとした記号操作するときに 置換公理とか冪集合の公理とか選択公理とか使ってない気がするんだけど。 さすがに文字列に関する性質を何も使ってないとは言わないけど ZFCほど超越的なものは使ってないと思う。自然数論の範囲内に収まるはず。 あと可算個の変数記号 v1, v2, v3, v4, v5, ........ は v', v'', v''', v'''', v''''' という風に v と ' の二記号だけで表現することもできる (スマリヤンの不完全性定理の本はこの方式を採用している)。 実際に計算機に実装するような場合、当然こういうやり方になる。 変数記号が有限個か可算無限個かという違いは大した違いじゃない。
記号列とその集合、素朴な自然数概念。 これらが誰にとっても同じモノを意味しているかというと、そんな保証はどこにもないよね。
259 :
132人目の素数さん :2011/07/30(土) 10:35:35.30
集合論の外側の論理学と集合論上での論理学が混同されている。 集合論の外側の1階論理の言語は元々紙の上に書かれた記号列として 論理式が定義されたり証明されたりする。 つまり集合論の外側で暗黙の了解で作られた論理。 集合論上の論理学は集合論の内部のオブジェクトへ対応する 述語として定義される。 AxiomとかBewとかProvみたいな述語もこれ。 (ただしこれに似た述語を扱いはじめたGedelの不完全性定理は、 単純な記号列を算術上に展開する方法を提供しているが、 証明過程では直接モデルの側は扱っていない。 彼は真偽値ではなく計算可能性など計算論的視点で証明してた。) 数学(ZFC)を記述する集合論Aは集合論A'上で展開可能で、 2つの集合論A,Bでの相対的無矛盾性などの証明が可能。 この議論の形式化の土台となる集合論A'がどういったものかは あまり本などで説明されないのだが、 累積的階層や順序数全体の集まりを記述するため Properクラスを記述可能なBGC(ZFCと無矛盾等価)などで なければならないと言われている。 ただし1階論理では記述不可能な数学的な命題も 存在すると言われている。(江田の数理論理学など参照) その場合2階以上の論理学は1階論理の中で形式化可能。 最近では集合論上の1階論理を自然に拡張した Ω-論理という従来より強い論理学が考案された。 The Continuum. Hypothesis, Part I, Part II, W. Hugh Woodin
260 :
132人目の素数さん :2011/07/30(土) 10:51:36.58
>>257 もちろん。
計算機で扱える数学は体系RCA0(弱い再帰的内包公理)で十分と言われる。
1自然数の公理
2弱い数学的帰納法
3弱い内包公理
の3つだけ。自然数とその集合だけ扱えれば問題ない。
>>260 記号列とその集合がその3つを満たすことを検証すればいいんですね?
>>260 > 計算機で扱える数学は体系RCA0
計算機が通常操作している数体系は、
要は計算機の仕組みは、
RCA0に一番似てるってだけだよ。
形式化されたものは何でも扱える。
変数単体で記号列になっていると考える必要はない。 x1とか書いたりするのは、人間の可読性のために過ぎない。 印字表現が何であるかは体系に影響を与えない。
>>259 暗黙というのは未定義の言葉や論理に頼らざるを得ないということですか?
>>260 記号の個数や集まりなどの素朴な数や集合概念と呼ぶような
ものはさすがに前提されるのですか?
まあいかに弱い公理系を設定しようとしてもそれを 書くための言語は自然言語でしかないからね。 赤ちゃんに公理系を見せても理解できないでしょw 文字が読み書きできて、「正しい」「正しくない」っていう 判断がつかないと何もできん
266 :
132人目の素数さん :2011/07/30(土) 13:26:16.92
>>264 > 暗黙というのは未定義の言葉や論理に頼らざるを得ないということですか?
最終的な議論の場はそう。
議論の場を改めて考え直そうというのが数理論理のはじまりと考えた方が良い。
無から数学をつくるという考えは不完全性定理などによって初期のころに終わった。
> 記号の個数や集まりなどの素朴な数や集合概念と呼ぶような
> ものはさすがに前提されるのですか?
RCA0のような2階算術は集合変数といくつかの公理の追加によって、
1階述語論理上で普通の集合論とは違う視点で記号列を解釈する「言語」。
(2階述語論理とは別の視点。)
よって記号列およびモデルの扱いは通常の1階論理にほぼ準拠する。
集合論と違って集合内部の細かい性質を無視して直接数学を扱う。
だから集合概念は前提としているいないというより、
集合の詳しい構造がZFCほど明らかにならない。
有限主義的なメタ数学の議論は 二階算術までいかなくてもPRAで大丈夫だと思うけど
268 :
132人目の素数さん :2011/07/30(土) 23:11:01.95
____iPNF ____↓ PA_→_PRA_→_iPRA_→_iΣ1^(+) ____↓ ____RCA_→_RCA0
ACA0がPAの保存拡大でε0なのか なるほど
恐らく間違っているのだろう....
271 :
132人目の素数さん :2011/07/31(日) 00:44:27.14
PRAはRCA+Σ1^0+IAの保存的拡大。 よってPRAのがRCA0より大きい。 またACA上ではPRAやPAは一般的に2階算術の拡大になる。
272 :
132人目の素数さん :2011/07/31(日) 06:46:46.14
別に祭り上げてないでしょ 環論の研究者を可換派と非可換派に分けるようなもので、 どっちが勝った負けたなんてのは意味が無いと思う
基地外は基礎の公理の否定を好む。
哲学屋は数学には複数の世界があることを受け入れられないからな
>>275 ただその複数の世界を設定するための言語は
根源的には自然言語ただひとつ。無からは生み出せない。
それに哲学者でもクリプキ、タルスキ、マーティンなど
数理論理に強い人もいる。数学者は数学者で疑いようのない
客観的真理などないのにあると思ってるトンデモが沢山いる。
>276 矛盾を内包する言語だったら何でもいいんじゃないの?
278 :
132人目の素数さん :2011/07/31(日) 17:12:22.47
「疑いのない客観的真理などない」の中身も時代とともに変わるからねえ
279 :
132人目の素数さん :2011/07/31(日) 17:27:13.56
>>276 >ただその複数の世界を設定するための言語は
根源的には自然言語ただひとつ。無からは生み出せない。
と
>数学者は数学者で疑いようのない
客観的真理などないのにあると思ってるトンデモが沢山いる。
この2つが頭の中で両立しているのか。都合のいい頭だ。
ばかちんでんがな
281 :
132人目の素数さん :2011/07/31(日) 19:11:48.80
哲学板にも論理学スレあるよ。
哲版からなんで出張ってくるの?
布教のためです
284 :
272 :2011/07/31(日) 19:51:57.69
>> 273 でも↓なんかを見ると、AFA派とFA派が論争していたのは事実でしょ? www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090616 渕野先生の文章を見ても、AFAに対するFAの主導権を主張しているし 可換環と非可換環の話とは違うと思う。 可換環論の研究者が非可換環に対して主導権主張したり、 その逆とかないでしょ? 前AFAスレの14氏が言うように 渕野先生も「集合論は集合に関する客観的な事実の探求である、という考え方を 完全に捨ててるわけじゃない」んじゃない?
285 :
132人目の素数さん :2011/07/31(日) 22:30:26.04
fuck! リンク先の議論の流れを良く考えよ。
上の方にあった基本的な質問に ZFCがどうのこうのって答えてる人いるけど、 命題論理の基礎レベルの質問だから、 素朴集合論で充分でしょ。
287 :
132人目の素数さん :2011/08/01(月) 07:46:50.39
あげ
RCA0がPRAよりも一階部分に関して弱いのは良いとしても、 ヒルベルト計画的な文脈で多重量化を許した二階算術を持ち出すと、 存在論的に多くのものを仮定し過ぎている(具体的には自然数の集合)とか言われてしまう気がする 純粋数学的にはどうでもいいことだけど
ヒルベルト計画的には、 算術の無矛盾性はあっさり示せる予定(示せたつもり)で、 さらに相対的に実数論の無矛盾性も示すってことだから、 いいんじゃないの?
290 :
272 :2011/08/02(火) 07:04:45.93
>285 リンク先って「ヒビルテ」のことだと思うけど、 ここの議論を見ても FA 派は、なんだかんだ言いつつも 「FA を認めるほうが自然」と言いたげだし (というかはっきり言ってる人もいる)、 渕野先生はそこに参加してなけど FA の主導権を主張している。 逆に、ここの議論に出てくる AFA 派は、数学として 「可換環」と「非可換環」のようなものだと AFA を擁護しているけど、 それも AFA が祀り上げてた「某佐藤さん」の「正しい」発言で。 人を貶すような発言じゃなく、きちんとした説明を頂きたい。
>可換環論の研究者が非可換環に対して主導権主張したり、 >その逆とかないでしょ? それに似たことをやってるのが272と、もしかしたら渕野先生なんで 批判自体がお門違いだと思う。284のリンク先見ても皆そう言ってるだろ。 まあ先生は〜〜派に分けたり、〜〜派の圧勝とかそんな低次元なこと言ったりしてないけど。 Vを累積的階層として見たい場合(集合論自身の研究)の場合には FAを仮定するのが当然だし、実際そうされている。 それは常識レベルの話で、誰もその点について議論はしてない。 272のリンク先では、渕野先生が集合論は数学の基礎だという観点から FAを認めるべきだと主張したのに対して、 「数学の基礎としての理論」にはFAも外延性公理も要らず、 できるだけ弱い理論を採用すべきだと言っている。 それを無視して、要はFAは正しいんでしょ?なんて言うのは何も議論を理解してない。
292 :
132人目の素数さん :2011/08/02(火) 09:41:52.88
「某佐藤さん」って誰なの?
293 :
132人目の素数さん :2011/08/02(火) 09:46:50.87
弱くすれば安全に見えて実はそうでは無かった、という例もあるからね。 ゲーデル解釈みたいに。
まあブラウアーに言わせれば 彼は単純に論理的に弱い理論を目指したという訳でもないから 無矛盾等価だと言われても、だからどうしたという感じかもしれない 直観主義数学は人によって公理の取り方が違うから困る
集合論の人が何らかの高利や仮説が「ただしい」と言った場合、
それ自体が、仮定として自然で(人為的でなくて)出てくる理論が直観に反しない
という意味である場合と
それとは別の、数学としての蓋然性の高い仮定から自然に出てくる
という意味である場合とがある
という程度のことでしかないと思うよ、
>>290 の勘違いレベルって。
まあ、
>>290 はさらに明後日の斜め上へ逸れようとしているが。
>>294 今現在ブラウアーの立場を取る人なんているの?
> 直観主義数学は人によって公理の取り方が違うから困る
いつの頃の竹内さんのセリフだよ。
ブラウアーは「公理を弱くしてみたらどうなるか考えてみよう」じゃなく、
「俺の数学的直感ではこの公理は正しくない」と言っている人だったのに、
現在の公理の強弱という観点からも、鋭い指摘を行っていたのが驚き。
>>295 基礎について大きな動きをもたらす数学者は、
俺の証明にはこの公理が必要ってケースが多かった、昔は。
基礎論、論理学、集合論以外にある専門分野での知識に基づいて。
297 :
272 :2011/08/02(火) 18:41:22.77
FAが正しいか正しくないかのどちらかしかない。 それが数学という活動だし、 決定できないのならばそれは人工的構築物にすぎないでしょうね。 僕はこの点で基礎論に眉唾を感じる。 まぶブラウアーとかの考えは受け入れやすいだろうな。
じゃあ平面幾何学に出て来る平行線の公理は正しいの?間違ってるの?
299 :
272 :2011/08/02(火) 18:52:05.87
それとこれとは無関係やろ おま、ユークリッド公準なめと? 非ユークリッドいうとんのは洒落てるゆーから こしらえた与太なん FA基礎論こえ数学全体包んドンで
平行線の公理は最初から必要とされてた公理なのに 整礎性公理はフォン・ノイマンが「技術的理由で」付け加えた公理が いつの間にか集合と言う概念を根本的に規定する基礎的な公理である、 みたいな顔をして居直っているからなお悪い。 キューネンに書いてあるようなことが本当のところ。
>>297 >FAが正しいか正しくないかのどちらかしかない。
超ダウト
誰にとっても同じモノを意味するただひとつの数学の世界 〃∩ ∧_∧ ⊂⌒( ・ω・) `ヽ_っ⌒/⌒c ⌒ ⌒
303 :
272 :2011/08/02(火) 22:40:41.80
私はいくつか前のスレにあった バベルの図書館的宇宙というものに注目しています。 つまり無機質な情報の海から人間が恣意的に自らのニューロンに合わせて 解釈を与えるという考えですね。
注目するだけならタダだ、いくらでも注目するがいいさ。
人間はひとりじゃない
> 291 匿名掲示板でもなければ「そんな低次元なこと」は言わないでしょ。 しかし内心思っているかどうかは別だ。 もっとも、旧帝国大学の博士論文の話とか暗殺のファトワがどうとか、 常識が通用しない人ではあるが。
暗殺の話は知らんが 旧帝大の博士論文の話はたぶん、相手側の論文の 水準が低過ぎただけだと思う
308 :
132人目の素数さん :2011/08/04(木) 16:41:38.40
水準が低過ぎたら、あんなこと書いても非常識ではない、と?
久しぶりに渕野先生の AFA の文章見てみたら、最近更新してたのね。 だからここで AFA vs FA の話が盛り上がっているのか。 AFA は、集合論の最先端の話についていけなくなった人がやってる、 ってその分野への差別意識丸出しのこと書いてるね。 確かに普通の人なら、匿名掲示板でもなければ書かないわなー。 逆に、(AFAの提唱者の)Aczel とか、 (あの文章でもAFAの論文が引用されてた)Rathjen の AFA に関する最先端の話を渕野先生は理解しているのかな? よく分からないけど、渕野先生って Aczel とか Rathjen とかより格上なの?
「AFA は、集合論の最先端の話についていけなくなった人がやってる」 とは言ってないでしょ。 たぶんあの文章でdisってる相手は日本人だと思う。
311 :
132人目の素数さん :2011/08/04(木) 19:07:22.56
2種類の異なる空間の間の数学を記述をするとき、 (例えばベクトル空間と非ベクトル空間) 述語論理を拡張したmany sorted logicを使って それぞれ別にstructureを定義すると聞きました。 (例えばstructureがそれぞれ1変数述語で P(x)がベクトル空間上の超平面x、Q(y)が非ベクトル空間の点yとしたとき、 すべてのベクトル空間の超平面に対して非ベクトル空間の点が対応するを ∀x(P(x)→...) のように記述するらしいのですが...。) ZFCで何か推移的なモデルがあれば全数学が展開できるので、 この中で2種類の空間の間の数学も記述可能であるように私には思えます。 通常の1階論理で表現不能でMSLだと表現可能な数学なんてあるんでしょうか?
312 :
132人目の素数さん :2011/08/04(木) 19:29:56.15
山姥チャンネルはやばかったらしい。
ないよ many sorted logicは、それぞれのsortごとに 述語P_i(x)を入れれば普通の述語論理で表現できる あと「非ベクトル空間」なんて用語は無い
314 :
132人目の素数さん :2011/08/04(木) 21:56:12.98
どうも...。ということは例えば普通の述語論理で、 ∀x(xがベクトル空間の点→...) の条件を書く代わりにモデルを分割して それぞれの変数や定数などで書ける部分を決めることで、 xなら既にベクトル空間上の点であることが、 述語論理の時点で決まっているというイメージでしょうか。 2階論理でしか扱えない文がこれで1階論理で書けそうな気もします...。 >P(x)がベクトル空間上の超平面x、Q(y)が非ベクトル空間の点yとしたとき、 >すべてのベクトル空間の超平面に対して非ベクトル空間の点が対応するを >∀x(P(x)→...) のように記述するらしいのですが...。) これは数学的に厳密ではないと思います。 異なった空間の対象を言いたかっただけです。 私の実際耳にした例ではユークリッド空間の「点」と「線」でした。
>>314 意味わかってないのにあんまりいい加減な改変例を出すのはやめたほうがいいよ
射影幾何学の公理をそのように記述することで、 双対性をはっきりと見せるというのはよくある方法なので、 そのたぐいの話を聞いたのでしょうね.
今回の更新で書き加わった部分は、はっきり言って 「〜〜派に分けたり、〜〜派の圧勝とか」よりも低次元だな。 業績と人格は無関係とはいえ。 そもそもその業績もどれほどのものなのか? 「「美しい数学」や「面白い数学」に対する多くの数学者が共有している価値観」 とやらから、AFA は面白くないと主張しているけど、 偉い数学者の発言を引用している訳でもない。 ということは、AFAを面白いと研究している(いた)人々より 自分の方がその「価値観」をよく分かっているということなのだろう。 つまりAczelよりも、Rathjenよりも。 集合論の大家Scottも non-well-founded set を扱っていた(Aczel本参照)。 Barwiseも hyperset という名前まで付けて研究してた。 ScottよりもBarwiseよりも偉いということなのだろう。 自信過剰もここまで行くとむしろ尊敬してしまう。 しかし日本語の文章でだけ攻撃的なのは自信のなさの表れか?
318 :
132人目の素数さん :2011/08/05(金) 02:12:05.63
「面白い数学」に対する多くの数学者が共有している価値観、 によると、集合論はおろか基礎論全体が面白くない数学なわけだが(藁
実際に二階算術の研究は本当のところはmany sortedな一階算術の理論に過ぎない 二階論理との違いは意味論を考えるときに初めて出て来るはず シンタックスはどっちもほぼ同じ 二階のZFCとNBGの違いみたいなもんだと思う
AFA派を攻撃する為に、基礎論全体を吹っ飛ばすような武器を持ち出したってとこか。 渕野先生の問題点はそれだけじゃなくて、基礎の公理の主導権を主張することで 可換環論と非可換環論のように互いに尊重しあえないことを宣伝する形になり 基礎論が数学の一部だと正しく認識してもらえなくなることだよね
主導権を主張してると思い込んでるやつの頭がめでたいだけだな……
>可換環論と非可換環論のように互いに尊重しあえないこと 何言ってんの? 別に可換環論の研究者はLie環の研究者といがみ合ったりとかしてない訳だが 日本の一部の旧帝大の大学人に変な人が居て、 基礎の公理は認められないとかと言っているけど 海外からは相手にされてないってだけでしょ
>別に可換環論の研究者はLie環の研究者といがみ合ったりとかしてない訳だが それが数学として健全な姿だろ。 とこらが件の文章は、AFA派とFA派がいがみ合ってる印象を与えてしまう。 だから正しく数学の一分野として見てくれなくなる、 ってのが320の言いたことだろ。 文脈から否定詞「ない」のスコープ読み取れや。
「可換環論と非可換環論のように」ってのはどこに掛かってると考えてもおかしい
それに、
>>272 ほど露骨に主導権がどうとかどっちの勝利だとか
言ってる人は他には居ないと思う
お前ゆとりか? (可換環論と非可換環論のように互いに尊重しあう)+「ない」 とパースすれば何もおかしくない。 お前の日本語経験値が低いだけだ。
間違った。正しくは (可換環論と非可換環論のように互いに尊重しあえる)+「ない」
>>317 > 自信過剰もここまで行くとむしろ尊敬してしまう。
研究者の場合、一般人よりもずっと割合多くないかね。
まるで自分に拍車入れるかのような言動の人。
ただ、人物で語ると面白くなくなるので、
そこは無視して返して、数学の論に集中した方がいい。
毎回同じような流れになるなこのスレw
拍車は掛けるものじゃなかろうか、入れたら危険だろ。
> 研究者の場合、一般人よりもずっと割合多くないかね。 > まるで自分に拍車入れるかのような言動の人。 禿堂。 誰でも「面白い」「面白くない」って価値観を持っていて 自分で面白いと思うトピックを選ぶ。 自分に自信がある人ならそれで十分だし、 他人の選ぶことに一々文句なんて付けない。 「数学者が共有している価値観」なんて虚構を持ち出すってのが そもそも自信のなさの表れな訳で。
他の数学者の無理解の中で生きていかなきゃいけないロジシャンとして、 「面白い数学」に対する多くの数学者が共有している価値観 なんてのは一番持ち出してはいけないものの筈なのに。 攻撃モードに入ると見境がなくなるんだよな、渕野センセは。
そんなことしたら、あきまん
世間から認知されない少数民族は辛辣なことを言う性質をもつ。
>>324 このスレの流れでAFAとかFAとか初めて知ったけど
件の文章から両方の研究者が互いにいがみあってる印象なんて全然もたなかったよ
被害妄想じゃね?
> 件の文章から両方の研究者が互いにいがみあってる印象なんて全然もたなかったよ 実際、いがみあってなんかない。 AFAを尊重できないFA派が約一名いらっしゃるってだけだろ それでもその一名が著名だったりすると、 基礎論が「正しく数学の一分野として見てくれなくなる」 ってのは至極まっとうな心配だと思う
>>330 掛ける、入れる、加える
全て問題ないです。
座布団一枚!
>尊重できてない そんな風には読み取れなかったよ アマチュア数学者の中には これを数学の新たな基礎においてその上に数学を作り直せば いろんな基礎論的な問題がすっきり解決される これは革命だ!みたいに思ってる人がいるけど それを数学の基礎として選ぶことで失われるさまざなものに対して 得られるものがそんなにあるとは思えない、という主張だと思った 別に反基礎の公理の研究そのものを否定していないでしょ 「これは革命だ!」「今の数学をこれで新たに作り直そう!」な人にツッコミ入れてるだけで 上の方で「より弱い体系を基礎におくべきだから、こっちが正しい」とか書いてる人がいるけど そっちはそっちでまた一つの主張なんだろうね ちなみに俺は前者の方に説得力を感じた
>>335 俺もそう思う
「一名」ってのが
>>272 のことだったら意味分かる
2ch外の元の文章はBarwiseやRathjanにちゃんと敬意を払った文章になっていると思う
284のリンク先をよく嫁 >「これは革命だ!」「今の数学をこれで新たに作り直そう!」な人 そんな奴がどこにいるんだ?ってのがそのリンク先の議論の出発点 > 別に反基礎の公理の研究そのものを否定していないでしょ 「否定する」の意味によるだろうが、 反基礎の公理の研究は(少なくとも現状では)面白くなってはいない、 という主張は読み取れる 単なる藁人形論法なのか、 藁人形論法に偽装して「反基礎の公理の研究そのものを否定」するようなことを書きたいのか 他の文章でもAFAに否定的なことを書いていることからして、 俺は後者ではないかと考える
>>341 の脳みそがおめでたいことになってるってことだけは間違いないとわかった。
343 :
132人目の素数さん :2011/08/05(金) 23:28:43.30
>>271 ACA0はPAの保存的拡大ですよね。
一方でACA0上ではPAがZ2の保存的拡大になるんですよね。
これ不思議なんですがどういうことなんでしょうか...
>>340 >272のことだったら
俺も最初そう思ったw(でも著名ってあったから、たぶんF先生だろうと)
>>284 の
>AFAに対するFAの主導権を主張
がそもそもなんのことかわからなかったというか。
それが「集合論を使えばAFAの集合論のモデルを作れる」のことだとすると
じゃあユークリッド幾何の世界の曲面や球面を使って非ユークリッド幾何の研究したら
それがユークリッド幾何の優位性を示していることになるのかよ、と。
少なくとも「AFAの研究は無意味だ」とか「AFAの研究なんかするな」みたいな主張は
俺にはまったく感じられなかったよ
>>341 ふーん
F先生=272=考えない人で解決ってことで。
332の言うことはもっともだけれど、 このスレが数学板の上の方に並んでいて 他の数学の連中の目に入るところに書くことも 見境ないんじゃないのかと。 328の言うように、もうやめようぜ、こんなつまらん話。 F先生は、確かに色々問題はあるけれども、 (Rathjenたち程じゃないにしても)きちんと業績もあるんだし、 数学者の評価にはそれで十分ジャマイカ。
347 :
132人目の素数さん :2011/08/06(土) 03:15:12.05
>F先生は、確かに色々問題はあるけれども、 数学者は多かれ少なかれ人格に問題がある人が多い。 業績がある=人格的にリッパ、という何の根拠もない 思い込みは捨てたほうがいい。
348 :
132人目の素数さん :2011/08/06(土) 03:18:50.86
ぶっちゃけ 「FAとAFAのどっちが正しいの?」 という問いは 「平行線は一本しかないと二本あると全然ないのどれが正しいの?」 という問いと全く同程度に見当違い。
F先生のヒトトナリを直に知っている身としては 341が言いたいことはよく分かるんだが 346の言う通りこれ以上は言わないことにする
AFAの研究は数学と言うよりも、 ラムダ計算とかオートマトンとか計算量理論とかと 同程度以上に計算機科学よりだと思う
AFA=Anti-Fuchino Axiom
>ACA0上ではPAがZ2の保存的拡大になる 「ACA0上で」の意味が分からんが、 PAの方がZ2より言語が小さいのに保存的「拡大」になぞなるわけがない
353 :
132人目の素数さん :2011/08/06(土) 22:03:13.60
証明論的除去定理のことでしょう。 任意の原始再帰的述語を保存しながら体系を小さくするテクニックです。 これ自体はPRAで形式化されます。 T1をT2に除去するときはT1≦T2とかくので、 (Σ_1)^0-IA≦PRA RCA+WKL+(Σ_1)^0≦PRA Z2≦PA : などの定理を逆の包含関係で捉えたと考えられます。 Z2≦PAのZ2などははじめはACAと考えられていたそうです。
354 :
132人目の素数さん :2011/08/06(土) 22:43:15.81
353補足。
定理を逆の包含関係で捉えたのが、
>>271 の書き込みです。
355 :
132人目の素数さん :2011/08/06(土) 22:46:08.62
>それが「集合論を使えばAFAの集合論のモデルを作れる」のことだとすると >じゃあユークリッド幾何の世界の曲面や球面を使って非ユークリッド幾何の研究したら >それがユークリッド幾何の優位性を示していることになるのかよ、と。 全くその通り! >(基礎の公理を含む)集合論での定理として記述したときの) >述語論理の完全性が,このようなことがいつでもできる, >ということの保証となっている 述語論理の完全性は基礎の公理とは関係なく証明できることだから 反基礎の公理を含む集合論での定理として記述したときの述語論理の完全性が、 基礎の公理を含む集合論のフラグメントのモデルを 反基礎の公理を含む集合論の中で作って、 その中で議論することを保証している。 つまり反基礎の公理を採用しても、 基礎の公理を必須とするような「理論展開」も保たれる。 ってことはどっちを採用しても同じことって訳だ。
全くその通りと答えたことにより、
>>356 の発言の価値の無さが完全に確定した。
> ってことはどっちを採用しても同じことって訳だ。 どっちを採用しても同じ筈なのに 『数学を展開するための基礎としての集合論』には基礎の公理、 とか言っているから主導権を主張していると解釈されるんだろ 反基礎の公理が必要(または有効)な「理論展開」には フラグメントのモデルを中に作るっていう面倒な方法で我慢しろと言っておいて、 基礎の公理が必要(または有効)な理論展開(超限帰納法とか)については 「well-founded part に制限したときに成り立つ結果と読みかえる」 のは「大きな犠牲」というのは、手前味噌過ぎないだろうか? 後者の方が前者よりも守るに値する、ということなのだろうけど、 どちらも『数学を展開するための基礎としての集合論』というときの 「数学」には含まれず、その意味の「数学」にはどっちでもいいことだ 自分の専門分野を贔屓しているといわれても仕方あるまい あんまり言うと346に怒られそうだな
たとえば自然数論や実数論の「展開」で重要な加法の可換性 ∀x,y ( x+y = y+x ) は集合論を採用すると「ωに制限したときに成り立つ結果と読みかえる」必要があるけど、 それが「大きな犠牲」なんだろうか?当たり前だろ、という気がする。 (もちろん、この場合にはその犠牲の「代償」はありがたいものですが。) 整礎部分に制限しないといけないことを「大きな犠牲」というのが分からない。
>T1をT2に除去する 除去は他動詞だろ! 何かをかにかに除去するって日本語になってない
第四文型なんじゃね SVO_1O_2
wikiったって**あの**wikipediaだろ、それも日本語の。苦笑しか起きないわww
そんじゃ苦笑しながらこの証明のどこがおかしいのか説明してよ。
選択公理なら弱めたものも研究するのが集合論で普通なら、 どうして基礎の公理は弱めたものを集合論でも研究してはだめなの? 部外者としてはそう思う。 「普通の数学」の対象を整理したらtoposができたように、 自然にAFA集合論が奥にひかえてるような「普通の数学」の対象は出現ないのかな。
基礎の公理を含めた集合論だけ考えることの妥当性(F先生による):
(1)ユニヴァースの整礎部分が基礎の公理を含む集合論の公理系を満たすものになること
(2)集合論の枠組の中で通常の数学を展開するのに必要となる集合はすべて整礎部分に入ること
(3)基礎の公理の性質を満たさない集合の存在を保証する公理を集合論の他の公理に付け加えても
整礎部分の集合に何ら新しい結論が得られないこと
http://math.cs.kitami-it.ac.jp/~fuchino/tmp/kikaku03.pdf より(一部改変)
これをパクると
V=L公理を含めた集合論だけ考えることの妥当性:
(1)ユニヴァースの構成可能部分Lが V=L公理を含む集合論の公理系を満たすものになること
(2)集合論の枠組の中で通常の数学を展開するのに必要となる集合はすべて構成可能部分Lで作れること
(3)V=L公理の性質を満たさない集合の存在を保証する公理(V≠L)を集合論の他の公理に付け加えても
構成可能部分の集合に何ら新しい結論が得られないこと
結論:V=L公理を弱めたものは集合論では研究してはいけない
367 :
132人目の素数さん :2011/08/07(日) 07:23:26.81
>>360 その件については全面的に謝罪します。
reductionが本来の英語でしたので、
これは還元や縮小などと訳されるべきでした。
しかしこう考えてはどうでしょうか?
初訳には様々な誤解による誤訳が付き物だが、
それは時間とともに良い形で浸透すると...。
368 :
132人目の素数さん :2011/08/07(日) 08:33:50.88
>>365 AFA集合論は研究されてるよ。
hyperset theoryとか呼ばれてる。
x={x}(xがアトム)みたいなのもできる。
AFAでの圏論とかもある。
369 :
132人目の素数さん :2011/08/07(日) 08:59:31.62
370 :
132人目の素数さん :2011/08/07(日) 10:57:21.08
>>344 >ユークリッド幾何の世界の曲面や球面を使って
>非ユークリッド幾何の研究したら
>それがユークリッド幾何の優位性を示している
>ことになるのかよ
よく、双曲幾何における双曲平面のモデルを
線形空間内の二葉双曲面にとることを
「ユークリッド幾何の中で
双曲幾何のモデルをとっている」
と理解する人がいるが、正しくない。
なぜなら、二葉双曲面を不変とする線形変換は
ユークリッド幾何における合同変換ではないから。
逆に双曲空間内でのホロ球面を
ユークリッド幾何におけるユークリッド平面の
モデルとするのは
「双曲幾何の中で
ユークリッド幾何のモデルをとっている」
といってよい。
もっともこのことから
「双曲幾何はユークリッド幾何よりも本質的だ」
というほど御目出度い頭を、私は有していない
本質的というんだったら、空間の曲率を変数化した幾何学を考えた方が良いんじゃないかね。 AFAてそういうところを目指しているんじゃないの?良く判らんけど。
その「証明論的還元」の定義を教えて。 あとZ2ってのは何なの?
>>366 傑作だ。しかしそのネタ、どこか既視感があるんだが...
374 :
132人目の素数さん :2011/08/07(日) 18:53:15.47
375 :
132人目の素数さん :2011/08/07(日) 18:55:26.51
>>332 ,
>>334 クラスのいじめられっ子ほど、もっと弱い(と勝手に思っている)者に対して
クラスの共通認識を振りかざす
弱い者はより弱い(と思ってる)者をいじめる、という構図
振りかざす「クラスの共通認識」もそいつの妄想
366のリンク先のF先生の文章、数学的におかしいと思うんだけど。 「∈関係を x \cup \mathcal{P}(x) \cup \mathcal{P}(\mathcal{P}(x)) \cup ... に制限したものが well-founded になる」ような x の全体がFAを含むZFCのモデルになるってあるけど、 それって推移的クラスにならないよね? y=\{ y \} となるアトム y をとってきて x = \{ y,\emptyset \} とすると この x は上の条件を満たすけれど要素の y は満たさない。 推移的モデルじゃないものを考えているのかな? 普通の well-founded part を作るには \mathcal{P} の代わりに \bigcup じゃないといけないと思うのだけど \mathcal{P} でも正しいのかな?誰か詳しい人教えて。
>>362 超限帰納法は基礎の公理とは無関係
F先生の単なる勘違い
>>365 AFAは基礎の公理を弱めたものではない
基礎の公理に「矛盾する」ものだ
>>375 Z_2 ≦ PA が ACA でいえるのなら Z_2 でもいえる
よって Z_2 |- Cons(PA)→Cons(Z_2) である
とこらが Z_2 |- Cons(PA) だから Z_2 |- Cons(Z_2)
不完全性定理の誤りを証明w
>>362 そこの記事では整列順序、より一般的に整礎的関係について
超限帰納法が証明されている。
∈が整礎的だというのが基礎の公理(整礎性公理ともいう)。
だからこの公理が無いと「基礎の公理が成り立つ部分については」という枕詞が
集合論の大部分の命題に必要になるのだが、それは嫌だというのが元の文章。
だから別にja.wikipedia.orgの記事の質が良い訳じゃないが
この件に関しては>362>363のほうが誤り
382 :
132人目の素数さん :2011/08/08(月) 00:02:44.15
ていうか、ZFから基礎の公理を除去したもので、 基礎の公理と、集合の∈について帰納法の公理の同等性が証明できるでしょう。
>>379 R⊆A×AがA上well-foundedというのは、 X = A だけでなくて
「任意のX⊆Aに対して」 X≠Ø → ∃y¬∃z (zRy)
となることだし、リンク先文章でも
∈関係を x∪P(x)∪PP(x)∪......... に制限したものの
「任意の部分集合が」∈極小元をもつ *
となってるから379が言っている点については問題ない気がする。
aの部分集合の部分集合はaの部分集合なので、
部分集合を取る操作に対して閉じてなきゃいけない。
xが満たすならyも満たさないといけない。逆にyがダメならx⊃yもダメ。
385 :
132人目の素数さん :2011/08/08(月) 00:36:50.19
糞ジャップは地球のゴミ
x∪P(x)∪PP(x)∪......... でもいいのかどうかは分からないが、 この部分を x の transitive closure にした議論が有名で 標準的な集合論の教科書には必ず出ている。 なぜわざわざこんな変な定義を持ち出したのかが知りたい。
>>384 サンクス。y \subset x なんだね:
y = \{ y \} \subset \{ y, \emptyset \} = x
でもそしたら x' = \{ x \} が反例にならない?
>>380 矛盾はいいすぎじゃね?
階層を成すって見方もあるわけだから。
>>384 空集合は部分集合だけど∈極小元持たないな
ここもF先生の勘違い?
基地外は基礎の公理に異常な興味を示す
>>380 「超限帰納法を駆使する集合論的数学の大きな部分を放棄する」という意味は
「基礎の公理が成立する部分に関しては ∈-induction によって集合論および
その影響のある数学がスムーズに展開されるということ放棄する」という意味
だろう。さすがに、そんな間違いは書かないだろう。
「∈-induction」と書くべきところを「超限帰納法」と書いたのは勘違いと言っていいだろ?
>>392 >「∈-induction」と書くべきところを「超限帰納法」と書いたのは勘違いと言っていいだろ?
実際の証明で、∈-inductionと順序数に関する超限帰納法のどちらが多く使われているかが問題だろうね。
>>395 御目出度い頭だな
順序数に関する超限帰納法は∈-inductionなんだがな
field が違うでしょ。
398 :
132人目の素数さん :2011/08/08(月) 19:57:59.23
新井の数学基礎論の102ページの 補題3.3.2の証明でなんで 3行目の Prov(p1,x)→... が補題の証明になるのか解説お願いします。
>>398 シークエント計算の用語で説明すると、
<p0,p1> を (→∃) で消してから、p1, p2 に (∃→) を適用。
これがわからないということは、もっと前の事項を確認する必要あり。
>>399 thanks
何項目か飛ばして読んでいたので...
真面目に読みます。
「数学基礎論」で ψ(x1,.........,xn)とψ[x1,.........,xn]の括弧の使い方が どう使い分けられているのか分からない。 何か全体的に表記法がユニークで分かりづらいことが多いと思う。 要はこういうことだ、というような類の日本語の説明は良い感じなんだが。
>>401 Ψ()は論理式Ψの変数が()内のものを考えるときに使う。
Ψ[]は上記プラス、論理式Ψに[]内の変数以外が現れることはないということらしい。
>>397 フィールドの違いは非本質的だよ、上の方でしている many-sorted logic と同じように。
A(x)を順序数に関する超限帰納法で証明することと x∈On → A(x) を∈-inductionで証明することはほぼ同じ。
逆に∈-inductionはrankを使って順序数に関する超限帰納法に簡単に直せる。
だから395みたいな比較は殆ど無意味になっちゃう。
392が問題にしているのは、順序数とか∈に関する超限帰納法ではなくて
一般の超限帰納法は基礎の公理とは関係なく成り立つ、ということだと思う。
「一般の」超限帰納法から、順序数とか∈に関する「特定の」超限帰納法が導けない、というのは変な話だけど、
実際それには基礎の公理が必要。
だから「順序数の」とか「∈-」とかつけない「超限帰納法」をそこに書くのは誤りで、F先生の勘違いだと思う。
>>379 、
>>387 確かに x' が反例になっているね。
>>366 のリンク先の文章の条件(1)を満たす集合全体を M とすると、
x'∈M だけど、その唯一の要素 x は M に入らない、従って推移的でない。
しかも x' は M の中で要素を持たないから空集合になる筈で、
そうすると等号も「本物の」等号とは別の関係で解釈しないといけない。
もしかしたら
>>366 みたいな批判を避けるための深い理由があるのかも知れないけど、
その文章の議論では普通の well-founded part の定義でいいと思うので、これもやっぱり勘違いじゃないかな。
>>389 それも勘違いだと思う。
こうしてみるとF先生、勘違いが多いね。
>>351 PFA=Pro-Fuchino Axiom
いや普通の数学で帰納法と言ったら自然数の上の帰納法を指すように、
超限帰納法といった場合には普通は∈に関する帰納法のことを言うでしょ。
あくまでその意味で書いてるのであって、ちゃんとした研究者の彼が
こんな初等的な事実について誤認しているとかそういう訳じゃないはず。
>>387 に関しては確かに反例になっているように思う。
和集合の公理と置換公理と選択公理以外は証明できるので
最初の二つのうちどっちかが成り立たないはず。
まあありそうなのは、∪を使う普通の構成は当然知ってて、
それを書くつもりで筆が滑った、とかかな。
研究者なんて専門分野を出ればただのバカ
>超限帰納法といった場合には普通は∈に関する帰納法のことを言うでしょ
そーかー?
>>362 のリンク先(ウィキペデァだけど)でも、
「集合と位相」の教科書でも、∈に関する帰納法なんて意味してないぞ。
>こんな初等的な事実について誤認しているとかそういう訳じゃないはず。
だから「勘違い」なんじゃないの?
>超限帰納法といった場合には普通は∈に関する帰納法のことを言うでしょ 専門バカっぷりを発揮だなw
故小平邦彦師のことば「専門バカでない者は唯のバカだ」
>392 が、わざと誤読をしているだけですね。 >超限帰納法を駆使する集合論的数学の大きな部分について, >そのような数学での結果を,ユニヴァースの well-founded part に制限したときに成り立つ結果と読みかえる
超限帰納法を使うのは九割九分ロジックだろ。 代数学とかの人は何故か多少無理してでもツォルンの補題を使う。 まあ分からんでもないけど。 ただの言葉遣いの趣味の問題で、それを数学的能力の問題にすり替えるのはおかしい。 俺も、∈を「含まれる」と読んだだけで 「含まれる ⊆」のことで「所属する ∈」の区別もつかないトンデモ発見!、 とか謎の煽りを受けたことあるけど、まあそのレベルの問題。 しかもそういう奴に限って言葉遣いや定義は本によって少しずつ違う、ということも知らんし よりにもよって広辞苑だのja.wikipedia.orgだの 全く当てにならん文献をソースに挙げて来たりする
> それを数学的能力の問題にすり替えるのはおかしい このスレでどこの誰がすり替えたのか聞いてみたい。 せいぜい「勘違い」くらいまでしか誰も言ってないんだがな。 この板の住人って被害妄想持つ奴が多いんだな。
そこで「多い」と言ってしまっては…
>>399 要は、
PA |― Prov(p1,x) → Prov(p0,Imp(x,y)) → Prov(<y,<p0,p1>>,y)
を推論規則で全称化して
PA |― Pr(x) → Pr(Imp(x,y)) → Pr(y)
であるとこまで論理式の列をつくれって話ですよね。
問題は、
PA |― Prov(p1,x) → Prov(p0,Imp(x,y)) → Prov(<y,<p0,p1>>,y)
自体はどうやってでてくるのかということなんです。
PA |― Prov(p1,x) ∧ Prov(p0,Imp(x,y)) → Prov(<y,<p0,p1>>,y)
なら作れるんですが...。
>>411 >俺も、∈を「含まれる」と読んだだけで
>「含まれる ⊆」のことで「所属する ∈」の区別もつかないトンデモ発見!、
>とか謎の煽りを受けたことあるけど、まあそのレベルの問題。
それを楽しめないようでは、こんなとこ来ちゃダメだ。
煽ってる側も分かっててそういっている可能性もかなり高いんだから。
きちんと定義を分かってないのであれば数学的能力の問題だと思うんだけど。 一方で、言葉の使い方の問題であったり 採用している定義が違うというのであればただ趣味の問題。 後者の問題に過ぎないのに前者の問題にしたがっている、ということ。
> 後者の問題に過ぎないのに前者の問題にしたがっている したのはお前だろ!
ずっと批判する流れだったから、渕野シンパが過敏になるのはまあ分かるんだが、
渕野シンパは
>>366 のような批判をどう考えているのだろうか?
「ちゃんとした研究者の彼」が、あの理由では V=L にも適用できてしまう、
という初等的な事実に気づかなかったのか?
419 :
414 :2011/08/09(火) 20:13:11.55
自己解決
元中部大の学生がまぎれこんでるな
趣味の問題に過ぎないと思ってるなら「勘違いしている」とかそんな言い方するか?
普通しないだろ。
>>418 それ、同じことをだいぶ昔に佐藤さんがweb上に書いてたはず。
なるほどな、と思って普通に読んでたし、渕野先生の記事読んでも
完全性定理とかを持ち出すのは無理あるだろjk、とか思ったりはする。
尤も、構成可能性に反するような公理(例えば巨大基数公理)を
いくら付け加えても構成可能集合について何ら新しい結論が得られない、
と言うのは本当かどうか怪しいと思うけど。
というか実数や実数の部分集合についてだいぶ違う結論が出て来ると思う。
「超限帰納法」=「∈に関する帰納法」というのは集合論だけで通用する言い回しではないでしょうか? 業界用「口語」は分かりませんが、集合論でも「普通」は言いすぎかと思います。 基礎論内部でも集合論を出ると余りしな言い方ではないでしょうか? 証明論で transfinite induction というときに、整礎な関係を∈に限ったりはしません。 基礎論の外に出たら「集合と位相」の教科書のように「一般の」超限帰納法しか指さないと思います。 読者層は「集合論の公理系についてのぼんやりとしたイメージくらいは持っている人」と明示してあるので、 集合論内部でしか通用しない言葉遣いをしてしまうのはまずいと思います。 「勘違い」という言葉がまずければ、「うっかり内輪向けの言葉が出てしまった」でしょうか。 >一方で、言葉の使い方の問題であったり >採用している定義が違うというのであればただ趣味の問題。 「趣味」をどれくらい広い意味で仰っているのか分かりませんが、 読者層に合わせた言葉遣いが出来ないのは「専門バカ」であって 「趣味の問題」では片付けられないのではないでしょうか。
>構成可能性に反するような公理(例えば巨大基数公理)を >いくら付け加えても構成可能集合について何ら新しい結論が得られない、 >と言うのは本当かどうか怪しいと思うけど。 F先生の原文は「基礎の公理での性質を満たさない集合の存在を保証する公理」だけど 単純に∃x¬(x∈WF)と理解するか、それより強い公理も含むのかってことだね。 前者の場合、V=Lに置き換えると∃x¬(x∈L)だから、これだけでは構成可能部に何ら新しい結論は得られないよね。 巨大基数公理を許すのなら後者で理解しないといけないけど、 今度は整礎部の集合について新しい結論が得られない、とは言えないよね。 ∃x¬(x∈WF)を導く巨大基数公理みたいなものも考えられるんだし。
渕野シンパも擁護を諦めたか。 シンパは一人だけか?
帰納法と言えば∈に関する帰納法が普通と言うのは言い過ぎかもしれない。 ただ、帰納法って言ったって 自然数の上の帰納法、論理式の構成に関する帰納法とかいろいろあるけど わざわざ〜に関する帰納法と毎回断らずに (論理記号の数に関する)帰納法により〜〜である、というのと同様に、 基礎の公理が無いと帰納法が使えないと言ったときの帰納法は 当然∈に関する超限帰納法と理解するべきかと。
>わざわざ〜に関する帰納法と毎回断らずに >(論理記号の数に関する)帰納法により〜〜である、というのと同様に、 毎回「は」断らないのと、最初っから断らないのは違うだろ >基礎の公理が無いと帰納法が使えないと言ったときの帰納法は >当然∈に関する超限帰納法と理解するべきかと。 その読者層にそれを求めるのは「専門バカ」の典型だろ
その人ほんとにシンパなの? 元々、非専門家向けに言葉遣いの配慮ができるという前提で (そうでない人もいただろうけど)勘違いという理解が大勢だったのに、 「そうじゃない、配慮なんてできない」と主張してるんだから。 どっちがシンパだか分からんね。
>>411 > 俺も、∈を「含まれる」と読んだだけで
> 「含まれる ⊆」のことで「所属する ∈」の区別もつかないトンデモ発見!、
> とか謎の煽りを受けたことあるけど
この件で顔真っ赤にしちゃった人。それで粘着してる。
超限帰納法は普通に順序数に関する帰納法でしょ。 それで普通に読める文章を曲解するのがおかしい。 元の文章のどこにも超限帰納法が成り立たなくなるとは書いていない。
>>423 うん、後者の解釈をすると(3)が言えない。前者の解釈にしないといけない。
だから V=L の方でも巨大基数公理は反論材料にならない。
>超限帰納法は普通に順序数に関する帰納法 超限帰納法の「普通」に新説が! 「∈帰納法が普通」説よりは説得力あるとは思うが 俺はもうこんなの相手する気が失せたので他の人ヨロシク。
わざと文脈を読まないから、そう思えるだけ。
433 :
421 :2011/08/10(水) 00:44:16.59
ちょっと待て
基礎の公理が無いと超限帰納法が使えないってのは誤りじゃないか?(
>>362 )
というレスに
そうだ、無関係な公理が要ると思ってるF先生は勘違いしているよ(
>>380 )
って言ってるんだから普通は(少なくとも非専門家は)
F先生はどこにどの公理が必要か分かってないんだよ、
って言っているように思うだろ。
だから俺その他の人が、
元の文章は単に、∈の整礎性を示すのに基礎の公理が要るという意味だよ
とわざわざ説明したのに、敢えてそれを無視して
∈に関する帰納法と、一般の整礎関係Rに関する帰納法は違うものなのにそれを混同しているから筆者の勘違い
とか、
いや集合と位相の教科書には後者しか書いてないから後者の意味なんだ
とか筋の通らないことを言い続ける奴がいるから、別にシンパでも何でもない俺が
言葉遣いの問題を勘違いというのは止めろと言わないといけなくなったんだよ。それだけの話。
曲解同士が言い争えば、そこにはトンデモが残るだけなのだよ。 枯れ枝だって親派やantiに見えてしまう
そんな文章の中の一単語が正しいとか間違いだとかいい加減やめようぜ。
文章の大意には何の関係もないし。もっと本質的な議論しようよ。
思うに
>>358 が核心を突いていると思う:
>反基礎の公理が必要(または有効)な「理論展開」には
>フラグメントのモデルを中に作るっていう面倒な方法で我慢しろと言っておいて、
>基礎の公理が必要(または有効)な理論展開(超限帰納法とか)については
>「well-founded part に制限したときに成り立つ結果と読みかえる」
>のは「大きな犠牲」というのは、手前味噌過ぎないだろうか?
相手には議論のたびにフラグメントを取ってそのモデル(推移的でない)で我慢せぃ、
自分たちは(フラグメントではない)推移的モデルでも我慢できない。
これにPFA派から反論とかあると面白いんだが。
>>435 このスレにF先生擁護派がいないんだから無理だろ
本人がこのスレに反応してくれて件の文章更新してくれれば盛り上がるだろうが
そんな小物な真似するような人には見えないし
しかしようもまあ文章の大意に関係のない一語の正否の議論だけでこれだけのレス数が消費できたものだわ
どんな馬鹿でも、あら探しをしたり、難くせをつけたり、苦情を言ったりできる。 そしてたいていの馬鹿がそれをやる。 -ベンジャミン・フランクリン-
シンパでもなんでもないが: 基礎の公理を付け加えないほうが、普通の数学者 には気持ちがよいというのはそうだろうが、集合論として 「∈-無限下降列をもつ」という公理が同程度に意味があるというのは、誰も 主張しないだろう。 「∈-無限下降列をもつ」という公理は、だだシステムとして、多少意味のある 解釈ができないこともないという程度だから、F-先生の怒りは、それで博士号 をとった結果がとくに面白くもない結果だということじゃないかな? 面白い結果がでれば、そんな文句もいわないだろう。つまんない結果なんじゃ ないの?誰が、指導教官かしらないが。
[SAB] [S] 東大,弁護士,Re, [A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, [B] DNC こなみcard 掃除 洗濯 飯 キリン水
[SAB] [S] 東大,弁護士,Re, [A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, [B] DNC こなみcard 掃除 洗濯 飯 キリン水
[SAB] [S] 東大,弁護士,Re, [A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, [B] DNC こなみcard 掃除 洗濯 飯 キリン水 風呂入った
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか?
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,
[S] 東大, 弁護士, Re,
>>427 F先生の講演でも記事でも、自分で掲げた「想定する聴衆」「想定する読者」に分かるようになったためしなんてないよ。
今回も「集合論の公理系についてのぼんやりとしたイメージくらいは持っている人」が
「基礎の公理が無いと帰納法が使えないと言ったときの帰納法は当然∈に関する超限帰納法と理解するべき」
なんて風に考えているはず。
>集合論として「∈-無限下降列をもつ」という公理が同程度に意味があるというのは、誰も主張しないだろう。 その「集合論として」が曲者だろ。 独立性証明にも記述集合論にも興味なくて、循環現象とかに興味があるような人には AFA の方が意味があるだろうし。 AFA の方が応用範囲が広がるんだから。
公理 AFA に意味があるということと、FA の代わりに AFA を採用した集合論の公理系に意味があるというこ とは別の話。 公理系を設定したこと自身に意味のある結果を出さな ければ、「そういう公理系もありますね」でおしまい。
462 :
132人目の素数さん :2011/08/10(水) 19:59:02.40
フォンノイマン自体も 基礎の公理の導入は技術的な問題と語っているからね。 しかしAFAの一種であるクワインのNFなんかでも数学は 矛盾なく記述できる。
>460 独立性証明にも記述集合論にも興味なくて、循環現象とかに興味があるような人 が、「集合論」に興味があるというのはおかしい。数学としての厚みがちがう。 強制法は、集合の構造を解明するのに使われていると考えるのが、集合論の何 十年間の結果だ。循環現象自体は無限を扱うときの手法だが、それだけでは 数学としての厚みがない。フォンノイマンは強制法ない時代の人だよ!
基礎の公理って無限集合を用意するかどうかぐらいの違いがあると思うけど…… あれの効果で各集合が升目に抑まることが保証されているのに。
465 :
132人目の素数さん :2011/08/10(水) 21:36:20.70
まぁZFCが要領の悪いまとめ方してるって話だろうな。 帰納法を直接公理に入れればシンプルだった。
基礎の公理って帰納法と等価なの?
対偶
>>435 に応えてスレを盛り上げてくれるのは嬉しいが、
どれもこれもF先生の主張の劣化版みたいなのばかりだ。
>>463 >数学としての厚みがちがう。
とかなんとか言ってるけど、厚みを比較できるほど、
Aczel や Barwise の循環現象を数学的に扱う為の仕事を理解できているのかね。
従来の数学では扱えない循環を扱うための計算機・情報科学の発展を理解できているのか。
(しかも集合論よりもそうした数学の方が数学の世界で認知されているという現実。)
F先生が集合論に対する他の数学者の無知について
知らないものはなかったことになる、とか嘆いていたけれど、
F先生や463の「循環現象の数学」に対する態度そのものだ。
「循環現象の数学」が重要なので、それが自然に展開できる集合論の体系の研究が重要という論理には飛躍がある。 それを展開できる体系は存在するだけで十分。
470 :
132人目の素数さん :2011/08/11(木) 01:41:48.01
>「循環現象の数学」が重要なので、それが自然に展開できる集合論の体系の研究が重要という論理には飛躍がある そら飛躍だ。それで?
それが自然に展開できる集合論の体系の研究を否定するのに、 「循環現象の数学」の重要性は無関係ということ。
それがどうした?
問題は、基礎の公理の『数学を展開するための基礎としての集合論』におけるステータスだったろ。 なんか論点がずれてないか?
核心を突いているって言った
>>358 の批判も、
『数学を展開するための基礎としての集合論』には基礎の公理を採用すべきだ、
ということに対してだろう。
>>469 君がそう思うのは自由。君には十分なんだろ。
寧ろF先生だとか数学の厚みだとか脱線しまくり 飲ま飲まイェイ
重要な「循環現象の数学」を展開できないなら 「数学を展開するための基礎」としては失格だわな
479 :
132人目の素数さん :2011/08/11(木) 07:40:04.14
AmazonでHugh Woodin の The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal が10000円でうってる!
数学と、数学を分析する超数学を分けることにしよう。 (後者だって数学だってのは置いておいてだ。) 「数学としての集合論 vs 数学の基礎としての集合論」で その「数学の基礎としての集合論」のウリは超数学に使えるってことだ。 当然、超数学の側の都合で、分析対象である数学を勝手に変えてはいかん。 客観性、これ科学のキホンね。 基礎の公理が嬉しいのは超数学の側の都合でしかない。 もちろん分析対象を変えなくて済む範囲ならそれでもいいかも知れん。 が「循環現象の数学」を「数学」から外さないと、となるとどうか。 「循環現象の数学」は計算機や情報科学であって数学じゃない、というのもありだ。 「基礎論なんて数学じゃない」と言われることも覚悟の上なら。
あくまで基礎の公理は数学としての集合論に必要なのであって メタ数学に必要なのではないよ 今のところ、Barwiseの"The Liar"(邦訳「うそつき」)は 論理学とか哲学とか或いは情報科学であっていわゆる数学では無いと思う。
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,
>>480 の観点からすると
>「循環現象の数学」が重要なので、それが自然に展開できる集合論の体系の研究が重要
とかいえるよね。
「集合論を使えば、これこれの命題が通常の数学では証明できないことが示せる」とか宣伝するためには。
通常の数学に「循環現象の数学」も入れられた方が宣伝価値が高まるわけで。
んなことない 強制法とかの普通の集合論を展開するためには 基礎の公理があった方が便利なのは確か AFAを使って命題の独立性を示せたなんていう 画期的なニュースは今のところ無い
492 :
132人目の素数さん :2011/08/11(木) 22:11:37.50
関係ないが 不完全性定理より先にモデル理論 勉強しといたほうが理解がスムーズじゃないか?
>>491 1回2回ならともかく、論点はぐらかしだか似たようなボケだかを何回もやってると誰にも相手にされなくなるぞ。
っつーか既に誰も相手相手してねぇか。
F先生とのイタさ競争なら余所でやれや。
>>492 不完全性定理はシンタックスがどうの、って矢田部さんに怒られるぅ!
495 :
132人目の素数さん :2011/08/12(金) 07:10:06.07
逆数学って最先端 今どうなってんの?
集合論を数学として扱ってくれないことに悔しさ満載の愚痴を垂れるくせに、
情報科学とかは数学扱いしない、数学として厚みがないとか言う、
F先生とか
>>463 の神経ってどうかと思う。
自分の受けた嫌がらせはもっと別の人に向けて憂さ晴らし?
少なくとも理論系なら、動機は情報からだったとしても、
公理を立ててから先の議論は純粋に数学的だし、
(もしかしたら基礎論以上に)膨大な研究の積み上げがあって
数学としてもかなり奥深いと思うけどね。
いや情報科学は情報科学だろ 物理学を数学扱いしないのが何もおかしくないのと一緒
>>497 物理と数学の境界領域のこと何も分かってないな。
動機を物理から貰って、そのあとは純粋に数学的にやるのは、数学として分類されるだろ。代数解析その他。
理論物理は確かに数学か物理かの二者択一なら物理だが(代数解析とかは二者択一でも数学)、 そんでも「理論物理は数学としての厚みがない」とか言ったらフツーに大問題だろ。
世間では集合論も情報科学扱いです!
>>496 情報科学の昨今の隆盛ぶりを見たら、理論系に限ったとしても
もしかしなくても基礎論以上だろうよ。
基礎論の昨今の衰退ぶりをみたら泣けて来た。
昨日の491の「スルーされ力」は見事だった
ネタか天然か知らんけど、よくあそこまで的外れなことを、と歓心する
>>497 =
>>491 だろ、相手なんかするなよな
別に理論物理の人は「数学としての厚み」なんか目指してないから。 数学的にローテクでも物理として意味あることが分かれば良い。 数理統計学とかゲーム理論とか、意思決定理論とか社会選択理論とか、 数学的としてみると大したことないけど応用上の意味がある、という例は結構あるでしょ? なぜAFAがそうだといかんのかが分からん
AczelのAFAの応用として有名な循環現象というのは、 「この文は偽である」のような自己言及文に 真偽値を与えるにはどうすれば良いのか、みたいなBarwiseたちの研究なので、 これを「数学」と言われるのはさすがにちょっと違和感がある。 論理学とか言語哲学とかとしてなら納得できるけどね。 「基礎論?ああ、クレタ人のパラドックスとかの奴でしょ?」 とか他の分野の数学者に言われると、まるで基礎論は哲学だから数学じゃない、 と言われてるようでちょっと個人的には哀しい気がするけどね。 集合論≒基礎の公理を認めるZF集合論の研究、というのは 位相空間論は道具だからそれ自身が重要な研究対象という感じじゃない、 と幾何や解析の人が言うくらいには正当な意見だと思う。 AFAなんて茶飲み話程度の話だとか、研究能力が無いから AFAなんか研究してるんだってのは暴論だけど。
>数理統計学とかゲーム理論とか、意思決定理論とか社会選択理論とか、 >数学的としてみると大したことないけど応用上の意味がある 「集合論とか数学としてみると大したことないけど」とか陰で言われていることを知らないと見える。
>>504 また妄想乙な発言を:
>なぜAFAがそうだといかんのかが分からん
お前は「あるべき歴史の国」人かよ
いいとかいかんとかでなく、現実としてどうなっているかだろ
>AczelのAFAの応用として有名な循環現象というのは、 >「この文は偽である」のような自己言及文に >真偽値を与えるにはどうすれば良いのか、みたいなBarwiseたちの研究なので はいはい。それしか知らないで偉そうなこと言わないように。 勉強しなおして出直してきましょうね。 >別に理論物理の人は「数学としての厚み」なんか目指してないから。 >数学的にローテクでも物理として意味あることが分かれば良い。 「数学としての厚み」が目標になっている分野って何よ。 503はそんなものを目標に研究しているのかね、哀れな研究人生だな。 そもそも「理論物理は数学として厚みがない」が問題なのは、 理論物理の人に反感持たれるからだとしか考えられないのか? そういう発言をした主の教養が疑われるって意味でも大問題だってのが分からんのか。 >数理統計学とかゲーム理論とか、意思決定理論とか社会選択理論とか、 >数学的としてみると大したことないけど応用上の意味がある、という例は結構あるでしょ? これで十分、暴言だろ。 数理統計なんてちょっとでも真面目に触れたことあれば 「数学的に大したことない」なんて口が裂けても言えないだろ。 集合論に関わると、他分野をバカにする癖が身につくのかね。
>>507 そうむきになるなって。
応用っぽい分野だとろくに知らないで「数学的には大したことない」
とか考える奴は結構いるだろ、「基礎研究やってる俺、頭いい」みたいに考える奴。
F先生もその傾向はあるし。そんな連中に何言っても無駄だ。
「理論物理は数学として厚みが無い」なんて誰も言ってないだろ。
目指してなくても結果としてそうなる場合はある。
或る分野が難解なのは(普通は)難解さを目指したからじゃないのと似たような話。
イージーな分野だと言いたいのではなくて
あくまでその分野に取って数学は応用のための道具に過ぎないというだけ。
数学的に高度でない、というのを即、バカにしていると言う風に見做す方が
よほど数学中心主義だと思うけどね。
あまりにも無意識的にそうなってしまうから気付かないのかもしれない。
>>507 AFAが応用されている例って他には何?
無知乙とかいって人を煽れば増える訳でもないよ
>数学的に高度でない、というのを即、バカにしていると言う風に見做す方が >よほど数学中心主義だと思うけどね。 これには賛成なんだが、だからと言って実際に数学的に高度な分野を「数学的に高度じゃない」というのはまずい。 数理統計とかは俺も少し齧った程度だが、そんな「数学的に大したことない」とは言えないと思った。 大学の教養でちょっと統計の勉強しただけで判断してるのなら、 集合と位相で齧っただけで「集合論は数学的に高度じゃない」というのと変わらんと思うよ。
で、結局
>>503 =
>>509 は何がいいたの?
「あくまでその分野に取って数学は応用のための道具に過ぎない」としても、
その現に応用されている数学を排除しての「数学を展開する基礎」なんて意味ないじゃん。
512 :
132人目の素数さん :2011/08/13(土) 11:26:17.34
456 :132人目の素数さん :2011/08/13(土) 11:25:49.45 The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal (De Gruyter Series in Logic and Its Applications) 8000とかw 買わんのなら数学やめた方が良いww
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
基地外が棲み付いたな
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[S] 東大, 弁護士, Re,
519 :
132人目の素数さん :2011/08/13(土) 13:36:03.31
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[S] 東大, 弁護士, Re,
[C] 朝鮮人 ニダー コリエイト ウリナラ起源 壇君 童話 〻
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
>>509 The Liar なんて一般向けの本だけで分かった気になるなよな。
Aczel の奴だけでも見てれば、応用が書いてあるのに。
プロセスとかの「数学的」計算モデル等。
それに限らず、計算のモデルでは一般に
関数とその定義域がどっちもプログラムっていう「循環現象」で色々面倒なことが起きる。
509は「数学として大したことない」=「バカにしている」を否定しているけれど だったらやたらと「あれは数学じゃない」「これは数学として大したことない」と何の為に言っている? 色々なものを数学から排除したいようにしか見えないんだが。 単に口先で上の公式を否定しただけで、発言の意図が見えてこないと、バカにしているようにしか見えないわけで もっとちゃんと説明した方がいいと思う。 流れを追ってみると「さっきと言ってること違うだろ」って思う箇所多数だし。
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
計算のモデルって普通デカルト閉圏なんかを使ってモデル化することが多いような
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
>>533 デカルト閉圏は型が付いている単純な計算の場合。関数とその定義域がどっちもプログラムという「循環現象」はない。
型がない場合、そういう「循環現象」があるので難しい。それを Dana Scott が解決した。
これが領域理論の端緒となった。
こうした理論は「情報」への応用がない、なんていうと多くの理論計算機科学屋の食い扶持がなくなるけど、
実際のところ、応用を意図しているというよりは純粋に数学的興味かと。
ちなみにAczelがAFAを応用したっていうプロセスってのは、
単純な計算じゃなくて、システムの保守管理とか特に終わりがあるわけではない継続的な計算。
これに数学的モデル(表示的意味論)を与えるのは型なしの場合以上に難しかった筈。
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG,
>>529 509って上の方で「勘違い」発言を「数学的能力に問題あり」発言だとかいう
独自理論立てて騒いでいた奴でしょ
今回もどれかの発言を独自理論で別の意味に理解して騒いでいるだけだと思う
多分
>>490 で自説を否定されたので反論してるんだろうけど
最初の
>>491 はずれ過ぎてて全員にスルーされたほかその後の発言もどう反論になってるのか分からんし
[G] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
AFAの応用は知らないけど、Scottの領域理論が数学的に厚みがないだとか 数学じゃなくて情報科学だとかって、見識がなさ過ぎると思うね 多くの理論計算機科学者は自分を数学者と考えているだろうし反感買うだけ 尤も我が世を謳歌している彼らは、集合論なんて弱小分野の人間にそう言われても屁でもないだろうけれど
>>509 キングじゃないので509の脳内は読めませんが、おそらく
AFAの応用先の理論は、数学じゃないか数学として厚みがないので
「集合論を使えば、これこれの命題が通常の数学では証明できないことが示せる」
と宣伝するときの「数学」に入ってなくても問題ない、ということかと思いました。
物理は数学扱いしないとか、理論物理は「厚み」を目指してない、とかが
どう関係あるのかはやっぱり分かりませんが。
あーあ、集合論学徒が(F先生の?)「知らないものはなかったことになる」を実践しちゃったのね
[S] 東大, 弁護士, Re,
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
Scottの領域理論は数学的に厚みが無いなんてどこにも書いてないと思うけども。 ゲーム理論は純粋数学的にはあまり興味深くはない、というような (しかもゲーム理論の研究は価値が低いと言っている訳ではない)レスと 型が無い場合はScottの領域理論によってモデルを与える、というレスとを 混ぜて新しい主張をでっち上げられても、主張してもいないことに対して反論しようがない。 だいたい463は俺のレスじゃないから、「厚みが無いとは何だ!」とか俺に言われたって困る。 「数学的厚み」なんてなくても役に立ちゃ良いじゃないか、とは思ってるけどね。 AFAにちょっとでも批判的な意見や、F先生の書いていることが 何から何まで間違っている訳ではない、というごく当然の注意まで、全て同一人の 「シンパ」のレスだと思い込んで反論するのはちょっと正気じゃない。 そういう党派的な議論の仕方は止めた方が良い。
non-wellfoundedなAFAとかの理論が集合論じゃないとは言わないが、 集合論の中でかなり辺縁的な分野であるのは事実なので、 全く同じくらい研究する価値のある分野だというとあまりにも言い過ぎになる。 「今ではブラウワーに端を発する直観主義的数学は、古典論理に基づく従来の数学と 同等の、いや寧ろより確固とした価値をもつ数学として盛んに研究されている」 みたいなことを素人に吹き込む人とかが居たら、さすがに「嘘付け」って言いたくなるでしょ。 だから「さすがに言い過ぎだろ」って突っ込んだだけだ。
558 :
132人目の素数さん :2011/08/14(日) 23:43:53.04
>>556 >AFAにちょっとでも批判的な意見や、F先生の書いていることが
>何から何まで間違っている訳ではない、というごく当然の注意まで、全て同一人の
>「シンパ」のレスだと思い込んで反論するのはちょっと正気じゃない。
2ちゃんってのはそういうところさ。楽しめないなら来ちゃいかん。
559 :
132人目の素数さん :2011/08/15(月) 00:35:08.36
>>557 AFAがその他集合論と「全く同じくらい研究する価値のある分野だ」とか
「同等の、いや寧ろより確固とした価値をもつ数学として盛んに研究されている」とかって
言ってるのはどのレスだね。このスレでそんなこと言ってる奴見た記憶がないんだがな。
お前こそ「そういう党派的な議論の仕方は止めた方が良い」ぞ。
おっと、557と556は同一人だと思っちゃいかんのかな?
誰が誰の発言だか判らんから、レス番でも良いからとりあえず名乗れ。
561 :
559 :2011/08/15(月) 01:22:04.91
そんなことしてもレス番騙る奴が出てきてもっとカオスになるだけ。 匿名掲示板ってのはそういうもんだと思って楽しめないなら(ry
間違われたり騙られたりしたくなけりゃ、トリップつけりゃいいだろ
過去のレスに付けるのは不可能。「俺は509だ」「いや違う」ってなるだけ。
>>558 正気じゃない反論を楽しむか全力で突っ込むかはその人の勝手でしょう。
>>560 >>272 以降の議論を続けたい人だけでもレス番をつけて欲しいですね。
>>561 あなたが2chに対して斜めに構えるのはあなたの勝手ですが、
そうしない人達に来ちゃいかんと言うのはただのひとりよがりです。
>>564 それがどうしたのですか?
今回は過去レスを書いた人が特定できないと困るケースではありません。
過去のレスを書いた本人が自分の意見はこれだと申告さえすれば、
別人が同意見だろうとなんの問題もありません。
>>559 全くだ。どんだけ頑張って拡大解釈しても精々、
490が「AFAはFAと同じかそれ以上に研究されるべき」と言ってると理解できないこともない。
それも、かくかくしかじかの宣伝をするのなら、という限定付きでだ。
現状でFA以上に盛んに研究されているなんて言った奴は誰一人いない。
「嘘つき」以外の応用例が出てきたんで体面だけ保ってさっさと去りたいだけなんだろうな。
尤も俺も表示的意味論とか言われても分からんから応用例の細かい話でこのスレが盛り上がられても付いていけないけど。
>かくかくしかじかの宣伝をするのなら そういう宣伝を現にF先生がしているのだが
まあ研究の総量とかの蓄積からして違うし仕方ない
>>557 >non-wellfoundedなAFAとかの理論が集合論じゃないとは言わないが、
>集合論の中でかなり辺縁的な分野であるのは事実なので、
>全く同じくらい研究する価値のある分野だというとあまりにも言い過ぎになる。
これをパクると
集合論とかの基礎論が数学じゃないとは言わないが、
数学の中でかなり辺縁的な分野であるのは事実なので、
全く同じくらい研究する価値のある分野だというとあまりにも言い過ぎになる。
まあ研究の総量とかの蓄積からして違うし仕方ない
[S] 東大, 弁護士, Re,
FAを強くしてみたり、弱くしてみたりするのは、面白いと思うが、 拒絶反応がある人がいるのにはびっくり。
基礎論よく知らんけど、いろんな公理系を作って満足して終わりみたいな気がする。 重要なのはその公理系からどんな面白い結果が出てくるかなんだけど、 そこら辺はバッサリ切る捨てているか、そんな結果は望むべくもないのか?
574 :
132人目の素数さん :2011/08/16(火) 21:42:42.62
>基礎論よく知らんけど、いろんな公理系を作って満足して終わりみたいな気がする。 >重要なのはその公理系からどんな面白い結果が出てくるかなんだけど、 >そこら辺はバッサリ切る捨てているか、そんな結果は望むべくもないのか? ロジック未経験の典型的な誤解。 何もないところにはじめに公理をつくってあとから発想が出てくるということはない。 また、公理(証明体系の公理図式にしても閉論理式という意味にしても)は ロジックやるときの開始地点というわけでもない。 言語に使われる記号や推論規則や論理式やモデルなんかが すべてしっかりと揃ってないと何もできない。 公理系から何が出るかというより、 むしろ公理だとかが持つ性質やそれを扱う技術が研究対象。
俺はAFAに特別シンパシーを持っているわけじゃないが、
基礎論の外向けには「価値がある」=「沢山の研究者の興味を惹く」を否定しておいて
(「ロジックの研究者は少ないが、研究する価値が低いわけじゃない」みたいな)
基礎論の内向けでは
>>557 みたいに上記のような等号を前提にAFA研究を批判してる
一部集合論の人々(当然F先生を含む)を見ていつも呆れてる。
そしてその自己矛盾に気づかないことに同じ数学者として鬱になる。
576 :
575 :2011/08/17(水) 00:26:07.39
「より価値がある」=「より沢山の研究者の興味を惹く」とすべきだったかも
FAとかAFAとかこだわるの止めて、いっそのこと公理もパラメータ化したらいいんじゃね?
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
579 :
132人目の素数さん :2011/08/17(水) 10:37:22.04
公理のパラメータ化って何よ?
別にAFAは「研究者が少ないから」どうだと言ってる訳じゃないし FAの反例になるような集合は、20世紀初頭の最初期に Mirimanovが研究した時からextraordinaryな集合と言われてるので 当初から病的な対象と思われていた訳で
> The Russian Dimitry Mirimanoff had pointed out that possibility two > years earlier. He had called such sets ”extraordinary,” but he > apparently regarded their existence more as a curiosity than a defect.
>Mirimanovが研究した時からextraordinaryな集合と言われてるので >当初から病的な対象と思われていた訳で そうすると研究する価値が低くなるというわけかい?
>579 ユークリッド幾何学と非ユークリッドを曲率で統合するような話。
>579 例えばユークリッド幾何学と非ユークリッド幾何学の平行線公理を曲率で統合するような話。
失礼……投稿ミスった。
基礎の公理の話はいい加減別スレ立ててやったらどうなんだ
[Girl25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] BCEFJMRST [Girl25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl [G25] BCEFJMRST
>>580 ルベーグ可測じゃない集合とか集合論で扱っているような集合は
普通の数学の視点ではそれこそ`extraordinary'なものだし、
ZFCから独立とか巨大基数公理に関係する命題も`extraordinary'と認識されている。
だから集合論なんてのは「辺縁的」なもので、
普通の数学と全く同じくらい研究する価値のあるとはいえないのかな?
>>584 ぜひその「曲率」にあたるものが何なのか示してくれ
FAは唯一集合に制限を課す公理なので、 どういう集合を認めるかって階層になるんじゃないの?
[G25] BCEFJMRST [Girl25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl [G25] BCEFJMRST
593 :
580 :2011/08/17(水) 17:22:48.01
>>589 たとえば整数論やら数理物理やらの研究者が
集合論を「辺縁的」だと思うのは或る意味では当然。
実際そういう「病的現象」は彼らの研究にとって大して役には立たないのだから。
純粋数学としてそれ自体に意味はあると思うけど、
あまり関連性のない分野があるのは当然だし仕方無いこと。
集合論「も」結構面白いのだ、と思ってもらう事は可能でも、
集合論も整数論と同じくらい数学として重要なのだ、と思ってもらうのはちょっと無理気味。
実際に応用や関連性が見つかってからじゃないと
辺縁的でないなどと主張しても、彼らにとっては説得力が無いと思う。
[G25] BCEFJMRST [Girl25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[13] Bike Combat Eminem Football Girl Justice
[13] Bike Combat Eminem Football Girl Justice Left Math Otaku Run Swim Tokyo
[13] Bike Combat Eminem Football Girl Justice Left Math Otaku Run Swim Tokyo v
[13] Bike Combat Eminem Football Girl Justice Left Math Otaku Run Swim Tokyo Virtua
[13] Bike Combat Eminem Football Girl Justice Left Math Otaku Run Swim Tokyo Virtua
>>593 そんな諦観に達さなくて良いと思う
他人の価値観に惑わされずもっと自分の価値観に自信を持って欲しい
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
>>584 AFA集合論はFA集合論を well-founded part として含むから
ある意味で統合したものになっている。
その意味で「数学を展開するための基礎」としては
AFA集合論の方が相応しいように見えるのだが、
F先生の件の文章は、FA集合論をAFA集合論の一部として扱うことを
(パラメータによって変化する中の一つとして扱うことに対応?)
「大きな犠牲」と言い張って拒否している。
寿限無をフルネームで呼ぶことに抵抗も面倒も感じないならAFA一択でいいんじゃないの?
略記の導入なんて普通にやることだろ
[S] 東大, 弁護士, Re,
阿保と基地外の絡み合い
[A] TS10,SBR,VFK10,TKK,VF1,LCCR,SINX, VF1M4,VF1L2,VF1H2,EMPC,MPE, 4231,4213,3331,3313,145,53A3,6236, EMPCB,EMJ,LP,CJ,F4,LC,DNA,RNA, SINT,JEL,23458,2348,DBT,GMO, AB,APLWJKSJ,PES,WE,CA,RR,ASL, EPH,ITU,261036,CBS6,1358,G1,AS3,M5, MLS,C1,LB,G4P6,DEWTA,4141, MARVEL,VF,FIFA,USA,BEN,ACT, DNC,UT,NOI,UOT,TST,MPCE,KIRIN, SUNTORY,SEGA,TMG,TMSBRG, TMSBRGJ,
[B] こなみcard 掃除 洗濯 飯 キリン水 風呂入った アマゾンでマスオ とんき センター漆原慎太郎古文 漆原慎太郎のセンター古文は今年中に新しいの出ますか? 漆原慎太郎 加地伸行 デザイナーズ ファッショナブル ファッショナブルなBike バナジウムすい 学参 TMSBRG, みずぜんたくばりかん せぢけんはみがきこ
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[S] 東大, 弁護士, Re,
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
[G25] Bike Girl Combat Girl Eminem Girl Football Girl Justice Girl Math Girl Run Girl Swim Girl Tokyo Girl
>>616 要するに、「AFA集合論を用いるが、ここではAFA集合論の各用語をすべて
そのwell-founded partの意味で用いる。」とするわけですね、わかります。
Bike Combat Eminem Football Justice Math Run Swim Tokyo
[Justice] Bike Combat Eminem Football Math Run Swim Tokyo
Bike Cmbat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
>>626 二つ目のAFAはFAの間違いではなくて?
つまり「AFA集合論を用いるが、ここではFA集合論の各用語をすべて
そのwell-founded partの意味で用いる。」でない?
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Bike Combat Eminem Football Justice Math Run Swim Tokyo
いいえ。
Marvel Sega
Biology Chemistry English Japanese Marvel
Bike Combat Eminem Football Justice Math Run Swim Tokyo
Marvel Sega
Marvel Sega Tokyo
[Justice] [トレーニングセブン] Bike Combat Eminem Football Math Run Swim [ブランドスリー] Marvel Sega Tokyo
[Justice] [7] Bike Combat Eminem Football Math Run Swim [3] Marvel Sega Tokyo
[1] Justice [3] Marvel Sega Tokyo [7] Bike Combat Eminem Football Math Run Swim
[1] Justice [3] Marvel Sega Tokyo [5] Bike Combat Football Run Swim [] Eminem Math マルコムX English Biology
[1] Justice [3] Marvel Sega Tokyo [7] Bike Combat Eminem Football Math Run Swim
[1] Justice Tokyo [2] Marvel Sega [7] Bike Combat Eminem Football Math Run Swim
[2] Justice Tokyo [2] Marvel Sega [7] Bike Combat Eminem Football Math Run Swim
[2] Justice Tokyo [2] Marvel Sega [7] Bike Combat Eminem Football Math Run Swim
Justice Marvel Sega Tokyo
[1] Justice [3] Marvel Sega Tokyo [7] Bike Combat Eminem Football Math Run Swim
654 :
137 :2011/08/19(金) 07:34:27.34
[1] Justice [3] Marvel Sega Tokyo [7] Bike Combat Eminem Football Math Run Swim
655 :
138 :2011/08/19(金) 07:41:33.47
[1] Justice [3] Marvel Sega Tokyo [8] Bike Combat Eminem Football Girl Math Run Swim
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Bike Combat Eminem Football Girl Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Akira Bike Combat Drike Eminem Football Girl Jacky Kage Lau Math Run Swim Virtua
削除
[1] Justice [3] Marvel Sega Tokyo [9] Akira Bike Combat Drike Eminem Football Girl Jacky Kage Lau Math Run Swim Virtua
[1] Justice [3] Marvel Sega Tokyo [9] Akira Bike Combat Drike Eminem Football Girl Jacky Kage Lau Math Run Swim Virtua
のをそのこそんそわ
[G9] Bike Combat Eminem Football Justice Math Run Swim Tokyo [2] Marvel Sega
[G9] Bike Combat Eminem Football Justice Math Run Swim Tokyo [B2] Marvel Sega
MARVEL SEGA TOKYO
671 :
132人目の素数さん :2011/08/22(月) 22:52:31.75
>>詳しい方へ 今のPAとかZFCとかよりも 現代の数学に合致するような 体系が逆数学的な研究を通して 得られる可能性ってあるのでしょうか? また、体系の研究で計算量のクラスや機械は現時点で有力ですか?
672 :
132人目の素数さん :2011/08/23(火) 19:38:55.96
>>29 すいませんが
述語論理の無矛盾性が証明できるなんて初耳です。
どうやって証明するんですか?
CE
674 :
132人目の素数さん :2011/08/23(火) 20:41:03.25
述語論理のある体系が無矛盾とかじゃなくて 述語論理自体が無矛盾という言い方がよく理解できないな。 等号付き2階とか否定記号なし2階が計算量クラス云々ならわかるが...
>>672 たとえば、一階の古典述語論理は古典命題論理の保存拡大であることを示す.
ついでに書いておくと、Gentzen は simple type theory の無矛盾性を証明している.
676 :
132人目の素数さん :2011/08/23(火) 21:44:47.56
あるよ
678 :
132人目の素数さん :2011/08/23(火) 22:20:35.90
[俺が尊敬する実用かつ文系科目かつ今現在に実在する日本人ベスト5(*五十音順)現人神依存症] 伊藤真(司法) 漆原慎太郎(国語) 小倉弘(英語) 小幡道昭(経済) 柴田孝之(司法)
[俺が尊敬する実用かつ文系科目かつ今現在に実在する日本人ベスト5(*五十音順)現人神依存症] 伊藤真(司法) 漆原慎太郎(国語) 小倉弘(英語) 小幡道昭(経済) 柴田孝之(司法)
>>678 詳しくはないが、竹内八杉の証明論入門でよくないか。
682 :
132人目の素数さん :2011/08/24(水) 00:48:56.88
[俺が尊敬する実虚用かつ文理系科目かつ今現在に実在する地球人ベスト5(*業績順)現人神依存症] ウラジーミル・ドリンフェルト(数学) 伊藤具(経済) 漆原慎大郎(英語) 小倉引(国語) 小幡道照(司法) 紫田孝之(国語)
[俺が尊敬する実用かつ文系科目かつ今現在という特殊に実在する日本人ベスト5(*五十音順)現人神依存症] 伊藤真(司法) 漆原慎太郎(国語) 小倉弘(英語) 小幡道昭(経済) 柴田孝之(司法)
[俺が尊敬する実用かつ文系科目かつ今現在という特殊の現実世界に実在する日本人ベスト5(*五十音順)現人神依存症] 伊藤真(司法) 漆原慎太郎(国語) 小倉弘(英語) 小幡道昭(経済) 柴田孝之(司法)
[俺が尊敬する実用かつ文系科目かつ今現在という特殊の現実世界に実在する日本人ベスト5(*五十音順)現人神依存症] 伊藤真(司法) 漆原慎太郎(国語) 小倉弘(英語) 小幡道昭(経済) 柴田孝之(司法)
>676 述語論理の無矛盾性の証明は、1点からなる構造で解釈すれば、すべて の公理が正となり、これが推論で保たれる。こんなことを押さえていないで 無矛盾性の証明が、、、なんていうやつはおかしい。
[俺が尊敬する実用的でかつ実生活に役立つ文系科目かつ試験かつ今現在という特殊の時間的中心点de現実世界に実在する日本人ベスト4(*五十音順)現人神依存症] ★伊藤真(司法) ★漆原慎太郎(国語) ★小倉弘(英語) ★柴田孝之(司法) [団体企業集団組織協会グループチームBest5【☆超能力☆】研究拠点架空作品] ★MARVEL(作品・ヒーローチーム・F4・キャラクター・アメリカの企業) ★東京大学(教養・社会的地位・学問・青春・超能力研究拠点) ★SPEC(作品) ★ジョジョ(作品) ★ダークエンジェル(作品) [] バーチャ(初3D格ゲ) ウイイレ(No.1サカゲ) マーブルのキャラ事典 小幡の本 掃除 うるしの記述 もし センター出願 インドアバーチャ インドアウイイレ ラミカ SPEC ジョジョ
[俺が尊敬する実用的でかつ実生活に役立つ文系科目かつ試験かつ今現在という特殊の時間的中心点de現実世界に実在する日本人ベスト4(*五十音順)現人神依存症] ★伊藤真(司法) ★漆原慎太郎(国語) ★小倉弘(英語) ★柴田孝之(司法) [団体企業集団組織協会グループチームBest5【☆超能力☆】研究拠点架空作品] ★MARVEL(作品・ヒーローチーム・F4・キャラクター・アメリカの企業) ★東京大学(教養・社会的地位・学問・青春・超能力研究拠点) ★SPEC(作品) ★ジョジョ(作品) ★ダークエンジェル(作品) [] バーチャ(初3D格ゲ) ウイイレ(No.1サカゲ) マーブルのキャラ事典 小幡の本 掃除 うるしの記述 もし センター出願 インドアバーチャ インドアウイイレ ラミカ SPEC ジョジョ
[俺が尊敬する実用的でかつ実生活に役立つ文系科目かつ試験かつ今現在という特殊の時間的中心点de現実世界に実在する日本人ベスト4(*五十音順)現人神依存症] ★伊藤真(司法) ★漆原慎太郎(国語) ★小倉弘(英語) ★柴田孝之(司法) [団体企業集団組織協会グループチームBest5【☆超能力☆】研究拠点架空作品] ★MARVEL(作品・ヒーローチーム・F4・キャラクター・アメリカの企業) ★東京大学(教養・社会的地位・学問・青春・超能力研究拠点) ★SPEC(作品) ★ジョジョ(作品) ★ダークエンジェル(作品) [] バーチャ(初3D格ゲ) ウイイレ(No.1サカゲ) マーブルのキャラ事典 小幡の本 掃除 うるしの記述 もし センター出願 インドアバーチャ インドアウイイレ ラミカ SPEC ジョジョ
>>686 おまアホやろ。自然数論の無矛盾性が、、、って話をしているときに、
自然数全体の集合ωで解釈すればすべての公理が正、とかいうのと同レベル。
>>672 が
>>29 に質問した話の流れが分かってないだけのか。
【138体系】 [S科目1] RE [A科目3] 東京大学 司法試験弁護士 超能力 [修身科目8(*アルファベット順)] BCEFGRSW []
【138体系】 [S科目1] RE [A科目3] 東京大学 司法試験弁護士 超能力 [修身科目8(*アルファベット順)] BCEFGRSW []
ABCEFGHRSW
>691 バカはお前だ。 自然数論は、無限集合がなければモデルがつくれないが、 述語論理なら1点でよいという話で、形式体系ばかり扱っている お前のようなうすらトンカチは気がつかない。
【138体系】 [S科目1] RE [A科目3] 東京大学 司法試験弁護士 超能力 [修身科目8(*アルファベット順)] BCEFGRSW []
猫
698 :
132人目の素数さん :2011/08/25(木) 15:13:54.10
>>695 1点だろうがなんだろうが、構造での解釈とか考えられないし
699 :
676 :2011/08/25(木) 19:53:40.88
何か俺のせいでガチンコ起きちゃったみたいなんで 俺が解決するね。 まず領域がシングルトンの構造が述語論理のモデルにならない場合。 1階論理に「<」のような非反射的順序を示す2項述語記号が デフォルトで定義されてる。 このとき∀a∀b(a<b)が1階論理のformulaだとしよう。 例えば構造の領域を{0}にする。 ∀a∀b(a<b)でa、bが変数だから、 {0}で解釈すると0<0、反射的でないので偽。 そもそも俺っちが言いたいのは1階論理とは何か? どの述語・関数記号、公理図式・推論規則を含むもののことか? っつーことなんです><;
当たり前のことだが、1階の述語論理といえば、論理に関する公理以外 含まないものをいう。 ∀a∀b(a<b) なんていうのは、論理以外の公理である。ただ、699 に書いてあることは、 論理と構造の関係がわかっていないことが顕わとなっている。 < がどう解釈されるかは自由なのだから、それでは偽となるとはいえない。
Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo
Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo
Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk
[11/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk
[13/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk
[13/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk
[13/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk
また「おかしい君」=
>>686 が訳分かってないで騒いでるよ。
>>29 に至る話の流れを見てからにしろよな。
述語論理の解釈に集合論使ったら循環論法だのなんだのって話だったとこから
(これについての是非はおいておくが)
述語論理の無矛盾性は集合論を使わなくてもできるっていうのが
>>29 だろ。
だからみんな解釈とか持ち出さなくていい
シンタクティカルな無矛盾性の証明方法を教えてた。
1点からなる構造で解釈なんて、失笑しか起きないぜ。
>>701 のレスは自分で話の流れを理解してませんと白状しているようなもん。
もっとも
>>699 も理解してないようだがな。
またおかしい君か
[261036暗号] [13/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk [10] 二喬 黒い三連星 ファンタスティックフォー
>>709 >1点からなる構造で解釈なんて、失笑しか起きないぜ。
Gentzen を笑ってやってください.
[261036暗号] [13/26] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Run Swim Tokyo Walk [10] 二喬 黒い三連星 ファンタスティックフォー
F先生祭りで大活躍だったおかしい君、今回も期待しとりまっせ!
715 :
676 :2011/08/26(金) 07:25:48.28
>>700 いいえ、私の例では、<がどう非反射的順序と解釈される
と言いたかったのではありません。
例えば、
|= x<y ←→ x≠y∧∃a(x+a=y)
のような論理的同値が1階論理にあったら、
{0} |= 0≠0
が出てきますよね。
つまり1階論理の公理図式や推論規則の取り方で
モデルができないように何とでもできちゃいますよねってことです///
716 :
sage :2011/08/26(金) 08:39:46.80
> |= x<y ←→ x≠y∧∃a(x+a=y) > のような論理的同値が1階論理にあったら、 なんて言葉遣いは普通はしない。 理論の公理にこのような論理式が含まれたら、と言いたいんだろうけど 今は他の人は、(たとえばトートロジーが推論規則のみから導かれるように) 公理無しで推論規則のみから⊥が導出されてしまう可能性が あるかどうかの話をしている。 あと普通非反射的順序と言ったら 実数の上の順序(R, <)とか集合代数の上の順序(P(X), ⊂)とか そういうのも当然入ると思う。
>709 1点集合といった途端に集合論だと思うおバカだね。 712 にも書いてあるが、Gentzen を読め。
[自己定義] ❶名前 ❷科目 ❸他者 ❹グループ ❺用語集 [❶名前] TS10 Tokyo Sterben つっちぃ しんちゃん 東京ステルベン 東京捨便 ウンコの神様 全てを水に流す男 全てを水に流す男の子 全てを水に流す男子
[❷科目] Arcade Bike Combat Eminem Football Girl Home Justice Marvel Nostalgia Otaku Run Swim Tokyo Walk
720 :
132人目の素数さん :2011/08/26(金) 15:22:11.19
変な箇条書きみたいなものが増えたんだけど アホが数学板に住み着いているの?
>>717 Genzenは有限の立場の問題。だから有限なら集合を使っても良い。
>>29 までの話の
722 :
721 :2011/08/26(金) 15:48:48.38
(...途中途切れた) 集合概念を使うかとは別の話だ。
俺も
>>29 の「述語論理の無矛盾性は自然数論で証明できる」への質問だから、
自然数論内での無矛盾性の証明を聞いているんだと思った。
でも「1点からなる構造で解釈すれば」ってところを自然数論内部で形式化するのは結構面倒で
>>686 が「こんなことを押さえていないで」っていうほど簡単ではないし、
カット除去の方がはるかに簡単。
まあでも
>>676 は「自然数論での証明」を聞きたいわけではなさそうだし、
いいんじゃないの?
>>722 >>30 とか見ると、集合概念を使うかじゃなくて、意味論を使うかどうかが問題なんじゃね?
29より後のレスだけど
[自己定義] 名前 科目 他者 グループ 用語集
【自己定義】 名前 科目 他者 グループ 用語集
1点構造で解釈するというのは言葉のアヤで、解釈というほどのものでは ない。ただ対応を定義するだけで、集合概念など無関係。カット除去定理 などよりは遥かに簡単なもので、LK でなくても、他のまともな論理体系 でも推論規則あるいは公理にあわせ簡単に述語論理の無矛盾性が示せる。 これは、数理論理学の基本常識。
728 :
676 :2011/08/26(金) 18:58:29.59
1点構造で解釈するとモデルができると言う主張は、
大抵の集合演算が1点だけをつかうと
1かつ1は1、1または1は1、1の否定は1・・・のように、
命題が全部恒真になるってことに起因していると思う。
いかに論理記号として可算無限個の変数を1階論理がもっていようと、
領域が1点の構造で解釈したら大抵モデルになるってのは想像がつく。
一方、わしは一般に述語論理において、
閉論理式Aと¬Aが同時に証明されることはない。
という定理が存在しているとでもいうのか?と疑問に思った。
述語論理の公理図式や言語のもつ記号なぞは人の数だけあるのに、
どういうアイディアで証明するんじゃろう、
そう思ったわけじゃ。素人はみな同じように考えるんじゃけのぉ?
>>716 合点
普通、述語論理の無矛盾性として教科書に書いてあるのは、 Gentzenのシーケント計算は 下の式に⊥があれば上の式にも⊥が出て来るという性質をもっているので 公理が何もなければ⊥は導出できない、というような議論だと思う。 「一点構造で対応を定義する」ということで具体的に どういう対応のことを想定しているのか良く分からない。
>>727 >>29 までのコンテキストでわざわざそんな言葉のアヤに気づかずそのままにしてるってのは
何も分かってないかコンテキストを理解していなかったかのどっちかだろ
>>723 カット除去の方法と解釈を使う方法と、
どっちが自然数論内部で形式化しやすいかは趣味の問題じゃない?
どっちにしろ
>>686 がいうようには簡単じゃないけどね
あと確かに初学者には前者(カット除去)がお勧めだな
後者は形式化されたメタ理論と対象理論を行ったり来たりなので混乱しやすい
前者はきっちり分けて考えられるので初学者にはこちらの方が学びやすいと思う
おかしい君と767がどっちも「自然数論で証明できる」って文脈を見失ってたってことで解決! おかしい君が話の流れ理解しないで的外れなこと言うのはいつものこと。 今回は質問者もそうだったので、彼のはずれっぷりが良いほうに転んだってこと。
>>731 > カット除去の方法と解釈を使う方法と、
> どっちが自然数論内部で形式化しやすいかは趣味の問題じゃない?
simple type theory の場合、前者はできない、後者はできるという違いがありますが。
> どっちにしろ
>>686 がいうようには簡単じゃないけどね
簡単にできますよ。論理式を書き換えて命題論理に還元するだけ。
>733 ちゃんとわかってる人がいて安心しました。
>>733 731が言うように混乱している人発見!
>簡単にできますよ。論理式を書き換えて命題論理に還元するだけ。
その還元を自然数論内部で形式化するのが大変なんだが。
733と675にシツモソ: 1階述語論理の無矛盾性が命題論理の無矛盾性に帰着されるのはいいんだけど そんで命題論理の無矛盾性はどうやって証明するの?
>simple type theory の場合、前者はできない、後者はできるという違いがありますが。 「この拡張には前者ができて後者はできない」 「あの拡張には後者ができて前者が出来ない」 「その拡張には(ry」とかの言い合いになりそうなヨカン
>>736 カット除去、またはすべての命題変数を真で解釈する。
>>738 それじゃ
>>733 の言ったこと意味なくね?
>>723 と
>>731 の内容で「一階述語論理」を「命題論理」に置換してもその通りだと思うし:
731':
カット除去の方法と解釈を使う方法と、
どっちが自然数論内部で形式化しやすいかは趣味の問題じゃない?
どっちにしろ
>>686 がいうようには簡単じゃないけどね
あと確かに初学者には前者(カット除去)がお勧めだな
後者は形式化されたメタ理論と対象理論を行ったり来たりなので混乱しやすい
前者はきっちり分けて考えられるので初学者にはこちらの方が学びやすいと思う
とすると
>>733 の「命題論理」は今度は何に置換すればいいんだ?
>>733 と
>>736 以降の流れにワロタ!
別の目的と別の文脈でGenzenがやったことを見て(恐らく解説を読んだ程度で)
それが絶対だ!と思っちゃったんだろうねw
741 :
671 :2011/08/28(日) 08:57:33.41
まぁ俺の質問に答えられずに AFAがどうとかGentzenの無矛盾性証明論に話題を逸らす人間ばかりだから。
742 :
671 :2011/08/28(日) 09:02:25.77
誤爆。上記書き込みは無視でお願いします
覆水盆に返らずという言葉がありましてね、
×誤爆 ○自演失敗
>>671 釣られて答えてやろう。可能性はゼロではない(斑目)
そもそも逆数学の目的がそういうものではないからなあ。 ただ公理に対する知識が凄く高まっているのは確か。 ヒルベルト先生もあの世で喜んでいるだろう。
マジレスすると、解釈を使って述語論理の無矛盾性を自然数論内で証明するには
>>733 が言うようにいったん命題論理に還元してからにしても直接やるにしても
ゲーデル数で表現された対象レベルの論理式の真偽を、
(形式化された)メタレベルで真偽を論じられる論理式で表現しないといけない。
つまりメタレベルの真偽と結びつけることが必要。
これを
>>731 は「初学者が混乱しやすい」と表現したのだろうし、
この意味で「解釈」は
>>727 のいうような「言葉のアヤ」ではなく
本質的な解釈、意味論の概念に本質的に依存しているのである。(なぜか論文調)
>>747 命題論理を自然数論に取り入れることをするのなら、特段難しい
ことではない。もともと、論理体系を自然数論にとりいれること自体
マジめに考えれば、面倒なことで、本当に計算機で動くようになる
のはもっと大変。
真偽は論じる必要はない、ただ対応を書くだけ。
>命題論理を自然数論に取り入れることをするのなら 相対無矛盾性を出す議論ともゲーデル数を直接扱う無矛盾性を出す議論ともとれる こんな言い回ししている時点で話にならんな。 >ただ対応を書くだけ これも相対無矛盾性の議論と勘違いしてるんじゃないかと思われる。
>>749 命題論理に domain なぞ必要ないぞ、バカ
>>750 自分で実際に手を動かして無矛盾性証明書いたことなくて、
どこかの解説書に「出来る」と書いてあるのを読んだことしかない奴等に言っても無駄だよ。
「初学者が混乱しやすい」どころか専門家でもしょっちゅう混乱してるしね。
どうも「モデルが存在すれば無矛盾」とか条件反射的に覚えているっぽいんだけど、
自然数論みたいに弱いメタセオリーだと「どういうモデルか」が問題なんだけどね。
(ZFCがメタセオリーの場合も、クラスサイズのモデルは相対無矛盾性にしか役立たない、のと同じ。)
>>命題論理を自然数論に取り入れることをするのなら >相対無矛盾性を出す議論ともゲーデル数を直接扱う無矛盾性を出す議論ともとれる どっちとも取れるというより、俺には前者の解釈しかできないな、「取り入れる」では。 一字一句にケチつける類の議論はしたくはないけれど、 748の頭の中にある議論は自然数論の無矛盾性に相対的な無矛盾性しか言えてないと思われる。
755 :
132人目の素数さん :2011/08/29(月) 00:03:42.27
専門家でも混乱したりミスすることってあるんですか?
有限と無限で違うと呪文のように唱えても説得力ないよ! どう違うのか説明できないようじゃ。
>755 そらあるよ、専門家だって人間だもん。 特に「モデルが存在すれば無矛盾」って勘違いするのはよくある間違いで この含意が言えないような弱い理論の内部での無矛盾性証明を モデルの存在を示しただけで終らせてしまうようなのを結構見かける。 ひどいのでは、ZFCでクラスサイズのモデルの存在を示して無矛盾性を導いていたり。
一階述語論理や命題論理の解釈による無矛盾性証明が、
自然数論内で出来るか出来ないかで議論になってるんではなくて、
>>686 が相手をバカにしたほど簡単かで議論になってる、
というのは不毛に見えなくもないのだが。
有益な議論にするために、どれくらい弱い自然数論の内部でいえるか
という議論にしてみてはどうか?
>758
相対的な無矛盾性証明と絶対的(?)な無矛盾性証明の違いとか、
セットモデルとクラスモデルの違いとかなかなか有益な話になっているじゃないか。
相手方が「無限じゃない」という呪文を唱えるしか能がないのが残念だが。
>
>>686 が相手をバカにしたほど簡単かで議論になってる
俺はその証明に使われる「解釈」が単なる「言葉のアヤ」なのか
本質的に意味論的なものなのか、という議論だと理解している。
既にたくさん
>>748 への批判が出ているから
重複になるかもしれないので恐縮だけど、748に質問:
>真偽は論じる必要はない、ただ対応を書くだけ
自然数論の中で命題論理の無矛盾性を示すには、
「xがコードしている論理式は真」っていう論理式(真理述語っていうの?)を作って
この論理式を証明の長さ(高さ?)に関する帰納法で証明していくんだよね?
真理述語って思いっきり真偽を論じていると思うんだけど?
対応を書くってどういうこと?
ロジックって、与えられた弱い体系から証明できないような命題を あまりにも直観的に自明だから当然成り立つだろうと思って、 仮定してしまう、という間違いが多いと思う。 そういう場合往々にして、〜〜が証明できるのは自明、なんて書いてあったりする。 事実に反する間違いに限って自明だということになっていたりするのはロジックに限らないだろうけども。 新井先生の「数学基礎論」のBSの件もそうで、 元ネタのDevlinから間違いを引き継いでいて (集合論の専門家が何人もチェックしているのに!)見逃している。 良くテキストに、完全性の逆の健全性のほうは自明だから良いでしょう、 とか書いてあることがより弱い体系での証明を考える際に本質的障害になる。
命題論理のカットのない体系を、自然数論で形式化しようとすれば 結局ゲーデルの不完全性定理の証明と同じ筋をふむことになる。 つまり原始帰納述語を自然数論で表現することをする。だから、 一般に形式化することは、面倒なのでは?
素因数分解の存在と一意性の証明程度には面倒でしょうね。 面倒と難しいということは別ですが。
>752 真理述語が定義できるモデルが、絶対的な(と言っていいのか?)無矛盾性を導けるモデルで 真理述語が定義できないモデルが相対的な無矛盾性証明にしか役に立たないモデルですね。 自然数論での無限モデルやZFCでのクラスモデルは、 一般には部分的な真理述語しか定義できないから無矛盾性は導けない。 有限モデルやセットモデルは、それぞれの形式体系で真理述語が定義できるので導ける。
>>764 そう、真理述語というか充足関係というか「解釈」を形式化した論理式の性質が重要。
もう一つ、この論理式に帰納法が適用できる、という条件も必要。
だから自然数論での無限モデルでも、ZFCでのクラスモデルでも、
これらの条件を満たせば無矛盾性が導けます。
領域が有限か無限かは余り本質的ではなく(述語論理か命題論理かも余り関係ない)
この真理述語の性質がクリティカル。
どういう述語を考えているかは、とうの昔に答えてあるんじゃないの?
無矛盾性を示したいのなら、真理述語である必要はないし。
述語論理は理解していると思っていたけど このスレみてたら勘違いだった。
知り合いのプログラマーによると チューリングの停止問題と ゲーデルの不完全性定理が数学的に等価ということですが この等価性は定理としてあるんでしょうか?
>>766 「対応がどうの」と言ってる
>>727 とか
>>748 のこと?
俺、エスパーじゃないんで、何言ってるのか分からんかったよ。
>>729 と
>>760 で二回も質問されてるけど、それ以上の説明なかったし。
誰かエスパーいない?
>>765 の言ってることと同じだったわけ?
そんでそれは、本質的に「解釈」というほどのものじゃなくて
言葉のアヤっていえるようなものだったわけ?
>767 他にどんなのならいいの?
772 :
272 :2011/08/30(火) 01:49:55.03
結局AFAの話は、FA派の惨敗ってこと? AFA派の圧勝という理解でよいの?
>772 スレ読んで自分で判断しろ。 AFAとFAを止揚する解がどっかにあるんだろうけど。多分。
272+500=772 記念のネタと思われ 結局 AFA では500もレスを消費しなかったと
>>771 以下の条件を満たしていれば何でもよい.
表現可能、演繹について閉じている、自明でない。
>775 具体的には?
>769 二つの数学の定理が同値、という場合、その同値自体はいい加減なもので、 厳密な数学的定理というわけではない。 なぜなら、厳密にいうと定理は真なので、自明に同値となってしまうから。 この問題を解決して厳密な数学の定理にするには、逆数学みたいに、 どちらの定理も導けない弱い理論をベースにするとかしないと無理。
Uは空でない集合、φ(x)、ψ(x)はxに関する条件とする。 φ(x)⇒ψ(x)と∀x∈U(φ(x)⇒ψ(x))のVenn図における違いがどうもよくわからんのだが
えっ?釣り?マジ?数学初心者スレへ逝け
780 :
132人目の素数さん :2011/08/30(火) 19:49:19.05
>>777 通常の数学で
停止問題から不完全性定理が証明できたり、
その逆を証明出来たりしますか?
>>780 構造は同じなので、統一した形式で証明したい場合、
決定問題のTuring受理性に帰着させるのが良いと思う。
チャイティン先生はベリーのパラドックスに関連させて、
2つの証明の類似性を指摘していた。
ちなみに同値とは言いがたい。そもそもドメインが違う。
>>780 777の意味分かってる?
不完全性定理は通常の数学で仮定なしに証明できるのだから
停止問題を仮定しても証明できるっしょ
仮定は必ず使わなければならないっていう関連性論理とかなら別だけど
(弱いベース理論の替わりに関連性論理でも777の問題を避けられるな)
>>767 =
>>775 766が折角指摘してるんだから「帰納法が成り立つ」って条件を忘れるなよ。
それともこの条件は不要だと言いたいのかい?
それはともかく、そういう条件を満たす述語があれば無矛盾性が導けるってのは
命題論理に限らず述語論理でも自然数論でもZFCでもすべてそうだろ。
>>733 の通りに命題論理にまで還元したからって何も変わらないない。
自然数論やZFCには「言葉のアヤ」でない真理述語しかないけれど、
命題論理なら真理述語以外にも具体的に作れるっていうことかい?
幾らその条件を満たせば何でもいいと言ったって
具体例が真理述語しかないのなら意味がない。
>>776 への回答を期待しているぜ!
785 :
784 :2011/08/31(水) 06:24:19.59
間違えた ×766 ○765
>>784 >自然数論やZFCには「言葉のアヤ」でない真理述語しかない
そんなこと,どこにも書いていませんが.
>>784 >
>>767 =
>>775 >766が折角指摘してるんだから「帰納法が成り立つ」って条件を忘れるなよ。
>それともこの条件は不要だと言いたいのかい?
帰納法が必要なのは「演繹規則について閉じてる」から
「(超準的な)演繹について閉じている」を示す部分だから必要ないのでは?
まあ
>>775 の書き方だと標準的な演繹だけとも読めるので、
その違いが正に問題になっているときにそんな書き方するなよ、
ということなら
>>784 に賛成する。
>その違いが正に問題になっている え?そうなの?「超準的」なんて初めて出てきたと思うけど
どっかの本で仕入れた知識をそのまま開陳しているだけで 文脈に合わせて適切な言い方をするとか高等なことできないんだろ
790 :
132人目の素数さん :2011/08/31(水) 18:53:51.89
命題論理のコンパクト性定理の証明なんですが、 「Σの命題を同時に真にする真偽値関数が存在しない」 から、 「すべての命題がΣからのトートロジー的帰結になる」 が得られるのは何故でしょうか?
>>788 問題なのは論理式の全体が無限で、証明の全体も無限ということ。
従ってメタレベルから見ると超準的な論理式や証明が出てきてしまう。
理論T1に相対的なT2の無矛盾性証明ならメタレベルの問題に過ぎないが、
理論T1内部でのT2の無矛盾性証明をするにはT1がメタレベルになるので
超準的な論理式や証明をT1の中で処理しないといけない。
その為に真理述語か
>>775 や
>>787 の条件を満たす述語が必要になる、
というのがこれまでの流れ。
標準的な論理式や証明しか処理できない場合、
相対的な無矛盾性証明にしかならない。
自然数論での述語論理の無矛盾性の証明は
命題論理に置きかえれば簡単と言ってた
>>733 はどこ行った?
述語論理から命題論理に還元しても
真理述語(かそれっぽい述語)を作らなきゃいかん
っていう一番のポイントは何も変わっとらんじゃないか!
そもそも自然数論とかの無矛盾性でいうモデルの話と 一般のn項述語記号を用いた素の述語論理の無矛盾性は違う話だと思う
なんか標準的な論理式や証明を「処理」した後に さらに超準的な論理式や証明も「処理」しないといけない、 みたいに書いてるけど、 そもそもT1の中でstandardな自然数とnonstandardな自然数を区別できる訳じゃなくて あくまでT1の外から見たとき初めて分かる違いに過ぎない。 「超準自然数回の演繹について閉じている」と 「演繹規則の有限回の適用について閉じている」の区別も同様で、 T1のなかでそういう区別はできないから、T1の中でのT2の無矛盾性証明を考えるときに 後者は示せるが前者は示せないとか言うのはナンセンスに近い。 そのような外延的な言い方よりも、どっちかというと 数学的帰納法における自然数の「性質」を表す述語Pが 充分多くないから非標準的構造をの可能性を排除できないと内包的に言う方が正しいように思う。
ある証明が標準的かどうかなんて趣味というか主観の問題。
>>786 それも「っていうことかい?」演算子のスコープに入っているのでは?
>>791 論理式や証明を扱うのがメタレベルなら、
超準的な論理式や証明が出てくるのはもう一つ上のメタメタレベルでは?
>>794 がいうように何か変。
>>794 最後の3行、まじ日本語でok
>>795 釣りか?マジなのか?
>793 君が思うのは勝手だが、根拠も何もなければ他の人は反応のしようがないぞ どんな反応が欲しいのかは知らないが
>>794 >「超準自然数回の演繹について閉じている」と
>「演繹規則の有限回の適用について閉じている」の区別も同様で、
>T1のなかでそういう区別はできないから、T1の中でのT2の無矛盾性証明を考えるときに
>後者は示せるが前者は示せないとか言うのはナンセンスに近い。
T1に対するメタ帰納法(
>>796 に従えば「メタメタ帰納法」)で示した場合、
後者の証明にはなっているが後者の証明にはなっていない、と言える。
よってその帰納法がT1の内部のものかどうかが重要な分かれ目。
799 :
798 :2011/09/01(木) 06:10:32.04
寝ぼけてるな、スマソ × 後者の証明にはなっているが後者の証明にはなっていない ○ 後者の証明にはなっているが前者の証明にはなっていない
「通常の数学」って何だよ
>「超準自然数回の演繹について閉じている」と >「演繹規則の有限回の適用について閉じている」の区別も同様で、 いやそもそもその区別っていうのがおかしい。 「演繹規則の有限回の適用について閉じている」という表現では 「超準自然数回の演繹について閉じている」ということなのか 「標準自然数回の演繹について閉じている」ということなのか どちらとも読めるから適切な言い方ではない、という話だったはず。
おっ!珍しくおかしい君がまともなことを言っている。
>>792 733が言ってたのは、証明の主要部分とは少なくとも言えませんね。
問題の先送りとでもいうか。
ついでに言えば733に賛同していた734もどこへ行ったのやら。
805 :
132人目の素数さん :2011/09/02(金) 03:35:06.57
まとめると、領域が有限になっても(あるいは命題論理みたいに領域がなくなっても) 論理式の全体や演繹の全体が無限であることに変わりなく、 それが無矛盾性証明の形式化をしようとする際に気をつけなければいけない点ということだね。
超準自然数と標準的自然数の違いを そんなに気にしてるのは約一名だと思う
>>777 とりマセさんが、不完全性定理と停止問題の関係をtwitterでつぶやいているよ
逆数学的には同値ではないっぽい
810 :
777 :2011/09/02(金) 23:10:08.07
そうみたいですね。 停止問題の方が強いと思ってたんですが、 実際は不完全性定理→停止問題は決定不可能 みたいですね・・・。 あとで証明してみようと思います。 チューリングマシンの停止問題の決定不可能性からRE等への間辺りが 自分の問題意識だったみたいです。
812 :
769 :2011/09/03(土) 00:02:14.35
>806 無矛盾ということを書こうと思えば、カットがあろうとなかろうと、 無限個ある証明を対象にするのだから、当然なことだ。コード化する とき数値的表現可能性に関する部分が、原始帰納的述語で書くことが 簡単に思い浮かぶ範囲、例えば、有限な対象領域なら問題ない。 このようなことを、簡単だ、常識だといっているのではないでしょうか? これを難しいというなら、一般に形式化すること自体難しいといっている のと変わらないと思いますが、、、。
自然数論で述語論理の無矛盾性を証明するのに、 「カット除去なんかより1点構造での解釈を考えた方がはるかに簡単」派と 「いやカット除去と1点構造での解釈を考えるのは同じくらい面倒」派の議論が発端だったのだから、 後者は結局のところ「一般に形式化すること自体難しい」と言いたいのでは? 俺はそんなことより、1点構造での解釈は、意味論というほどのものでもない、 という前者派の一部の主張を詳しく知りたいのが。
AFはアメリカ留学中初めて体験した。
>>782 超限帰納法が重要になる議論を、余帰納法に置き換えてもほぼ同様にできる、
というのはその手の業界ではよく知られた話。
FAが∈に関する帰納法を許し、AFAが余帰納法を許す公理だと考えれば至極当然のこと。
むしろ余帰納法ではダメだという例をきちんと示すほうが大発見。
よくFA派の人が「この論法はFAを本質的に使うからAFAにすると困る」みたいなことを言ってるけど、
本当に余帰納法に置換えてやろうと試してみたのかよ、と突っ込みたくなる。
停止問題を持つ形式体系は全て不完全である。
>>809 とりマセ氏は
「停止問題が決定不可能である」ということを知っていても「ACA_0 は RCA_0 より真に強い」ということしか導けません
とか
「ゲーデルの不完全性定理」を知っていれば「WKL_0 は RCA_0 より真に強い」ということを導ける
とか言っているので、
>>777 の言うのとは少し違うんじゃ?
>>777 のは、
「停止問題が決定不可能である」は ACA_0 と RCA_0 上同値
とか
「ゲーデルの不完全性定理」は WKL_0 と RCA_0 上同値
とかそういう話でしょ。いやその同値が正しいのか知らないんだけど。
>816 AFA で何が出来るのかよく知らないで AFA を批判する人がいるってことだね。 別に AFA に限った話じゃないような。
820 :
あんでぃ :2011/09/05(月) 16:25:15.68
[T4RM] Tokyo 4units Re Money game [T4RM]
821 :
769 :2011/09/05(月) 20:29:49.73
田中の数学基礎論講義の PartA最初のページの問1、 「ある形式体系Tで論理式∃xA(x)が証明できても A(t)が証明できるような項tが存在するとは限らない。 そのような体系Tと論理式∃xA(x)の例をあげよ。」 の解答お願いします。
それだけだとZFCのφとか{φ}とかωとか2^ωとかω1とか 無数にtrivialな例があるんだけど、 本当はHerbrandの定理とかの話とはちょっとズレるんだよね
823 :
132人目の素数さん :2011/09/05(月) 21:18:29.14
>>822 その下に
「上の問題ができないと、ヘンキンの定数記号を用いた
完全性定理の証明は何をやっているのかわからないと思う」
とありました。
私は形式体系に関数がなければ良いだけと思うんですが。
その本では定数(constant)記号は関数記号の一種として扱ってるのかな?
825 :
132人目の素数さん :2011/09/06(火) 07:17:21.03
アリティー0の関数を定数としていますね。 項の定義は、 変数記号と、変数記号を引数に持つ関数記号ですね。
826 :
132人目の素数さん :2011/09/06(火) 18:44:59.57
完全性定理の後に答え載ってました(爆 A(x)≡(x=0∧σ)∨(x=1∧¬σ) でしたね(^^;
あくまで答の一例だからね
>826 σか¬σが証明可能なセンテンスならダメじゃないか。
829 :
132人目の素数さん :2011/09/06(火) 23:14:54.22
>>828 σと独立な形式体系という条件を忘れてました。
良くわかりましたね(^^;
830 :
132人目の素数さん :2011/09/07(水) 08:35:29.09
>829 σ と 独立な形式体系という2つの組の例をあげないと答えにならないのでは、、、。 そのような例をあげることができる人には、(x=0∧σ)∨(x=1∧¬σ) もわかる からヒントになっているのかな?
831 :
132人目の素数さん :2011/09/07(水) 18:33:20.47
>>830 私はよくわかりませんでした。
算術の公理系Tは
σを証明も反証もできない、さらに0と1を定数として持つ。
A(x)←→(x=0∧σ)∨(x=1∧¬σ)
とおくと
T |― A(0)∨A(1)
だそうですが、なぜこれが証明できるのか不明ですね。
トートロジーだろうが
σがどんな式だろうが σ∨¬σは証明できる
834 :
132人目の素数さん :2011/09/07(水) 21:12:05.30
つまり、 T |― A(0)∨A(1) でA(0)は¬A(1)だとでも言うのでしょうか?
>831 独立命題というと難しいものしか思い浮かべられないかもしれません。 しかし、公理系が弱ければ弱いほど、独立命題は増えるわけです。 ですから、形式体系として述語論理そのものを選んでもよいのですが、 算術の体系 T をとりましょう。そして、それに P(x) という述語を付け加えた 体系 T_P を考えます。すると、∃x P(x) は述語 P の解釈により、正しい場合も 間違っている場合もあります。つまり独立命題です。
ZFのスコーレム化ZF^skは ∀x∃yφ(x,y)から∀xφ(x,f(x))が導ける訳なので ZFCと実質的に同じものですよね?
>>835 その本では等号に関する公理は素の述語論理に含まれている?
というか独立な「文」でないといけないの?
自由変数が現れている論理式は演繹関係の対象外?
正確に言うと擬トートロジー(quasi-tautology)だな
A(0)∨A(1)は述語論理の規則のみで証明できる。
>>834 は不完全性定理について書いた本じゃなくて
述語論理のみについて丁寧に書いた本を一冊読んだ方が良いかもしれない。
>>836 その通りです。
ZFにスコーレム関数を付け加えると
選択公理が証明できます。
841 :
132人目の素数さん :2011/09/08(木) 22:00:46.95
>>839 述語論理の本も並行して読んでるんですが
この論理式がどうしても公理から出せないんですよね・・・。
(0=0)∧(1=1)∧(σ∨¬σ) ------------------------ ((0=0)∧(1=1)∧σ) ∨ ((0=0)∧(1=1)∧¬σ) --------------------------------------- (0=0∧σ)∨(1=1∧¬σ) ----------------------------------------------- (0=0∧σ)∨(0=1∧¬σ)∨(1=0∧σ)∨(1=1∧¬σ) これすなわち A(0)∨A(1)
等号公理は使っているわな
>843 = という記号を使って、等号公理を使わないのなら = という記号 を使わないのが当然。
845 :
132人目の素数さん :2011/09/09(金) 08:03:03.80
わしの本では x=xと x=y→A(x)→A(y)は公理あり
847 :
834 :2011/09/09(金) 19:01:47.87
ウシュカヴィッツの公理系とかいうのが使われてますね。 |―A ⇒ |―A∧A の証明もままならないですね(^^;
>>846 確かに、いわれるとおりですね。きっとわかっていないでしょう。
849 :
834 :2011/09/09(金) 22:24:12.19
(^^; (^^; (^^; (^^; (^^;
なんかみんな x=x のことを「等号公理(equality axiom)」って言ってるみたいだけど、それは x=y→A(x)→A(y) のことだよ。 x=xのほうは「同一性公理(identity axiom)」な。
851 :
834 :2011/09/09(金) 22:40:28.77
すいませんが 日本の本でヒルベルト流の推論体系に 詳しいのがあったら教えてもらえませんか。
おっと、専ブラの仕様で 名前欄になぜか834と 別の人のレス番が出てしまった。
( ´_ゝ`)フーン
本人登場か
>>850 両方あわせて「等号公理」と呼ぶ流儀も標準的かと
856 :
132人目の素数さん :2011/09/10(土) 07:44:18.11
T |― A かつ T |― B ⇒ T |― A∧B ウシュカヴィッツの公理系で証明よろ。
>>855 そうなのか?「等号に関する公理」と呼んで総称するならわかるが。
>>856 ぐぐっても何にも出てこん。解説よろ。
858 :
132人目の素数さん :2011/09/10(土) 09:00:00.06
>>857 ウシュカヴィッツの公理は、
P1.x→(y→x)
P2.(x→(y→z))→((x→y)→(x→z))
P3.(¬x→¬y)→(y→x)
にMPを追加したものですね。
>>856 はたった今自己解決しましたが。
補題として、|― x→xが出る。
|― A、|― B と仮定する。
P2から、((A→¬B)→(A→¬B))→(((A→¬B)→A)→((A→¬B)→¬B))
補題から、(A→¬B)→(A→¬B)
よってMPによって、((A→¬B)→A)→((A→¬B)→¬B)-----@。
一方P1から、A→((A→¬B)→A) だが、仮定より、(A→¬B)→A-----A。
そして@とAについてMPを使えば、(A→¬B)→¬B。
P3を使って対偶をとると、B→¬(A→¬B) だが、
仮定によって¬(A→¬B)。
¬(A→¬B)≡¬(¬A∨¬B)≡(A∧B)
よって |― A∧B。(^^;
いつの間にか練習問題レベルの話題になっているが、もともとは
>>821 が最初だったよな。
それに応えて
>>822 がHerbrandの定理のことにちょっと言及してるけど、実は何の関連が
あるのかさっぱりだった。
Herbrandの定理とどう繋がるのか誰か教えてくれない?
860 :
132人目の素数さん :2011/09/10(土) 09:24:16.99
>>821 の言語では定数(項)として0,1をもち、
T |― ∃xA(x) ⇒ T |― A(0)∨A(1) が成り立つ。
エルブランの定理は上記を一般化して、
言語Lの理論Tで、T |― ∃xA(x) ならば、
Lの有限個の項t0,t1,...,tnについて、
T |― A(t0)∨A(t1)∨...∨A(tn)。
このとき必ず T |― A(t) (項tが1個だけ)となる保証はない。
そのため、完全性定理の証明でヘンキン定数を
わざわざ付け加える必要があるということが言いたかったのでは?
861 :
859 :2011/09/10(土) 09:34:09.72
>>860 おお、Herbrandの定理とかConsistencyTheorem(Hilbert-Ackermann)とか
何を言わんとしているのか良くわからなかったんだけど、少し見えてきた。
ありがとうございます。
862 :
132人目の素数さん :2011/09/10(土) 11:33:43.67
>>842 (0=0∧σ)∨(1=1∧¬σ)
-----------------------------------------------
(0=0∧σ)∨(0=1∧¬σ)∨(1=0∧σ)∨(1=1∧¬σ)
これの詳細よろ(^^;
>>862 直接
A
-------
M∨A
が認められてる体系なら
A∨B
-------------
A∨M∨N∨B
は明らかだけど、あんたの体系ではどうなのさ?
865 :
132人目の素数さん :2011/09/10(土) 19:45:08.66
>>840 嘘付け
スコーレム閉包とっても元の体系の保存的拡大にしかならん
>ZFにスコーレム関数を付け加えると をどう解釈するかですな。 スコーレム化のことなのか、公理図式にスコーレム関数が現れる論理式を許すのか。
>>866 前原のイプシロン定理のことをいっているのなら,それは公理のない場合だけ.
ZFなら当然,選択公理が導かれる.それについて間違った論文もすでに
有名なジャーナルから出版されている,
その間違った論文の書誌情報kwsk
ZFのスコーレム化では、スコーレム関数は分出公理や置換公理の論理式には現れてはいけないわけだが
どうやって(スコーレム関数なしの言語で形式化された)選択公理を導くのか説明キボンヌ
>>836 の
>∀x∃yφ(x,y)から∀xφ(x,f(x))が導ける訳なので
っていうfは、集合としてこのfのグラフは定義できないんじゃね?
(適当な集合サイズの定義域に限定しても。)
{<x,y>|y=f(x)}ってスコーレム化前の言語では定義不可能だから
分出公理の適用外だと思うんだけど。
>>868 は「当然」と言っているけど確かにどう当然なのか分からんな
868はもう寝ちまったのか それともいま焦って本をひっくりかえしているのか
非論理的公理のない体系をスコーレム化しても意味ないような。
>>868 は
>>867 を読んでから書いているはずだから
そんな単純な間違いはしていないと思うのだが、、、
結局 ZF^{sk} は ZFC を含むの?
868は直前の
>>867 を読んでも理解できずにそのまんまの間違いをしたんだろ
かいわいそだからこれ以上追及すんなや
870に書いてある分出公理の論理式に、新たな論理式を加えなければ保存 となることはよく知られている。だから「前原のイプシロン定理」に 触れているんじゃないでしょうか?
>>877 分出公理だけが問題か?置換公理に加えても保存性は崩れない?
868のいう間違った論文って868が間違ってるとおもってるってだけじゃね?
>>878 http://plato.stanford.edu/entries/epsilon-calculus/ に Hilbert の
Second epsilon theorem: Suppose Γ ∪ {A} is a set of formulae not
involving the epsilon symbol. If A is derivable from Γ in the epsilon
calculus, then A is derivable from Γ in predicate logic.
というのがあります。
Maehara showed how to prove the second epsilon theorem using cut
elimination, and then strengthened the theorem to include the schema
of extensionality, in
って書いてあります。ですからそのことではないでしょうか?
間違った論文のことはわかりませんが、、、。
>>878 http://plato.stanford.edu/entries/epsilon-calculus/ に Hilbert の
Second epsilon theorem: Suppose Γ ∪ {A} is a set of formulae not
involving the epsilon symbol. If A is derivable from Γ in the epsilon
calculus, then A is derivable from Γ in predicate logic.
というのがあります。
Maehara showed how to prove the second epsilon theorem using cut
elimination, and then strengthened the theorem to include the schema
of extensionality, in
って書いてあります。ですからそのことではないでしょうか?
間違った論文のことはわかりませんが、、、。
>>879 置換公理というのが何をさしているのかわかりませんが、Zermelo の公理系で
分出公理を置換公理で置き換えたのが ZFC だから、その場合の置換公理は、他
の公理も使えば分出公理より強いので、何をいっているのかわかりません。
そうでないのなら、上記の URL で調べてみては、、、。
>>881 あのね、置換公理の標準的な定式化には二つあってね。
強置換公理と呼ばれる方は分出公理を導くので「Zermelo集合論で分出公理を置換公理で置き換えたのが ZF」と言える。
もう一つの定式化では分出公理を導かないので「Zermelo集合論に置換公理を加えたのが ZF」となる。
>>879 の書き方を見て、後者の意味だと読み取れないかな?
置換公理の定式化を一つしか知らないようだと、スタンフォードの事典なんて読むのはまだ早いと思うよ。
痴漢公理
結局、痴漢公理にだけスコーレム関数の出現を許した場合、ZFの保存拡大になるの?
それより間違った論文というのを見てみたい
数学木曽論を学ぶのにお勧めの大学はどこでしょう? 高校数学の論理と集合って単元にはまってしまいまして。
888 :
132人目の素数さん :2011/09/16(金) 03:19:38.43
京大文学部には林晋さんがいるね
林さんは既に木曾論なんてやってないだろ
じゃあ僕がやるお お勧めの教科書教えてくれお
>>886 >高校数学の論理と集合って単元にはまってしまいまして
それだけで基礎論を大学選びの基準にしてしまうのはどうかと思いますよ。
どこでもいいから数学科に進学して学部の4年間ゆっくり考えるのが良いかと。
数学の基礎体力さえあれば基礎論なんて大学院から始めても遅くないですし。
> どこでもいいから いやいやw サイコロ降るわけにもいかないから、基準の一つを得ようとしただけでしょ。
どうでもいいが、次にスレ立てるときには「木曽論」でどうかね。 基礎的な数学の質問避けにはいいかもしれん。
>>886 数学者は人格に難のある人が多い。
(じっさいこのスレの上の方でとある先生の常識の有無が話題になってた)
そして木曽論は研究者の数が少ないので
その数少ない研究者に嫌われると他の選択肢がほとんどない。
大学選びというか先生選びは慎重にね。
895 :
132人目の素数さん :2011/09/16(金) 18:22:19.84
いいね、木曽論をNGWORDにすればいいってことだし。
897 :
132人目の素数さん :2011/09/16(金) 19:59:46.90
木曽よりも木曾のが良いだろう 數樂木曾論
変にスレ名をいじるよりも普通に基礎論はスレ名から排除して数理論理学のスレでいいだろ むしろ実態はそっちの方に近いし
899 :
132人目の素数さん :2011/09/16(金) 21:02:17.99
集合論・数理論理学 その9 はどうだろう? 数理論理学に含まれるという考えもあるかもしれないが、 集合論スレが全くないので。 數樂木曾論 其之九 も悪くないけど。
集合論だと素朴集合論もあるので数理論理学の範囲外になることもある
Silver の特異基数の定理は素朴集合論の範囲なんですか?
902 :
132人目の素数さん :2011/09/16(金) 22:15:16.10
公理的集合論・数理論理学その9 で良いんじゃないの。
そのへんを日本じゃ数学基礎論て呼んでるんだから、今のままでいいだろ。
904 :
132人目の素数さん :2011/09/16(金) 23:03:06.68
それだと数学の基礎と間違えるから。
数学木曾論・数理論理学 その9 に決まり!
906 :
132人目の素数さん :2011/09/17(土) 06:15:51.69
數學木曾論・數理論理學 其之九 くらいに韜晦した方がいいだろ、素人フィルターになるし。
なんという閉鎖的な思考
「数学の基礎的な質問」みたいなのには閉鎖的にしたいけれど、
ロジックに興味のある高校生・専門外の人にはオープンにしたいよね。
玄人には「数理論理学」が好まれているようだけど、
高校生や専門外には「基礎論」の方がまだまだ通用する気がする。
とすると
>>905 案くらいが妥当かと。
どうせ基礎的な質問だったら喜んで嫌みったらしくいじめるくせに。
910 :
886 :2011/09/17(土) 17:48:25.97
色々とありがとうございました。
911 :
132人目の素数さん :2011/09/17(土) 18:47:09.64
それにしてもなぜ木曾なんだか。 802 :132人目の素数さん :sage :2011/09/17(土) 16:06:23.55 結局、基礎論にも圏論にも特に意味は無い、ということ? 803 :132人目の素数さん :sage :2011/09/17(土) 18:11:32.37 圏論には意味あると思うけど基礎論は無駄だね
別に起訴でも木祖でもなんでもいいんだが
せっかく高校生君
>>886 が興味持って来てくれたんだし
それを記念して木曾でいいじゃないの
913 :
132人目の素数さん :2011/09/17(土) 19:26:02.15
スレタイ検索で来る人も多いのだから「基礎論」の方が良い ジャニーズ板はよそ者が来ないようにするために判りにくいスレタイにしていて、スレタイ一覧がカオスになっている
数学者がジャニーズ板とか見るんだw
915 :
132人目の素数さん :2011/09/17(土) 19:49:41.44
俺は数学者でなく 数学マニアだが半角2次元も良く見るよ
んじゃまた喜んで嫌みったらしくいじめるか
数学基礎論は英語にしたら? 数理論理学 Foundations of Mathematics その9 とか。
918 :
132人目の素数さん :2011/09/17(土) 23:10:11.57
英語にすると文字数増えてスレタイが読み難くなるんだよね・・・ シンプルに 數學木曾論・數理邏輯學 那個九 で良いと思うけど。
どこがシンプル?
920 :
132人目の素数さん :2011/09/18(日) 02:18:38.59
もう飽きた
923 :
132人目の素数さん :2011/09/23(金) 23:38:07.24
Booleの『論理の数学的分析』面白いな
924 :
132人目の素数さん :2011/09/24(土) 00:03:14.54
んなマニアックな本よんどランで 最先端の論文追わんか
いっそ、数学糞論にすれば。 糞好き以外来なくなるw
>>886 >数学木曽論を学ぶのにお勧めの大学はどこでしょう?
>高校数学の論理と集合って単元にはまってしまいまして。
日本の大学の学部では大したことは教えないから
どこにいっても大して変わりませんよ。
>>892 >基準の一つを得ようとしただけでしょ。
試験の成績で十分でしょう。
東大に入れるほど優秀、ってわけじゃないでしょw
>>893 >基礎的な数学の質問避け
本気なら、決して「数学基礎論」と書かないことだな。
>>903 みたいに
>そのへんを日本じゃ数学基礎論て呼んでるんだから
なんてバカいう奴がいたら、鎮静剤で眠らせろw
そもそも、集合論と数理論理学を一緒くたにするのは 整数論と代数幾何学を一緒くたにするくらいセンスがない。
930 :
↑ :2011/09/25(日) 18:31:11.35
同感!
整数論と代数幾何を一緒くたにすると数論幾何になって、それはそれでいい感じなんだけど。
ロジックの日本語は数理論理学じゃないの? 集合論は英語では明らかに logic に含まれるけど。
naiveとaxiomaticは全く扱いも分野も違う どこで英語をならったのか知らないけど寝言は寝てから言おうね
アメリカでもイギリスでもロジックと言えば 現代的なつまり公理的な集合論は確実に含まれるよ。
そう、だから
>>932 は「明らかに」舌足らずなんだよ
どうでもいいけど数理論理学はmathematical logicな。 単にlogicって言うのなら学問的には古典論理から現代論理まで含めた論理学一般のことを指す。
937 :
132人目の素数さん :2011/09/26(月) 01:19:55.84
>>936 数学を語る文脈で語ってたら単にlogicでいいでしょう。
紛れそうなときだけ使い分ければよい。
938 :
132人目の素数さん :2011/09/26(月) 07:46:41.77
本を読まなくてもスレに書き込めるようにテンプレ作ってみた。 数理論理学入門 ●命題論理 命題論理記号:¬,∧,∨,→,⊥ 原子命題:a,b,c... ※a=「1+1=2」,b=「2は素数」など。 原始命題は命題。a,bが命題のとき¬a,a∧b,a∨b,a→bは命題。 真理値関数V:命題aが真ならf(a)=1,偽ならf(a)=0とする。 aが原子命題のときV(a)=f(a) V(¬a)=1⇔V(a)=0 V(a∧b)=1⇔V(a)=1かつV(b)=1 V(a∨b)=1⇔V(a)=1またはV(b)=1 V(a→b)=1⇔V(a)=0またはV(b)=1 Vは一意に存在。トートロジーとは任意のVでV(a)=1となる命題a( |= a と書く)。 |= a→(b→a) |= (a→(b→c))→((a→b)→(a→c)) |= (¬b→¬a)→(a→b) 上の3つのトートロジーを公理と呼ぶ、まとめて理論と呼ぶ(集合Tや{a}と書く)。 理論Tのすべての公理を1にする関数Vが命題pを1にすることを T |= p と書く。 公理は定理。a→bとaが定理ならbも定理。(MP,三段論法,cut等と呼ぶ) aが定理ならaは証明可能( |― a と書く)。 有名なトートロジー:|= ¬a→(a→b),|= ¬¬a→a 演繹定理:T∪{a} |― b ⇔ T |― a→b 命題aとbで |― a→b∧b→aならaをbに書換え可能でa≡bと書く。 a→b≡¬a∨b,¬a∨¬b≡¬(a∧b),⊥≡¬(a→a)など。 T |― ⊥ のときTは矛盾すると言う、そうでないなら無矛盾。 T∪{¬a} |― ⊥ ⇔ T |― a 。 命題論理の完全性定理:|= a ⇔ |― a 命題論理のコンパクト性定理:理論Tの任意の部分集合Aの命題がトートロジー⇒Tの命題はトートロジー。
コンパクト性で「有限」いらないの?
940 :
官軍 :2011/09/26(月) 12:57:19.35
>>938 ご苦労様。 でも。全部、ナンセンスか「完全に間違うとる」。(^o^)
数理論理学じゃ長すぎて言いにくいから数論と呼ぼう!!
スーロン
しゅごく初歩的な質問ですが、命題論理や述語論理の ¬,∧,∨,→,∀,∃ などといったいろいろな記号は あくまで意味を持たない「ただの記号」なのですか?
944 :
↑ :2011/09/28(水) 07:19:19.64
んなこたぁない。
945 :
132人目の素数さん :2011/09/28(水) 15:51:14.49
Booleの「論理の数学的分析」は翻訳されてるのに「思考の法則」はされてないのは 何故なんだ 翻訳するなら後者の方が良い気がするんだがな
>>945 共立出版社で翻訳出版される予定らしい。
# Boole は、下層階級の生まれで、出世する為には、ギリシア語や
ラテン語をマスターしなければならないと信じていた。
その為、Booleの書いた本(英語)を読むには、ギリシア語や
ラテン語の知識を要する。 (^o^)
947 :
132人目の素数さん :2011/09/28(水) 17:52:38.45
ええ?
原著を読んだことのある奴ならわかるがそんなこたない。
949 :
132人目の素数さん :2011/09/29(木) 01:05:59.29
>>943 記号そのものには意味はない。
代わりに机や椅子の記号でも良い。
952 :
132人目の素数さん :2011/09/29(木) 19:01:35.75
歴史的には形式主義と呼ばれる立場と呼ばれる。
ああ眠い。基地外ばっかりじゃんここ。
954 :
132人目の素数さん :2011/09/29(木) 23:12:45.53
2ちゃんは馬鹿の巣窟。 これ常識。
>>946 共立に確認したら予定は無いと言われたぞ糞が。死ね
>>955 :132人目の素数さん:2011/09/29(木) 23:48:44.64
>>946 共立に確認したら予定は無いと言われたぞ糞が。死ね
講座「数学の歴史」のなかで、ブールの「思考の法則」ものっていた。
ブールの英語はむずかしいんで諦めたのかな。 (^o^) (^o^) (^o^)
# Dover出版社から、リプリント版がでているよ。
リプリント版のことなど既知だ 訳が有るかが問題なんだよ糞コテ死ね
クヌース・ベンディックスの完備化アルゴリズムをお勉強したい。 完全な証明求む。 オススメの項書き換え系の教科書は何?
>>961 二番目のやつ注文しますた。足らん場合一番目行きます。アリ。
963 :
961 :2011/09/30(金) 20:30:15.82
KBもグレブナー基底も互除法のわりと 素直な一般化というか高次元化だよね。
次スレ新たに立て直した方がいいんじゃない?
967 :
132人目の素数さん :2011/10/02(日) 20:50:31.03
ん? もう次スレ立ってるよ スレタイも同意があったじゃん
一部同意がないから966みたいな書き込みがあるんだろ 俺もああいうのは奇をてらいすぎてていけすかない
969 :
132人目の素数さん :2011/10/02(日) 21:07:31.57
それじゃあ この2次方程式の解き方を教えてください みたいなレスで溢れかえっても良いってのかい?
970 :
132人目の素数さん :2011/10/02(日) 21:08:10.22
「木曾」の部分には同意もあったが、その他の箇所について同意した人はいなかったように思う。 住人の合意があったとは到底認めがたい。 が、既に作ってしまったスレを放棄すべきだというほどいま立ってる次スレに反対する気はない。
まあ一スレ消化してみてから考えれば良いじゃん
「数学基礎論」は誤解される可能性があるのでどうにかするべきだと思ますが、 「数理論理学」はそういう心配もないわけで読みやすくぱっと見てすぐに分かる字体を使うべきだと思います。
974 :
132人目の素数さん :2011/10/02(日) 21:37:07.64
そもそも木曾だけでもおかしいのだが。 まぁスレタイなんてどうでもいいのでは?
「この2次方程式の解き方を教えてください」みたいなレスを避けるために おかしい箇所があるのは仕方ないが、そういう「おかしい」部分は最小限にすべきってことだろ。 ロジックのスレッドだとすぐに分からないようなスレタイでもいいとは思わないよ。
967=969=970=974の 次スレ立ててしまった者勝ち! みたいな態度が気に入らない
スレタイどころかテンプレも変わってるじゃん だからふざけて立てたスレかと思ったんだが
>命題論理のコンパクト性定理: >理論Tの任意の有限部分集合Aの命題がトートロジー⇒Tの命題はトートロジー。 これをふざけてないといわずしてなんと言おうか。
979 :
132人目の素数さん :2011/10/02(日) 22:07:33.61
ホントだ過去ログのテンプレがなくなってる
樹形図はなくなった方が良かったけど
>>978 ふざけてるなら修正すればいいと思う、俺はそれでも別にいいと思うけど
文句あるなら自分で立てればいいのに
同意もないのに勝手に立てちゃだめだろ
どれが誰やら確定できない状態で同意も糞もない ただスレ立てるの早すぎ
同意が得られたと思うものが他にあるなら 早すぎないと思うタイミングで立てることを止めたりはしないぞ
>>980 ロジック系のスレッド乱立させて、全員この板から追い出されろっていうのか?
そういうこと(文句があっても自分で別のスレッドを立てられない)分かってて
その物言いは「次スレ立ててしまった者勝ち! 」と同義だ。
>>984 同意が得られたものを立てるべきだという話なのに
なぜそれが乱立するんだ?
そもそも、乱立するほど反対者がいるのか?
988 :
132人目の素数さん :2011/10/03(月) 14:20:06.85
スレ乱立の実例を見せてくれたわけですね。わかります。
稾稾稾
乱立するなら板から消えろよお前ら
991 :
132人目の素数さん :2011/10/03(月) 19:52:36.46
乱立する⇒お前らは板から消えるべき いくらなんでも不条理すぎるだろう!
荒れてますね この状況だと議論することもできないし とりあえずスレタイそのままで次スレ立ててじっくり議論したうえで スレタイ変更するならその次のスレから適用する方が無難かな ということで次スレ立ててきます
994 :
132人目の素数さん :2011/10/03(月) 20:33:50.35
wwwww
995 :
132人目の素数さん :2011/10/03(月) 20:35:40.66
あとテンプレのコンパクト性定理を修正しときました。
スレ立て合戦で自制できた「数学木曾論・数理論理学」に好感
「数学木曾論・数理論理学」派えらい!
1001 :
1001 :
Over 1000 Thread このスレッドは1000を超えました。 もう書けないので、新しいスレッドを立ててくださいです。。。