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

[0286 １３２人目の素数さん 2024/05/14(火) 20:04:39.98 ID:SL8NPmh1]

>>281
>アッカーマン関数ってあるじゃん
>あれって原始帰納的関数じゃないよ
じゃあ>>271も原始帰納的関数ではない？

[0287 １３２人目の素数さん 2024/05/15(水) 04:37:59.45 ID:ocJISfUq]

>>272
結局これなんだったん？
推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね？トートロジーであることの定義をこねくり回したりしたら知らんけど

[0288 １３２人目の素数さん 2024/05/15(水) 05:45:00.98 ID:jnpUU+rE]

>>285
>何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？

というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない
ここで「除く」というのは「帰納的でない」という返答を返すという意味
帰納的な場合だけ「帰納的だ」といえばいいのであればOK　これが帰納的可算集合

>>286
原始帰納的関数の定義を確認してごらん
その上で、その定義の方法で実現可能か確認してごらん
それが答えだよ

[0289 １３２人目の素数さん 2024/05/15(水) 05:47:44.02 ID:jnpUU+rE]

>>284
＞トートロジーの否定から任意の命題が出るっての形では
＞推論規則や公理には採用できないって話してるつもりなんだけど

矛盾を導くのに、全く無関係な命題が入っていてもOKなら
それが爆発律と同じことっていってるけど理解できてる？

論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ

[0290 １３２人目の素数さん 2024/05/15(水) 06:50:18.85 ID:vwN3FcOM]

>>288
>帰納的な場合だけ「帰納的だ」といえばいいのであればOK
その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな？
つまり関数と言っても数学的な意味（値が定まる）でなくて
プログラミングでいう関数なのね？

[0291 １３２人目の素数さん 2024/05/15(水) 08:27:08.07 ID:ruXG29YD]

>>290
関数の記法は決まっている筈（つまりプログラムとして書けることが必須）
その上で、答えが返ってこない場合は終わらない、という感じ（停止判定）

＞関数と言っても数学的な意味（値が定まる）でなくてプログラミングでいう関数なのね？
プログラムで書けない関数は初めから勘定外かと
（プログラムとして書ける＝ゲーデルコード化可能）

[0292 １３２人目の素数さん 2024/05/15(水) 08:36:06.59 ID:vwN3FcOM]

>>291
ふむサンクス

[0293 １３２人目の素数さん 2024/05/15(水) 17:46:57.18 ID:dJj5Zqh2]

>>289
何言ってるのか全然わからん

[0294 １３２人目の素数さん 2024/05/15(水) 18:25:46.35 ID:jnpUU+rE]

>>293
脳味噌ある？

[0295 １３２人目の素数さん 2024/05/15(水) 18:26:14.03 ID:dJj5Zqh2]

>>289
なんの話をしてるのかそこからまずわからん
爆発律に関して何を話してるのかいな？

[0296 １３２人目の素数さん 2024/05/15(水) 18:32:02.10 ID:jnpUU+rE]

　矛盾Q∧¬Qから任意の命題Pが証明可能
⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾
⇔任意の命題の否定¬Pから排中律（矛盾の否定）¬Q∨Qが証明可能

[0297 １３２人目の素数さん 2024/05/15(水) 18:45:28.94 ID:dJj5Zqh2]

>>296
爆発律が推論規則に入ってる場合の話をしてるの？入ってない場合の話をしてるの？
問題の建て付けのところからすでにわからんのだが

[0298 １３２人目の素数さん 2024/05/15(水) 19:05:41.36 ID:+zn+M4xO]

爆発律を推論規則に入れる意味ある？

[0299 １３２人目の素数さん 2024/05/15(水) 19:15:06.38 ID:vwN3FcOM]

>>298
古典論理なら
二重否定の除去DNEから
自然と導かれるよ
逆に言えば
それがトートロジーでないなら
二重否定の除去がいつもできると限らないことになる

[0300 １３２人目の素数さん 2024/05/15(水) 19:31:06.15 ID:dJj5Zqh2]

>>298
自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる

[0301 １３２人目の素数さん 2024/05/15(水) 19:51:19.75 ID:vwN3FcOM]

>>300
>ヒルベルトスタイルに排中律
ヒルベルト式だと排中律は内包されてるんじゃないの？
たとえばP∨Qは¬P→QにP∧Qは¬(P→¬Q)にするんでしょ？
論理演算が→と¬しかないから
排中律ないと制限きついでしょ

[0302 １３２人目の素数さん 2024/05/15(水) 19:59:55.29 ID:dJj5Zqh2]

>>296
> 　矛盾Q∧¬Qから任意の命題Pが証明可能
これは「任意のPとQにたいして、Q∧¬Q ⊢ P」を意図してるの？それとも「⊢Q∧¬Q ならば ⊢P」なのか？
他の行も同じで何を書いてるつもりなのかさっぱりわからんし
⊢の定義をまずしないと何を言ってるのかさっぱりなんだが…

[0303 １３２人目の素数さん 2024/05/15(水) 20:05:21.61 ID:dJj5Zqh2]

