X



トップページ数学
356コメント163KB
数学基礎論・数理論理学 その19
0001132人目の素数さん
垢版 |
2023/10/06(金) 22:38:03.74ID:tsskr+sA
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
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/
0306132人目の素数さん
垢版 |
2024/05/15(水) 21:12:08.89ID:dJj5Zqh2
>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ
0309132人目の素数さん
垢版 |
2024/05/16(木) 07:30:47.04ID:iQRAo/4g
>>306
たとえば
P∨Qを¬P→Qとするか¬Q→Pとするか
これらが同等であるべきことから
Q=¬Pのとき
¬P→¬Pと¬¬P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ
0310132人目の素数さん
垢版 |
2024/05/16(木) 07:59:05.45ID:Z2w1oqQM
爆発律君こそ、何がしたいんだろ?

制限するって何をどう?
まあ、Weakeningを入れないとかそういうことなんだろうけど
0311132人目の素数さん
垢版 |
2024/05/16(木) 11:43:21.19ID:WmP+w3aC
>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ
0312132人目の素数さん
垢版 |
2024/05/16(木) 13:56:53.51ID:9U85ZyDM
>>311
ゲンツェンのシークエント計算ではいかんのかい?
そこの構造規則っていうのがあるだろ?
それ見直すってのはどうよ
0313132人目の素数さん
垢版 |
2024/05/16(木) 14:12:27.05ID:x1lVhHOe
>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな
0314132人目の素数さん
垢版 |
2024/05/16(木) 15:02:57.28ID:iQRAo/4g
>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん
0315132人目の素数さん
垢版 |
2024/05/16(木) 15:54:59.58ID:x1lVhHOe
>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた
0316132人目の素数さん
垢版 |
2024/05/16(木) 16:51:01.20ID:x1lVhHOe
>>312
ちょっと考えてみたけど
A ⊢ A
A, ¬A ⊢
A, ¬A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない?

とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ
0317132人目の素数さん
垢版 |
2024/05/16(木) 16:56:13.93ID:arX/sd11
横だけど、こういうとき論理の規則、p->q等、は何を前提とするの?
0318132人目の素数さん
垢版 |
2024/05/16(木) 17:05:19.42ID:HKUIjE5U
>0個から1個への弱化を禁止

これが正解じゃね?
0321132人目の素数さん
垢版 |
2024/05/16(木) 18:00:38.18ID:arX/sd11
>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK

こんな感じね、中味はしらんけど
0322132人目の素数さん
垢版 |
2024/05/18(土) 05:07:28.76ID:irl6hz/v
二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ?体系になんか秘密があるのか?
0324132人目の素数さん
垢版 |
2024/05/18(土) 22:26:11.96ID:dFtrDe5F
>>322
1)シーケント計算で最小論理はどういうもの?
2)シーケント計算でLJは後件が一つ以下となる理由は?
0325132人目の素数さん
垢版 |
2024/05/18(土) 23:29:20.65ID:irl6hz/v
>>324
1しらん
2そうするとなんかうまくいったから

