数学基礎論・数理論理学　その19

**１３２人目の素数さん** · 2024/05/18(土) 22:26:11.96

>>322
1）シーケント計算で最小論理はどういうもの？
2）シーケント計算でLJは後件が一つ以下となる理由は？

**１３２人目の素数さん** · 2024/05/18(土) 23:29:20.65

>>324
1しらん
2そうするとなんかうまくいったから

これ何の話なんだ？なんで急に質問が飛んできたんだ…

**１３２人目の素数さん** · 2024/05/19(日) 04:22:38.75

やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…

**１３２人目の素数さん** · 2024/05/19(日) 04:38:39.75

>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)

**１３２人目の素数さん** · 2024/05/19(日) 05:32:11.17

>>327
さんくす
そっかFalse→￢Aの形は爆発律いらんのだったわ

**１３２人目の素数さん** · 2024/05/19(日) 09:32:12.73

>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて

**１３２人目の素数さん** · 2024/05/19(日) 09:32:37.81

自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて

**１３２人目の素数さん** · 2024/05/19(日) 09:32:56.87

もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない

**１３２人目の素数さん** · 2024/05/19(日) 09:44:26.86

>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨￢Pおよび
二重否定の除去￢￢P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ

**１３２人目の素数さん** · 2024/05/19(日) 10:04:10.74

>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし

**１３２人目の素数さん** · 2024/05/19(日) 10:23:12.56

>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる

**１３２人目の素数さん** · 2024/05/19(日) 21:17:58.59

とりあえず、左側を1個以下にするのは
A, ￢A ⊢ ￢B
もなくなっちゃうんだよなあ
A∧￢A ⊢ ￢B
ならでるんかな
でなさそうだけども

**１３２人目の素数さん** · 2024/05/19(日) 23:35:06.40

ウィキペのシーケント計算の項目に
∧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で
これは推論規則というよりは
論理式の列の性質というべき

**１３２人目の素数さん** · 2024/05/19(日) 23:51:19.28

結局カンニングして、￢はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった

**１３２人目の素数さん** · 2024/05/20(月) 00:08:32.42

ここでシーケント（推件）とは自然演繹における推論図の状況を表し
カットは自然演繹で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を制限するあるいは別の推論規則にする必要があるはず

**１３２人目の素数さん** · 2024/05/20(月) 00:13:18.37

やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる

**１３２人目の素数さん** · 2024/05/20(月) 00:18:53.06

>>337
>￢はいれずにFalseをいれて、
￢を入れないとは￢LRを使わないということ？
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個？？
それでどうやって
A,￢A⊢￢B
導くの？

**１３２人目の素数さん** · 2024/05/20(月) 00:25:18.56

あーもしかして￢を入れないとは
演算として∧∨→だけてこと？
なんかそれもやりすぎなような気もするけど
確かに
￢Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを￢Aにすればいいのか
（この置き換えは最小論理でも許されるはず）
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな

**１３２人目の素数さん** · 2024/05/20(月) 00:50:24.32

>>340
￢のルールは消して、￢A := A→Falseにして
Γ ⊢ Δ
---------
Γ, False ⊢ Δ
を追加

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

でできたぽい

**１３２人目の素数さん** · 2024/05/20(月) 00:52:09.24

￢LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人

**１３２人目の素数さん** · 2024/05/20(月) 00:55:16.05

>>341
LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず

**１３２人目の素数さん** · 2024/05/20(月) 00:55:17.04

こっちのがいいか
A⊢A　人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね

**１３２人目の素数さん** · 2024/05/20(月) 01:03:14.51

>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
￢の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
￢Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ

**１３２人目の素数さん** · 2024/05/20(月) 01:11:16.91

>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの？

**１３２人目の素数さん** · 2024/05/20(月) 01:22:12.63

A⊢Aは公理だけど
⊢は公理じゃないから（むしろこれは真から偽が出ることを意味するからありえない推件）
￢Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね

**１３２人目の素数さん** · 2024/05/20(月) 01:25:52.41

