数学基礎論・数理論理学 その19
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 (「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。) 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 (数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照) 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学 その18 https://rio2016.5ch.net/test/read.cgi/math/1474357543/ >>318 A ⊢ A A ⊢ A, B A, ¬A ⊢ B わいの挙げた2つは両方ゴミだったw >>317 形式的体系 • ヒルベルト流 • 自然演繹 • シーケント計算LK こんな感じね、中味はしらんけど 二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが これどうやるんだ?体系になんか秘密があるのか? >>322 1)シーケント計算で最小論理はどういうもの? 2)シーケント計算でLJは後件が一つ以下となる理由は? >>324 1しらん 2そうするとなんかうまくいったから これ何の話なんだ?なんで急に質問が飛んできたんだ… やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん… >>326 google(二重否定除去と矛盾の公理の関係に関する一考察) >>327 さんくす そっかFalse→¬Aの形は爆発律いらんのだったわ >>325 >2そうするとなんかうまくいったから 何でうまくいくのかよくわからなくて 自然演繹ならそもそも使える道具に 排中律や二重否定の除去を入れないから ああ直観論理だなあと思えるけれど LJで健全性完全性を証明できても どこに後件を1つ以下にすることが 効いてくるのか感覚がよくわからなくて もちろん複数の後件を許せば排中律や 二重否定の除去が出てしまうから 出ないようにするには1つ以下に しなくてはならないことはいいのだけど 証明能力がちょうど直観論理と一致する ことと後件を1つ以下に限ることの 関連性が感覚的にわからない >>324 >1)シーケント計算で最小論理はどういうもの? 自然演繹なら矛盾律人→Pと排中律P∨¬Pおよび 二重否定の除去¬¬P→Pを公理や推論規則から外すだけだけど 明示的に矛盾律を含めないLJから矛盾律を外すには どうしたらいいんだろ >>319 こちらは許容し(最小論理で証明できるから) >>316 こちらはできないようにするために >>318 これで上手くいくんだろうか? A, ¬A ⊢ ¬B もできなくなるからそもそもダメそうだし >>316 はできなくなるけれど >A, ¬A ⊢ B A, ¬A ⊢ Bが証明できないことが 証明できるようなA,Bの例が示せないといけないし >>314 >見たけどこれ >ヒルベルト式じゃ無いやん これてクリーネの体系ていうやつの変種では? NOT-1,2,3を除いてFALSEってのを入れてる とりあえず、左側を1個以下にするのは A, ¬A ⊢ ¬B もなくなっちゃうんだよなあ A∧¬A ⊢ ¬B ならでるんかな でなさそうだけども ウィキペのシーケント計算の項目に ∧LL ○,A⊢○ ○,A∧B⊢○ ∧LR ○,B⊢○ ○,A∧B⊢○ ∧R ○⊢A,○ ○⊢B,○ ○⊢A∧B,○ ∨L ○,A⊢○ ○,B⊢○ ○,A∨B⊢○ ∨RL ○⊢A,○ ○⊢A∨B,○ ∨RR ○⊢B,○ ○⊢A∨B,○ →L ○⊢A,○ ○,B⊢○ ○,A→B⊢○ →R ○,A⊢B,○ ○⊢A→B,○ ¬L ○⊢A,○ ○,¬A⊢○ ¬R ○,A⊢○ ○⊢¬A,○ カット ○⊢A,○ ○,A⊢○ ○⊢○ Identity公理 A⊢A あとはweakening cntraction permutationで これは推論規則というよりは 論理式の列の性質というべき 結局カンニングして、¬はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった ここでシーケント(推件)とは自然演繹における推論図の状況を表し カットは自然演繹で2つの推論図をAで繋げること ∧Lは自然演繹の∧E ∧Rは自然演繹の∧I ∨Lは自然演繹の∨Eと∨Iの組み合わせ ∨Rは自然演繹の∨I →Lは自然演繹の→Eとカットの組み合わせ →Rは自然演繹の→I ¬Lは自然演繹の¬Eと後件における人の消去 ¬Rは後件における人の導入と自然演繹の¬I Identity公理は自然演繹における無駄な推論図を意味している となると シーケント計算における矛盾律は¬LRに内包されているんだと思うね というのもなぜ後件で人を導入消去できるかといえば人∨A→Aがトートロジー すなわち人→Aが成り立つことから来てるから てことでLJから矛盾律を除外するなら ¬LRを制限するあるいは別の推論規則にする必要があるはず やっぱ自然演繹の方がずっと自然だわ シーケント計算は形が対称で綺麗だけど かなり技巧的というか本質が覆われてる >>337 >¬はいれずにFalseをいれて、 ¬を入れないとは¬LRを使わないということ? それはやりすぎだろ >右側をピッタリ1個に制限 常に後件に論理式が1個?? それでどうやって A,¬A⊢¬B 導くの? あーもしかして¬を入れないとは 演算として∧∨→だけてこと? なんかそれもやりすぎなような気もするけど 確かに ¬Aはまず最初にA→人で置き換えればいいし 結果にA→人の部分があったらそれを¬Aにすればいいのか (この置き換えは最小論理でも許されるはず) その上で人⊢Aを公理にするかしないかで LJとMLを区別すればいいのかな >>340 ¬のルールは消して、¬A := A→Falseにして Γ ⊢ Δ --------- Γ, False ⊢ Δ を追加 目標は A, A→False ⊢ B→False なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと A, A→False,B ⊢ False →右 A, A→False ⊢ False 弱左 A ⊢ A とFalse ⊢ False →左 でできたぽい ¬LRを推論規則から削除して矛盾律人⊢Aも入れないことにして A,A→人⊢B→人 を導けばいい これはこんな風にできるね A⊢A 人⊢人 A,A→人⊢人 A,A→人,B⊢人 A,A→人⊢B→人 >>341 LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず こっちのがいいか A⊢A 人⊢人 A,A→人⊢人 A,A→人,B⊢人 A,A→人⊢B→人 >>342 同じね >>344 >右側が1つに制限するかか1つ以下に制限するかの違い ¬の代わりに人を導入することで 後件が空であることを明示的に 人と書いているだけじゃないかな ¬Lが無くなることで 後件が元々空でない推件からは 後件を空の推件を導けなくなってるよ >>344 >LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず じゃあ 後件が空であってもいいことにした場合に A,A→人⊢B はどう導くの? A⊢Aは公理だけど ⊢は公理じゃないから(むしろこれは真から偽が出ることを意味するからありえない推件) ¬Lを除外したことで後件が空の推件は決して現れないようになった だから後件が空であることを許しても仕方ない よってLJに戻すにはなんらかの公理なり推論規則を追加しないと 追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね A⊢A 人⊢人 人⊢B A,A→人⊢人 人⊢B A,A→人⊢B こんな感じ ↑これが数学板の実力です 専門板なのに異常にレベルが低い せいぜい数学の少しできる高校生レベル 1階の述語論理で ∀xP(x)はxの全てについてのP(x)の∧で (∀xP(x))⊢P(t)は∧Eに P(x)⊢(∀xP(x))は∧Iに過ぎないし ∃xP(x)はxの全てについてのP(x)の∨で P(t)⊢(∃xP(x))も∨Iに (∃xP(x)),P(x)→Q⊢Qも∨Eに過ぎない 論理式の列を有限に限る必要はないと思う むしろ上記のように全ての集合に対して全部とすることを許せば 1階の述語論理と変数のない命題論理(ただし命題変数は全ての集合に対するP(t)の全て)は全く同じものと分かる なぜ 全ての集合に対しての論理式の列を許さず ∀xP(x)や∃xP(x)にするのだろう 全ての集合に対しての論理式の列を考えることで 何かパラドクスが起こるのかしらん >なぜ全ての集合に対しての論理式の列を許さず >∀xP(x)や∃xP(x)にするのだろう 論理式が有限文字数で書けないから 推論が有限回ですまないだろう そんなものを人間は扱い得ないと思われる パラドックスとかいう以前 いきなり全ての集合を登場させなくても たとえば ∀x∈N∃n∈N(x<n) =∀x∈N(x<0∨x<1∨x<2∨…) =(0<0∨0<1∨0<2∨…)∧(1<0∨1<1∨1<2∨…)∧(2<0∨2<1∨2<2∨…)∧… でいいのでは? 意味的には全く同じものだし 論理式の全体が定義できないかも?と思わなくもないが 多分大丈夫じゃないかな >>358 >論理式が有限文字数で書けないから なんだけど 想定はできるよ 書けなくてはいけないということ自体に意味があるのかな? >>358 >そんなものを人間は扱い得ないと思われる コンピュータには無理そうと思われるけどね >多分大丈夫じゃないかな 楽天家はみなそういうが、皆死んでった・・・ 無限論理というものがあるのは知ってるが 普及してないのはきっと上手くいってないからだろう >>362 ,363 自然で∀も∃もいらないのに上手くいかないのってなぜかな 人間が無限を知覚するのにある一定の型にそったもの(P(x))しか考えられないてこともないと思うんだけど不思議 >>364 >なぜかな 僕のせいじゃないよ >不思議 だから僕のせいじゃないって >>365 それは全部に証明がつけられてもその全部を∧したものに証明がないてことで 感覚的には当然かなと思える てのは 証明の長さは有限じゃないといけないように思うから 無限を許すのは論理式の列だけで 証明の長さも無限を許すてのはどうかなあ まあ絶対禁止というのでもなくてもいいかとも思うが >>365 そうか P(x)だけ考える場合 証明はどのxについても同じ長さだから 全部合わせても並列で同じ長さてことが効くのかも? >>357 >なぜ >全ての集合に対しての論理式の列を許さず ? 全ての集合を範囲とする量化はできるよ ∀S:Set. S=S >>368 それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I 全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法 ∧が有限個だと全く規則を要求しない この関係を保ったまま無限に持っていくのは気持ち悪いね >>372 全く同じ証明でなくても長さが同じなら 無限の証明を並列にまとめて一つにみなして 長さ有限の証明としていいように思うけどね 並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない 式の記述を有限長にするなら、そもそも記載できる内容が制限される 存在記号の除去の意味がよくわかりません。 なぜあれが除去なの? 誰か教えて! >>375 存在記号はオアの一般化だからよ オアの除去はいわゆるジレンマ つまりどっち選んでも辿り着くところが同じてこと 存在記号の除去だと どれでも辿り着くところが同じならそう結論てこと 記号論理の同一性で 〜∃x∃y(Fx∧Fy∧(x≠y)) を変換すると ∀x∀y((Fx∧Fy)⊃(x=y)) になると書いてあるのですが、どうすればそうなるのかがわかりません。 途中の過程を詳しく教えてもらえないでしょうか? ∀x∀y=∀(x,y) ∃x∃y=∃(x,y) ¬∀x=∃x¬ ¬(A∧B)=¬A∨¬B=A→¬B=A⊃¬B ¬¬C=C わざわざ京大まで来て、ダメットの写真をスライドに映して顔がどうとか講義してた非常勤講師、小物感 P:4の倍数 ならば Q:偶数 を普通は P→Q と表すけれど P⊃Q と書くこともあるよな Pである集合とQである集合を考えたら {n|P}⊂{n|Q} だから混乱するけれど これをあえて P⊃Q と書くのは P:4の倍数 である性質は Q:偶数 である性質を 含んでいるから のような説明をされる時もある P⊃Q の由来ってこれなの? 自分の感覚だと → と同じように左から右に向いているように見えるから ⊃ としたのかなとも思うんだけど >>380 確かこいつだったと思うけど、キムタクがドラマで「世の中には閉じたやつと開いたやつがいるんだ」と言ってたとかなんとかの話マジどうでもよかったな 京大でそんな話するなよ read.cgi ver 07.5.5 2024/06/08 Walang Kapalit ★ | Donguri System Team 5ちゃんねる