数学基礎論・数理論理学　その11

1 名前：１３２人目の素数さん mailto:sage [2012/01/02(月) 23:04:29.50 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その10 uni.2ch.net/test/read.cgi/math/1319895756/ 45 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 20:20:55.15 ] >>31 ＞今の計算機の原理が変わらない限り一階論理がなくなることはない。 今の計算機の原理と一階論理にはどんな関係があるの？ 量子計算機とかDNA計算機とかだと、一階論理ではなくなる？ 46 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 20:41:38.99 ] >>42 透明性はエレクトラのパラドクスの発生や宵の明星・明けの明星の問題の話です。 論理へクリプキ意味論を導入すると、 文は一般に内包で、意味論側で可能世界が与えられると外延と解釈できるようになります。 このような不透明な体系、例えば様相論理は数学の記述は難しいとクワインが指摘したのです。 数学は2つの対象が等しいならば、両者で同じことが成り立つという客観（神の視点）を持つからです。 一方で普段通りに、モデル理論を意味論、1階論理を構文論とすれば、 自然言語の透明性が保存され外延交換が成り立ちます。 （実はその後、クワインは透明性を持つ体系での厳密科学の形式化を断念していますが...） 勿論自明なやり方でなら一階論理を含む様相論理で数学を書くことは可能ですが。 47 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 20:59:09.91 ] >>46 内包と外延の分析に有益というのは、様相論理の利点の一つだろうが、 それだけが様相論理を評価する場合の唯一の視点というわけではない。 Baltag のSTSでは、また別の視点が強調されている。 そこで「数学や一階論理の様な神の視点の立場に合致しなかった」と評価するのは ちとずれているんではあるまいか？ 48 名前：１３２人目の素数さん [2012/01/03(火) 21:19:02.83 ] >>16 >そのうち、記述論理が一階述語論理にとって替わるのかな？ >様相論理を記述論理に直して再チャレンジってことかな？ えー？記述論理って述語論理のちゃちなサブセットだろ？ 49 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:23:21.74 ] あちゃー、隔離スレではトンデモ学者に矢田部さんが味方認定されちゃってる。可哀想に。 50 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:29:49.63 ] AMC（空でない集合たちの族に対して、それらの各々の非空有限部分集合の族が取れる、という公理）から 選択公理をどうやって証明したらいいのか分かりません。 外延性公理と正則性公理が必要なのだそうですが、誰か分かる方いますか？ 51 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:51:52.07 ] >>49 俺も何度か経験あるけど、お前のトンデモ理論を俺が支持しているかのように書くのはやめてくれ、と思う。 ツワモノになると、自分のトンデモ理論が正しいと公式に表明してくれ、とかメール送ってくるし。 52 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 22:01:09.38 ] >>44>>47 STSは全く知りませんでしたね。だとすると誤読でしたね。 確かにクリプキの指示とかの話は内包論理に関する様相論理の話でしかない。 >>45 ＞今の計算機の原理と一階論理にはどんな関係があるの？ 一階論理程度の表現能力があれば十分だというところですね。 ホーン節はじめ分解原理・SLD導出・失敗による否定・エルブランモデル。 論理プログラムは部分帰納関数の表現まで使える...。 ＞量子計算機とかDNA計算機とかだと、一階論理ではなくなる？ 拡張する必要はあるでしょうね。 53 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 22:35:03.01 ] >>40 直観主義ブラウワーと形式主義ヒルベルトの論争があったように、 直観主義は本来は形式化に反対するものなので、 その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、 現代的視点で形式化した場合に、と断りを付けておくけど： 有名どころは、 扇定理(Fan Theorem) と 連続選択公理(実数の選択関数で連続なものが取れる) かな。これだけでブラウワーの数学が形式化できるのか、 もっと公理が必要なのかはよく知らない。 54 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 22:40:31.56 ] 補足すると、連続選択公理からは「実数値関数はすべて連続である」という定理が出る。 この定理は勿論、古典論理（とそんなに強くない数学的公理）上では矛盾するけれど。 だから、直観主義は、排中律を拒否して論理を弱めているので、古典論理より定理が少なくなる、というのはある意味嘘。 弱めているのは論理の部分だけで、非論理的公理の部分は一方が他方より強いとか弱いとかって関係にはない。 55 名前：ただのバカ [2012/01/03(火) 22:47:42.05 ] これからの論理は直観にいくよりも矛盾許容論理。 定理ごっそり増える 56 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 22:51:18.72 ] >>52 >＞今の計算機の原理と一階論理にはどんな関係があるの？ >一階論理程度の表現能力があれば十分だというところですね。 十分というだけで、必要でないのなら、 一階論理の断片となる論理がとって替わる可能性があるってことでは？ >今の計算機の原理が変わらない限り一階論理がなくなることはない。 と辻褄があっていない。 57 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:00:43.67 ] >>27 Every two elementarily equivalent models have isomorphic ultrapowers Saharon Shelah Israel Journal of Mathematics Volume 10, Number 2, 224-233, DOI: 10.1007/BF02771574 www.springerlink.com/content/j67206441630333u/ 58 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 23:11:44.90 ] >>56 もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。 ホーン節の分解システムも一階論理の断片だったりするし。 逆に一階論理に推移閉包や述語定数を添加する場合もある。 ペアノ算術の関数や述語をダイレクトに添加した例もよく見る。 ソフト側では、それ以上のファジーや適切論理なんかまで使うけど。 59 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:12:31.51 ] >>57 >>57さんへの文句ではないが、 なんでリンク先は出版年を明記してないんだろう？ 60 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:14:32.92 ] >もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。 それ言ったら様相論理も含まれるやん。一階論理はある程度の断片だし。 一階論理の代替になれなかった様相論理の次の候補、という話してるのに。 61 名前：１３２人目の素数さん [2012/01/03(火) 23:19:43.61 ] 低次元な議論は 　も　う　や　め　て　く　れ 62 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:22:25.47 ] >>59 確かに不思議ですね。出版は1971年だそうです。 最初のページを見てみると、 この手の話は一般連続体仮説G.C.H.を仮定した結果が多いみたいですね。 概要でもGCHを使わずに、と強調していますし。 これなら置換公理を使っていても全然不思議ではありませんね。 63 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 23:27:25.77 ] >>60 様相論理が一階論理の断片と考えられるといえばそうだけど、 わざわざ様相論理といったときは、大抵モーダルオペレータや 関係構造やらフレームやらを使用する意図があるという前提で。 （計算機で一階論理の述語や関数の引数を制限するのは別の理由。） 64 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:55:11.91 ] >>62 選択公理や正則性公理も当然使われているだろうな。 65 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 00:17:53.20 ] 第二不完全性の証明は結局分かったんだろうか？ 実際のところ、証明に必要な帰納法はΣ_1帰納法で十分だったの？ 66 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 00:22:44.64 ] >>55 ネタにマジレスかも知らんが、矛盾許容論理というと古典論理より弱い。 従って非論理的公理をいじらないのなら定理が増えるなんてことはあり得ない。 67 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 01:10:08.95 ] こっちに現れるんだろうからコピペしとこ 999 ：１３２人目の素数さん：2012/01/03(火) 00:46:52.02 　　数理学厨は >>917, >>923 で皮肉られて言い返せなくなったと見えて、姿を消したな。 　　前回は、伝統を良しとして歴史的偶然を批判するっていう自己矛盾を指摘されて言い返せず、 　　暫く消えていたがそのうち何事もなかったように現れた。 　　今後もまたほとぼりがさめたと判断した頃に現れるのだろう、新スレに。 68 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 01:44:23.59 ] >>57 その結果面白いね。 前スレで話題になっていた van Benthem's characterization theorem って、 ふたつの pointed model が modal equivalence であることと、 ultrafilter extension で bisimular であることが同値ってことだったけど、 一階述語論理にすると ultrafilter extension → ultraproduct bisimular → isomorphic という類推ができる。それなのに様相論理では普通に証明できるのに、 一階述語論理については集合論的な公理が必要だとすると、不思議だねえ。 69 名前：１３２人目の素数さん [2012/01/04(水) 02:14:16.13 ] >>36 天才と言われるクリプケが可能世界意味論を提案する前の様相論理は何を研究していたのか？ 70 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 02:28:24.73 ] >>54 ビショップの直観主義数学は、古典論理上の数学より弱いって聞いたけど 71 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 04:21:21.24 ] ああ、僧正と橋々の構成的解析ね。 72 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 05:08:22.74 ] 橋々？僧正は Bishop のことだな。 73 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 07:34:38.51 ] >>69 最初期はルイスやゲーデルやタルスキやマッキンゼーらが シンタックスのみで研究していた。 ただし関係構造が必要なのは知られていて、 カルナップの意味論なんかが考案された。 既にプライアーの時相論理が開発されていて、 自然数をドメインとして＜を関係として持つモデルがあった。 50年代の終わりにようやくクリプキ構造の完全性定理が出来る。 74 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 08:33:11.69 ] >>69 様相論理の体系で S4 とか S5 とかはあるのに、S1, S2, S3 がないのは不思議だよね？ これはクリプキ意味論以前から様相論理が研究されていた名残り。 S1, S2, S3 は通常の可能世界意味論を持たない。 少し変更を加えれば（非正則世界を許す）S2 と S3 は完全な意味論が可能世界意味論で作れる。 しかし S1 はどうやってもその手の意味論は与えられなかったはず、詳しくは知らない。 あと、S6 以降の体系も世の中にはある。 75 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:05:15.50 ] >>74 S1 から始まる体系の系列は、Lewis が厳密内意（論理学スレで話題になってた）の研究で提案したもので、 様相論理の研究と言ってしまっていいのかは疑問。 もっとも A ⊰ B を □(A→B) と、逆に □A を ⊥⊰ A と理解することで、 厳密内意と様相は同じものとみなしていいんだけどね。 （少なくとも S2 以上は。S1 はどうだったか忘れた。） ある意味、適切論理の先行研究ともいえる。 76 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:25:30.07 ] 俺は>>68はいいこと言ったと思う。こういうものの見方が必要だと思うんだ。 だからこそ、哲学はこのスレから出て行けとか、哲学的論理学はスレから分けるべきだとか、 そういう「排除の論理」には賛成しかねる。数学系の論理学と哲学系のそれが、 近いことをやっていて、スレが一緒で問題がないのなら、そのまま一緒にやっていくのがいい。 「排除の論理」の人々は、分類フリークっていうか分類することが目的になってると思うんだよね。 77 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:37:31.81 ] >>75 >逆に □A を ⊥⊰ A と理解することで T ⊰ A じゃなくて？ >>76 禿堂。数学系の論理学と哲学系の論理学だけじゃなくて、計算機系の論理学もな。 78 名前：１３２人目の素数さん mailto:age [2012/01/04(水) 10:00:03.96 ] おっと、ここで「数学じゃない」厨が現れて、 哲学なんかと仲良くしようというなら哲学板へスレごと移動しる！ とか言い出すに一票。 79 名前：１３２人目の素数さん mailto:age [2012/01/04(水) 10:01:48.99 ] >>77 >T ⊰ A じゃなくて？ 仰るとおりでございます。 80 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 11:26:40.86 ] >>74 またS6以降はどう決まるのでしょうか？ 81 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 14:07:47.35 ] 我々エイリアンからすれば、 おまいら地球人のやってるコトは全て児戯。 82 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 14:36:24.27 ] 今時のプログラミング言語の型理論の基礎はSystem F、 要するに二階λ計算、大体二階直観論理相当。 一階述語論理で十分なんて馬鹿げてる。 動作原理としてはノイマン型でロジックとは関係ないし。 83 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 15:05:06.21 ] >>80 S6: home.utah.edu/~nahaj/logic/structures/systems/s6.html S7: home.utah.edu/~nahaj/logic/structures/systems/s7.html S8: home.utah.edu/~nahaj/logic/structures/systems/s8.html S9: home.utah.edu/~nahaj/logic/structures/systems/s9.html 84 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 16:02:50.44 ] >>82 つまりこれまでの論理プログラムなどのハード計算が使い物にならないので、 非古典論理や型の理論などのソフト計算が導入されている。ということでしょうか？ ＞動作原理としてはノイマン型でロジックとは関係ないし。 チューリング機械であるという見方の一方でブール代数を扱うという見方もあるのではないでしょうか？ 人の推論と計算機の間にロジックが必要なのではないでしょうか？ >>83 非常に便利です。 これらはどの様相論理の本にも載っていませんでした。 85 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 16:05:56.20 ] 訂正： 型理論はソフト計算とは無関係でしょうが...。 86 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 19:03:32.23 ] 命題論理とスイッチ回路の初等的過ぎる疑問:: ラッセル方式でNORだけの公理は割とみじかく書き下しできるのに NANDだけだといやになるほど長くなる 一方 回路設計をNAND素子オンリーで組むのはラクチンなのに NOR素子オンリーで組むのはなぜか苦労する（手間が時間が） ・・・トンデモ本「数理示申學序説の前書き」より自分で引用 これ数学SFに使おうと思いますが玄人の眼からみると幼すぎますか できれば評価レスキボンヌ 87 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 19:15:18.41 ] >>84 ハード計算、ソフト計算ってのが何を意味してるかわからん。 論理プログラムとの関係もわからん。 88 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 21:45:22.34 ] >>87 ハード計算が計算機の立場の情報処理技術、 ソフト計算が人間の立場の情報処理技術。 論理について考えると、 命題論理・一階述語論理はハード計算。 様相論理・時相論理・多値論理・関係論理・ﾊﾟﾗｺﾝｼｽﾃﾝﾄ論理・曖昧論理・ ファジー論理はソフト計算。 だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。 89 名前：１３２人目の素数さん [2012/01/04(水) 22:20:43.07 ] >>88 あんたはやっぱり少し見えてる。 >人と計算機の間にロジック について差し支えない範囲で語ってくれんか？ 90 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 23:35:52.71 ] >>89 そんなに詳しく考えているのではないですが、 計算機の内部でブール代数に基くビット演算が起こっていると考えられますが、 （実際のハードウェアがどうなっているかは知りませんが、） これを厳密かつ人が扱いやすく定義し理論的保障を与えるために、 形式的言語として命題論理のような論理演算システムが必要と考えています。 （もちろん状態遷移系でもチューリング機械でもレジスター機械でも何を駆使してもよいのですが。） とりわけ一階論理は人の推論に比較的合っているうえにそこそこの表現力も持っているのではないでしょうか？ もちろんプログラムなどの側で有用なのは言うまでもないでしょう。 91 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 23:37:10.93 ] ばかだろ 92 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 23:43:09.11 ] >>31 >今の計算機の原理が変わらない限り一階論理がなくなることはない。 これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？ >>88 ハード計算とソフト計算はあなたが考えた独自用語ですよね？ ソフト計算とはヒューリスティクスという意味でしょうか？ >だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。 チューリング等価なプログラミング言語であるprologで あなたが示したすべての論理をソフトウェアとして実現できます。 だから一階述語論理の応用はハード計算とは言えません。 ソフト計算に分類した論理を使えばヒューリスティクスを自然に表現できる、 という主張なら納得できるのですが。 93 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 23:55:11.56 ] >>92 ＞これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？ 大抵は組み合わせて使います。 ＞ハード計算とソフト計算はあなたが考えた独自用語ですよね？ ＞ソフト計算とはヒューリスティクスという意味でしょうか？ Soft computingとHard computingのことですね。 ＞チューリング等価なプログラミング言語であるprologで ＞あなたが示したすべての論理をソフトウェアとして実現できます。 例えばそのProlog自体の基礎となっているのが論理プログラムなどという話しですね。 94 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 08:51:28.00 ] >>83 番号が大きいほうだけではなくて、S1 より弱い S0 なんてのもあるのか。 そのサイトは便利だ、�dクス 95 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 09:06:25.42 ] >>74 非正則世界ってなんですか？ 96 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 14:57:03.04 ] Sπ 97 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:02:59.82 ] >>95 非正規世界(non-normal world)のことだろ。 数学用語ではnormalは普通「正規」と訳される。「正則」はregularね。 非正規世界では、□Aという形の論理式は問答無用で偽とする。 それ以外のconnectiveの意味論は通常通りとする。 正規世界では通常のクリプキ意味論。 S2やS3はこんな意味論で完全になるそうだ。 98 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:18:28.07 ] >>83 とりあえず、このリストは命題論理だけでもかなり漏れている。 有名なのを列挙してみると Alt_n、Grz、Triv、Verum、A*、Dum、K4BW_n、K4BD_n、K4_n,m 、Ord_t、E_t、O_n、RD、LD、Z_t、Ds_n、Q_t、R_t、Rd_t、Lin 、CSM0、CSM1、CSM2、CSM3、NB1、NB2、Int(＝ρS4) 、For、Cl(＝ρS5)、SmL、KC(＝ρS4.2)、LC(＝ρS4.3)、SL、KP、BD_n 、BW_n、BTW_n、T_n、B_n、NL_n、FS、MIPC、IntK...。 さらに様相システムは、先頭にρ、τ、σが付くし、 後ろには-や、添加したオペレータが付き得る。 また各システムで、S4ｘS4や(Grz)^nのように 2つ以上のシステム内のオペレータが干渉し合う体系も起こり得る。 99 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:23:55.92 ] 誰も「すべてを網羅している」なんて言ってないよーな 100 名前：１３２人目の素数さん [2012/01/05(木) 19:34:21.83 ] Vopěnka cardinal ってなんでしょうか？ Vopěnka principle (VP) は前スレで話題になっていましたが。 101 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:40:15.42 ] 様相論理も部分構造論理も、幾らでも新たな体系を作ろうと思えば作れる。 研究と称して、そういった体系のお決まりの性質（完全性、有限モデル性、決定可能性、カット除去等々）を これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。 よってそれらをすべて網羅する必要があるとは思われない。 102 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 20:20:30.73 ] >>76 分類フリークといえば、少し前に一人で樹形図書きまくってたアホがいたな。 同一人物かね。 103 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 21:17:22.87 ] 何それｗｗｗ ちょっと見てみたいｗ 104 名前：スレタイスレ446 mailto:sage [2012/01/05(木) 21:17:32.98 ] >>99>>101 ＞幾らでも新たな体系を作ろうと思えば作れる。 その通りです。 ただし、>>98に掲載されている体系は、 （恐らくHandbook Of Philosophical Logicの３巻からの引用。） ほとんどがK4やS4の拡張で、 複雑なペトリネット・公理的集合論・線形時相論理などに関する 統一的な研究に由来するようですね。 105 名前：１３２人目の素数さん [2012/01/05(木) 21:18:41.38 ] 数セミの渕野先生の文章読んだけど、何か苫米地英人っぽい偏狭さを感じる。 106 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 21:19:47.51 ] >>70 通常「直観主義数学」と言えばブラウワーの数学（を形式化したもの）を指すでしょ。 ビショップとかマルティンレーフとか、それ以外の直観主義論理上の理論は構成主義と呼ぶと思う。 論理を直観主義にしたものすべてを直観主義数学と呼ぶのは、浅学の窮みｗｗ 107 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 21:37:14.88 ] F先生が偏狭なのはいまさら(ry 108 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:00:50.90 ] >>103 こんなの↓ 980 : 半角混ぜるとずれるので、 : 2011/06/28(火) 21:22:21.01 　　数理論理学━┳━逆数学━━━━┳━高階逆数学 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限ゲーム決定理論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━構成的逆数学 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━計算論的逆数学 　　＿＿＿＿＿＿┣━非古典論理━━┳━様相論理 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━部分構造論理 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━代数的論理 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━高階述語論理 　　＿＿＿＿＿＿┣━公理的集合論━┳━連続体仮説━━━強制法・反復強制法 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━SH・◇・CH・ADなど 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━内部モデル・決定性公理 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━巨大基数・超巨大基数・Rの基数不変量 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限集合組合せ理論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━PCF理論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━Generic Multiverses・Ω-論理 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━集合論その他(GB,NF,KP) 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━推移的クラスの微細構造論 109 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:01:10.29 ] 　　＿＿＿＿＿＿┣━モデル理論━━┳━幾何学的モデル論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━超準的数学 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━ダイアレクティカ圏・HyperDoctrine 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━真の算術など 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━有限モデル理論 　　＿＿＿＿＿＿┣━再帰理論━━━┳━計算量理論━┳━記述計算量理論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┃＿＿＿＿＿＿＿┗━次数理論━━━非可解性次数 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━型付ラムダ計算 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━順序数上の再帰理論・高階再帰論 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━解析的階層 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━コルモロゴフ複雑性・チャイティン数 　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━抽象機械 　　＿＿＿＿＿＿┗━証明論━━━━┳━定理自動証明 　　＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┣━新井先生とかRathjenの業績 　　＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┗━構成的数学━━━構成的型理論━━━直観主義型理論 110 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:08:14.80 ] >>105 どこらへんで偏狭さを感じたんだい？ 111 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:31:12.35 ] >>104 >ほとんどがK4やS4の拡張で、 >複雑なペトリネット・公理的集合論・線形時相論理などに関する >統一的な研究に由来するようですね。 統一的な研究に由来する体系なのに、 名称に体系だった趣がまるで感じられないのはなぜ？ 112 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:41:31.65 ] 人の名前から付いてたり 公理を表す文字だったり 体系の性質に注目して居たりするからでは 113 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:50:44.20 ] 「新井先生とかRathjenの業績」って分野の名称だったんだｗ 114 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:53:21.20 ] >>113 定義上、二人しか結果の出せない分野だな。 つーかそういう瑣末な問題以前の問題が多すぎる、その樹形図は。 115 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 22:57:54.23 ] >>112 自分で幾つもの体系を提案するのに、異なる名付け方法を採用するか？ 一人（一グループ）の人間が、一つの研究の中で、いくつものの体系の名称を付けるのなら、 統一的な名前の付け方を採用するのが普通ではないんだろうか？ 116 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 00:53:27.05 ] >>104 > （恐らくHandbook Of Philosophical Logicの３巻からの引用。） 全４巻の旧版の方？　それとも未だ未完結で全１８？巻の新版の方？ 117 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 02:11:00.43 ] >>114 逆に言えばその二人はその分野以外では業績が出せない。 なぜならどんな業績を出しても「新井先生とかRathjenの業績」という分類になるから。 118 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 03:15:34.28 ] アホのしかもだいぶ昔のレスを肴に、よーもまーそこまで下らん話ができるもんだな。 119 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 04:40:22.16 ] またF先生祭になる伊予柑 120 名前：スレタイスレ446 mailto:sage [2012/01/06(金) 07:09:34.47 ] >>116 新版の方。 ２章の様相論理の発展。 121 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 07:17:36.41 ] そこには非正規世界のある可能世界意味論とか書いてありますか？ 122 名前：スレタイスレ446 mailto:sage [2012/01/06(金) 08:01:41.06 ] >>121 載っている。 非正規世界(non-normal world)って名称ではないけど。 あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、 記述されている。 このシステムのクラスNExt(L)自体の順序構造も調べられているよう。 123 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 08:02:05.66 ] ファジー論理のハンドブックも進行中みたいだね。 www.mathfuzzlog.org/index.php/Handbook_of_Mathematical_Fuzzy_Logic 124 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 08:30:55.97 ] >あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、 >記述されている。 記述する、の主語はなんでしょう？ 125 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 08:50:41.10 ] >非正規世界(non-normal world)って名称ではないけど。 >あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、 >記述されている。 あのう、非正規世界というのは、正規でない体系(S2, S3など)を扱う為に導入したから 名称も非正規世界ということになったわけでして。 126 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 09:17:59.72 ] >>100 Vopěnka 関連は最近流行っているみたい。 Archive for Mathematical Logic では、 2011年だけで2本も（少ない？）関連論文が出ている。 no access Indestructibility of Vopěnka’s Principle Andrew D. Brooke-Taylor 2011, Volume 50, Numbers 5-6, Pages 515-529 www.springerlink.com/content/v336j98247687155/ C^{(n)}-cardinals Joan Bagaria Online First, 22 December 2011 www.springerlink.com/content/n6330090pxr6832n/ 127 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 10:28:49.07 ] Vopenka とか膨大基数とか拡張可能とか C^{(n)}-基数とか、色々な基数が出てくるけど、 その間の関係ってどうなっているの？ 誰か関係を表にした奴へのリンクとか貼ってくれないかな？ 128 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 12:41:03.21 ] 前スレの 935 ：１３２人目の素数さん Vopěnka's principle（VP）:="Cが言語のモデルの宇宙としてのプロパークラスとしたとき、 Cの2つの要素を任意にとると、片方がもう片方に初等埋め込み可能" 「VP⇒拡張可能基数」が成り立つからかなり強い仮定。 また膨大基数kを仮定すると、V_k（累積的階層）がVPのモデルになる。 が累積的階層であるとき、この階層のランクの添え字の基数がVopěnka基数。 に対して 958 ：１３２人目の素数さん：2012/01/02(月) 13:24:57.89 >>931 >Vopěnka's principle でググっていたら www.imub.ub.es/hocard11/Problems.pdf が出て来た。 VP に同値な命題がいくつか書いてあり、 さらに WVP なる物もあった。このなかで一つ分からないのが accessible category の定義だ。 accessible ordinal (cardinal) と似たような感じだとは思うが 解説希望 と質問したのだが、未だに回答が無い。 129 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 18:48:10.19 ] 970 ：958：2012/01/02(月) 22:32:22.66 　　こに質問に誰も答えられないと云う事は・・・ 975 ：１３２人目の素数さん：2012/01/02(月) 22:43:55.95 　　>>970 　　そんなローカルな研究解説できる人間などほとんどいない。 　　あなたが調べられる以上の情報は期待できないだろう。 　　Jech本にもVPまでしかのっとらんしな 130 名前：スレタイスレ446 mailto:sage [2012/01/06(金) 19:02:30.54 ] >>124 主語は集合論だと思いますよ、明文化されてはいませんが。 NExt(L)は様相システムLの正規に拡張したシステム全体の集合族。 公理に関して順序関係を定義していくと、完備分配束が出来たりする。 >>125 いえ、Handbook Of Philosophical Logicの３巻でnon-normal worldって名称が使われていないという意味です。 131 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 20:07:47.44 ] >>130 122のレスは >載っている。 >非正規世界(non-normal world)って名称ではないけど。 という部分と、 >あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、 >記述されている。 >このシステムのクラスNExt(L)自体の順序構造も調べられているよう。 の部分は完全に別の話をしているという理解でいいの？ 同じ話題だとすると、正規でない L について「正規なまま拡張」なんてできない訳で、 何言っているかやっぱり分からんのだ。 132 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 20:16:52.31 ] >主語は集合論だと思いますよ、明文化されてはいませんが。 自分の発言について「思いますよ」とは恐れ入るな。 133 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 20:51:57.69 ] >>132 NExt(L)で記述したのは別人だから別におかしくないのでは？ 134 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 20:57:57.94 ] 「あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、 記述されている。」と書いたのはスレタイスレ446氏だろ？偽者なのか？ 自分で「記述されている」と言っておいてその主語が何かについて 「集合論だと思いますよ」と書いたのも彼／彼女だろう。 135 名前：スレタイスレ446 mailto:sage [2012/01/06(金) 21:19:27.32 ] >>131 ＞の部分は完全に別の話をしているという理解でいいの？ そう。改行していないだけ。 >>132 件の本に記述されているのは確か。 しかし、どういった理論（少なくとも集合が扱える）に基いているか不明だということ。 136 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 21:33:31.67 ] >>128 すべての質問に回答が付くと思うな。 スルーされたくなければスルーされないような書き方を研究するんだな。 137 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 21:59:17.28 ] １階述語論理の証明体系について皆さんにお聞きしたいことがあります。 全称化：「A→Bから∀ｘA→Bが出てくる（ただしｘはBに自由に現れない）」という推論規則がありますが、 これから理論Tについて「T|-AならばT|-∀xA」を示すにはどうすればいいのでしょう。 命題論理のトートロジーや∀xA(x)→A(t)（tは代入可能な項）、等号の公理は論理公理に入っているものとしてください。 三段論法も推論規則に入っています。 138 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 22:28:15.65 ] >>128 accessible ordinal (cardinal) の解説希望。 139 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 23:29:10.95 ] >>135 そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？ 前スレの「考える人」と同じ臭いを感じる。 結局、何が記述されていると言っていたワケ？ 140 名前：１３２人目の素数さん mailto:sage [2012/01/06(金) 23:55:13.51 ] 知識も話題も豊富なスレタイスレ446氏は、こまめにレスを返したりする性格も相俟って このスレの主になりつつあるわけだけど、 >>139が指摘しているようなささっと書いたレスが意味不明な場合があって （単なるタイポだろうけど、それがときとして致命的に読みにくくなる） そこを直さないと主としての風格というか権威は得られないと思う。 141 名前：１３２人目の素数さん mailto:sage [2012/01/07(土) 04:36:23.17 ] アスペ＝マツシンについて詳しく知りたい方へ logsoku.com/thread/science.2ch.net/math/1057850128/ 142 名前：１３２人目の素数さん mailto:sage [2012/01/07(土) 06:21:44.06 ] たかが２ｃｈのスレで権威ねえ。 言いたいことは分からんでもないがｗ 143 名前：１３２人目の素数さん mailto:sage [2012/01/07(土) 08:38:42.87 ] >>137 少なくとも書かれている規則からだけでは無理。 何故なら ∀ｘA という形の論理式を問答無用で偽と解釈する （それ以外は通常の解釈をする）意味論を考えると、 それら規則はすべて真であることを保存するが、 証明しようとしているのは真を保存しない。 何か忘れている規則があるはず。 144 名前：１３２人目の素数さん mailto:sage [2012/01/07(土) 09:05:13.62 ] >>137 全称化は向きが逆だろ。 「A→BからA→∀ｘBが出る（ただしｘはAに自由に現れない）」 T|-AならT|-¬∀ｘA→A 全称化よりT|-¬∀ｘA→∀ｘA よってT|-∀ｘA 145 名前：１３２人目の素数さん mailto:sage [2012/01/07(土) 09:48:30.24 ] >>143 すみません、「A→BからA→∀ｘ」の間違いでした。 >>144 >T|-AならT|-¬∀ｘA→A この部分と >よってT|-∀ｘA この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？

---

---

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

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