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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 552 名前：１３２人目の素数さん [2005/07/19(火) 20:01:17 ] 「ゲーデルの不完全性定理」(レイモンド・スマリヤン) と比べたら、どちらがお勧めですか？ 553 名前：１３２人目の素数さん mailto:age [2005/07/19(火) 23:26:11 ] >Dover だったら薄い基礎論の入門書 ってなんのことだっけ？ >>552「の原書」と>>550だったら前者の方が より高い視点から書いてある割に分かりやすいので お勧めな気がする． もっとも>>550は古典だからしょうがないけど． 554 名前：１３２人目の素数さん mailto:sage [2005/07/20(水) 12:50:25 ] >>553 What is Mathematical Logic? by J. N. Crossley これ。15年も前に読んだ本なので、思い出すのに時間がかかったよ。 555 名前：１３２人目の素数さん mailto:sage [2005/07/20(水) 18:31:03 ] ああ、田中尚夫の邦語訳がある奴ですね 良書っぽいですね 556 名前：１３２人目の素数さん mailto:sage [2005/07/28(木) 16:57:03 ] Doverだったらそれこそスマリヤンの First-Order Logicがあるじゃん。 557 名前：１３２人目の素数さん mailto:sage [2005/07/28(木) 17:03:46 ] 良い本っぽいけど（持ってるけど読む暇無いのです） 「不完全性定理関係」じゃないですね 558 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 01:12:39 ] だったら、河合塾の基礎論シリーズの「入門」か「いざない」はどうかな？ 559 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 02:50:54 ] >>556 タブロー法のすごくいい本だけど、一階述語論理だからなあ。 560 名前：１３２人目の素数さん mailto:sage [2005/07/29(金) 03:13:17 ] いざないって不完全性定理と集合論の入門書としては結構良いよね 証明の細部を追いすぎないという点でも 入門と集合論の巻はそれの詳細ver.だね 561 名前：１３２人目の素数さん [2005/07/29(金) 15:28:46 ] age 562 名前：１３２人目の素数さん mailto:sage [2005/07/30(土) 10:46:23 ] >>557　>>559 ああ、そういうことかぁ。 ところで不完全性定理に関しては、 漏れは日本人の書いた物は、肝心のポイントが 明らかになっていない気がするな。 ホフスタッターのGEBとかスマリヤンとかを読めば それが分かると思うけど。 563 名前：１３２人目の素数さん mailto:sage [2005/07/31(日) 09:03:19 ] 読んでわかっている人ってあんまりいないと思いますけど。 不完全性定理が形式体系についての定理だってわかっている人が 少ないと思いますから。 564 名前：１３２人目の素数さん mailto:sage [2005/07/31(日) 18:02:56 ] 途中までだけど、draftがここから落とせます。 ttp://www.godelbook.net/ 565 名前：１３２人目の素数さん [2005/08/01(月) 15:59:48 ] バカっ質問ですが、 n変数関数とか言う時のnってなんのnですか？ 566 名前：１３２人目の素数さん mailto:sage [2005/08/01(月) 16:11:45 ] >>565 ここは基礎の数学スレじゃなくて数学基礎論のスレだ 激しくスレ違い 567 名前：１３２人目の素数さん [2005/08/01(月) 23:12:22 ] n変数関数つったのがまずかったか n変項述語記号って言えばよかったか ま、バカな質問には違いないけどな 568 名前：１３２人目の素数さん mailto:sage [2005/08/02(火) 05:30:21 ] 質問の意図が全く分からないんですが なんのnってnに種類があるんですか？ >>566 記号論理とか再帰函数論の質問かもしれないと 思えないのは修行が足りない 569 名前：１３２人目の素数さん mailto:sage [2005/08/02(火) 06:58:09 ] >>568 結構、いい質問だと思うよ。この手の議論のときｎの種類についていくつか いえないと、「あなた、全然わかっていない」ってことだから。 570 名前：１３２人目の素数さん [2005/08/02(火) 19:49:20 ] >>569 どういうこと？詳しく教えて！ 571 名前：１３２人目の素数さん mailto:sage [2005/08/03(水) 04:12:42 ] >>569 だからあんたの日本語が通じてないんだよ 種類なんて専門用語は無い 572 名前：１３２人目の素数さん mailto:sage [2005/08/03(水) 13:19:55 ] 5=7-2 573 名前：１３２人目の素数さん mailto:sage [2005/08/04(木) 20:24:00 ] >>568 > 再帰函数論 ふつー帰納的関数っていうんでは 574 名前：１３２人目の素数さん mailto:sage [2005/08/04(木) 23:07:30 ] 純粋数学系の人は帰納的という人が多いね ただ例えば 「Recursion TheoryにおいてInductionとRecursionの関係を 理解するのは大事である」 とかを訳そうと思ったら一寸大変かと 575 名前：１３２人目の素数さん mailto:sage [2005/08/05(金) 07:19:46 ] >>574 Recursion Theory において,InductionとRecursion は違う意味で 使うことあるの？ 計算機関係の人は、定義になっていないものも Recursion って呼ぶ みたいだけど、定義になっているものを呼ぶ場合、違う意味にはなら ないと思いますが、、、。 576 名前：１３２人目の素数さん mailto:sage [2005/08/21(日) 02:23:18 ] 保守 的拡大 577 名前：１３２人目の素数さん [2005/08/23(火) 08:23:31 ] age 578 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 13:19:41 ] 自然数論や、集合論の形式的体系は大抵の本に載っていて簡単に知ることができますが、 数理論理学そのものを形式化するなんてのは無駄でしょうか？例えばGentzenのカット除去定理 の形式的証明をつくれないかな、なんて考えようとしてみたのですが、いくら考えてもなんか 混乱してしまうと言うか何と言うか．．． どなたか、お知恵を拝借できないものでしょうか。 579 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 15:55:48 ] >>578 cut elimination なら頑張ればできると思う けど正直なところ面倒臭そうであまり考えたくない 580 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 20:58:19 ] >>578 そのメリットは？ 581 名前：１３２人目の素数さん mailto:sage [2005/08/23(火) 21:12:16 ] 自己満足 582 名前：578 mailto:sage [2005/08/23(火) 23:34:49 ] >>580 >>581 メリットはまったくご指摘のとおり自己満足です。最近数学やってて自分の論理展開に よく不安を感じるんですが、そうするとなぜか論理展開の形式化に走っちゃうんです。 ですからバカな疑問なんだろうなあ、とはつくづく思っています。 もし皆さんならどんな関数記号を導入しますか？述語記号はどんなものにしますか？ もちろんそれはどんな公理を用意するかという疑問なんですが．．． ペアノの公理なんか今までなんとも思ってなかったんですが、何もない時期にああいう 公理を抽出するってのはやっぱりすごいことだったんでしょうねえ。しみじみ。 583 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 00:21:56 ] Gentzenのカット除去定理の形式的証明を書くだけなら、 ε_0より大きい順序数の整礎性が扱える形式的体系で その形式的証明を書けばいいと思うが、 それには数理論理学が分かってないと無理では？ 584 名前：578 mailto:sage [2005/08/24(水) 01:30:46 ] >>583 ＞それには数理論理学が分かってないと無理では？ どの程度わかってないといけないでしょうか？私は前原昭二の 数理論理学（培風館）、数学基礎論入門（朝倉書店） を読んだ程度（面目ないっす）ですが、具体的にはあと何をやればいいのでしょうか？ どんな関数記号や述語記号を取るかというのは自明なんでしょうか？ こんなバカですけど、よろしくお願いいたします。 585 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 01:33:42 ] 〜を満たす論理体系では〜である型の定理があるから 参考にすると良いかも Ebbinghaus et al.,のUTMとか 586 名前：１３２人目の素数さん mailto:sage [2005/08/24(水) 09:28:12 ] >>584 形式化できるかどうかの判断をどこで、どのようにするかを決めて おかないと形式化できたかどうかがわからなくなる。 587 名前：１３２人目の素数さん [2005/08/24(水) 09:59:12 ] >>582 ＞最近数学やってて自分の論理展開によく不安を感じるんですが それは単に注意力の問題で、形式化では解決できることではないね。 注意力散漫だと、いくら形式化しても肝心な前提をうっかり抜く。 おまけに思い込みが激しいと、いくらうまくいかなくても 実は必要な前提を欠いていることになかなか気づかない。 588 名前：１３２人目の素数さん [2005/09/03(土) 10:07:16 ] age 589 名前：１３２人目の素数さん mailto:sage [2005/09/03(土) 20:16:03 ] こっちにも初学者こないかな 590 名前：１３２人目の素数さん mailto:sage [2005/09/03(土) 20:22:32 ] いらん 591 名前：１３２人目の素数さん mailto:sage [2005/09/04(日) 22:46:28 ] >>587 同意 592 名前：１３２人目の素数さん [2005/09/06(火) 23:25:07 ] 一階述語論理の公理系 （A1）　α⇒（β⇒α） （A2）　（α⇒（β⇒γ））⇒（（α⇒β）⇒（α⇒γ）） （A3）　（α⇒β）⇒（（α⇒¬β）⇒¬α） （A4）　∀xα⇒α{x := t} 　　　　　　ただし, {x := t} はαに適用可能な代入 （A5）　∀x（α⇒β）⇒（α⇒∀xβ） 　　　　　　ただし, αにおいて x は自由に現れない （MP）　 α α⇒β β （GEN） α ∀xα 一階述語論理の公理系 （A1）　α⇒（β⇒α） （A2）　（α⇒（β⇒γ））⇒（（α⇒β）⇒（α⇒γ）） （A3）　（α⇒β）⇒（（α⇒¬β）⇒¬α） （A4）　∀xα⇒α{x := t} 　　　　　　ただし, {x := t} はαに適用可能な代入 （MP）　 α α⇒β β （GEN） α⇒βがえられたら、α⇒∀xβを導き出してよい（ただしαにおいてx は自由に現れない） 手元に、この二つの公理系があるのですが、違いについて教えてください。 593 名前：１３２人目の素数さん [2005/09/07(水) 06:04:35 ] こういう数理論理学というものを学ぶためには 高校の数学ではどのくらいまでやっておく必要がありますか？ ざっと見た感じ微分積分とかは出てきませんよね。 594 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 08:19:05 ] 「〜してください。」って言い方はなんか少し高飛車だよな。 595 名前：１３２人目の素数さん [2005/09/07(水) 13:32:45 ] どなたか教えていただけないでしょうか、くらいに訂正します、( つд｀。) 596 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 14:27:23 ] >>592 両者共に演繹的には等価なもの。 597 名前：１３２人目の素数さん mailto:sage [2005/09/07(水) 15:49:48 ] どっちもHilbert流だし、 ただの公理の選び方とか定式化とかの違いだと思うけどな 要するに大した違いは無く、趣味の問題、と >>593 数学的帰納法とか対偶とかは流石に知っといたほうがいいでしょうね(^_^;) ∈とか⊂とか⇔とか∪とかの記号の意味も、 本によっては常識として、説明してくれないかもしれません まあ微分積分とか、ベクトルとかは知っている必要は無いですね 598 名前：593 [2005/09/07(水) 19:30:25 ] >>597 数学の基礎知識について質問したものですが、その答えによると、 高校の数�TAぐらいの知識で、高度なものは無理としても、基本を 理解することは可能とういうことなのですか。 599 名前：１３２人目の素数さん [2005/09/07(水) 22:43:36 ] ちょっと書き直しました 一階述語論理の公理系 (A1) A⇒(B⇒A) (A2) (A⇒(B⇒C))⇒((A⇒B)⇒(A⇒C)) (A3) (¬A⇒¬B)⇒(B⇒A) (A4)∀xAx⇒At 　（t は任意の項，Axは x を自由変数として含む論理式， AtはAxの自由変数 x を項 t に置き換えたものをあらわす） (A5)∀x (A⇒Bx)⇒(A⇒∀xBx) （Aは x を自由変数として含まない論理式， Bxは x を自由変数として含む論理式） （MP）　 α α⇒β β （GEN） α ∀xα 存在汎化　Atから∃xAxを導きだしてよい　（ｔは任意の項） 存在例化　∃xAxとAa→C、からCを導きだしてよい　（aは新しい項の記号であること、Cには項aが含まれていないこと） が （A5）あたりに潜んでいるはずなんですが、力量不足でよくわかりません。 上の一階述語論理の公理系で、存在汎化、存在例化、と同じ導出をする仕方を、どなたか、教えていただけないでしょうか >>593 基本ということなら、もう、ほとんど、論理学に終始することになるんだろうと思います。 600 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 01:41:53 ] >>599 存在汎化 ∀x¬A(x) ⇒ ¬A(t)　　(A4) から A(t) ⇒ ¬∀x¬A(x)。 存在例化 A(a)⇒C から(GEN)により ∀x(A(x)⇒C)。 一方 ∀x(¬C⇒¬A(x)) ⇒ (¬C⇒∀x¬A(x))　　(A5) から ∀x(A(x)⇒C) ⇒ (∃xA(x)⇒C)。 601 名前：１３２人目の素数さん [2005/09/08(木) 10:01:10 ] ありがとうございます！！！ あと、上の一階述語論理の公理系を、等号付きの一階述語論理の公理系にしたいのですが、付け加える公理は A6　　∀x（x＝x） A7　　(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）) （φはｎ変数関数記号で、φ(・・・・ｘ・・・・）は項φ(・・・・ｘ・・・・）のｘのあらわれのひとつ以上（いくつでもよい）をｙでおきかえてえられる項とする） で足りますか？ むかしどこかで取ったメモに、 A7　　∀x∀ｙ(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）) というのを見つけたのですが、これは俺の書き誤りでしょうか？ あと、A8　　∀x∀ｙ（（（x＝ｙ）∧Ax）→Ay）　　（AyはAxのxのところ（必ずしもそのすべてでなくともよい）を、yに置き換えた論理式である。） というのも・・ 質問してばかりで、心苦しいですが、もう少しだけ、どなたか、お付き合いください。 よろしくお願いします。 602 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 12:06:56 ] >>601 A7 を閉じるかどうかはおいといて、A8 がなきゃ等号公理としては 普通だめだろ。 603 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 12:15:09 ] term 使わない体系なら A7 はいらないから、普通に等号公理と言ったら、 反射律(A6)＋ライプニッツ則（A8）。 （宿題）推移律、及び対称律を導き出せ 604 名前：603 mailto:sage [2005/09/08(木) 12:19:09 ] あれ、A8 は同一者不可識別の原理だな？ちょいまち、ちょっと脳内検索させてくれ。 603は保留。 605 名前：603 mailto:sage [2005/09/08(木) 12:52:21 ] 脳内検索、つーか暗算終了。603 保留解除ね。 606 名前：１３２人目の素数さん [2005/09/08(木) 17:25:04 ] 関数記号を使う等号付きの一階述語論理の公理系ということになると、A7が必要になってくるようなのですが、 そのときは、 A7　　∀x∀ｙ(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）) これでいいのでしょうか （こっちA7　　(x=y)→(φ(・・・・ｘ・・・・）＝φ(・・・・y・・・・）)じゃなくて） ＞（宿題） ∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ） と ∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ） とが、導出できるんだろう、ことは、状況からして、なんとなくわかりますが、とりあえず、今の俺には、ﾑﾘﾎﾟです。 >>599でもさらしましたが、 証明に関する経験も力量も、今の俺には、ほとんど、残念ながらないのですね。 607 名前：１３２人目の素数さん mailto:sage [2005/09/08(木) 20:07:40 ] >>606 > ∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ） ∧ が現れる規則がないから ⇒ だけで書かないと。 608 名前：１３２人目の素数さん [2005/09/09(金) 00:10:36 ] ∀ｘ∀ｙ∀ｚ（（¬（ｘ＝ｙ→¬ｙ＝ｚ））→ｘ＝ｚ） ということになるんでしょうか ＞（宿題）推移律、及び対称律を導き出せ も気になってはいるんですが、 とりあえず、 関数記号を使う等号付きの一階述語論理の公理系の公理A7 についての解説をどなたかよろしくおねがいします 609 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 00:22:42 ] 「完全性」が成り立たない形式的体系ってどんなものがあるんですか? つまり、任意のモデルに対して真な(閉)論理式であって、 その形式的体系内で証明不可能であるようなものを持つ形式的体系です。 命題論理とか1階及び2階述語論理とか様相論理は完全らしいので、 自分が名前を知っていてかつ完全性の正否を知らないのは高階述語論理くらいです。 というか、完全性と健全性が「成り立つように」意味論を整備しておくんですか? 610 名前：609 mailto:sage [2005/09/09(金) 00:38:16 ] 気付いてみれば、命題論理から推論規則を除けば公理以外は全て証明不可能ですね… でもこの例では、人工的だし、意味論が意味不明になってしまっています (命題変数に真偽値を与えるのがこれのモデルと言えるのかどうか)。 人工的でなく、意味論が良く整備されていて、 かつ完全性が成り立たない形式的体系ってあるんですか? 611 名前：１３２人目の素数さん [2005/09/09(金) 08:02:31 ] 一階の理論の完全性を証明するためのアプローチの仕方って、 たしか、その理論の公理系で証明可能でない論理式を真でないにするその理論のモデルをつくる方法を考える、ってことでしょ （だから、その形式的体系で証明可能でないなら、任意のモデルに対して、真である、ではない、と、） 一階の理論全般に言えることだったか、ある算術の理論に関する内容であったかは忘れましたが ついでにおれも、似たような質問、 一階の理論（関数記号を用いる等号記号付きの一階述語論理を利用して作られる理論）は、必ず、同型ではないモデルを持つ（範疇的でない）、とのことらしいですが、 もっと弱い論理を利用して作られる理論なら、範疇的であるものもあるのでしょうか？ 例えば、関数記号を用いず、一項述語記号しか、表現として持たないような一階述語論理を利用して作られる理論からして、すでに範疇的でないということですか？ それよりも、 誰か、A7についてのコメントを・・ 612 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 09:52:04 ] A7は項でなく論理式(あるいは、原子論理式)φ について 　　 (x = y)∧φ(・・・x・・・） → φ(・・・y・・・） が普通。項に関するものは A6 と組み合わせると出てくる。 613 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 09:53:40 ] >>611 ＞誰か、A7についてのコメントを・・ についてだけど、 ＞＞（宿題） ＞∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ） ＞と ＞∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ） ＞とが、導出できるんだろう、ことは、状況からして、なんとなくわかりますが、とりあえず、今の俺には、ﾑﾘﾎﾟです。 なんて言い方してるってことは、入門書さえ読んだことないってことでしょ？ そういう努力しない人にはあまり教える気になる人は出てこない気がするなあ。 614 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 11:54:16 ] >>613 それもだけど、 607 名前：１３２人目の素数さん ﾒｪﾙ：sage 投稿日：2005/09/08(木) 20:07:40 >>606 > ∀ｘ∀ｙ∀ｚ（（ｘ＝ｙ∧ｙ＝ｚ）→ｘ＝ｚ） ∧ が現れる規則がないから ⇒ だけで書かないと。 608 名前：１３２人目の素数さん 投稿日：2005/09/09(金) 00:10:36 ∀ｘ∀ｙ∀ｚ（（¬（ｘ＝ｙ→¬ｙ＝ｚ））→ｘ＝ｚ） ということになるんでしょうか の方が激しく気になる。 615 名前：609 mailto:sage [2005/09/09(金) 16:06:32 ] 検索してみると、「1階様相μ計算」という形式的体系は完全ではないようです。 とすると、ある論理を形式化して意味論を与える際、 健全性は必須としても、完全性は必ずしも追求しないのですね。 616 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 16:55:06 ] >>615 純粋数学としてはどうか知らんが、計算機などでの応用においては 証明システムが嘘をつかないことが保障されてたらそれでいいのではないかと思う。 617 名前：１３２人目の素数さん mailto:sage [2005/09/09(金) 17:14:41 ] >>616 なるほど。健全性が「その証明システムが嘘をつかない」と表現されるのですか。 自分は計算機基礎論を良く知りませんが、 その意味では確かに完全性は強すぎる要請のようですね。 ありがとうございました。 618 名前：１３２人目の素数さん [2005/09/16(金) 06:22:34 ] 最近よく聞く「数学の哲学」とか言う分野って基本的にこの 数学基礎論みたいなことやってるんですよね？ 619 名前：１３２人目の素数さん mailto:sage [2005/09/16(金) 16:03:56 ] 数学の哲学は分析哲学の一分野とかだと思っとけばいいんじゃないのかな その分野の人は数学といえば集合論とか基礎論のことだとか思ってたりするｗ 基礎論はともかく、Logicといわれたら完全な別物だと思って良いかと 620 名前：１３２人目の素数さん [2005/09/19(月) 16:00:41 ] 自然演繹法ってのは、普通の一階述語論理の公理系での証明と、同じことやってるんですかね？ それとも、証明よりも、論理式を導出する力が強いんですか？ 例えば、 →導入則　　　　　Aを仮定し、その仮定のもとでBが導かれるとき、（Aという仮定なしに）A→Bを導くことができる と言うときの、（Aという仮定なしに）というのがよくわからないんですが、 仮定された論理式は、キャンセルされてるから、仮定された論理式は置かれていないので、 証明やってるのと、同じこと、ということですかね？ 621 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 16:17:26 ] →導入則ってこれのことだよね。  A ├ B ------- ├ A→B 普通の一階述語論理の公理系って？ 622 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 18:54:03 ] 強さは同じ 数学基礎論入門に、片方で導ける論理式はもう一方で示せることの証明も載ってる （まあこんなの読まなくても大体証明のやり方は見当付くと思うけど） 623 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 21:55:25 ] >Aを仮定し、その仮定のもとでBが導かれる ”普通の一階述語論理の公理系”に公理として論理式「A」を加えると、論理式「B」の証明が作れる >（Aという仮定なしに）A→Bを導くことができる ”普通の一階述語論理の公理系”にて、論理式「A→B」の証明が作れる 624 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 23:32:44 ] 自明でないのは演繹定理だけだな。 証明図の高さに関する帰納法で証明。 625 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 03:01:09 ] 演繹定理なしだと、証明問題がやたらムズイねｗｗｗ 626 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 13:18:13 ] >>619 ＞その分野の人は数学といえば集合論とか基礎論のことだとか思ってたりするｗ マジレスすると、まだそのあたりまでしか総括できていないだけ。 627 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 18:58:10 ] まだっていうか、数論幾何とか微分位相幾何学とか複素多様体論とか、 そもそも哲学の人は総括するつもりないでしょ まあ無くて構わないけど 628 名前：１３２人目の素数さん mailto:sage [2005/09/21(水) 11:47:03 ] レスくれた方、 ありがとうございました。 629 名前：１３２人目の素数さん [2005/09/21(水) 21:05:40 ] （例えば、）ロビンソン算術の公理系でのある論理式の証明を考えるときに、 根性が足らんくて、この論理式は、私には、証明可能できない、というのではなくて、 この論理式は証明可能でない、というのは、どうやって言ってるんですか？ ∀ｘ（0＋ｘ＝ｘ）はロビンソン算術の公理系で証明可能でない、というのを本で見たんですが、 630 名前：１３２人目の素数さん mailto:age [2005/09/21(水) 22:57:12 ] たとえばそれが成り立たないモデルを作るとか 『数の体系と超準モデル』の五章に問題として載ってるみたいですよ 本で見た、というのがこの本のことだったら済みません 631 名前：１３２人目の素数さん mailto:sage [2005/09/22(木) 21:36:13 ] いえ、いえ、どうもです。 とりあえず、図書館逝って借りて読んでみます。 632 名前：１３２人目の素数さん mailto:age [2005/09/23(金) 00:21:11 ] pp.116の問題1ね 問題1 次のことを証明せよ(1).........（略） (3) Qで∀ｘ（0＋ｘ＝ｘ）は証明できない 巻末に答えが載ってます 633 名前：１３２人目の素数さん [2005/09/29(木) 15:40:59 ] 295 ：１３２人目の素数さん ：2005/09/29(木) 11:58:46 夫馬です。 黒木先生。この基礎論・計算科学屋を叩いて下さい。 「完全証明」という専門用語を使い、「今まで数学 的に完全な証明がなかった！」というように素人に 思い込ませる。コケオドシをやっています。ポモ的 です。やっつけて下さいな。 ＞フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの ＞数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大 ＞工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との ＞約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り ＞などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が ＞完成。中村教授らは「完全証明したのは世界初」としている。 www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html 634 名前：１３２人目の素数さん [2005/09/29(木) 15:41:58 ] 302 ：１３２人目の素数さん ：2005/09/29(木) 15:16:20 >>301 ポモ的なのに叩かないのは、そういう理由だったんだね！ 土建屋＝宇沢＝長谷川＝黒木 ← 隠れポモ野郎 禿藁＝Ｕ健爾 ← 隠れポモ野郎 あほ鴨＝中村 ← 隠れポモ野郎 303 ：１３２人目の素数さん ：2005/09/29(木) 15:26:53 >>302 >>295 こいつらって、結局 ポモと同じでしょ。 ＞そして、別の場所で、極端なことを言っているのではないかと非難された場合には、 ＞3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。 www.math.tohoku.ac.jp/~kuroki/FN/relativism.html 635 名前：１３２人目の素数さん [2005/10/04(火) 21:26:07 ] 構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である、ってのは、 自然数上の足し算のみの体系は構文論的に完全で、モデル（Ｎ,＋,s,0）によって充足されてて、 証明可能でない論理式を加えたものは充足可能でないから、証明可能である論理式の範囲とモデル（Ｎ,＋,s,0）のもとで真である論理式との範囲が一致して、 で、モデル（Ｎ,＋,s,0）のもとで真である論理式の範囲を定義できる、ということですか？ 636 名前：１３２人目の素数さん [2005/10/05(水) 18:26:58 ] 358 ：今年のＡＡを振り返る ：04/12/29 09:28:40 　↓無職の引き篭もりのキモヲタの精神障害者フマ 　　　　　　　　〜∞ 　　 　／⌒⌒￣￣￣＼　〜∞ 　　／　　　　　　　　　　 ＼　　　〜〜〜〜〜 　　|　　　　　＿___丿ﾉﾉ.＿_|　　つ〜ん 　　|　　　 ／Ｕ　 .＿）　 .＿）　　　　ﾌﾟｩ〜ん 　　|　　　| 　 　　　　　 　 （　　　　〜〜〜 　　|　ノ（６ 　 ∵　（　。。） ）　　＿＿＿＿＿＿＿ 　　 　　　　　Ｕ　 　　) ３ .ﾉ　 /　＿＿＿＿＿＿__ ／ 　＼ ヽ ,,_　 Ｕ　 ___,,ノ　　/　/ 　　　 　＼,,＿__＿＿_,ノ ＼/　/　　＿＿＿＿＿ 　　　　　　 　　　　　　　 　./　/　　/| ..　 　　　　　　　　　　　　./　/　　./ .| 　　「殺人的ブスいないかなぁ？僕ちゃんブス大好き☆」 637 名前：１３２人目の素数さん [2005/10/05(水) 21:47:41 ] 質問の仕方がなんかまずかったみたいです（ｺﾞﾒﾝﾅｻｲ 率直に聞きます 構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である って、どういうことか、何方か教えていただけないでしょうか 638 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 22:32:50 ] >>637 真である論理式すべてといったら、算術的に定義できないに決まっている のではないでしょうか？ それとも、ある部分集合というなら、空集合は算術的に定義できますね。 何を訊いているんですかね。 639 名前：１３２人目の素数さん [2005/10/05(水) 23:10:06 ] 『数学基礎論講義』という本を読んでいるのですが、 構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、 とありまして、 ・構造で真である論理式の集合を算術的に定義する、というのはどういうことか、 ・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、 ・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、 について、よくわからないでいる、という次第です 640 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 23:19:32 ] >>637 算術的に定義できる、の定義が知りたいんじゃないの？ >>639 ゲーデル数でも考えて自然数の部分集合として考えているんじゃないのかな？ しらんけど 641 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 01:44:26 ] ってかそんな言い回しが未定義で使われてるわけないと思うのだが。 論理式のゲーデル数を入力とするある算術的な手続きによって 全ての論理式の真偽が決定可能である、といった感じかなあ。 642 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 02:54:04 ] いや、あの本は未定義で使われてたかと こういう定理もあるよ、というコメントの部分に書かれてた 何の定理だっけ 643 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 04:21:55 ] >>642 ＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 ゲーデルの定理と同じことだけど名前は知らん。 ＞構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、 プレスバーガー(Presburger)の定理 644 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 06:01:00 ] > ＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 > ゲーデルの定理と同じことだけど 不完全性よりは弱くね？ 645 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 09:12:34 ] Tarskiの定理だっけ？ 646 名前：１３２人目の素数さん [2005/10/06(木) 10:56:46 ] ありがとうございました。 あと、 『数学基礎論講義』で、 構造（Ｎ,＋,・,s,0）で真である論理式の集合を公理とする理論は完全であるが、具体的には、なにがこの理論の公理なのかがわからないので、このままでは使えない。 ある理論が数学として妥当であるためには、その公理の集合が再帰的であること、が最低限要請される。 という部分があって、 理論の固有の公理の集合は再帰的である必要がある。 ということかな？とも思ったんですが、 r.e.公理化可能という言葉もあるし、理論の固有の公理の集合はr.eであればよかったんじゃなかったっけ？ と、ちょっと、よくわからないでいます。 647 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 11:59:15 ] >>646 r.e.では不便。 公理でないときの判定ができないから。 r.e.の意味を理解していれば自然に分かる筈 理解してないなら分からないだろうが。 648 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:11:55 ] ＞・構造で真である論理式の集合を算術的に定義する、 ＞というのはどういうことか、 つまり構造で真である論理式のゲーデル数の集合が、 算術的性質によって記述できること。 649 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:19:06 ] ＞・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、 プレスバーガーの証明を読め。 ちなみにこの結果は、ゲーデルの不完全性定理の直前に出された。 650 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:23:10 ] ＞・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、 "ゲーデル・エッシャー・バッハ"を読め。 651 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 13:49:23 ] お前は出てくんな 652 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 14:29:14 ] >>651 お前こそ消えろ

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef