数学基礎論・数理論理学 その19 (550ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
338: 2024/05/20(月)00:08 ID:scxUAhLA(1/10) AAS
ここでシーケント（推件）とは自然演繹における推論図の状況を表し
カットは自然演繹で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を制限するあるいは別の推論規則にする必要があるはず
339: 2024/05/20(月)00:13 ID:scxUAhLA(2/10) AAS
やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる
340(1): 2024/05/20(月)00:18 ID:scxUAhLA(3/10) AAS
>>337
>￢はいれずにFalseをいれて、
¬を入れないとは¬LRを使わないということ？
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個？？
それでどうやって
A,¬A⊢¬B
導くの？
341(1): 2024/05/20(月)00:25 ID:scxUAhLA(4/10) AAS
あーもしかして¬を入れないとは
演算として∧∨→だけてこと？
なんかそれもやりすぎなような気もするけど
確かに
¬Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを¬Aにすればいいのか
（この置き換えは最小論理でも許されるはず）
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな
343: 2024/05/20(月)00:52 ID:scxUAhLA(5/10) AAS
¬LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
345: 2024/05/20(月)00:55 ID:scxUAhLA(6/10) AAS
こっちのがいいか
A⊢A 人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね
346: 2024/05/20(月)01:03 ID:scxUAhLA(7/10) AAS
>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
¬の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
¬Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ
347(1): 2024/05/20(月)01:11 ID:scxUAhLA(8/10) AAS
>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの？
348(1): 2024/05/20(月)01:22 ID:scxUAhLA(9/10) AAS
A⊢Aは公理だけど
⊢は公理じゃないから（むしろこれは真から偽が出ることを意味するからありえない推件）
¬Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね
349: 2024/05/20(月)01:25 ID:scxUAhLA(10/10) AAS
A⊢A 人⊢人 人⊢B
A,A→人⊢人 人⊢B
A,A→人⊢B
こんな感じ
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ
ぬこの手 ぬこTOP 0.042s