A⊢A　人⊢人　人⊢B
A,A→人⊢人　人⊢B
A,A→人⊢B
こんな感じ

**１３２人目の素数さん** · 2024/05/20(月) 01:29:19.02

>>347
なんかカンニングした
https://ncatlab.org/nlab/show/sequent+calculus
をだいぶ読み間違えてたわ

**１３２人目の素数さん** · 2024/05/20(月) 01:30:17.54

>>348
そう、そこ読み間違えてたっぽい

**１３２人目の素数さん** · 2024/05/22(水) 21:30:43.90

ここFランばっかだなw

**１３２人目の素数さん** · 2024/05/22(水) 21:52:48.92

>>352
Fランに詳しい人キタ

**１３２人目の素数さん** · 2024/05/22(水) 22:29:00.77

東都路地

**１３２人目の素数さん** · 2024/05/22(水) 22:45:38.90

↑これが数学板の実力です
専門板なのに異常にレベルが低い
せいぜい数学の少しできる高校生レベル

**１３２人目の素数さん** · 2024/05/23(木) 00:44:50.15

糖登呂爺

**１３２人目の素数さん** · 2024/05/25(土) 15:15:31.40

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)にするのだろう
全ての集合に対しての論理式の列を考えることで
何かパラドクスが起こるのかしらん

**１３２人目の素数さん** · 2024/05/25(土) 15:32:44.59

＞なぜ全ての集合に対しての論理式の列を許さず
＞∀xP(x)や∃xP(x)にするのだろう

論理式が有限文字数で書けないから
推論が有限回ですまないだろう
そんなものを人間は扱い得ないと思われる
パラドックスとかいう以前

**１３２人目の素数さん** · 2024/05/25(土) 15:37:16.77

いきなり全ての集合を登場させなくても
たとえば
∀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∨…)∧…
でいいのでは？
意味的には全く同じものだし
論理式の全体が定義できないかも？と思わなくもないが
多分大丈夫じゃないかな

**１３２人目の素数さん** · 2024/05/25(土) 15:38:13.34

>>358
>論理式が有限文字数で書けないから
なんだけど
想定はできるよ
書けなくてはいけないということ自体に意味があるのかな？

**１３２人目の素数さん** · 2024/05/25(土) 15:39:05.45

>>358
>そんなものを人間は扱い得ないと思われる
コンピュータには無理そうと思われるけどね

**１３２人目の素数さん** · 2024/05/25(土) 15:53:05.79

＞多分大丈夫じゃないかな
　楽天家はみなそういうが、皆死んでった・・・

**１３２人目の素数さん** · 2024/05/25(土) 15:54:01.06

無限論理というものがあるのは知ってるが
普及してないのはきっと上手くいってないからだろう

**１３２人目の素数さん** · 2024/05/25(土) 18:13:41.23

>>362,363
自然で∀も∃もいらないのに上手くいかないのってなぜかな
人間が無限を知覚するのにある一定の型にそったもの（P(x)）しか考えられないてこともないと思うんだけど不思議

**１３２人目の素数さん** · 2024/05/25(土) 18:35:14.01

ω矛盾してるようなのはどうするんやろ

**１３２人目の素数さん** · 2024/05/25(土) 19:14:06.79

>>364
>なぜかな
僕のせいじゃないよ
>不思議
だから僕のせいじゃないって

**１３２人目の素数さん** · 2024/05/25(土) 19:55:35.71

>>365
それは全部に証明がつけられてもその全部を∧したものに証明がないてことで
感覚的には当然かなと思える
てのは
証明の長さは有限じゃないといけないように思うから
無限を許すのは論理式の列だけで
証明の長さも無限を許すてのはどうかなあ
まあ絶対禁止というのでもなくてもいいかとも思うが

**１３２人目の素数さん** · 2024/05/25(土) 20:14:11.89

>>365
そうか
P(x)だけ考える場合
証明はどのxについても同じ長さだから
全部合わせても並列で同じ長さてことが効くのかも？

**１３２人目の素数さん** · 2024/05/25(土) 21:15:54.39

