- 1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ]
- 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学のスレッド その6
kamome.2ch.net/test/read.cgi/math/1265884076/
- 675 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 10:03:01.43 ]
- エムシラ＝ネットのオモチャ
- 676 名前：１３２人目の素数さん [2011/06/05(日) 11:46:10.91 ]
- (･∀･) ﾆﾔﾆﾔ
- 677 名前：１３２人目の素数さん [2011/06/05(日) 17:51:14.99 ]
-
松芯痰
むかしゃ（昔は）ネットの
鼻つまみ
今じゃネットの笑いもの
啄木 圖
- 678 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 18:15:33.77 ]
-
某スレより引用＆編集。 m(_ _)m
＞具体的に、どの主張でもって M_SHIRAISHI 氏が *大、dai, dai, DAI 先生* であると確信されるに到ったのですか？
松本真吾氏と M_SHIRAISHI氏との論戦は、意外にも！、 M_SHIRAISHI氏の連戦連勝であったことです。
罵倒が多く混っており、それは戴けないと思ったけれども、「それ」を差し引いて読んでみると、
M_SHIRAISHI氏の論旨は極めて明解／明晰であり、松本真吾氏は*完敗*に終わった。
- 679 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 18:55:07.22 ]
- どちらもキチガイなので勝った負けたは論評に値せんよ
- 680 名前：１３２人目の素数さん [2011/06/05(日) 18:56:14.10 ]
- それらを包括する概念がメドベージェフ還元。
- 681 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 23:03:13.21 ]
- 官軍は必ず勝つ。
丸（○）書いて、しめ（〆）書いて、屁こいて、マンコ舐めて、糞して、寝るスッ！
- 682 名前：猫 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 00:44:01.96 ]
- >理由があるかどうかはともかく、痴漢で懲戒免職後に受け入れてくれる大学などないだろう。
>未練があろうが、日本の大学への復活は無理。
>最近の研究業績はいまいちなので、海外の大学で給料をもらうのも無理。
猫
- 683 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 00:45:48.46 ]
- あんでぃ
- 684 名前：１３２人目の素数さん [2011/06/06(月) 02:16:53.05 ]
- 本スレマダー？
- 685 名前：猫は根気 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 02:49:17.12 ]
- >>683
今後もそういう風に精進して下さいませ。
猫
- 686 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 06:41:01.57 ]
- >>685
バカですみません
あんでぃ
- 687 名前：猫と貉 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 08:35:51.83 ]
- >>686
『あんでぃ』へ、
貴方は馬鹿ではアリマセン。ですが貴方の計画は私が阻止スルという考
え方を私はしています。但しもし貴方の考えを私が正確に理解していれ
ばですけど。
猫
- 688 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 10:46:44.22 ]
- >>687
私に計画はアリマセン
私の計画をどのように貴方ハ捉えていますでしょうカ？
バカですみません
あんでぃ
- 689 名前：１３２人目の素数さん mailto:sage [2011/06/07(火) 09:47:55.46 ]
- >> ﾜﾗﾀ｡ ﾁｮｳ､｣ﾈｼﾞﾚｿ｡
- 690 名前：１３２人目の素数さん mailto:sage [2011/06/08(水) 14:32:08.51 ]
- 無計画という計画が存在するか？
無関係という関係が存在するか？
- 691 名前：１３２人目の素数さん [2011/06/09(木) 22:24:03.46 ]
- 大学の数学の講義で，命題p→qを証明する際に
教授がq'→p'として対偶が元の命題と同値であることを
用いて証明する方法を背理法と述べていましたが
誤りですよね？
講義後に背理法を用いて証明した内容を質問しに言ったら背理法は「q'→p'として〜」と言われて話が通じませんでした。
- 692 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:31:04.48 ]
- 対偶法ですね
- 693 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:54:00.85 ]
- 背理法の一種に対偶法があると理解するのが一般的だな。
- 694 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:57:13.64 ]
- 異端の中では一般的なんだろう
- 695 名前：266 mailto:sage [2011/06/09(木) 23:03:23.15 ]
- 矛盾からは何でも証明できるような体系であれば（大抵は）
>>693の逆も言える
つまり、背理法も対偶法も見た目が違うだけで同じこと
- 696 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:05:03.13 ]
- 失敬
名前欄の266は忘れてくれ
- 697 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:06:07.29 ]
- 釣り師の存在を把握した
- 698 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:17:58.84 ]
- 数理論理学の教科書によく書かれている、解釈、構造、モデルとか、いわゆる意味論について
について聞きたいんだが、
この解釈とか構造とか呼ばれるのもって結局何なの？
対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？
でもそうすると、実数濃度の対象領域は定義できないし、どうするの？
あと、教科書とかに解釈の例として、「peano算術公理の解釈として自然数をとる」
として、各記号を通常の自然数論と同じように解釈する、
とか平気で書いてあるけど、じゃあその「自然数」ってなんなのかという話になる。
こんな書き方が許されるなら、ZFCの解釈として、「集合を取り、各記号を通常の集合論と同じにする」といえば、
もうこれはFZCの解釈なの？
あと、解釈（構造）の定義に平気で「集合」とか、「写像」とか
集合論に属する言葉を使ってるがこれは集合論が信頼できるという前提に立っているのか？
- 699 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:25:06.61 ]
- メタレベルで名前付けただけのところに、勝手に意味論がどうたら言い出して自ら煙に巻かれてるだけのように見える
- 700 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:36:06.22 ]
- qを仮定して矛盾するからq'というのを背理法というのは問題があるけど、
この場合はq'を仮定して矛盾するからqという議論だから
実質的には同じことをやっている。
あまり問題無いと思うけど。
- 701 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:39:13.42 ]
- ＞対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？
そんなこと無いけど。
「意味論」と「メタレベルの議論」の違いは、
集合論の独立性証明とかを一度勉強しないとなかなか違いは理解しにくいと思う。
数学やらずに哲学的な話ばかりしてても仕方ないし。
- 702 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 00:23:05.73 ]
- >698みたいな疑問は、チューリングマシンを勉強するのが一番の近道だと思うけど、どうかね？
- 703 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:19:39.65 ]
- ＞＞対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？
＞そんなこと無いけど。
じゃあ対象領域とか関数記号の解釈はどういった方法で決定（定義）するの？
そもそもこの解釈の存在で恒心、充足可能とか定義することにどれだけの意味があるんだ？
そのような用語を導入すると、何かいいことでもあるの？
どうせ、すべての解釈で命題が真になるかどうかなんて議論できないわけだし。
純粋形式的に推論規則で何かの論理式が導出できるか、できないかで論じればいいんじゃないの？
- 704 名前：703 mailto:sage [2011/06/10(金) 01:31:26.30 ]
- ためしに、「解釈」（構造）の例を挙げてみてほしい。
有限の場合は理解できるけど、無限の対象領域を持つ「解釈」とはどういう様相をしているのか。
本とかでは有限でない場合は「対象領域として自然数全体をとり、関数記号の解釈を通常の意味での加算＋*とする」
などと書かれているが、「解釈」っていうのはこんな曖昧で直感的なものでいいのか？
形式的体系って人間の直感や経験を排斥して完全に記号的に決められた範囲で、
理論を運用するためのものなのに、
それの議論の中で「解釈」のような直感的、曖昧な概念を使わなければならないとしたら、
形式的体系を作る意味ないじゃん。
- 705 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:32:40.87 ]
- 意味論って単にブール値函数を割り当てる程度のことのはずだけど、
この哲学厨っぽいひとが逝ってる意味論ってそれとはぜんぜん違うんだよね？
- 706 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:35:17.32 ]
- 恒真てのは、（許された操作を通して）記号列として等価だから
その記号列にどうブール値を割り当てても問題ないってことでしょ？
- 707 名前：703 mailto:sage [2011/06/10(金) 02:01:39.58 ]
- >>705
まさに、
＞ブール値函数を割り当てる程度のこと
という意味の意味論ですが。
対象領域が有限のときはいいとしても、
対象領域が無限のときにどうするんだ？という疑問だが。
ためしに、デデキント実数論の解釈を与えてみてほしい。
- 708 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 08:10:25.00 ]
- タルスキーの意味論は、別に
「人間の直感や経験を排斥して完全に記号的に決められた範囲で、
理論を運用するためのもの」じゃないので。
形式主義とか直観主義とかの系列にモデル論を無理に加えようとするからおかしくなるだけ。
- 709 名前：703 mailto:sage [2011/06/10(金) 18:20:41.40 ]
- >>708
じゃあ意味論って何の意味があるの？あと、結局実数論の解釈（構造）はどうなるんだよ。
Dedekind実数論を以下の公理で定義するとき、その解釈をひとつ例示してみてほしい。
Pを任意の述語として
E1. ∀x(x=x)
E2. ∀x∀y(x=y∧P(x)⇒P(y))
F1. ∀x∀y∀z((x+y)+z=x+(y+z))
F2. ∀x∀y(x+y=y+x)
F3. ∀x(x+0=x)
F4. ∀x(x+(-x)=0)
F5. ∀x∀y∀z((x*y)*z=x*(y*z))
F6. ∀x∀y(x*y=y*x)
F6. ∀x(x*1=x)
F7. ∀x(¬x=0⇒x*x^(-1)=1)
F8. ∀x∀y∀z(x*(y+z)=x*y+x*z)
O2. ∀x∀y(x≦y∧y≦x⇒x=y)
O3. ∀x∀y∀z(x≦y∧y≦z⇒x≦z)
O4. ∀x∀y(x≦y∨y≦x)
OF1. ∀x∀y∀z(x≦y⇒x+z≦y+z)
OF2. ∀x∀y∀z(x≦y∧0≦z⇒xz≦yz)
C1. ∀x∀y(P(x)∧¬P(y)⇒x≦y)
⇒∃z∀x∀y(P(x)∧¬P(y)⇒(x≦z≦y))
っていわれたときにぃ、じゃぁ対象領域が規定できないじゃない！ってたしか気づくと思うんですけどもぉ、
- 710 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 18:29:08.44 ]
- 実数は高階になるだけ。
充足可能性に付いて抽象的な理解を深めるには、
エルブラン基底などはいかが?
Samuel Buss, On Herbrand's Theorem
citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.5.1636
- 711 名前：703 mailto:sage [2011/06/10(金) 18:37:20.41 ]
- なんで結局解釈（構造）の具体例を挙げられないの？
このことからして、モデルとか解釈とか、
それを元に定義された恒真とか充足可能とかいう概念が怪しいものだと言えるのではないか
- 712 名前：あんでぃは弱虫 ◆AdkZFxa49I [2011/06/10(金) 18:48:07.38 ]
- >>709
顔文字にしか見えン。
あんでぃ
- 713 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:21:41.23 ]
- 実数体Rを取れば当然モデルになってるでしょ。
自明過ぎてこれが嫌ならR^NをN上の超フィルタUで割ればそれもモデルになる。
意味論というのは、いわゆる有限の立場とか云われるような奴とは違う。
あくまで無限群論とか函数解析だとかと全く同様にZFCを前提にしたその上の理論で、
>>709の公理系は完全だろうかとか、濃度κのモデルは同型を除いて
どのくらいあるだろうかとか、例えばそういうことを研究する分野。
集合論は使っちゃいけないんだと>>703が勝手に思い込んでるのがまずいだけ。
- 714 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:30:28.54 ]
- 黎明期の記号論理学にはフレーゲ→ラッセル→ヒルベルトの公理論と
ブール→パース→シュレーダー→タルスキーの意味論という二つの相異なる源流があって
それぞれ目指すものが違うのにそれを混同するからおかしなことになる。
ゲーデルと20世紀の論理学2 完全性定理とモデル理論の第三部とか
講談社学術文庫の論理分析哲学とか読むと多少は分かるようになるかもしれない。
- 715 名前：１３２人目の素数さん [2011/06/10(金) 22:34:17.92 ]
- 論理体系と代数モデルって本読んだ人います？
この本読んで数学・論理学センスを上げたいんですが。
- 716 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:47:03.85 ]
- >>713
自分は>>703氏とは違うけどよーわかってない人間ですが、
>意味論というのは、・・・ZFCを前提にしたその上の理論で、
やっぱそうなんですか。
完全性定理とかも明らかにZFCを前提にしてるようだし、そのあたりがずっとひっかかって
たんだけど、「ZFCを前提にしたその上の理論だ」とあからさまに言ってもらって
やっと少しわかるって感じです。
一応確認させてください。
> 実数体Rを取れば当然モデルになってるでしょ。
というのは、
・ZFCのモデルMが存在するという前提をおく
・MをいじってM'という構造を作れば実数論の公理系のモデルになることがわかる
・M'をRとよぶ
ということですか？
- 717 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/10(金) 23:09:40.49 ]
- 完全性定理はじめ、モデル理論の定理は全部通常の数学を前提にしてるよ。
さらに言えば、完全性定理は証明には選択公理が必要。
デデキントの実数論に相当する論理式が
実数体Rという議論領域での解釈で恒真になるからRをモデルと呼ぶだけだよ。
- 718 名前：716 mailto:sage [2011/06/11(土) 00:19:15.45 ]
- >>717どうも。
上2行了解します。
下2行についての実数体Rという議論領域が存在するか否かとかは
そもそも問題にしないというか、理論からモノが生まれるわけじゃなく
その逆だってことですよね。
ただ、完全性定理の証明についてはそういう納得の仕方ができない。
- 719 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 01:40:33.84 ]
- >>718
述語論理の完全性定理なら選択公理より少し弱いもので足りる。
選択公理のようなものが必要なことは、
LKの証明図を逆にたどる方法での証明を考えてみよう。
木の存在を要求してるだろう。
- 720 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 06:15:56.76 ]
- >>718
論理学で完全性定理を証明するのは、
解析学でコーシーの定理を証明するのと同じことだよ。
位相空間を定義するのと同じように、
言語Lや論理式を定義して、議論領域Mを定義して、
それらの間の関係や性質を調べてるだけだよ。
- 721 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 07:29:41.81 ]
- いままで猶予しておりましたが、奴のあまりのしつこさと、被害の大きさから、
見逃すわけにはいかず、不本意でですが、このようなお知らせを投稿させていただきます。
ここに現れるM.SHIRAISHIという異常者に一年以上にわたり虐待を受けております。
この男、私の居住する地域住民に対して、ひどい侮辱と罵倒を一年以上にわたり繰り返し、
ひどい名誉毀損行為を行い、我々の利益や健全な生活を妨害しております。
それによって今もひどく迷惑しています。
この男の投稿記録です。
groups.google.com/groups?hl=ja&lr=&ie=UTF-8&q=author:eurms%40apionet.or.jp+
この男について何か知っておられることがありましたら、お知らせください。
お願いします。
また他にもこの男に被害を受けられた方がいたら、ご連絡ください。
www.age.ne.jp/x/eurms/KakuRitsu-0.html
- 722 名前：716 mailto:sage [2011/06/11(土) 07:47:16.38 ]
- >>719
> LKの証明図を逆にたどる方法での証明を考えてみよう。
ん・・・わからんですｗ
「式Aがvalid → Aの証明が存在する」を示すことについて言ってるんですよね？
validであることから証明図へのとっかかりが何なのかわからんです。
>>720
> 解析学でコーシーの定理を証明するのと同じことだよ。
一瞬戸惑ったｗ
たとえ話、ですよね？
- 723 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 08:16:13.89 ]
- >>722
> >>719
> > LKの証明図を逆にたどる方法での証明を考えてみよう。
> ん・・・わからんですｗ
> 「式Aがvalid → Aの証明が存在する」を示すことについて言ってるんですよね？
> validであることから証明図へのとっかかりが何なのかわからんです。
完全性定理の証明に選択公理かそれに近い言明が必要な理由を説明してるんだと思う。
（シュッテ流の証明といわれるもの。）
>
> >>720
> > 解析学でコーシーの定理を証明するのと同じことだよ。
> 一瞬戸惑ったｗ
> たとえ話、ですよね？
そうです。
どちらも習慣による数学に基いてるということ。
ZFC、NGB、ニュー・ファンデーション、トポス...何によって
形式化されるかは不明だし、知る必要もないです。
ただし、議論領域がどういった数学に基いているのかとは別の話です。
- 724 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 10:41:51.18 ]
- 直感主義述語論理の強完全性定理の証明にはACA0があればおｋ
つまりRCA0 + arithmetical comprehension axiom
- 725 名前：あんでぃは存在 ◆AdkZFxa49I [2011/06/11(土) 10:42:47.73 ]
- 難しい話しですね。
あんでぃ
- 726 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 10:43:46.62 ]
- 古典論理だとWKL0だから、RCA0 + weak K nig's lemma
- 727 名前：703 mailto:sage [2011/06/11(土) 12:51:09.69 ]
- なんだ、モデルとかは、ZFCの上での議論だったのか。それなら納得出来る。
しかし、だとすると、FZC自身の解釈、やモデルといったものは
どうやって議論するんだ？他の公理系を使ってそのなかでモデルを作るとかしか思い浮かばないけど、
それだと相対的な議論しかできないような。
- 728 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 14:42:39.48 ]
- >>704
>形式的体系って人間の直感や経験を排斥して完全に記号的に決められた範囲で、
>理論を運用するためのものなのに
当初はそう思われて作られていったけれど、現実は違うんだろ。
思うに今はそもそも論を見直す段階だというか、見直しもかけずに
運用してきたことに何の疑念も覚えなかった状況をなんとかしないといけない。
- 729 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 15:03:20.35 ]
- ある言語の理論とそのモデルとの間の
数学的な操作は通常の数学を前提としている。
しかし、通常の数学である
ZFCという論理式の集合のモデルを探す場合、
ZFC上で議論することは不完全性定理によってできない。
普通ZFCとそのモデルを議論する場所はZFCよりも大きい。
例えば推移的クラスというのはクラスを扱える
BGという集合論上で行われている。
- 730 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/11(土) 15:16:12.41 ]
- 例えば推移的クラスというのは
↓
例えばZFCのモデルとなる推移的クラスというのは
- 731 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 17:21:57.98 ]
- >>664
＞ゲーデルの、いわゆる、「不完全性定理」は見直されなければならぬ。
「ゲーデルの定理−利用と誤用の不完全ガイド−」でも読んで寝ろ。
- 732 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 17:56:05.10 ]
- >>452
＞和書しか読竹内の本がありがたく感じる。
＞もちろん良い本だけど。
ｶﾜｲｿ（ﾅﾐﾀﾞ
- 733 名前：703 mailto:sage [2011/06/11(土) 20:01:46.50 ]
- 誤爆かいな？
- 734 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 20:35:01.15 ]
- ZFC自身のモデルとかも普通はZFCで議論すると思うけど。
というか現代の集合論はまさにそれをやっている。
BGとZFCは無矛盾等価なので
ZFCに無いモデルがBGに存在するというようなことは無い。
もちろんZFC自身がモデルをもつことはZFCでは示せないし、
また記号∈は∈でそのまま解釈したいと言った特殊な事情があるので
実際にはZFCの任意有限部分を一つ取ってそのモデルを取ったりする。
- 735 名前：716 mailto:sage [2011/06/12(日) 01:56:47.78 ]
- 完全性定理に選択公理が必要なことについては、
必要であることそれ自体は理解できるが、かえってそれゆえに結果に対する疑念に
とらわれてしまっていました。
つまり、本当に証明が存在するんだろうか、って。
この疑問自体に問題があったのかも、と今になって思い始めてますがうまく表現できません。
- 736 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 02:34:03.50 ]
- 選択公理は必要ない。もっと弱いものでいい。
- 737 名前：716 mailto:sage [2011/06/12(日) 06:23:59.28 ]
- んじゃ、
×完全性定理に選択公理が必要なことについては、
〇完全性定理に選択公理（の弱いやつ）が必要なことについては、
- 738 名前：716 mailto:sage [2011/06/12(日) 09:41:25.67 ]
- 具体物についての「確定しているはずでは？」という考えかも。
Q平行線の存在は証明できるか？
Aできない。平行線公理は独立。
Qでも実際にどうなってるかは確定してるはずでは？
Aそれは物理学の領域。数学的には複数の選択があり得る。
Qアキレスが亀に追いついた時点でランプは点いてるの？消えてるの？
Aどっちとも言えないよ。
Qでも確定してるはずでは？
A追いつくまでの点滅過程をいくら定義しても追いついた時点の状態を規定したことにはならないよ。
↑ここまではわかってるつもりなんだけど、
Q公理を追加していった極大点としてのcomplete theoryなんて存在するの？
A選択公理の弱い奴を必要とするけど、あるよ。
Q「証明」がwell definedな概念なら、証明可能か否かは確定してるはずでは？
A・・・
↑最後の答えとして何が適切なのか、自分でもどんな答えを望んでいるんだかわからなくなってきた。
- 739 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 10:32:43.81 ]
- >>738
>Q公理を追加していった極大点としてのcomplete theoryなんて存在するの？
>A選択公理の弱い奴を必要とするけど、あるよ。
>Q「証明」がwell definedな概念なら、証明可能か否かは確定してるはずでは？
>A・・・
そもそも、何が「追加すべき公理」か、確定できない。
- 740 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 10:43:29.03 ]
- >>738
「･･･は確定しているはずでは？」
全般に対する返答は以下の通り
「なぜそう思ったんですか？」
- 741 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:11:03.47 ]
- 完全性定理を理解してないからでしょう。
- 742 名前：716 mailto:sage [2011/06/12(日) 11:13:54.23 ]
- >>740
> 「なぜそう思ったんですか？」
に対する返答があいまいな状態なのですよ。
何かの錯覚にとらわれているんだろうと自分でも気づき始める。
→その正体がわからない→こういう場所で質問をしてみる→わかったり、わからなかったり
>>738に書いたことはかなり未整理でした。
>>739 > そもそも、何が「追加すべき公理」か、確定できない。
ちょっと戸惑ったけど、complete theoryを作る過程での公理の追加について言ってるんですよね？
してみると、「証明」というものが「well definedで確定しているはず」かどうかは問題点じゃなくて、
理論（公理系）というものが何なのか「立場によって違う」のか・・
何が「追加すべき公理」か確定できないけどcomplete theoryというものは存在するよ。
だからそのcanaonical modelを考えればいいんだよ。
Qそんなもの存在しないって立場は？
A
設問をこう変えればいいのか・・・
- 743 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:34:54.97 ]
- とりあえず逆数学の勉強してみれば?
www.amazon.co.jp/dp/4879999709
証明論も数学の一つに過ぎないってよくわかると思う。
追加追加って言うけど、元の公理系に対して、
追加した公理も、それがないと証明できない定理も同値だから。
どっちを追加してもいい。
- 744 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:45:16.56 ]
- >>737
> 〇完全性定理に選択公理（の弱いやつ）が必要なことについては、
違う。選択公理とは全く違う弱い公理しか必要ない。上に書いてあるだろう。
- 745 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 13:38:32.60 ]
- 選択公理って、任意の全射 f: X --> S に対して、s: S --> X で fs が恒等射となるものがあるってことですよね？
- 746 名前：716 mailto:sage [2011/06/12(日) 14:31:57.00 ]
- >>744
> 違う。選択公理とは全く違う弱い公理しか必要ない。上に書いてあるだろう。
上に書いてあることをさらってみると・・・
>>133 > 「数学のロジックと集合論」によると完全性定理は選択公理よりもちょっと弱いらしいよ
>>717 > さらに言えば、完全性定理は証明には選択公理が必要。
>>719 > 述語論理の完全性定理なら選択公理より少し弱いもので足りる。
>>723 > 完全性定理の証明に選択公理かそれに近い言明が必要な理由を説明してるんだと思う。
>>736 > 選択公理は必要ない。もっと弱いものでいい。
選択公理（の弱いやつ）、じゃニュアンス遠いんですかね。
- 747 名前：１３２人目の素数さん [2011/06/12(日) 15:06:32.25 ]
- 弱ケーニッヒじゃなかったかな。なら選択公理の弱いやつとか言いたくないだろうな。
- 748 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 16:27:01.40 ]
- 普通の公理系は整列されているから、完全性定理の証明に選択公理はいらない。
- 749 名前：716 mailto:sage [2011/06/12(日) 19:02:53.66 ]
- >>747
情報どうも。
"弱Konig"でぐぐってみたところ京大のサイトでヒットしましたが、内容はちょっとすぐにはわかりませんね。
>>748
もうちょっと詳しくお願いできないでしょうか。
- 750 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:12:24.28 ]
- まーた出てきたか「考えない人」
- 751 名前：716 mailto:sage [2011/06/12(日) 20:21:25.22 ]
- >>750
それって前スレかどこかで活躍してたコテでしょ？それとは違いますよ。
同様にうざいよ、というんでしたらごめんなさい。
と思ったらこのスレでも>>599にいたか。
- 752 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:29:48.85 ]
- >>746
完全性定理を
古典述語論理の論理記号から代数（ブール代数になる）作って、
意味づけする方針で証明すれば、
「ブール代数がある適当な集合代数で表現できる。」ことが必要だと
わかる、これがACから証明できWKLと同じだということで納得できませんか。
肝心なのをひろい忘れてるじゃないか。
>>724 >直感主義述語論理の強完全性定理の証明にはACA0があればおｋ
>>726 >古典論理だとWKL0だから、RCA0 + weak K nig's lemma
- 753 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:33:01.12 ]
- あれウムラオトって表記できなかったっけ？
- 754 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:02:44.34 ]
- König
- 755 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:10:49.16 ]
- kingかと思った
そういやkingってどこ行ったんだ？
- 756 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/12(日) 21:31:30.64 ]
- >>749
弱ケーニッヒは
「無限の高さを持つ木の枝分かれが有限個なら、
枝の少なくとも1本は無限の高さをもつ」
というイメージ。
- 757 名前：716 mailto:sage [2011/06/12(日) 21:32:59.94 ]
- >>752
> 納得できませんか。
いろいろ質問したあげく申し訳ないのですが、これらの説明をちゃんと理解して
納得するだけの基盤がまだ自分に整ってないと判断しました。
なので納得できるorできない、とか回答できません。
WKLも理解してないんですが、ACと同様に超越的な主張なんですよね？
「ある理論において妥当な式はその理論で証明が存在する」という具体的な主張を
証明するために、どうしても超越的な手段を必要とする、これはなぜだ？
という疑問に対する手っ取り早い回答が得たかったんですが、まだ勉強が足りなかったようです。
- 758 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:45:09.63 ]
- >>756をそれほど超越的に感じるのか?
>>756
イメージというか定義そのものだな。
- 759 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 22:18:12.51 ]
- >>757
とりあえず逆数学勉強することを勧めるよ。
あんたの好きそうな話題を専門的に研究する分野。
- 760 名前：716 mailto:sage [2011/06/12(日) 22:26:53.14 ]
- >>758
ああ、>>756を読む前に書き込んでました。
ACと同じ程度には超越的に感じますけどね。
WKLもACも、それを否定するor使わない、という立場が成り立つと思うんですが。
仮定： 無限の高さを持つ木の枝分かれが有限個
結論： 枝の少なくとも1本は無限の高さをもつ
イメージですが、これは「普通の仮定に対する強い結論」
仮定： ある理論のすべてのモデルに対して式Aが妥当
結論： その理論で式Aの証明が存在する
こっちは、「強い仮定に対する強い結論」というイメージ。
後者を得るために前者が必須になる？
>>759
>>743で紹介されてたやつですか。とりあえず丸善で斜め読みしてみます。安いしｗ
- 761 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 23:34:04.59 ]
- >>760
『逆数学と2階算術』安いのはいいけど、
薄くて、高度なことを説明してるので基礎知識がないと読みにくいよ。
数理論理学（数学基礎論）の基礎知識として
新井 敏康『数学基礎論』を買っておく、読み通おせとは言わないから。
齋藤 正彦 『数学の基礎―集合・数・位相』で初歩的なことを確認。
完全性定理なら林 晋「数理論理学』もおすすめ。
- 762 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/13(月) 00:26:49.61 ]
- >>760
「高さが無限で枝分かれが有限個の木は、
その枝の少なくとも1本の高さが無限」（WKL）
↓
「枝分かれが無限個の木は、
その高さが有限またはその枝の少なくとも1本の高さが無限」
↓
「枝の長さがすべて有限の木は、枝分かれが有限個」
これが、
LKの証明図を下から辿る時に必要になるが
完全性定理の肝と言うわけではない。
- 763 名前：１３２人目の素数さん [2011/06/13(月) 05:48:12.46 ]
- どうでもいいが
ケーニッヒ≠弱ケーニッヒ
- 764 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/13(月) 07:00:58.82 ]
- 1回の枝分かれで、
2個にしか分かれないのがWKL
いくつにでも枝分かれできるのがKL。
KL→WKL。
3つ以上の論理式から1つの論理式を得るような
推論規則はないためWKLで十分。
- 765 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 11:20:14.65 ]
- >>764
> 2個
< 有限個
- 766 名前：716 mailto:sage [2011/06/13(月) 20:43:13.01 ]
- きょう丸善に『逆数学と2階算術』探しに逝ったけど「絶版在庫切れ」だと。
内容確認できないけどアマゾンで注文しました。
まあ1470円だからいいか。
- 767 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 20:45:21.34 ]
- sinθって書いて下さい
- 768 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 21:50:20.44 ]
- >>760
RCA0で完全性定理が成り立つドメインがあると思えば追求してみればいい。
- 769 名前：703 mailto:sage [2011/06/13(月) 22:08:58.52 ]
- モデルの話でZFCを前提にしていいのはわかったけど、
じゃあ「任意の解釈で」みたいな言及はどう扱うの？
ZFCにクラスを「ねじ込んだ」体系ではクラスに関して∀量化子とかは使えないわけだが、
「任意の解釈で論理値trueをもつ」とかいうのはどうやって証明するの？
はじめからクラスと集合の概念があるあの体系（名前は忘れたが）を使うしかないんじゃないか？
- 770 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 00:01:21.01 ]
- ZFCのCを無条件に前提にする必要はない。
- 771 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 00:49:21.76 ]
- ZFの話に便乗して質問です。
ZFから無限公理を外した公理系って、何か特別な名前がついていたりしますでしょうか？
無限公理の否定を持つ有限集合ではなくて、単に無限公理が存在しないようなものです。
- 772 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:15:28.50 ]
- 名前付いてないと思いますが、
Nの存在は仮定しても無限公理がないと証明できない定理があるのは知られています。
つまり研究対象になってます。
- 773 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:33:10.08 ]
- >>769
セマンティクスを全部放棄してシンタックスのみで議論すればよい
- 774 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:56:01.23 ]
- >772
サンクスです。
無限を嫌う人が多いので無限公理を外した公理系も整備されているかと思ったのですが、
そうではないようですね。
- 775 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 07:00:58.96 ]
- 普通モデルとか解釈とかは集合であるようなものをとる。
集合としてのモデルが存在することと無矛盾性が同値だというのが完全性定理なので。
クラスに対する操作は若干制限されているから集合と同様に扱う事は出来ない。
|
 |
