数学基礎論・数理論理学 その19 (605ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
327(1): １３２人目の素数さん [] 2024/05/19(日)04:38 ID:MeSZkcgn(1/8)
>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)
329: １３２人目の素数さん [] 2024/05/19(日)09:32 ID:MeSZkcgn(2/8)
>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて
330: １３２人目の素数さん [] 2024/05/19(日)09:32 ID:MeSZkcgn(3/8)
自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて
331: １３２人目の素数さん [] 2024/05/19(日)09:32 ID:MeSZkcgn(4/8)
もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない
332: １３２人目の素数さん [] 2024/05/19(日)09:44 ID:MeSZkcgn(5/8)
>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨¬Pおよび
二重否定の除去¬¬P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ
333: １３２人目の素数さん [] 2024/05/19(日)10:04 ID:MeSZkcgn(6/8)
>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし
334: １３２人目の素数さん [] 2024/05/19(日)10:23 ID:MeSZkcgn(7/8)
>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる
336: １３２人目の素数さん [] 2024/05/19(日)23:35 ID:MeSZkcgn(8/8)
ウィキペのシーケント計算の項目に
∧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で
これは推論規則というよりは
論理式の列の性質というべき
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s