数学基礎論・数理論理学のスレッド　その7

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/ 480 名前：１３２人目の素数さん mailto:sage [2011/03/22(火) 18:59:09.84 ] >>466 >429は一般に言えることなの？ p を命題変数とする。勝手な論理式 A に対し、 p が証明可能ならば A も証明可能 しかし、p→A は一般にはトートロジーではない。 証明可能の条件をもうちょっと強めると、古典命題論理の範囲では Mints による定理があって、逆にあたることが成立する。 481 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 00:53:46.06 ] >算術の定理に必要な関数記号を論理学の述語で代用するということは、 >数学を二階述語論理で直接展開するということでしょうか。 は、私がそういうことかなと推測した内容で、本が言っている内容かはわかりません 数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない じゃあどうやって？ 述語でやろうというのか？しかし・・ という感じで質問に来ました 482 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:44:06.57 ] 非古典論理の階層（１） Modal logic 　Classical modal logic 　　Regular modal logic 　　Normal modal logic 　Modern modal logic 　　Temporal logic 　　　Propositional dynamic logic 　　　Linear temporal logic 　　　Interval temporal logic 　　　　Graphical interval logic 　　　　Signed interval logic 　　　　Future interval logic 　　　Kinetic logic 　　Dynamic logic 　　　Propositional dynamic logic 　　　Multimodal logic 　　Hennessy-Milner logic 　　Epistemic modal logic 　　Public announcement logic 　　Product update logic 　　Deontic logic 　　　Dyadic deontic logic 　　Imperative logic 483 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:44:42.49 ] 非古典論理の階層（２） Algorithmic logic Branching-time logic 　CTL* 　　Computational tree logic Tense logic Computational verb logic Hybrid logic Quantum logic Many-valued logic 　Fuzzy logic 　　T-norm fuzzy logics 　　　Monoidal t-norm based logic 　　　Product fuzzy logic 　　　Nilpotent minimum logic 　　　Lukasiewicz logic 　　　Godel-Dummett logic 　　　Basic fuzzy logic 　Post logic 　Kleene logic 　Provability logic 　　Interpretability logic 484 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:45:10.90 ] 非古典論理の階層（３） Bayesian logic Probabilistic logic Subjective logic Combinations logic Substructural logic 　Relevant logic 　Linear logic 　　Strict logic 　　Full linear logic 　　Modern Lambek calculus 　　　Non-commutative logic 　　　　Cyclic linear logic 　　　　Pomset logic 　　　　BV 　　　　NEL 　　Bunched logic 　Affine logic 　　Direct logic 　　Full affine logic 485 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:45:50.52 ] 非古典論理の階層（４） Paraconsistent logic 　LP 　FDE Doxastic logic Floyd-Hoare logic Description logic Minimal logic Independence-friendly logic Dependence logic branching quantifier logic Non-monotonic logic 　Default logic Autoepistemic logic Free logic Connexive logic Combinatory logic Categorical logic Q0 Logic Ω-logic Separation logic ： ： 486 名前：１３２人目の素数さん [2011/03/24(木) 00:05:02.46 ] 分岐量化子とか客観論理が好みですね... まぁ私は全て知っていましたけど。 487 名前：１３２人目の素数さん [2011/03/24(木) 00:49:54.63 ] そんなにいっぱいあるんですか… それらを(ある程度)統一した強力な体系とかあるんでしょうか？ 488 名前：１３２人目の素数さん [2011/03/24(木) 07:37:33.20 ] Wikipedia 489 名前：368 ◆jkwVJMjC32 [2011/03/24(木) 08:08:58.26 ] >>481 > 数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない > じゃあどうやって？ > 述語でやろうというのか？しかし・・ > という感じで質問に来ました 述語論理で必ずしも算術をする必要があるのでしょうか？ Boolosの定理は算術の存在を仮定しなくても、成り立つように思えます。 一般的な論理と数学に必要な論理は分離していった歴史がありますから。 490 名前：１３２人目の素数さん [2011/03/24(木) 21:08:48.47 ] Paraconsistent logic 矛盾許容論理... もう何でもありだな。 491 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/24(木) 21:56:46.43 ] 上記リストの中から、 興味のあるものや、詳しく知りたいものがあったら 言ってもらって結構です。 大抵答えられます。 492 名前：１３２人目の素数さん mailto:sage [2011/03/25(金) 16:41:52.80 ] intuitionistic logic がないのは何故だろう? 493 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/25(金) 23:47:24.56 ] >>492 直観主義論理は上記リストから見ると、 ちょっと古いのではないでしょうか。 古典論理から中間論理、直観主義論理、そして超直観主義論理までの 意味論はクリプキが可能世界の導入によって自然に拡張しましたから、 当然、上の非標準論理の基礎にはなっています。 しかし上のリストは恐らく、 様相論理を基本的な枠組みとして取り入れた 論理を紹介する意図があったのではないでしょうか。 いずれにしろ、個人の仕事なのですから 上記リストに抜けがあることは致し方ないでしょう。 それよりも良い検索キーワード集を提供してもらえたことに感謝しましょう。 494 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 18:29:03.87 ] Public announcement logicって名前が面白いな どういうことをやるんだろう？ Taoのblogに載ってたようなcommon knowledge的な話とかかな？ あとInterpretability logic とΩ-logic について宜しく 495 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 19:45:59.19 ] >>493 368の過去レスを見るとそんな偉そうな総括が言える力量とは思えない おそらくハッタリであろう 496 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 20:33:19.56 ] ロジックの本を読むのは初めてなのに それが日本最高峰の教科書と言っちゃうくらいだからな>>188 497 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/26(土) 22:32:27.30 ] >>496 正確にははじめてではないですね。 知識と信念の論理という本がはじめてですね。 この本で命題論理・述語論理から 様相論理、デフォルト論理やメンタル・スペース理論まで まとめて学習しました。 理解できない部分は論理と計算のしくみという本で補填しました。 またこの本で完全性定理や不完全性定理を学習しました。 498 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/27(日) 08:26:17.10 ] 公開告知の論理PAL（Public announcement logic） 動的認識論理DEL（Dynamic Epistemic Logic）の一種で、 公開告知やプライベートなどの多種の言語伝達に依存して エージェントたちの認識状態が変化するというアイデアによる。 様相論理を基礎にしている。 例 APLにおける文φの意味の公開告知の型がφ！であるとき、 様相演算子を[φ！]、<φ！>と置く。さらに命題ξに対して、 公開告知の後、[φ！]ξが真する。 ξが「K_aχ：エージェントaがχを知っている」で定義されるとき、 公開告知によって[φ！]K_aχが真。 これは公開告知による知識の変化を記述している。 おっしゃられる通り、common knowledge やmutual knowledge への拡張もされています。 また認識論理の代わりに義務論理を選択することで、 指令論理ECL（Eliminative Command Logic）なども作られました。 関連 DEUL (Dynamic Epistemic Upgrade Logic） DDEPL（Dynamic Deontic Epistemic Preference Logic） Arbitrary Public Announcement Logic (APAL) Future Event Logic（FEL） カテゴリ 数理論理学｜計算機科学 499 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/27(日) 09:08:57.64 ] 解釈可能性論理Interpretability logic 証明可能性論理GLを拡張したもので、さまざま種類があります。 算術的に完全なILMやモンターギュの公理を加えた最小論理IL、 持続公理をILに加えたILPなど。 p、q...は束、 ∧、∨、→、⇒は様相論理のオペレータ 定義1 d(p)＝1 d(⊥)＝0 d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1 公理2 略 自分よりも弱い理論の文を自分の中に置き換えて 数学的な性質を比較するという感じでしょうか。 500 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/29(火) 23:09:07.72 ] 解釈可能論理(IL) GL＋述語記号△ 二項様相演算子△を以下のように定義する。 理論Tにおける、A△Bの算術的な実現は TにBの実現を加えたものは、TにAの実現を加えたものを解釈可能である。 つまり、Tの言語の論理式で、 T＋B |― C implies T＋A |― f(C) となるような比較解釈可能関数ｆが存在する。 定義１ 式Aの次数d(A)を次を満たす。 ・d(p)＝1 ・d(⊥)＝0 ・d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1 定義２ ILの公理 K:□(p→q)→(□p→□q) L:□(p→p)→□p J1:□(p→q)→(p△q) J2：(p△q)∧(q△r)→(p△r) J3:(p△r)∧(q△r)→((p∨q)△r) J5:(◇p)△p ILの推論規則 MP 501 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/29(火) 23:09:26.37 ] 定義３ ILPの公理 ILの公理に以下の公理を加えたもの P:(p△q)→□((p△q)　(永続公理) 定義４ 論理式Aと論理Lについて、L+Aとは、 L∪{A}を含む論理式の最小の集合で、 様相論理のMP、置換、必然性の3つの規則において閉じている論理。 定義５ IK4とは、 K、J1、J2、J3、J5に、 4：□p→□□p を加えた6つの公理とすべてのトートロジーを含む最小の論理式の集合で、 様相論理のMP、置換、必然性の3つの規則において閉じている論理。 定理１ IK4 ⇔ △-free fragment が様相論理K4となるILの部分論理。 定理２ IK4＋PはILPの部分論理。 定理３ IL＝IK4＋L ILP＝IL＋P＝IK4＋P＋L 定理４ IL、ILPはクリプキ構造で完全。 502 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 19:18:55.66 ] 定義６ Γ_A≡Γ−{A}を論理式の集合、 ◎∈{□,◇,¬}を接頭辞としたとき、 ◎Γ≡{◎A｜A∈Γ} Γ△⊥≡{A△⊥｜A∈Γ} と表現し、推件式は以下のように表現する。 Γ→�� 定義７ 推件式GIK4Pの公理 A→A ⊥→ 503 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 21:24:29.35 ] 定義８ 論理式Aの部分論理式の集合をSub(A) Γ∪∆の各論理式の部分論理式の集合をSub(Γ → ∆)で表す。 定義９ GIK4Pの推論規則。 (T→)Γ→∆：A,Γ→∆　 (→T)Γ→∆：Γ→∆,A　 (cut)Γ→∆,A、A,Π→Λ:Γ,ΠA→ ∆A,Λ　 (∧→i)Ai,Γ→∆：A1∧A2,Γ→∆　 (→∧)Γ→∆,A、Γ→∆,B：Γ→∆,A∧B　 (∨→)A,Γ→∆、B,Γ→∆：A∨B,Γ→∆　 (→∨i)Γ→∆,Ai：Γ→∆,A1∨A2　 (⊃→)Γ→∆,A、B,Γ→∆：A⊃B,Γ→∆　 (→⊃)A,Γ→∆,B：Γ→∆,A⊃B　 (△K4P)A,{B,X1,···,Xn}△⊥,Σ→B,X1,···,Xn、Σ→Y1△B、…、Σ→Yn△B： X1△Y1,···,Xn△Yn,Σ→A△B　 504 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 21:29:12.26 ] 残念ながらこの論理の肝である、 シーケンス計算は、 証明図が奇抜な形をしているため 掲示板に書くことはできませんでした。 505 名前：１３２人目の素数さん [2011/04/03(日) 01:45:35.55 ] N型推論図ってすごい使いにくいような気がする。 これのメリットって何があるの？ 506 名前：論理体系の表現能力 [2011/04/03(日) 12:08:08.76 ] ↑たかい ↑ 様相論理（時相論理・認識論理・信念論理...） ↑ 中間論理 ↑ 超直観主義述語論理 ↑ 超直観主義命題論理 ↑ 直観主義述語論理 ↑ 直観主義命題論理 ↑ 部分構造論理(ランベック計算・線形論理、矛盾許容論理、ウシュカヴィッチ多値論理、ファジー論理、適切論理...) ↑ ↑ひくい 大体こんな関係じゃないでしょうか？>>487 507 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 19:08:36.22 ] 予習が完了しました。 今夜からΩ-論理の説明をはじめましょう。 508 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 20:39:42.43 ] >>491で大抵答えられますって言ってたのは 勉強したら答えられるようになりますって意味だったの？ 勉強したての人間の説明は何が本質的なのか全然分かんないから勘弁してほしい 509 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 21:28:09.34 ] いえ、「Ω-論理以外」は何でも答えられるという意味である。 上記のリストにΩ-論理はない。 510 名前：１３２人目の素数さん [2011/04/06(水) 10:18:46.30 ] １０は３で割り切れないって言うけど１０人分のケーキを三人に分けることはできるんだが？ hatsukari.2ch.net/test/read.cgi/news/1302019119/l50 511 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 11:09:08.03 ] >>510 凄い発見だな！僕は自分の人生さえ割り切りが付かないぞ！ 512 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 22:33:49.35 ] 仏教論理もこのスレでいいの？ 513 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 23:42:36.65 ] >>512 現在仏教論理は主流ではないですね。 量化が特殊なので非常に研究が難しい。 イスラエルでマルグリス（超剛性定理で有名な）らにより 研究されているキリスト教的論理学との関連が指摘されています。 キリスト教的論理学の推論規則ではほとんどの仮定が落ちません。 514 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:01:16.27 ] インド論理⊇仏教論理∪易罫 515 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:03:17.55 ] 仏教論理は様相論理 516 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 13:06:25.30 ] 区体論はこのスレでいいんすか？ 517 名前：１３２人目の素数さん mailto:sage [2011/04/08(金) 20:06:05.60 ] >>494 > Taoのblogに載ってたようなcommon knowledge的な話とかかな？ え？ テレンス・タオってロジックにも進出しているの？ 天才に来られると萎縮するわ... 518 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:12:13.38 ] >>505 N型推論図（フレーゲ流）はNKなどの公理を持たない体系で、 仮定を落とすのを記述するのに使われることが多いです。 L型推論図はシーケント計算など仮定がない体系で使われます。 一般的な数学はNKのN型推論図などを用いると表現しやすいです。 シーケント計算のL型推論図は様々な論理式を 証明するのに下から辿れるので使いやすいです。 本によっては → が |― と書かれていたりしてまちまち。 またHKは仮定がないのでL型で書かれることが多いです。 （HKは公理の変形が複雑だが部分構造論理で使われるそうな） それから論理式の左側にtermと呼ばれるものをつけて、 証明の経路を辿れるようにしたものもありますね。 この際、NKの仮定をラムダ項に対応させることが出来、 カリー・ハワード対応と呼ばれることもあります。 仮定の落ちる回数に制限を設ける論理もあったと思います。 519 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:16:06.90 ] ま初歩的な証明論程度の質問ならなんでも 答えられるので何でも聞いて良いですよ。 520 名前：１３２人目の素数さん mailto:sage [2011/04/10(日) 21:52:24.80 ] 実は証明論に公理は不要である。 これを知らないから無駄な努力をしてしまう。 521 名前：１３２人目の素数さん mailto:sage [2011/04/13(水) 23:51:38.10 ] kamome.2ch.net/test/read.cgi/math/1293882228/980 岩波書店5月　『数学基礎論』新井敏康　著 ttp://www.iwanami.co.jp/hensyu/science/next.html 気合入ってるなあ　楽しみ みすずから出たトルケル・フランセーンの本もかなり良いよ。 ロジック専攻というレベルじゃなくて不完全性周りが まさに著者の専門だからかなり細かいことまで徹底的に書いている。 但し著者独自の主張じゃないか、と思うようなことも無いではないけどね。 訳者の田中先生って今どうしてるんだろうか。 今年春に東工大で講演会やるみたいな話あった気がするけどどうなってるのかな。 522 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 07:08:42.36 ] 微積分みたく入門書ばかりがどんどん増えていきますね。 メドベージェフ次数が日本に紹介されるまではまだかかるでしょうね。 523 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 08:18:58.10 ] 　　ま　　た　　お　　前　　か 524 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:12:25.74 ] 日本語の本は入門書のみで十分。 後は英語の世界。 525 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:20:30.70 ] >>521 内容は Shoenfield のと同じようなもん？ 526 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 20:55:12.37 ] >>525 Shoenfield は証明論がなかったですよ。 それから計算理論が何を指しているのかが分かりません。 ページ数が気になりますね。 解説を読む限り強制法にも触れてそうですね。 ただメドベージェフ還元まではいかないと思いますね。 527 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:34:06.56 ] 帰納関数論でしょ。 528 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:39:51.30 ] 原子帰納関数を導入してから、 ゲーデルが証明したのに近い不完全性定理を導入するってことですか。 算術的階層やペアノ算術までいくShoenfieldよりは進まないということかな。 529 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 22:15:29.27 ] ペアノ算術やらないわけない。 入門篇で原始帰納関数、基礎編で超限帰納法やるんじゃないだろうか。 530 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 00:58:48.51 ] 集合論をかなりやってから証明論に進む構成だから、 新井先生の専門とかから考えるなら、 再帰的Mahlo順序数とかを使うKP（ZFの断片）に対する順序数解析とかに 触れたりして現代の証明論を紹介したいのかな、とか思ってるんだけど。 PohlersのProof Theory: The First Step into Impredicativity（11章）とか RathjenのThe art of ordinal analysis www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf とかの後半（2.2. Set theories.以降）とか。 新井先生のarxiv.org/abs/1102.0596で言うなら4 Jäger以降の内容。 ちょっと希望的観測過ぎるか。 531 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 20:27:40.85 ] 順序数解析はやっぱり入れるんじゃないか 532 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 01:08:11.68 ] にわかで申し訳ないんですが、 モデル理論とはどのようなものなんでしょうか ゲーデルあたりの研究成果を元に生まれたとは聞いたんですが 533 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 07:46:53.79 ] 理論のモデルを研究することですね。 534 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 17:24:57.55 ] >>532 タルスキが最初だよ。 ゲーデルと並行して研究されてた。 535 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 22:55:12.90 ] >>533 >>534 なるほど 「モデル」がどういう意味なのか分からなくて困ってましたが 要は意味論のことなんですかね ありがとうございました 536 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 23:57:38.44 ] 正確には意味論がモデルと等しいわけではないですね。 1階述語論理の意味論は構造と呼ばれており、 この構造である理論のどんな論理式を解釈しても、 真になれば構造が理論のモデルになるとされますね。 つまりある理論を「まともに」解釈できる構造のことですね。 無矛盾な理論はモデルをもつ。 という完全性定理がモデル理論の初期の研究成果です。 それからコンパクト定理とレーベンハイム・スコーレムの定理は どんな本にも載っていますね。 例えば、 可能世界で有名なクリプキ構造は様相論理のモデル、 チューリング・マシンはある計算理論のモデル、 2^ωが型なしラムダ計算のモデルになったりしますね。 ハインティング代数やブール代数などの代数的構造を モデルにすることで、論理学を代数にする手法もあります。 モデル間の同型写像を考えて構造同士の関係・分類もできます。 連続体仮説のZFCからの独立性を証明する強制法のアイデアも 提供しておりますし、モデル自体をZFC上で形式化する研究もあります。 また様々な階数の述語論理を計算の複雑さの階層 （EXPとかPSPACEとかNPとか...）に対応させ、 算術的階層などと組み合わせて現代数学の全体像を浮かび上がらせる 記述計算量理論というものにもアイデアを提供してます。 大雑把にいって証明論に対して存在しているようにも思われます。 537 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 00:03:25.54 ] 訂正： つまりある理論を「まともに」解釈できる構造のことですね。 ↓ つまりある理論を「正当に」解釈できる構造のことですね。 まともでない解釈も存在しますからね。 538 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 11:25:13.19 ] なるほどなるほど 面白そうですね 丁寧にありがとうございました！ 539 名前：１３２人目の素数さん mailto:sage [2011/04/22(金) 21:46:08.83 ] 上の方で登場したヒルベルトの公理なんですが、 これっていくつ位存在するんですか？ リストみたいなものってありますか？ それから今使われてる公理はなぜ使われるようになったんですか？ 540 名前：１３２人目の素数さん mailto:sage [2011/04/23(土) 08:16:45.01 ] ベクトル空間の基底の取り方みたいなもので無数にあるよ たぶん自分で独自に選んで本書く人も多いんじゃないかな 541 名前：１３２人目の素数さん [2011/04/23(土) 11:40:28.66 ] 自称論理学者（ID:M/m1hILG）がとんでもない論理を展開中 yuzuru.2ch.net/test/read.cgi/edu/1291023518/l50 542 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 00:15:26.75 ] 例えばヒルベルト流命題論理の 含意断片論理（論理記号が'→'だけのもの）で、 大抵の教科書に出てくる公理のように メタ変数が3個で論理記号4個でカッコの付け方が正常な論理式の総数だけでも、 ざっと概算したところ100万個を超えた。 一般の命題論理の¬や∧、∨など5種類ほど加えると数十億に到達するらしい。 公理選択で重要なのは、「独立」を調べること。 MPを推論規則にもつとき、 A→A A→A→A A→A→A→A の3つで上の2つの文は下の文から証明可能なので公理に不要。 「完全性」「健全性」「独立」などの条件が重要で、 定理自動証明機械なども研究された。 歴史的にほとんどの証明体系が意味から出発している。 にもかかわらずそのほとんどが上記条件を満たすのである。 543 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 07:10:00.79 ] 数十億ではなく6億くらいですね。 カッコの付け方が位相みたいに、 シンプルに計算できないので正確ではないですが。 544 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:39:01.16 ] おい、公理系の独立性はたいして重要で無いだろ。 おまいは、命題論理の公理系学んだとき、その独立性チェックしたか？ 多くの教科書同様、完全性と違ってしてないはずだ。 545 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:57:23.11 ] 独立でなくてもいいのなら、明らかに無限通りあるからじゃない？ 546 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 20:39:31.01 ] 大抵の教科書に掲載されているHKの公理は、 ある程度意味のあるもの、 例えばLKとの同等性が示せるものだとかに 絞られているわけです。 つまり独立性を示す努力は本の著者というか、 「論理の歴史」が勝手に代替してくれているわけですね。 私が言いたかったヒルベルト流とは推論がMPだけという意味です。 そして独立性の証明は完全性よりはるかに煩雑です。 確かに必須ではありませんが、 無から公理を創造する場合は独立に近くする努力はするべきですね。 547 名前：１３２人目の素数さん [2011/04/24(日) 22:41:45.58 ] 論理学をやる人は高踏趣味があるのかやたら専門用語を散りばめた文章を書く。 少し解りにくいことも解っていて当然なような口ぶりだ。 548 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 22:53:10.92 ] 分かっている人ほど簡素な文を書く 分かったふりをする人は難解な文を書く 549 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 01:06:51.10 ] >544 重要でなければ強制法とかの技法も要らない気がするけど。 550 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 07:12:08.71 ] いや述語論理の独立性の話だろ Principia Mathemticaの公理なんか 独立じゃないことが数十年後に判ったんだぞ 551 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 11:42:06.24 ] 独立性の証明は難しいことが多い。 しかし証明が必要になることはまず無い。 552 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 16:59:17.12 ] 与えられた体系の中での命題の独立性と、 公理系そのものの独立性の話の話は区別しないと。 前者は気にするのが普通だし、重要な問題であることも多い。 後者はよほど特別なことがない限り、気にすることはない。 553 名前：546 mailto:sage [2011/04/25(月) 20:50:54.18 ] >>547 それは私のレスポンスに関するものでしょうか。 そうであるとしたら具体的どこに高等趣味があるのかを、 該当箇所の引用したうえで述べてください。 >>551 詳しそうなので質問します。 独立の証明の有益な方法はありますか？ それから証明する必要がないとはいえ、 テキスト中のHKは大抵独立だったり完全だったり 無矛盾だったりして、 「子供が安全に遊べるように人為的に作ったアスレチック」で あることが多いとは思いませんか？ >>548>>550>>552 同感です。 554 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:04:40.48 ] 自覚あるんだね 555 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:22:09.77 ] いつぞやこのスレで総スカンを食らったコテの匂いがプンプンする 556 名前：546 mailto:sage [2011/04/25(月) 21:23:12.91 ] >>554 ローマに入ればローマに従えというか、 論理学を語る時だけ独特の文体になることは確かだと思います。 しかし、文章の中に含まれる専門用語は他の数学に比べれば かなり少ないと思いますが？ （まさか専門スレッドでテクニカルターム禁止だというわけでもないだろうし。） それに難解なことなんか言ってないんですよ。 普通に1階述語論理までやっていれば言いたいことは 分かると思うんですが。 557 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:34:54.22 ] それを言うなら郷に入っては郷に従えだ 英語のことわざとごっちゃにするなよ、半可通 558 名前：546 mailto:sage [2011/04/25(月) 21:45:09.44 ] >>557 >郷に入っては郷に従えだ あえてローマに入ればローマに従え といったんですが。 意図的に日常さはんじをちゃめしごとと読んだり、 既出をガイシュツと呼んだりする、 当たり前だのクラッカーみたいなノリで言ったんですよ。 これに関して本気で突っ込むそちらの方が半可通なのでは？ 559 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:58:46.82 ] 図星みたいだ 560 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 23:02:07.21 ] これはみっともない 561 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 00:10:16.55 ] >>558 ばーか 562 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 07:15:02.06 ] どうでもいいことで何を議論してるんだか…… Shoenfieldの第一章の演習問題は独立性を公理それぞれに対して証明しているよね 著者がそういう細かいことにこだわる人だったのかもしれない 563 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:09:34.17 ] >>552 > 与えられた体系の中での命題の独立性と、 > 公理系そのものの独立性の話の話は区別しないと。 前者はどういう意味? ある形式系で命題が形式系の他の公理から独立なら それは公理として認めないと真には成り得ないけど? 後者の「公理系そのものの独立性」って公理系が何対して独立なの? 564 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:11:21.23 ] >>562 独立でない公理があるなら、それは公理としては不必要なんだから、 基礎論的な意識の強い学者は当然こだわるわな。 565 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 18:31:40.30 ] >>563 そういう根本的なことから理解出来てないと、ビックリする 566 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:05:38.43 ] いくつかの公理・推論規則と それから証明可能なすべての論理式の集合をS、T、 ある公理または推論規則をA、 S＝T∪{A} としたとき、 TでAが証明できない。⇒SでAは独立。 Aが任意⇒Sは独立。 独立性証明のテクニック⇒3値論理。 567 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:22:28.23 ] おー久しぶりだな「考える人」 正直もう二度と見たくなかったが。 568 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:25:18.26 ] 訂正： 誤 Aが任意⇒Sは独立。 正 上記条件プラスAが任意⇒Sは独立。 計算機科学とかでは体系が 独立じゃないと一般的に色々複雑になるらしい。 569 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:04:15.53 ] >>564 集合論のZFとかだと各公理は独立じゃなかったりするでしょ。 独立性が大事かどうかというと、あまり大事じゃない場合も多い。 少なくとも完全性に比べると些事。 >>566 一般的にはAも¬Aも証明できないときに「独立」という気がするけど。 反証可能な場合は普通は含めない。 あとAが任意って何が言いたいのか分からない。 任意の式Aが証明不可能だということはあり得ない。 三値の真偽値の割り当てで証明不可能性が証明できることもあるけど 証明できないことも多いと思う。 570 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:07:16.28 ] >>569 ここはエレキな人が多過ぎて困りますなあw 571 名前：566 mailto:sage [2011/04/26(火) 22:10:07.14 ] >>569 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Aを証明できないことをいう。 さらにその公理系Sの中のすべての公理と推論規則が独立なら 公理系Sは独立。 という主張をうまく書こうとしたところ変な文章になっただけです。 なぜ、「Aも¬Aも証明できないときに「独立」」という定義に しないかといえば、 ¬という記号が公理系で必ずしも定義されているか不明だからです。 （公理的集合論やるなら気にしなくてもいいかもしれませんが。） 例えば¬AがA→⊥のメタ理論的な略記だとしても、 ⊥が公理・推論規則に含まれていないために、 単なる命題変数になっている場合もあるかもしれません。 それから3値論理はそういう方法もありますよ、位に行っただけです。 一般的に独立を証明する巧い手段は知りません。 572 名前：１３２人目の素数さん mailto:sage [2011/04/27(水) 00:21:21.26 ] そういや、公理がそれぞれ独立なZFて誰か考えないのかな？ どうすれば良いのか想像もつかないけど…… 573 名前：１３２人目の素数さん [2011/04/29(金) 08:43:43.06 ] 数理論理学の組み合わせ論的研究の本OR分野を教えてください。 上の論理式の総数みたいなやつです。 574 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 09:47:53.77 ] www.amazon.co.jp/dp/4320122097/ 575 名前：１３２人目の素数さん [2011/04/29(金) 23:10:35.52 ] >>558 ＞意図的に日常さはんじをちゃめしごとと読んだり、 ＞既出をガイシュツと呼んだりする、 ＞当たり前だのクラッカーみたいなノリで言ったんですよ。 若者＝バカモノっていうのはホントだね。 ホルモンが無駄に出てるせいかな？ 576 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:29:08.45 ] >>558が若いのか結構年取ってるのかも分からないし 仮に若かったって若者が皆バカって訳じゃないと思うけどなあ 577 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:44:05.25 ] >>571 それ「独立 independent」じゃなくて普通に「証明不可能 unprovable」で良い話だよね 578 名前：１３２人目の素数さん [2011/04/30(土) 10:50:22.25 ] >>577 大抵の論理学の本に書かれている定義に準拠しているなら、 独立は証明不可能より条件が強いと思います。 独立性は「公理と推論規則に無駄がない」という主張です。 証明不可能は理論の持つ公理と推論規則だけで 特定の論理式の証明図が書けないという主張です。 579 名前：謝罪 mailto:sage [2011/04/30(土) 10:56:05.79 ] >>571 を読み返してみたところ間違っていました。 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Sで証明可能な式でTでは証明できないものが存在すること。 でした。 580 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 11:18:11.62 ] >>579 謝罪を受理しました。 では続きまして、『賠償』を求めます。 宜しくお願い致します。

---

---

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

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