>>301
直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ

なんかurl貼ろうとしたら怒られたんだが…

[0304 １３２人目の素数さん 2024/05/15(水) 20:10:29.20 ID:dJj5Zqh2]

>>301
あと古典と違って、君の言ってる問題があるから

＞しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため {→,⊥}, {∧,¬},
{∨,¬} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。

こうなってる

[0305 １３２人目の素数さん 2024/05/15(水) 20:46:33.12 ID:vwN3FcOM]

>>304
>直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する
が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った

[0306 １３２人目の素数さん 2024/05/15(水) 21:12:08.89 ID:dJj5Zqh2]

>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ

[0307 １３２人目の素数さん 2024/05/16(木) 04:39:12.20 ID:WmP+w3aC]

結局、トートロジーおじは何が言いたかったんやろ

[0308 １３２人目の素数さん 2024/05/16(木) 04:52:31.12 ID:arX/sd11]

自説

[0309 １３２人目の素数さん 2024/05/16(木) 07:30:47.04 ID:iQRAo/4g]

>>306
たとえば
P∨Qを¬P→Qとするか¬Q→Pとするか
これらが同等であるべきことから
Q=¬Pのとき
¬P→¬Pと¬¬P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ

[0310 １３２人目の素数さん 2024/05/16(木) 07:59:05.45 ID:Z2w1oqQM]

爆発律君こそ、何がしたいんだろ？

制限するって何をどう？
まあ、Weakeningを入れないとかそういうことなんだろうけど

[0311 １３２人目の素数さん 2024/05/16(木) 11:43:21.19 ID:WmP+w3aC]

>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ

[0312 １３２人目の素数さん 2024/05/16(木) 13:56:53.51 ID:9U85ZyDM]

>>311
ゲンツェンのシークエント計算ではいかんのかい？
そこの構造規則っていうのがあるだろ？
それ見直すってのはどうよ

[0313 １３２人目の素数さん 2024/05/16(木) 14:12:27.05 ID:x1lVhHOe]

>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな

[0314 １３２人目の素数さん 2024/05/16(木) 15:02:57.28 ID:iQRAo/4g]

>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん

[0315 １３２人目の素数さん 2024/05/16(木) 15:54:59.58 ID:x1lVhHOe]

>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた

[0316 １３２人目の素数さん 2024/05/16(木) 16:51:01.20 ID:x1lVhHOe]

>>312
ちょっと考えてみたけど
A ⊢ A
A, ¬A ⊢
A, ¬A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない？

とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ

[0317 １３２人目の素数さん 2024/05/16(木) 16:56:13.93 ID:arX/sd11]

横だけど、こういうとき論理の規則、p->q等、は何を前提とするの？

[0318 １３２人目の素数さん 2024/05/16(木) 17:05:19.42 ID:HKUIjE5U]

＞0個から1個への弱化を禁止

これが正解じゃね？

[0319 １３２人目の素数さん 2024/05/16(木) 17:32:59.62 ID:x1lVhHOe]

>>318
A ⊢ A
A, ￢A ⊢
A, ￢A, B ⊢
A, ￢A ⊢ ¬B
ちょっと弱い爆発律が導けちゃった

[0320 １３２人目の素数さん 2024/05/16(木) 17:57:26.21 ID:x1lVhHOe]

>>318
A ⊢ A
A ⊢ A, B
A, ￢A ⊢ B
わいの挙げた2つは両方ゴミだったw

[0321 １３２人目の素数さん 2024/05/16(木) 18:00:38.18 ID:arX/sd11]

>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK

こんな感じね、中味はしらんけど

[0322 １３２人目の素数さん 2024/05/18(土) 05:07:28.76 ID:irl6hz/v]

二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ？体系になんか秘密があるのか？

[0323 １３２人目の素数さん 2024/05/18(土) 08:02:33.90 ID:kpZOEtRa]

40−16÷4÷2=

[0324 １３２人目の素数さん 2024/05/18(土) 22:26:11.96 ID:dFtrDe5F]

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

[0325 １３２人目の素数さん 2024/05/18(土) 23:29:20.65 ID:irl6hz/v]

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

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

[0326 １３２人目の素数さん 2024/05/19(日) 04:22:38.75 ID:S2r1dLN0]

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

[0327 １３２人目の素数さん 2024/05/19(日) 04:38:39.75 ID:MeSZkcgn]

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

[0328 １３２人目の素数さん 2024/05/19(日) 05:32:11.17 ID:S2r1dLN0]

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

[0329 １３２人目の素数さん 2024/05/19(日) 09:32:12.73 ID:MeSZkcgn]

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

[0330 １３２人目の素数さん 2024/05/19(日) 09:32:37.81 ID:MeSZkcgn]

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

[0331 １３２人目の素数さん 2024/05/19(日) 09:32:56.87 ID:MeSZkcgn]

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

[0332 １３２人目の素数さん 2024/05/19(日) 09:44:26.86 ID:MeSZkcgn]

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

[0333 １３２人目の素数さん 2024/05/19(日) 10:04:10.74 ID:MeSZkcgn]

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

