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

**１３２人目の素数さん** · 2023/10/06(金) 22:38:03.74

数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
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/

**１３２人目の素数さん** · 2024/05/14(火) 16:52:03.82

>>274
それは単純な式なら分かるけどさ
複数の式で定義されている
しかもその複数の式に使われている
帰納的な記法が一定の範疇に収まらないのを
どうするのかなと

**１３２人目の素数さん** · 2024/05/14(火) 17:00:40.30

人間が見て帰納的だと分かる記述でも
いくらでも記法を新しく追加できるから
あるコーディング手法で定義された関数全体が加算だったとして
そこで使われる帰納的記法に収まらない記法を使って記述される帰納的関数は
そのコーディング手法では記述できないから
その帰納的関すに使われた記法も含めたさらに大きなコーディング手法を導入してコーディングするんでしょ？
でもまたその範疇に収まらないのが出てきて・・・・って終わらないんじゃないの？
可算集合の可算なcofinalな集合は可算でも
帰納的記法はいくらでもつまり非可算でもあり得るんじゃ無い？

**１３２人目の素数さん** · 2024/05/14(火) 17:26:47.26

その困難を避けるには
どんな非可算に多い帰納的記法を使って定義した帰納的関数も
ある一定の記法にしたがって定義した帰納的関数と同じ関数になることを証明できればいいんだけど
はてさてソレ可能なのかしらん
だって人間の想像力は「無限大」で>>271みたいなへんてこな記述だって思いつくわけでしょ

**１３２人目の素数さん** · 2024/05/14(火) 17:28:17.45

各個撃破で>>271は一定の記法に書き直せるかもしれないけど
それじゃ安心できないんだなあ

**１３２人目の素数さん** · 2024/05/14(火) 18:09:41.37

ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると
g(n)=max_(m<n)fm(n)
と定義した関数はいずれはどのfnよりも値が大きくなるから
gが帰納的関数なら
すべての帰納的関数よりいずれは大きくなるはずなのに
g<g+1だから矛盾よね
だからgは帰納的関数じゃ無いんだけど
この定義ってホントに帰納的な記述じゃないのかな？
ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ？
ならfnみたいな付番も帰納的にできるんじゃなくて？

**１３２人目の素数さん** · 2024/05/14(火) 18:15:20.60

>>275
>帰納的な記法が一定の範疇に収まらない
そんなことある？

>>276
>いくらでも記法を新しく追加できる
>そこで使われる帰納的記法に収まらない記法を
>使って記述される帰納的関数は
>そのコーディング手法では記述できないから
>その帰納的関すに使われた記法も含めた
>さらに大きなコーディング手法を導入して
>コーディングするんでしょ？
収まらないってことある？

>>277
>どんな非可算に多い帰納的記法を使って定義した帰納的関数も
>ある一定の記法にしたがって定義した帰納的関数と
>同じ関数になることを証明できればいいんだけど
なんで帰納的記法が非可算になるの？
そんなことないけどな

>>278
>各個撃破で一定の記法に書き直せるかもしれないけど
>それじゃ安心できないんだなあ
包括的に一定の記法で書き表せるけど
安心できないのはそれが理解できてないからじゃね？

あと、いっとくけど、原始帰納的関数ね

**１３２人目の素数さん** · 2024/05/14(火) 18:20:05.17

>>279
「PRAで」って条件忘れてる？
primitive recursive arithmeticだよ

君がいう関数はもちろん作れるけど
それってprimitive recursive functionではないよ

アッカーマン関数ってあるじゃん
あれって原始帰納的関数じゃないよ

**１３２人目の素数さん** · 2024/05/14(火) 18:24:57.12

もしかして帰納的可算集合は帰納的集合かって聞いてる？
それならもちろん違うよ

**１３２人目の素数さん** · 2024/05/14(火) 19:00:19.07

Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の
概念を理解していない
それに尽きる

**１３２人目の素数さん** · 2024/05/14(火) 19:49:17.01

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

**１３２人目の素数さん** · 2024/05/14(火) 20:03:42.67

>>280
>あと、いっとくけど、原始帰納的関数ね
ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど
何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？

**１３２人目の素数さん** · 2024/05/14(火) 20:04:39.98

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

**１３２人目の素数さん** · 2024/05/15(水) 04:37:59.45

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

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

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

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

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

**１３２人目の素数さん** · 2024/05/15(水) 05:47:44.02

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

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

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

**１３２人目の素数さん** · 2024/05/15(水) 06:50:18.85

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

**１３２人目の素数さん** · 2024/05/15(水) 08:27:08.07

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

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

**１３２人目の素数さん** · 2024/05/15(水) 08:36:06.59

>>291
ふむサンクス

**１３２人目の素数さん** · 2024/05/15(水) 17:46:57.18

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

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

>>293
脳味噌ある？

**１３２人目の素数さん** · 2024/05/15(水) 18:26:14.03

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

**１３２人目の素数さん** · 2024/05/15(水) 18:32:02.10

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

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

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

**１３２人目の素数さん** · 2024/05/15(水) 19:05:41.36

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

**１３２人目の素数さん** · 2024/05/15(水) 19:15:06.38

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

**１３２人目の素数さん** · 2024/05/15(水) 19:31:06.15

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

**１３２人目の素数さん** · 2024/05/15(水) 19:51:19.75

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

**１３２人目の素数さん** · 2024/05/15(水) 19:59:55.29

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

**１３２人目の素数さん** · 2024/05/15(水) 20:05:21.61

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

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

**１３２人目の素数さん** · 2024/05/15(水) 20:10:29.20

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

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

こうなってる

**１３２人目の素数さん** · 2024/05/15(水) 20:46:33.12

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

**１３２人目の素数さん** · 2024/05/15(水) 21:12:08.89

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

**１３２人目の素数さん** · 2024/05/16(木) 04:39:12.20

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

**１３２人目の素数さん** · 2024/05/16(木) 04:52:31.12

自説

**１３２人目の素数さん** · 2024/05/16(木) 07:30:47.04

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

**１３２人目の素数さん** · 2024/05/16(木) 07:59:05.45

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

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

**１３２人目の素数さん** · 2024/05/16(木) 11:43:21.19

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

**１３２人目の素数さん** · 2024/05/16(木) 13:56:53.51

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

**１３２人目の素数さん** · 2024/05/16(木) 14:12:27.05

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

**１３２人目の素数さん** · 2024/05/16(木) 15:02:57.28

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

**１３２人目の素数さん** · 2024/05/16(木) 15:54:59.58

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

**１３２人目の素数さん** · 2024/05/16(木) 16:51:01.20

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

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

**１３２人目の素数さん** · 2024/05/16(木) 16:56:13.93

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

**１３２人目の素数さん** · 2024/05/16(木) 17:05:19.42

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

これが正解じゃね？

**１３２人目の素数さん** · 2024/05/16(木) 17:32:59.62

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

**１３２人目の素数さん** · 2024/05/16(木) 17:57:26.21

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

**１３２人目の素数さん** · 2024/05/16(木) 18:00:38.18

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

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

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

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

**１３２人目の素数さん** · 2024/05/18(土) 08:02:33.90

40－16÷4÷2=

**１３２人目の素数さん** · 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

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