>>357
>なぜ
>全ての集合に対しての論理式の列を許さず

？
全ての集合を範囲とする量化はできるよ
∀S:Set. S=S

**１３２人目の素数さん** · 2024/05/25(土) 21:20:33.31

>>369
∀使わずそれを並列にするってことよ

**１３２人目の素数さん** · 2024/05/25(土) 21:21:00.33

内容は同じでしょ？許容してもいいんじゃないかな

**１３２人目の素数さん** · 2024/05/25(土) 23:37:41.74

>>368
それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I
全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法
∧が有限個だと全く規則を要求しない
この関係を保ったまま無限に持っていくのは気持ち悪いね

**１３２人目の素数さん** · 2024/05/26(日) 08:07:06.94

>>372
全く同じ証明でなくても長さが同じなら
無限の証明を並列にまとめて一つにみなして
長さ有限の証明としていいように思うけどね

**１３２人目の素数さん** · 2024/05/28(火) 10:30:28.58

並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない
式の記述を有限長にするなら、そもそも記載できる内容が制限される

**１３２人目の素数さん** · 2024/06/01(土) 18:53:52.35

存在記号の除去の意味がよくわかりません。
なぜあれが除去なの?
誰か教えて！

**１３２人目の素数さん** · 2024/06/01(土) 18:58:37.27

>>375
存在記号はオアの一般化だからよ
オアの除去はいわゆるジレンマ
つまりどっち選んでも辿り着くところが同じてこと
存在記号の除去だと
どれでも辿り着くところが同じならそう結論てこと

**１３２人目の素数さん** · 2024/06/03(月) 09:54:43.55

記号論理の同一性で
～∃x∃y(Fx∧Fy∧(x≠y))
を変換すると
∀x∀y((Fx∧Fy)⊃(x＝y))
になると書いてあるのですが、どうすればそうなるのかがわかりません。
途中の過程を詳しく教えてもらえないでしょうか？

**１３２人目の素数さん** · 2024/06/03(月) 23:24:05.73

∀x∀y=∀(x,y)
∃x∃y=∃(x,y)
￢∀x=∃x￢
￢(A∧B)=￢A∨￢B=A→￢B=A⊃￢B
￢￢C=C

**１３２人目の素数さん** · 2024/06/03(月) 23:25:19.65

>>378
>￢∀x=∃x￢
￢∃x=∀x￢

**１３２人目の素数さん** · 2024/06/07(金) 08:06:17.00

わざわざ京大まで来て、ダメットの写真をスライドに映して顔がどうとか講義してた非常勤講師、小物感

**１３２人目の素数さん** · 2024/06/09(日) 10:02:36.73

P:4の倍数　ならば　Q:偶数
を普通は
P→Q
と表すけれど
P⊃Q
と書くこともあるよな
Pである集合とQである集合を考えたら
{n|P}⊂{n|Q}
だから混乱するけれど
これをあえて
P⊃Q
と書くのは
P:4の倍数　である性質は　Q:偶数　である性質を　含んでいるから
のような説明をされる時もある
P⊃Q
の由来ってこれなの？
自分の感覚だと
→
と同じように左から右に向いているように見えるから
⊃
としたのかなとも思うんだけど

**１３２人目の素数さん** · 2024/06/12(水) 08:49:22.90

排中律の証明とか言ってる奴笑える

**１３２人目の素数さん** · 2024/06/18(火) 10:38:57.99

>>380
確かこいつだったと思うけど、キムタクがドラマで「世の中には閉じたやつと開いたやつがいるんだ」と言ってたとかなんとかの話マジどうでもよかったな
京大でそんな話するなよ

**１３２人目の素数さん** · 2024/06/22(土) 10:35:01.14

今だけです
https://i.imgur.com/3Y8ax2T.jpg

**１３２人目の素数さん** · 2024/06/22(土) 16:14:48.13

>>384
これは良かったよなあ

数学基礎論・数理論理学 その19

数学基礎論・数理論理学　その19