[0334 １３２人目の素数さん 2024/05/19(日) 10:23:12.56 ID:MeSZkcgn]

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

[0335 １３２人目の素数さん 2024/05/19(日) 21:17:58.59 ID:S2r1dLN0]

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

[0336 １３２人目の素数さん 2024/05/19(日) 23:35:06.40 ID: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で
これは推論規則というよりは
論理式の列の性質というべき

[0337 １３２人目の素数さん 2024/05/19(日) 23:51:19.28 ID:S2r1dLN0]

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

[0338 １３２人目の素数さん 2024/05/20(月) 00:08:32.42 ID: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を制限するあるいは別の推論規則にする必要があるはず

[0339 １３２人目の素数さん 2024/05/20(月) 00:13:18.37 ID:scxUAhLA]

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

[0340 １３２人目の素数さん 2024/05/20(月) 00:18:53.06 ID:scxUAhLA]

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

[0341 １３２人目の素数さん 2024/05/20(月) 00:25:18.56 ID:scxUAhLA]

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

[0342 １３２人目の素数さん 2024/05/20(月) 00:50:24.32 ID:os7gXi5h]

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

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

でできたぽい

[0343 １３２人目の素数さん 2024/05/20(月) 00:52:09.24 ID:scxUAhLA]

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

[0344 １３２人目の素数さん 2024/05/20(月) 00:55:16.05 ID:os7gXi5h]

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

[0345 １３２人目の素数さん 2024/05/20(月) 00:55:17.04 ID:scxUAhLA]

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

[0346 １３２人目の素数さん 2024/05/20(月) 01:03:14.51 ID:scxUAhLA]

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

[0347 １３２人目の素数さん 2024/05/20(月) 01:11:16.91 ID:scxUAhLA]

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

[0348 １３２人目の素数さん 2024/05/20(月) 01:22:12.63 ID:scxUAhLA]

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

[0349 １３２人目の素数さん 2024/05/20(月) 01:25:52.41 ID:scxUAhLA]

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

[0350 １３２人目の素数さん 2024/05/20(月) 01:29:19.02 ID:os7gXi5h]

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

[0351 １３２人目の素数さん 2024/05/20(月) 01:30:17.54 ID:os7gXi5h]

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

[0352 １３２人目の素数さん 2024/05/22(水) 21:30:43.90 ID:VDYRR5Y/]

ここFランばっかだなw

[0353 １３２人目の素数さん 2024/05/22(水) 21:52:48.92 ID:U3WgW+/X]

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

[0354 １３２人目の素数さん 2024/05/22(水) 22:29:00.77 ID:hbcyxk4S]

東都路地

[0355 １３２人目の素数さん 2024/05/22(水) 22:45:38.90 ID:T8l1ODsI]

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

[0356 １３２人目の素数さん 2024/05/23(木) 00:44:50.15 ID:KmslQbbB]

糖登呂爺

[0357 １３２人目の素数さん 2024/05/25(土) 15:15:31.40 ID:LLIp+91v]

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

[0358 １３２人目の素数さん 2024/05/25(土) 15:32:44.59 ID:43OvMs57]

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

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

[0359 １３２人目の素数さん 2024/05/25(土) 15:37:16.77 ID:LLIp+91v]

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

[0360 １３２人目の素数さん 2024/05/25(土) 15:38:13.34 ID:LLIp+91v]

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

[0361 １３２人目の素数さん 2024/05/25(土) 15:39:05.45 ID:LLIp+91v]

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

[0362 １３２人目の素数さん 2024/05/25(土) 15:53:05.79 ID:43OvMs57]

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

[0363 １３２人目の素数さん 2024/05/25(土) 15:54:01.06 ID:43OvMs57]

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

[0364 １３２人目の素数さん 2024/05/25(土) 18:13:41.23 ID:LLIp+91v]

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

[0365 １３２人目の素数さん 2024/05/25(土) 18:35:14.01 ID:KzALYiRl]

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

[0366 １３２人目の素数さん 2024/05/25(土) 19:14:06.79 ID:43OvMs57]

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

[0367 １３２人目の素数さん 2024/05/25(土) 19:55:35.71 ID:LLIp+91v]

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

[0368 １３２人目の素数さん 2024/05/25(土) 20:14:11.89 ID:LLIp+91v]

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

[0369 １３２人目の素数さん 2024/05/25(土) 21:15:54.39 ID:GO36pM1y]

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

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

[0370 １３２人目の素数さん 2024/05/25(土) 21:20:33.31 ID:LLIp+91v]

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

[0371 １３２人目の素数さん 2024/05/25(土) 21:21:00.33 ID:LLIp+91v]

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

[0372 １３２人目の素数さん 2024/05/25(土) 23:37:41.74 ID:rXUC6gQ+]

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

[0373 １３２人目の素数さん 2024/05/26(日) 08:07:06.94 ID:7TSndvVz]

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

[0374 １３２人目の素数さん 2024/05/28(火) 10:30:28.58 ID:a3dJh3ee]

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