これ何の話なんだ?なんで急に質問が飛んできたんだ…
0326132人目の素数さん
垢版 |
2024/05/19(日) 04:22:38.75ID:S2r1dLN0
やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…
0327132人目の素数さん
垢版 |
2024/05/19(日) 04:38:39.75ID:MeSZkcgn
>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)
0329132人目の素数さん
垢版 |
2024/05/19(日) 09:32:12.73ID:MeSZkcgn
>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて
0330132人目の素数さん
垢版 |
2024/05/19(日) 09:32:37.81ID:MeSZkcgn
自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて
0331132人目の素数さん
垢版 |
2024/05/19(日) 09:32:56.87ID:MeSZkcgn
もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない
0332132人目の素数さん
垢版 |
2024/05/19(日) 09:44:26.86ID:MeSZkcgn
>>324
>1)シーケント計算で最小論理はどういうもの?
自然演繹なら矛盾律人→Pと排中律P∨¬Pおよび
二重否定の除去¬¬P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ
0333132人目の素数さん
垢版 |
2024/05/19(日) 10:04:10.74ID:MeSZkcgn
>>319
こちらは許容し(最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか?
A, ¬A ⊢ ¬B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ¬A ⊢ B
A, ¬A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし
0334132人目の素数さん
垢版 |
2024/05/19(日) 10:23:12.56ID:MeSZkcgn
>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では?
NOT-1,2,3を除いてFALSEってのを入れてる
0335132人目の素数さん
垢版 |
2024/05/19(日) 21:17:58.59ID:S2r1dLN0
とりあえず、左側を1個以下にするのは
A, ¬A ⊢ ¬B
もなくなっちゃうんだよなあ
A∧¬A ⊢ ¬B
ならでるんかな
でなさそうだけども
0336132人目の素数さん
垢版 |
2024/05/19(日) 23:35:06.40ID:MeSZkcgn
ウィキペのシーケント計算の項目に
∧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で
これは推論規則というよりは
論理式の列の性質というべき
0337132人目の素数さん
垢版 |
2024/05/19(日) 23:51:19.28ID:S2r1dLN0
結局カンニングして、¬はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった
0338132人目の素数さん
垢版 |
2024/05/20(月) 00:08:32.42ID:scxUAhLA
ここでシーケント(推件)とは自然演繹における推論図の状況を表し
カットは自然演繹で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を制限するあるいは別の推論規則にする必要があるはず
0339132人目の素数さん
垢版 |
2024/05/20(月) 00:13:18.37ID:scxUAhLA
やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる
0340132人目の素数さん
垢版 |
2024/05/20(月) 00:18:53.06ID:scxUAhLA
>>337
>¬はいれずにFalseをいれて、
¬を入れないとは¬LRを使わないということ?
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個??
それでどうやって
A,¬A⊢¬B
導くの?
0341132人目の素数さん
垢版 |
2024/05/20(月) 00:25:18.56ID:scxUAhLA
あーもしかして¬を入れないとは
演算として∧∨→だけてこと?
なんかそれもやりすぎなような気もするけど
確かに
¬Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを¬Aにすればいいのか
(この置き換えは最小論理でも許されるはず)
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな
0342132人目の素数さん
垢版 |
2024/05/20(月) 00:50:24.32ID:os7gXi5h
>>340
¬のルールは消して、¬A := A→Falseにして
Γ ⊢ Δ
---------
Γ, False ⊢ Δ
を追加

目標は
A, A→False ⊢ B→False
なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと
A, A→False,B ⊢ False →右
A, A→False ⊢ False 弱左
A ⊢ A とFalse ⊢ False →左

でできたぽい
0343132人目の素数さん
垢版 |
2024/05/20(月) 00:52:09.24ID:scxUAhLA
¬LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
0345132人目の素数さん
垢版 |
2024/05/20(月) 00:55:17.04ID:scxUAhLA
こっちのがいいか
A⊢A 人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね
0346132人目の素数さん
垢版 |
2024/05/20(月) 01:03:14.51ID:scxUAhLA
>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
¬の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
¬Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ
0347132人目の素数さん
垢版 |
2024/05/20(月) 01:11:16.91ID:scxUAhLA
>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの?
0348132人目の素数さん
垢版 |
2024/05/20(月) 01:22:12.63ID:scxUAhLA
A⊢Aは公理だけど
⊢は公理じゃないから(むしろこれは真から偽が出ることを意味するからありえない推件)
¬Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね
0349132人目の素数さん
垢版 |
2024/05/20(月) 01:25:52.41ID:scxUAhLA
A⊢A 人⊢人 人⊢B
A,A→人⊢人 人⊢B
A,A→人⊢B
こんな感じ
0352132人目の素数さん
垢版 |
2024/05/22(水) 21:30:43.90ID:VDYRR5Y/
ここFランばっかだなw
0353132人目の素数さん
垢版 |
2024/05/22(水) 21:52:48.92ID:U3WgW+/X
>>352
Fランに詳しい人キタ
0355132人目の素数さん
垢版 |
2024/05/22(水) 22:45:38.90ID:T8l1ODsI
↑これが数学板の実力です
専門板なのに異常にレベルが低い
せいぜい数学の少しできる高校生レベル
レスを投稿する


ニューススポーツなんでも実況