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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 515 名前：１３２人目の素数さん mailto:sage [2005/06/26(日) 15:35:41 ] 鴨に私怨を持つのは構わんけど それをこんな所に書かれてもきちがいが変なこと書いている， くらいの印象を受けるだけなんだが． 516 名前：１３２人目の素数さん [2005/06/26(日) 20:20:12 ] 大事なのは 鴨は、基地外達に私怨を持たれるようなことに精を出している ということ 517 名前：１３２人目の素数さん mailto:sage [2005/06/26(日) 20:36:15 ] いや2ちゃんで叩かれている数学者なんていくらでも たくさん居るし，ほとんどがただの悪口雑言だし． 518 名前：１３２人目の素数さん [2005/06/26(日) 20:38:06 ] ２ちゃんで叩かれている数学者＝禿藁 519 名前：１３２人目の素数さん mailto:sage [2005/06/29(水) 19:24:43 ] むやみに人の悪口をいってはいけませんよ。 520 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 02:08:34 ] 筋金入りの文系で高校で数�UBまでしか学ばなかったんですけど、 数学基礎論に興味持っています。というか哲学で敷衍されている ゲーデルの「不完全性定理」を理解したいなと思っているんですけど、 そこに到達するのに最適な入門書はあるでしょうか。 『形式論理学』（リチャード・ジェフリー）を教養課程のときに読んだことが ある程度なので、難しいかもしれませんが。 521 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 03:25:35 ] 広瀬健　横田一正　ゲーデルの世界　海鳴社 なんかがいいかな？ 522 名前：１３２人目の素数さん mailto:sage [2005/07/02(土) 20:34:25 ] 数学的帰納法判ってりゃ最初は十分だよ． もっとも中にはそれじゃ難しい本もあるけど． 523 名前：１３２人目の素数さん [2005/07/03(日) 03:36:40 ] age 524 名前：１３２人目の素数さん mailto:sage [2005/07/03(日) 04:32:37 ] というかその分野の本て多くないので全部当たればよし 525 名前：１３２人目の素数さん mailto:sage [2005/07/03(日) 05:51:14 ] いや結構あるぞ 526 名前：１３２人目の素数さん [2005/07/05(火) 20:29:19 ] 半径６２センチに２００粒 半径７０センチに２６８粒 62*62*3.14=12070 √12070が109だから、 縦横に109本の線を引いてその交点にゴマを配置すればいいのかな？ 70*70*3.14=15386 √15386が124だから、 縦横に124本の線を引いてその交点にゴマを配置すればいいのかな？ 密度はたぶん↓ １２４センチの面積：12070/200=60 １４０センチの面積：15386/268=77 数学苦手で。。。。(笑) 527 名前：１３２人目の素数さん [2005/07/05(火) 21:54:20 ] まず、公文式に通いなさい。 528 名前：１３２人目の素数さん mailto:sage [2005/07/05(火) 22:59:43 ] 最近の公文式はゲーデルやゲンツェンの定理までやるのだろうか？ 529 名前：１３２人目の素数さん mailto:sage [2005/07/06(水) 00:50:31 ] >>526 スレ違い 530 名前：１３２人目の素数さん [2005/07/09(土) 11:37:07 ] 数学基礎論の最近の発展について書かれた書物はありませんか？ 531 名前：１３２人目の素数さん mailto:sage [2005/07/09(土) 19:07:19 ] >>530 BSLに、各分野の最近の進展についてのサーヴェイがよく載ってるから、それを 読むのが一番手っ取り早いかと。 ttp://www.math.ucla.edu/~asl/bsltoc.htm 532 名前：１３２人目の素数さん [2005/07/11(月) 16:48:51 ] ある公理系で、証明可能である論理式に対応するゲーデル数を入力したときに、1を出力して終了する機械が作れるらしい、ということは本を読んでて、なんとなくわかったんですが、 ある公理系で、証明可能でない論理式に対応するゲーデル数を入力したときに、0を出力して終了する機械、というのも作れるんですか？ 533 名前：１３２人目の素数さん mailto:sage [2005/07/11(月) 21:11:19 ] >>532 公理系によって、可能だったりそうでなかったりする。 534 名前：１３２人目の素数さん [2005/07/11(月) 23:21:13 ] ロビンソン算術の公理系Qだとどうなりますか？ ロビンソン算術の公理系Qで、 ＞証明可能である論理式に対応するゲーデル数を入力したときに、1を出力して終了する機械が作れるらしい、ということは本を読んでて、なんとなくわかったんですが、 ロビンソン算術の公理系Qで、 ＞証明可能でない論理式に対応するゲーデル数を入力したときに、0を出力して終了する機械、というのも作れるんですか？ ということでした 535 名前：１３２人目の素数さん mailto:sage [2005/07/11(月) 23:59:56 ] >>534 上はできるけど下はできない。Qの非定理の集合はr.e.ではないから。 これがQが決定不可能であるということの意味。 536 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 00:59:17 ] >>533 なるほど、それが、決定可能、決定不可能、っつーことですね >>533 >>534 ありがとうございました 537 名前：１３２人目の素数さん [2005/07/12(火) 16:59:58 ] ＞Qの非定理の集合はr.e.ではない ところで、r.e.ではない集合、というものは、一般に、どういうふうに捉えられているのですか？ r.e.ではない集合も集合として扱う、枚挙が可能でないのは、ただ、機械の限界によるものだ、としてるのか、 機械で枚挙可能でないようなものは、集合としては定義できない、そんなものは集合として扱わない、というふうに考えてるのか 再帰的に枚挙可能である、ということが言われてる時点で、なんらかのステイタスとして認められているような気もするんですが、 r.e.ではない集合も集合として一応扱われているみたいだし、 集合であって、r.e.であるにこしたことはないが、r.e.でなくても、まぁ、別にかまわない、くらいのものなのでしょうか？ 538 名前：１３２人目の素数さん [2005/07/12(火) 18:13:56 ] ここの場所に書き込むべきかわかりませんが... a+b+c=2のとき2^a+2^b+2^cの最大値って存在するのでしょうか？ 539 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 18:24:28 ] ＞鴨さんが研究会議を開催します。 実際には、鴨は実行委員の一人だっていうだけ。 540 名前：１３２人目の素数さん [2005/07/12(火) 20:13:05 ] G=2^a+2^b+2^c-r(a+b+c-2) Ga=log2(2^a)-r=0 2^a=2^b=2^c a=b=c=2/3 3*2^2/3 541 名前：１３２人目の素数さん [2005/07/12(火) 20:23:40 ] ↑これって最小値では？？ 542 名前：１３２人目の素数さん [2005/07/12(火) 20:31:08 ] こまかいことはしらん 543 名前：１３２人目の素数さん mailto:sage [2005/07/12(火) 22:15:40 ] スレ違い 544 名前：１３２人目の素数さん mailto:sage [2005/07/13(水) 00:42:59 ] >>537 質問が漠然としすぎていあなたが何を言いたいのか分からない． r.e.ではないNの部分集合も集合ですよ． 545 名前：１３２人目の素数さん [2005/07/13(水) 01:23:15 ] ************************************************** 数学基礎論サマースクール2005のご案内 ************************************************** ・期間：2005年8月8日(月)から10日（水) ・場所：法政大学市ヶ谷キャンパス内，ボアソナードタワー26階 スカイホール（東京都千代田区富士見） ・テーマ：モデル理論 www.i.hosei.ac.jp/~ikeda/summ2005/program.html 546 名前：１３２人目の素数さん [2005/07/17(日) 15:37:10 ] descriptive set theory関係の話題ですけど、誰か知っている人はいませんか。 定義： 位相空間 X は以下の条件を満たすときBaire空間であるといわれる。 内点を持たない閉部分集合の可算和集合は内点を持たない。 この定義の「可算」を別の濃度に置き換えたものを 考えているのですが、文献が見つかりません。 547 名前：１３２人目の素数さん mailto:sage [2005/07/17(日) 16:15:31 ] >>546 それは descriptive set theory 関係でなく、set theory です。 Kunen の Set Theory の2 章の書いてあります。 548 名前：546 mailto:sage [2005/07/17(日) 16:38:11 ] サンクス！ こんなアッサリ知りたいことが分かるとは。 にちゃんってスゴい人がいるんだな。 549 名前：１３２人目の素数さん [2005/07/18(月) 21:39:06 ] 不完全性定理関係の書籍(洋書)で著名なものがあれば教えていただけませんか？ 550 名前：１３２人目の素数さん mailto:sage [2005/07/18(月) 21:49:41 ] >>549 これが一番安いかな？ K. Goedel, On Formally Undecidable Propositions of Principia Mathematica and Related Systems ttp://www.amazon.com/exec/obidos/tg/detail/-/0486669807/ 551 名前：１３２人目の素数さん mailto:sage [2005/07/19(火) 09:54:16 ] >>550 それは原論文の英訳。ちょっとそれだけでどうにかするのは無理と思われ。 Dover だったら薄い基礎論の入門書がアルからそっちの方がいいんじゃないか？ 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階様相μ計算」という形式的体系は完全ではないようです。 とすると、ある論理を形式化して意味論を与える際、 健全性は必須としても、完全性は必ずしも追求しないのですね。

---

---

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

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