数学基礎論・数理論理学　その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/ 232 名前：１３２人目の素数さん [2012/01/09(月) 17:56:53.11 ] >>231 もうググったよ。それでも分からん。 ただし、 >>230 を投稿したのは私では無い。 233 名前：１３２人目の素数さん [2012/01/09(月) 19:52:48.35 ] 日本人は韓国に来るな 234 名前：１３２人目の素数さん mailto:age [2012/01/09(月) 19:55:21.11 ] 韓国人は日本にくるな 235 名前：１３２人目の素数さん [2012/01/09(月) 20:34:25.35 ] ゆとり民族、ゴミジャップ 236 名前：１３２人目の素数さん mailto:sage [2012/01/09(月) 20:57:36.69 ] 関数f(x)がx=aで微分可能なとき、{Af}'(a)=Af'=(a)を証明せよ できる人いる？ 237 名前：１３２人目の素数さん mailto:sage [2012/01/10(火) 01:11:47.07 ] >>230 accessible ordinal (cardinal) = not inaccessible ordinal (cardinal) なんじゃね？二重否定の除去！ 238 名前：１３２人目の素数さん mailto:sage [2012/01/10(火) 05:38:37.97 ] >>232 ぐぐればふつうに出てくるぞ： en.wikipedia.org/wiki/Accessible_category 239 名前：１３２人目の素数さん mailto:age [2012/01/10(火) 10:06:39.78 ] >>238 いかにも巨大基数と関係が出て来そうな定義だな。 240 名前：１３２人目の素数さん mailto:sage [2012/01/10(火) 15:34:56.39 ] 巨大基数と膨大基数の違いをおしえれ 241 名前：１３２人目の素数さん mailto:sage [2012/01/10(火) 16:14:01.75 ] >>235 キムチ野郎 242 名前：１３２人目の素数さん mailto:age [2012/01/11(水) 01:15:54.22 ] コピペ 75 ：１３２人目の素数さん：2012/01/10(火) 16:38:44.94 　　uni.2ch.net/test/read.cgi/math/1317556554/89-94 　　ということなんで選択公理廃止！ 　　以後、決定性公理を採用します。 243 名前：１３２人目の素数さん mailto:sage [2012/01/11(水) 02:12:16.17 ] 決定性公理：すべての数学体系は決定可能である。 244 名前：１３２人目の素数さん [2012/01/11(水) 02:39:26.08 ] 確かに今の日本はゆとり国家 245 名前：１３２人目の素数さん [2012/01/11(水) 04:00:59.17 ] これが古代史に伝わる数百年に一度、 彼の地に誕生するというスーパーゆとり民族か。 246 名前：１３２人目の素数さん mailto:sage [2012/01/11(水) 06:54:52.94 ] >>54 直観主義数学ではすべての実数値関数が連続ということですが、 ということは実数の集合はすべて可測ということですか？ 247 名前：１３２人目の素数さん mailto:sage [2012/01/11(水) 16:35:14.91 ] >>240 字義的には huge cardinal が巨大基数と訳されるべきだろうな。 ま、定着しちまったものは仕方がない。 定訳をおかしいおかしい言っているとマツシンになっちまうしな。 248 名前：１３２人目の素数さん mailto:sage [2012/01/11(水) 16:42:57.80 ] >>247 > 定訳をおかしいおかしい言っているとマツシンになっちまうしな。 で、常識的な公理をおかしいおかしい言ってるとエムシラになるってかｗｗｗ 249 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 01:45:57.67 ] このスレを見ると、住人に人気があるのは ・様相論理 ・証明可能性述語 ・巨大基数 みたいだな。選択公理関係もはやってる？ 250 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 06:37:25.16 ] >>246 可測というにはルベーグ測度が定義できないと話にならない。 何かそれっぽいものは直観主義でも定義できるらしいが、 どこまでできればそれをルベーグ測度と呼んでいいのか、という問題になる。 251 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 07:14:54.37 ] >>238 232はググりもしなかったことが明らかになったな 252 名前：１３２人目の素数さん [2012/01/12(木) 07:56:39.56 ] 12 ：１３２人目の素数さん ：2012/01/12(木) 01:18:39.79 数学基礎論・数理論理学　その11 (p)uni.2ch.net/test/read.cgi/math/1325513069/ の奴らは (p)www.imub.ub.es/hocard11/ のような研究集会があった事すら知らん奴が多いようだな 可哀想な数学を知らない人達・・・ 253 名前：１３２人目の素数さん [2012/01/12(木) 08:01:08.02 ] すいません、 私は現在統合失調症で職を持たない身なのですが、 明日の論理学の世界に貢献したいと考えております。 そこで以下のように公理系のデータベースの構築をはじめようと考えております。 www4.atwiki.jp/mathe_logic/pages/14.html すべての公理系をクリックすればアウトプットできるような 巨大なデータベースの構築を目指します。 もちろんリンクなどでの立体的なデータ構造を考えております。 データの保管はOracleサーバを考えております。 よろしこお願いします。 254 名前：１３２人目の素数さん [2012/01/12(木) 08:06:19.15 ] また、個々の体系が何を意味しているのかは分かりません。 一アマチュアプログラマーとして皆様に貢献したいです。 上のリストは以前紹介された様相論理のデータベースをもとにしています。 私はマジ基地ですが、よろしこお願いします。 255 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 17:14:23.11 ] >>252 そいつ（巨大基数スレ12）は232か？ だとすると自分の怠慢を棚にあげてよくもまーｗｗ 256 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 20:06:42.71 ] >>250 すべての関数が連続ならば、積分を考えるには開集合に測度を持たせられれば十分だろ。 ルベーグ測度なんてのはルベーグ積分の為にあるものなんだから。 直観主義でも開集合には測度を定義できるんですよね？ 257 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 21:13:52.74 ] こんなんあるよ us.metamath.org/index.html これの部分構造論理とか線型論理とか様相論理とかのver.があれば 勉強・研究する人には便利だろうな 258 名前：１３２人目の素数さん mailto:sage [2012/01/12(木) 21:30:54.87 ] いちおうE. BishopのConstructive Analysisとか Foundations of Constructive Analysisとかには Lebesgue measureが定義してあるみたいだよ ただ「直観主義数学ではすべての実数値関数が連続」 とかいうときの「実数値関数」とか「連続」という言葉の意味は 普通の数学でいうときのそれとは違うと考えるべきだと思うけどね A が B より強いというのは A → B が成立して A と B が両立する場合に言うのが 普通なのでそういう意味では片方が他方より強いという関係にはないけど、 数学的公理の部分で、形式的には古典的数学と互いに背反するような 公理ないし定義を採用していることにはなると思う 259 名前：１３２人目の素数さん [2012/01/13(金) 00:01:25.37 ] >>257 なんでそんなめんどくさい貼り方するの？ us.metamath.org/index.html 260 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 01:49:59.23 ] >>258 >ただ「直観主義数学ではすべての実数値関数が連続」 >とかいうときの「実数値関数」とか「連続」という言葉の意味は >普通の数学でいうときのそれとは違うと考えるべきだと思うけどね もっともだとは思うが、 それを言い出すと A → B の意味も直観主義と古典論理では違うし、 何から何まですべて違うことになる。 確かに公理系Tに公理を一つ加えただけで Tに元々含まれる公理の意味は変わるともいえる、背景が違うのだから。 しかし、ある程度の差異は捨象して同一視してしまって比較するってのが 学問というものじゃないかい？ 261 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 02:25:16.86 ] 部分構造論理では最近は何が流行っているのでしょう？ 詳しい方、解説をお願いします。 262 名前：１３２人目の素数さん [2012/01/13(金) 02:40:34.56 ] 421 ：「名無しわざとか？」とかイヤミを言われた：2012/01/12(木) 08:03:41.44 ID:3+R7T9ps 誰も解答を書かないので>>360の解答を。 連立方程式 { x-4=y+4 { x+4=2(y-4) これを解いてy=20,x=28 Aさんが28個。Bさんが20個。 つーことで、アイジャグの320番台と328番台が高設定だ！ 朝から全ツッパしろ！！！ 爆死覚悟でやってみてーけど、ヲレ明日は忍者屋敷イカネーといけないので凹 P.S つるかめ算とかやってたような頭の柔らかい小学生とかはもっと簡単に解けちゃうのか？ kohada.2ch.net/test/read.cgi/slotj/1321424162/310-312 263 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 06:16:18.84 ] 線型論理も部分構造論理の一つと考えれば、部分構造論理の中で線型論理は断然はやってるね。 264 名前：GMG ◆.5wljPk1.c mailto:sage [2012/01/13(金) 08:29:02.49 ] 180=nα+B=B+(n-1)α＋α 265 名前：１３２人目の素数さん [2012/01/13(金) 18:24:27.23 ] Lukasiewicz 論理をよく聞くかな。部分構造論理の中では直観主義論理に次いで綺麗な構造らしい。 en.wikipedia.org/wiki/%C5%81ukasiewicz_logic 266 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 18:29:14.69 ] 古典命題論理をストローク一本、公理一本で展開することに何かメリットある？ 267 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 18:40:40.82 ] そら時と場合によるだろう。かなり特殊だけど役に立つ場面はあるだろうね。 268 名前：１３２人目の素数さん [2012/01/13(金) 20:34:54.20 ] 次の性質を持つ集合 x は一般に何と呼ばれているのですか? ∀y∀z [ [x ∋ y ∋ z ] ⇒ [ x ∋ z ] ] 269 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine [2012/01/13(金) 20:38:02.94 ] >>268 　ニートの、ゴミ・クズ・カスの、クソガキ！！！！！！！！！ 270 名前：スレタイ446 [2012/01/13(金) 21:24:28.35 ] 遺伝的集合とか推移的集合じゃないの？ 271 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 22:15:53.14 ] メンバーのメンバーはメンバーなり。 272 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 22:16:38.49 ] 昔懐かし稲垣メンバー。 273 名前：１３２人目の素数さん [2012/01/13(金) 22:28:49.43 ] >>270 ググってもそれらしき物は出て来なかったが。 274 名前：１３２人目の素数さん mailto:sage [2012/01/13(金) 23:31:01.63 ] >>273 英語てググりなさい 275 名前：１３２人目の素数さん [2012/01/13(金) 23:59:55.45 ] hereditary set, transitive set でググったら、 en.wikipedia.org/wiki/Transitive_set が有った。 しかしその意味合い (定義では無くて背景などの関連事項) が良く分からない。 276 名前：１３２人目の素数さん [2012/01/14(土) 04:18:22.31 ] >>127 巨大基数の表なんざ、ぐぐればすぐに出てくるぞ： en.wikipedia.org/wiki/List_of_large_cardinal_properties 277 名前：１３２人目の素数さん [2012/01/14(土) 04:40:42.26 ] >>276 29 種類どころか僅かしか無かった。 278 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 05:12:44.76 ] どう見ても29種類以上、書いてあるけどな 279 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 06:05:32.06 ] >>275 関係Rが推移的とは ∀y∀z [ [x R y R z ] ⇒ [ x R z ] ] 280 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 06:57:56.92 ] お、スレタイスレ446氏が降臨している！リクエストをコピペしとく。 173 ：１３２人目の素数さん：2012/01/08(日) 19:43:41.45 　　スレタイスレ446氏にはこっちのスレで 　　「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」 　　の数学的側面を語ってもらいたいな。 281 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 07:20:03.82 ] >>279 ＞関係Rが推移的とは ∀y∀z [ [x R y R z ] ⇒ [ x R z ] ] ∀x∀y∀z [ [ [x R y ] & [ y R z ] ] ⇒ [ x R z ] ] ぢゃないのか？ 282 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 07:26:00.16 ] ∀xがあるかないかの違いしか見つけられんが 283 名前：１３２人目の素数さん mailto:age [2012/01/14(土) 07:55:28.45 ] 1. inaccessible 2. alpha-inaccessible 3. hyper-inaccessible 4. Mahlo 5. alpha-Mahlo 6. hyper-Mahlo 7. reflecting 8. weakly compact 9. Pi^n_m-indescribable 10. totally indescribable 11. lambda-unfoldable 12. unfoldable 13. v-indescribable 14. lambda-shrewd 15. shrewd 16. ethereal 17. subtle 18. almost ineffable 19. ineffable 20. n-ineffable 21. totally ineffable 22. remarkable 23. omega-Erdos 24. 0-sharp 25. omega_1-Erdos 26. almost Ramsey 27. Jonsson 28. Rowbottom 29. Ramsey 30. ineffably Ramsey 31. measurable 284 名前：１３２人目の素数さん mailto:age [2012/01/14(土) 08:01:54.67 ] 32. 0-dagger 33. lambda-strong 34. strong 35. tall 36. Woodin 37. weakly hyper-Woodin 38. Shelah 39. hyper-Woodin 40. superstrong 41. subcompact 42. strongly compact 43. supercompact 44. eta-extendible 45. extendible 46. Vopenka 47. almost huge 48. super almost huge 49. huge 50. superhuge 51. n-superstrong 52. n-almost huge 53. n-super almost huge 54. n-huge 55. n-superhuge 56. I3 57. I2 58. I1 59. I0 60. Reinhardt 285 名前：１３２人目の素数さん mailto:age [2012/01/14(土) 08:09:56.67 ] >>283-284 乙。大体のは聞いたことあったけど、数えてみると60もあるんだ。 他に俺の知ってるのは hypermeasurable とかかな。 286 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 08:25:15.60 ] weakly inaccessible とか strongly inaccessible とかは？ 287 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 08:34:30.11 ] どうしてこうもググりもしない教えてクンが多いのか 288 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 10:33:29.38 ] >>284 dagger が無いんだが・・・と書こうとしたら次に出て来た。 289 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 16:42:22.90 ] >>252 巨大基数厨の諸君に告ぐ。 巨大基数の集合論とその応用　そのアレフ 0 uni.2ch.net/test/read.cgi/math/1326526644/ 290 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 20:12:09.02 ] >>275 公理的集合論では与えられた集合が推移的じゃないと 困る場面が山のようにある 順序数は普通、∈で整列順序付けされる推移的集合として定義される 与えられた集合と同型な推移的集合を作るテクニックとかもある 291 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 20:13:31.75 ] 巨大基数スレも乱立かよ。 マツシンといい、やっぱり基礎論はトンデモ多発分野なだけある。 292 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 21:47:13.19 ] >>291 マツシンて誰？ 293 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 21:51:36.40 ] >>292 >>141あたりを参照 294 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 23:08:59.21 ] >>101 巨大基数公理も、幾らでも新たな公理を作ろうと思えば作れる。 研究と称して、そういった公理のお決まりの性質（○○基数から導けて△△基数を導く等々）を これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。 よってそれらをすべて網羅する必要があるとは思われない。 295 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 23:09:39.74 ] >>293 2003年ってもう9年前じゃん。バカじゃね？ 296 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 23:13:08.90 ] 8年ぶりにマツシンが活動期に入ったんだろ 297 名前：１３２人目の素数さん [2012/01/14(土) 23:21:45.54 ] >>290 テクニックって一階？二階？三階？ 298 名前：１３２人目の素数さん mailto:sage [2012/01/14(土) 23:44:02.56 ] >>294 ネタにマジレスですまんが、 そういう研究で論文が通ったのは精々80年代まで。 いまどきそれだけじゃ、査読を通らん。 非古典論理に比べてかなり健全だろ？ 299 名前：スレタイ446 [2012/01/15(日) 00:05:24.66 ] >>280 レシュネフスキーの数学理論は現在の記述論理にかなり近い。 プロトセティックは型理論のようなもので、 オントロジーは真偽ではなく存在の有無を実現するためのε記号を扱う論理学。 aεb（aはbである。）。 この上にメレオロジーを定義してクラスClを実現する。 （「クラス−真のクラス」は集合とならない、実際にはGBの断片＋α） グッドマンの方はこのメレオロジーの変種の個体計算などを形式化してる。 300 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 01:13:40.04 ] いくつかシツモソ ＞この上にメレオロジーを定義してクラスClを実現する クラスCIってなんですか？ ＞実際にはGBの断片＋α どういう断片ですか？αは具体的には？ 301 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 02:22:08.13 ] >>296 マツシンは8年間活動自粛してたわけではないぞ。 その間も他人のブログのコメント欄なんかを中心に精力的に活動してた。 302 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 03:13:55.87 ] >>298 巨大基数の健全性ｗ 303 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 04:02:33.74 ] マツシンタンとかエムシラとかsikiとか人生とか長生きしてるよな。今井は生きてる？鑑定団に出たあたりまでは確認したけど。 304 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 05:52:42.90 ] このスレが巨大基数について一番専門的な話をしているようなので、質問です。 large large cardinal (大巨大基数?)とか small large cardinal (小巨大基数?)とか middle large cardinal (中巨大基数?)とか ってそれぞれどの基数ですか？ 305 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 06:22:31.35 ] large small cardinal とか small small cardinal とかってなんですかｗｗ 306 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 07:37:38.92 ] >>294 前半部分は全くその通りだが 「...というオリジナリティのかけらもない論文が多すぎる」というのは 現状をまるっきり分かっていない奴の言うこと。 そんな論文見かけたことすらないね。 307 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 08:15:59.80 ] ネタにマジレスかこわるい 308 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 08:48:03.56 ] >>304 ncatlab.org/nlab/show/large+cardinal ここ見ると31の measurable cardinal が境界だそうだ。 だから 1-30 が small large cardinal で 32-60 が large large cardinal なんじゃないの？ middle large cardinal って聞いたことないけど、measurable のこと？ 309 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 13:57:59.29 ] >>296　>>301　>>303 何年間も同じ奴を追っかけて・・・ヒマだなおまえら。 310 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 14:04:05.75 ] logic systemのリスト化...ソフトウェアにするか動的ウェブで実現するか... 311 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 16:17:21.91 ] 追っかけなくても勝手に現れに来るからｗ 312 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 20:05:32.35 ] >>308 Stanford Encyclopedia of Philophy の Koellner の記事 (plato.stanford.edu/entries/independence-large-cardinals/)から引用： A large cardinal is small if the associated large cardinal axiom can hold in Gödel's constructible universe L, that is, if “V ⊨ κ is a φ-cardinal” is consistent, then “L ⊨ κ is a φ-cardinal” is consistent. Otherwise the large cardinal is large. この定義によると24のゼロシャープはもう large large cardinal のはずだが。 313 名前：スレタイ446 mailto:sage [2012/01/15(日) 20:29:39.02 ] >>300 クラスClは (a,b)(a＝b≡C(a)＝C(b)) cl(a)≡(Ex)(a＝C(x)) で、定義される。このEは1階論理の量化記号みたいなもの。 Clは何らかの個体の集まりなんだけど、 その集まりの集まりは元の集まりと変わらない。というのが彼のクラスの特徴。 こうすると最上位概念の存在によって循環がなくなる。 1項述語Cl,Ob,二項述語∈,＝が存在して、 ・等号＝に関する公理 ・外延性公理　(a,b)(cl(a)(cl(b))→(x)(x∈a≡x∈b)→a＝b) ・(a,b)(a∈b→ob(a)(cl(b)) ・内包性公理　(Ea)(cl(a)((x)(x∈a N≡ob(Y).ψ(x)))) GodelとBernaysの公理的集合論の断片になる。 あとはクラスclとobに関する操作が多少加わる。 とはいえ、集合論いらない数学は Feferman・Aczelの構成的数学などもある。 それらをオントロジーの枠組みで実現しているものだろう。 314 名前：１３２人目の素数さん mailto:sage [2012/01/15(日) 20:58:47.50 ] >>312 0^\sharp は cardinal ではないからその定義は意味をなさない罠ｗｗ 315 名前：１３２人目の素数さん mailto:sage [2012/01/16(月) 01:16:26.67 ] >>304 俺は>>308の流儀と>>312の流儀、どちらも聞いたことがあるけど、 きんちんとした定義はないんじゃないかな？ だから23までが small large cardinal 32以降が large large cardinal でいいんじゃない？ ついでにその間の24-31が middle large cardinal とか新説を唱えてみる。 316 名前：１３２人目の素数さん mailto:sage [2012/01/16(月) 06:53:15.92 ] >>313 その理論の強さはどれくらい？ZFC より弱いの強いの？ 317 名前：１３２人目の素数さん mailto:sage [2012/01/16(月) 08:14:12.21 ] >とはいえ、集合論いらない数学は >Feferman・Aczelの構成的数学などもある。 >それらをオントロジーの枠組みで実現しているものだろう。 「それら」は何を指していますか？「実現している」の主語はなんですか？ スレタイスレ446氏のレスは相変わらず読みにくいんですが。 318 名前：１３２人目の素数さん mailto:sage [2012/01/16(月) 08:38:47.03 ] コアモデルがあるような巨大基数は小さいとか言ってみるテスト 319 名前：１３２人目の素数さん mailto:sage [2012/01/16(月) 09:34:52.00 ] ?してみるテストって久しぶりに見たw 320 名前：１３２人目の素数さん mailto:sage [2012/01/17(火) 02:32:53.13 ] >>314 κ is a 0-sharp cardinal if there is a non-trivial elementary embedding j: L → L whose critical point is κ と定義すれば>>312の定義が適用できる！ 321 名前：１３２人目の素数さん mailto:sage [2012/01/17(火) 06:40:24.56 ] つまり、0-sharp cardinal は cardinal でないこともあるってことだね。 322 名前：１３２人目の素数さん mailto:sage [2012/01/17(火) 17:16:10.88 ] 312の定義に意味を持たせるには if“V ⊨ κ is a φ-cardinal”then“κ is in L” であればいいので、“κ is cardinal”である必要はないのね。 323 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 01:46:48.73 ] >>321, >>322 普通に>>320は、最初に「For a cardinalκ, 」を補えばいいだろうが！ 324 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 04:32:03.92 ] 基礎論最大の未解決問題ってなんなのでしょうか？ 325 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 05:51:34.40 ] >>323 では 0-sharp cardinal の存在と（通常の意味の）0-sharp の存在は同値？ 326 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 08:50:07.59 ] >>324 間違いなく「P対NP問題」でしょう。 基礎論の各分野での最大の未解決問題となると、分かりませんが。 327 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 17:46:55.71 ] >>325 Silver indiscernible は順序さえ保てば自由に動かせて 非可算基数はすべて Silver indiscernible なのだから、 critical point を特定の非可算基数になるような L から L への elementary embedding なんて (0^\sharp の存在から)簡単に作れる。 328 名前：１３２人目の素数さん [2012/01/18(水) 18:30:36.14 ] 自動定理証明系で 証明仮定（証明図）がすべて出力できるソフトウェアはありますか？ 329 名前：１３２人目の素数さん [2012/01/18(水) 19:17:07.58 ] >>328 自分で作れば良い。全ての図を少しずつ列挙し、 同時に一方ではそれらが証明図になって居るかどうか少しずつ判定すれば良い。 330 名前：１３２人目の素数さん [2012/01/18(水) 19:39:04.24 ] >>329 それって普通の対話型証明ソフトと変わらないですよね？ 私は公理からの論理式のシーケント列を見たいのです。 331 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 23:53:47.48 ] 　３２８の件　スルー　お願いします 332 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 01:45:57.11 ] >>327の言う通りなので、 κ is a real-sharp cardinal if for any a⊂ω, there is a non-trivial elementary embedding j: L[a] → L[a] whose critical point is κ と定義すれば、“∀a⊂ω(a-sharp exists)”も real-sharp cardinal の存在と同値になって>>312の定義が適用できる！ dagger についても同様。

---

---

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

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