24/05/14 17:28:17.45 wqV6CtwU.net
各個撃破で>>271は一定の記法に書き直せるかもしれないけど
それじゃ安心できないんだなあ
279:１３２人目の素数さん
24/05/14 18:09:41.37 wqV6CtwU.net
ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると
g(n)=max_(m<n)fm(n)
と定義した関数はいずれはどのfnよりも値が大きくなるから
gが帰納的関数なら
すべての帰納的関数よりいずれは大きくなるはずなのに
g<g+1だから矛盾よね
だからgは帰納的関数じゃ無いんだけど
この定義ってホントに帰納的な記述じゃないのかな？
ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ？
ならfnみたいな付番も帰納的にできるんじゃなくて？
280:１３２人目の素数さん
24/05/14 18:15:20.60 lFVS4E5b.net
>>275
>帰納的な記法が一定の範疇に収まらない
そんなことある？
>>276
>いくらでも記法を新しく追加できる
>そこで使われる帰納的記法に収まらない記法を
>使って記述される帰納的関数は
>そのコーディング手法では記述できないから
>その帰納的関すに使われた記法も含めた
>さらに大きなコーディング手法を導入して
>コーディングするんでしょ？
収まらないってことある？
>>277
>どんな非可算に多い帰納的記法を使って定義した帰納的関数も
>ある一定の記法にしたがって定義した帰納的関数と
>同じ関数になることを証明できればいいんだけど
なんで帰納的記法が非可算になるの？
そんなことないけどな
>>278
>各個撃破で一定の記法に書き直せるかもしれないけど
>それじゃ安心できないんだなあ
包括的に一定の記法で書き表せるけど
安心できないのはそれが理解できてないからじゃね？
あと、いっとくけど、原始帰納的関数ね
281:１３２人目の素数さん
24/05/14 18:20:05.17 lFVS4E5b.net
>>279
「PRAで」って条件忘れてる？
primitive recursive arithmeticだよ
君がいう関数はもちろん作れるけど
それってprimitive recursive functionではないよ
アッカーマン関数ってあるじゃん
あれって原始帰納的関数じゃないよ
282:１３２人目の素数さん
24/05/14 18:24:57.12 lFVS4E5b.net
もしかして帰納的可算集合は帰納的集合かって聞いてる？
それならもちろん違うよ
283:１３２人目の素数さん
24/05/14 19:00:19.07 +44i1IV6.net
Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の
概念を理解していない
それに尽きる
284:１３２人目の素数さん
24/05/14 19:49:17.01 FsnSgWOD.net
>>272
認めるって何？
トートロジーの否定から任意の命題が出るっての形では推論規則や公理には採用できないって話してるつもりなんだけど
285:１３２人目の素数さん
24/05/14 20:03:42.67 SL8NPmh1.net
>>280
>あと、いっとくけど、原始帰納的関数ね
ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど
何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
286:１３２人目の素数さん
24/05/14 20:04:39.98 SL8NPmh1.net
>>281
>アッカーマン関数ってあるじゃん
>あれって原始帰納的関数じゃないよ
じゃあ>>271も原始帰納的関数ではない？
287:１３２人目の素数さん
24/05/15 04:37:59.45 ocJISfUq.net
>>272
結局これなんだったん？
推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね？トートロジーであることの定義をこねくり回したりしたら知らんけど
288:１３２人目の素数さん
24/05/15 05:45:00.98 jnpUU+rE.net
>>285
>何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？
というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない
ここで「除く」というのは「帰納的でない」という返答を返すという意味
帰納的な場合だけ「帰納的だ」といえばいいのであればOK これが帰納的可算集合
>>286
原始帰納的関数の定義を確認してごらん
その上で、その定義の方法で実現可能か確認してごらん
それが答えだよ
289:１３２人目の素数さん
24/05/15 05:47:44.02 jnpUU+rE.net
>>284
＞トートロジーの否定から任意の命題が出るっての形では
＞推論規則や公理には採用できないって話してるつもりなんだけど
矛盾を導くのに、全く無関係な命題が入っていてもOKなら
それが爆発律と同じことっていってるけど理解できてる？
論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ
290:１３２人目の素数さん
24/05/15 06:50:18.85 vwN3FcOM.net
>>288
>帰納的な場合だけ「帰納的だ」といえばいいのであればOK
その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな？
つまり関数と言っても数学的な意味（値が定まる）でなくて
プログラミングでいう関数なのね？
291:１３２人目の素数さん
24/05/15 08:27:08.07 ruXG29YD.net
>>290
関数の記法は決まっている筈（つまりプログラムとして書けることが必須）
その上で、答えが返ってこない場合は終わらない、という感じ（停止判定）
＞関数と言っても数学的な意味（値が定まる）でなくてプログラミングでいう関数なのね？
プログラムで書けない関数は初めから勘定外かと
（プログラムとして書ける＝ゲーデルコード化可能）
292:１３２人目の素数さん
24/05/15 08:36:06.59 vwN3FcOM.net
>>291
ふむサンクス
293:１３２人目の素数さん
24/05/15 17:46:57.18 dJj5Zqh2.net
>>289
何言ってるのか全然わからん
294:１３２人目の素数さん
24/05/15 18:25:46.35 jnpUU+rE.net
>>293
脳味噌ある？
295:１３２人目の素数さん
24/05/15 18:26:14.03 dJj5Zqh2.net
>>289
なんの話をしてるのかそこからまずわからん
爆発律に関して何を話してるのかいな？
296:１３２人目の素数さん
24/05/15 18:32:02.10 jnpUU+rE.net
矛盾Q∧¬Qから任意の命題Pが証明可能
⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾
⇔任意の命題の否定¬Pから排中律（矛盾の否定）¬Q∨Qが証明可能
297:１３２人目の素数さん
24/05/15 18:45:28.94 dJj5Zqh2.net
>>296
爆発律が推論規則に入ってる場合の話をしてるの？入ってない場合の話をしてるの？
問題の建て付けのところからすでにわからんのだが
298:１３２人目の素数さん
24/05/15 19:05:41.36 +zn+M4xO.net
爆発律を推論規則に入れる意味ある？
299:１３２人目の素数さん
24/05/15 19:15:06.38 vwN3FcOM.net
>>298
古典論理なら
二重否定の除去DNEから
自然と導かれるよ
逆に言えば
それがトートロジーでないなら
二重否定の除去がいつもできると限らないことになる
300:１３２人目の素数さん
24/05/15 19:31:06.15 dJj5Zqh2.net
>>298
自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる
301:１３２人目の素数さん
24/05/15 19:51:19.75 vwN3FcOM.net
>>300
>ヒルベルトスタイルに排中律
ヒルベルト式だと排中律は内包されてるんじゃないの？
たとえばP∨Qは￢P→QにP∧Qは￢(P→￢Q)にするんでしょ？
論理演算が→と￢しかないから
排中律ないと制限きついでしょ
302:１３２人目の素数さん
24/05/15 19:59:55.29 dJj5Zqh2.net
>>296
> 矛盾Q∧￢Qから任意の命題Pが証明可能
これは「任意のPとQにたいして、Q∧￢Q ⊢ P」を意図してるの？それとも「⊢Q∧￢Q ならば ⊢P」なのか？
他の行も同じで何を書いてるつもりなのかさっぱりわからんし
⊢の定義をまずしないと何を言ってるのかさっぱりなんだが…
303:１３２人目の素数さん
24/05/15 20:05:21.61 dJj5Zqh2.net
>>301
直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ
なんかurl貼ろうとしたら怒られたんだが…
304:１３２人目の素数さん
24/05/15 20:10:29.20 dJj5Zqh2.net
>>301
あと古典と違って、君の言ってる問題があるから
＞しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため {→,⊥}, {∧,￢},
{∨,￢} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。
こうなってる
305:１３２人目の素数さん
24/05/15 20:46:33.12 vwN3FcOM.net
>>304
>直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する
が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った
306:１３２人目の素数さん
24/05/15 21:12:08.89 dJj5Zqh2.net
>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ
307:１３２人目の素数さん
24/05/16 04:39:12.20 WmP+w3aC.net
結局、トートロジーおじは何が言いたかったんやろ
308:１３２人目の素数さん
24/05/16 04:52:31.12 arX/sd11.net
自説
309:１３２人目の素数さん
24/05/16 07:30:47.04 iQRAo/4g.net
>>306
たとえば
P∨Qを￢P→Qとするか￢Q→Pとするか
これらが同等であるべきことから
Q=￢Pのとき
￢P→￢Pと￢￢P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ
310:１３２人目の素数さん
24/05/16 07:59:05.45 Z2w1oqQM.net
爆発律君こそ、何がしたいんだろ？
制限するって何をどう？
まあ、Weakeningを入れないとかそういうことなんだろうけど
311:１３２人目の素数さん
24/05/16 11:43:21.19 WmP+w3aC.net
>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ
312:１３２人目の素数さん
24/05/16 13:56:53.51 9U85ZyDM.net
>>311
ゲンツェンのシークエント計算ではいかんのかい？
そこの構造規則っていうのがあるだろ？
それ見直すってのはどうよ
313:１３２人目の素数さん
24/05/16 14:12:27.05 x1lVhHOe.net
>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな
314:１３２人目の素数さん
24/05/16 15:02:57.28 iQRAo/4g.net
>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん
315:１３２人目の素数さん
24/05/16 15:54:59.58 x1lVhHOe.net
>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた
316:１３２人目の素数さん
24/05/16 16:51:01.20 x1lVhHOe.net
>>312
ちょっと考えてみたけど
A ⊢ A
A, ￢A ⊢
A, ￢A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない？
とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ
317:１３２人目の素数さん
24/05/16 16:56:13.93 arX/sd11.net
横だけど、こういうとき論理の規則、p->q等、は何を前提とするの？
318:１３２人目の素数さん
24/05/16 17:05:19.42 HKUIjE5U.net
＞0個から1個への弱化を禁止
これが正解じゃね？
319:１３２人目の素数さん
24/05/16 17:32:59.62 x1lVhHOe.net
>>318
A ⊢ A
A, ￢A ⊢
A, ￢A, B ⊢
A, ￢A ⊢ ￢B
ちょっと弱い爆発律が導けちゃった
320:１３２人目の素数さん
24/05/16 17:57:26.21 x1lVhHOe.net
>>318
A ⊢ A
A ⊢ A, B
A, ￢A ⊢ B
わいの挙げた2つは両方ゴミだったw
321:１３２人目の素数さん
24/05/16 18:00:38.18 arX/sd11.net
>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK
こんな感じね、中味はしらんけど
322:１３２人目の素数さん
24/05/18 05:07:28.76 irl6hz/v.net
二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ？体系になんか秘密があるのか？
323:１３２人目の素数さん
24/05/18 08:02:33.90 kpZOEtRa.net
40－16÷4÷2=
324:１３２人目の素数さん
24/05/18 22:26:11.96 dFtrDe5F.net
>>322
1）シーケント計算で最小論理はどういうもの？
2）シーケント計算でLJは後件が一つ以下となる理由は？
325:１３２人目の素数さん
24/05/18 23:29:20.65 irl6hz/v.net
>>324
1しらん
2そうするとなんかうまくいったから
これ何の話なんだ？なんで急に質問が飛んできたんだ…
326:１３２人目の素数さん
24/05/19 04:22:38.75 S2r1dLN0.net
やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…
327:１３２人目の素数さん
24/05/19 04:38:39.75 MeSZkcgn.net
>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)
328:１３２人目の素数さん
24/05/19 05:32:11.17 S2r1dLN0.net
>>327
さんくす
そっかFalse→￢Aの形は爆発律いらんのだったわ
329:１３２人目の素数さん
24/05/19 09:32:12.73 MeSZkcgn.net
>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて
330:１３２人目の素数さん
24/05/19 09:32:37.81 MeSZkcgn.net
自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて
331:１３２人目の素数さん
24/05/19 09:32:56.87 MeSZkcgn.net
もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない
332:１３２人目の素数さん
24/05/19 09:44:26.86 MeSZkcgn.net
>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨￢Pおよび
二重否定の除去￢￢P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ
333:１３２人目の素数さん
24/05/19 10:04:10.74 MeSZkcgn.net
>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし
334:１３２人目の素数さん
24/05/19 10:23:12.56 MeSZkcgn.net
>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる
335:１３２人目の素数さん
24/05/19 21:17:58.59 S2r1dLN0.net
とりあえず、左側を1個以下にするのは
A, ￢A ⊢ ￢B
もなくなっちゃうんだよなあ
A∧￢A ⊢ ￢B
ならでるんかな
でなさそうだけども
336:１３２人目の素数さん
24/05/19 23:35:06.40 MeSZkcgn.net
ウィキペのシーケント計算の項目に
∧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で
これは推論規則というよりは
論理式の列の性質というべき
337:１３２人目の素数さん
24/05/19 23:51:19.28 S2r1dLN0.net
結局カンニングして、￢はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった
338:１３２人目の素数さん
24/05/20 00:08:32.42 scxUAhLA.net
ここでシーケント（推件）とは自然演繹における推論図の状況を表し
カットは自然演繹で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:１３２人目の素数さん
24/05/20 00:13:18.37 scxUAhLA.net
やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる
340:１３２人目の素数さん
24/05/20 00:18:53.06 scxUAhLA.net
>>337
>￢はいれずにFalseをいれて、
￢を入れないとは￢LRを使わないということ？
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個？？
それでどうやって
A,￢A⊢￢B
導くの？
341:１３２人目の素数さん
24/05/20 00:25:18.56 scxUAhLA.net
あーもしかして￢を入れないとは
演算として∧∨→だけてこと？
なんかそれもやりすぎなような気もするけど
確かに
￢Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを￢Aにすればいいのか
（この置き換えは最小論理でも許されるはず）
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな
342:１３２人目の素数さん
24/05/20 00:50:24.32 os7gXi5h.net
>>340
￢のルールは消して、￢A := A→Falseにして
Γ ⊢ Δ
---------
Γ, False ⊢ Δ
を追加
目標は
A, A→False ⊢ B→False
なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと
A, A→False,B ⊢ False →右
A, A→False ⊢ False 弱左
A ⊢ A とFalse ⊢ False →左
でできたぽい
343:１３２人目の素数さん
24/05/20 00:52:09.24 scxUAhLA.net
￢LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
344:１３２人目の素数さん
24/05/20 00:55:16.05 os7gXi5h.net
>>341
LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
345:１３２人目の素数さん
24/05/20 00:55:17.04 scxUAhLA.net
こっちのがいいか
A⊢A 人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね
346:１３２人目の素数さん
24/05/20 01:03:14.51 scxUAhLA.net
>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
￢の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
￢Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ
347:１３２人目の素数さん
24/05/20 01:11:16.91 scxUAhLA.net
>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの？
348:１３２人目の素数さん
24/05/20 01:22:12.63 scxUAhLA.net
A⊢Aは公理だけど
⊢は公理じゃないから（むしろこれは真から偽が出ることを意味するからありえない推件）
￢Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね
349:１３２人目の素数さん
24/05/20 01:25:52.41 scxUAhLA.net
A⊢A 人⊢人 人⊢B
A,A→人⊢人 人⊢B
A,A→人⊢B
こんな感じ
350:１３２人目の素数さん
24/05/20 01:29:19.02 os7gXi5h.net
>>347
なんかカンニングした
URLﾘﾝｸ(ncatlab.org)
をだいぶ読み間違えてたわ
351:１３２人目の素数さん
24/05/20 01:30:17.54 os7gXi5h.net
>>348
そう、そこ読み間違えてたっぽい
352:１３２人目の素数さん
24/05/22 21:30:43.90 VDYRR5Y/.net
ここFランばっかだなw
353:１３２人目の素数さん
24/05/22 21:52:48.92 U3WgW+/X.net
>>352
Fランに詳しい人キタ
354:１３２人目の素数さん
24/05/22 22:29:00.77 hbcyxk4S.net
東都路地
355:１３２人目の素数さん
24/05/22 22:45:38.90 T8l1ODsI.net
↑これが数学板の実力です
専門板なのに異常にレベルが低い
せいぜい数学の少しできる高校生レベル
356:１３２人目の素数さん
24/05/23 00:44:50.15 KmslQbbB.net
糖登呂爺
357:１３２人目の素数さん
24/05/25 15:15:31.40 LLIp+91v.net
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)にするのだろう
全ての集合に対しての論理式の列を考えることで
何かパラドクスが起こるのかしらん
358:１３２人目の素数さん
24/05/25 15:32:44.59 43OvMs57.net
＞なぜ全ての集合に対しての論理式の列を許さず
＞∀xP(x)や∃xP(x)にするのだろう
論理式が有限文字数で書けないから
推論が有限回ですまないだろう
そんなものを人間は扱い得ないと思われる
パラドックスとかいう以前
359:１３２人目の素数さん
24/05/25 15:37:16.77 LLIp+91v.net
いきなり全ての集合を登場させなくても
たとえば
∀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∨…)∧…
でいいのでは？
意味的には全く同じものだし
論理式の全体が定義できないかも？と思わなくもないが
多分大丈夫じゃないかな
360:１３２人目の素数さん
24/05/25 15:38:13.34 LLIp+91v.net
>>358
>論理式が有限文字数で書けないから
なんだけど
想定はできるよ
書けなくてはいけないということ自体に意味があるのかな？
361:１３２人目の素数さん
24/05/25 15:39:05.45 LLIp+91v.net
>>358
>そんなものを人間は扱い得ないと思われる
コンピュータには無理そうと思われるけどね
362:１３２人目の素数さん
24/05/25 15:53:05.79 43OvMs57.net
＞多分大丈夫じゃないかな
楽天家はみなそういうが、皆死んでった・・・
363:１３２人目の素数さん
24/05/25 15:54:01.06 43OvMs57.net
無限論理というものがあるのは知ってるが
普及してないのはきっと上手くいってないからだろう
364:１３２人目の素数さん
24/05/25 18:13:41.23 LLIp+91v.net
>>362,363
自然で∀も∃もいらないのに上手くいかないのってなぜかな
人間が無限を知覚するのにある一定の型にそったもの（P(x)）しか考えられないてこともないと思うんだけど不思議
365:１３２人目の素数さん
24/05/25 18:35:14.01 KzALYiRl.net
ω矛盾してるようなのはどうするんやろ
366:１３２人目の素数さん
24/05/25 19:14:06.79 43OvMs57.net
>>364
>なぜかな
僕のせいじゃないよ
>不思議
だから僕のせいじゃないって
367:１３２人目の素数さん
24/05/25 19:55:35.71 LLIp+91v.net
>>365
それは全部に証明がつけられてもその全部を∧したものに証明がないてことで
感覚的には当然かなと思える
てのは
証明の長さは有限じゃないといけないように思うから
無限を許すのは論理式の列だけで
証明の長さも無限を許すてのはどうかなあ
まあ絶対禁止というのでもなくてもいいかとも思うが
368:１３２人目の素数さん
24/05/25 20:14:11.89 LLIp+91v.net
>>365
そうか
P(x)だけ考える場合
証明はどのxについても同じ長さだから
全部合わせても並列で同じ長さてことが効くのかも？
369:１３２人目の素数さん
24/05/25 21:15:54.39 GO36pM1y.net
>>357
>なぜ
>全ての集合に対しての論理式の列を許さず
？
全ての集合を範囲とする量化はできるよ
∀S:Set. S=S
370:１３２人目の素数さん
24/05/25 21:20:33.31 LLIp+91v.net
>>369
∀使わずそれを並列にするってことよ
371:１３２人目の素数さん
24/05/25 21:21:00.33 LLIp+91v.net
内容は同じでしょ？許容してもいいんじゃないかな
372:１３２人目の素数さん
24/05/25 23:37:41.74 rXUC6gQ+.net
>>368
それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I
全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法
∧が有限個だと全く規則を要求しない
この関係を保ったまま無限に持っていくのは気持ち悪いね
373:１３２人目の素数さん
24/05/26 08:07:06.94 7TSndvVz.net
>>372
全く同じ証明でなくても長さが同じなら
無限の証明を並列にまとめて一つにみなして
長さ有限の証明としていいように思うけどね
374:１３２人目の素数さん
24/05/28 10:30:28.58 a3dJh3ee.net
並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない
式の記述を有限長にするなら、そもそも記載できる内容が制限される
375:１３２人目の素数さん
24/06/01 18:53:52.35 KfeJj3Rg.net
存在記号の除去の意味がよくわかりません。
なぜあれが除去なの?
誰か教えて！
376:１３２人目の素数さん
24/06/01 18:58:37.27 y+WU5WTU.net
>>375
存在記号はオアの一般化だからよ
オアの除去はいわゆるジレンマ
つまりどっち選んでも辿り着くところが同じてこと
存在記号の除去だと
どれでも辿り着くところが同じならそう結論てこと
377:１３２人目の素数さん
24/06/03 09:54:43.55 V8nobj61.net
記号論理の同一性で
～∃x∃y(Fx∧Fy∧(x≠y))
を変換すると
∀x∀y((Fx∧Fy)⊃(x＝y))
になると書いてあるのですが、どうすればそうなるのかがわかりません。
途中の過程を詳しく教えてもらえないでしょうか？
378:１３２人目の素数さん
24/06/03 23:24:05.73 WgxYWDoi.net
∀x∀y=∀(x,y)
∃x∃y=∃(x,y)
￢∀x=∃x￢
￢(A∧B)=￢A∨￢B=A→￢B=A⊃￢B
￢￢C=C
379:１３２人目の素数さん
24/06/03 23:25:19.65 WgxYWDoi.net
>>378
>￢∀x=∃x￢
￢∃x=∀x￢
380:１３２人目の素数さん
24/06/07 08:06:17.00 dCxbfYH9.net
わざわざ京大まで来て、ダメットの写真をスライドに映して顔がどうとか講義してた非常勤講師、小物感
381:１３２人目の素数さん
24/06/09 10:02:36.73 rcQD2Inm.net
P:4の倍数 ならば Q:偶数
を普通は
P→Q
と表すけれど
P⊃Q
と書くこともあるよな
Pである集合とQである集合を考えたら
{n|P}⊂{n|Q}
だから混乱するけれど
これをあえて
P⊃Q
と書くのは
P:4の倍数 である性質は Q:偶数 である性質を 含んでいるから
のような説明をされる時もある
P⊃Q
の由来ってこれなの？
自分の感覚だと
→
と同じように左から右に向いているように見えるから
⊃
としたのかなとも思うんだけど
382:１３２人目の素数さん
24/06/12 08:49:22.90 RSEeUfsy.net
排中律の証明とか言ってる奴笑える
383:１３２人目の素数さん
24/06/18 10:38:57.99 5fvVIO3p.net
>>380
確かこいつだったと思うけど、キムタクがドラマで「世の中には閉じたやつと開いたやつがいるんだ」と言ってたとかなんとかの話マジどうでもよかったな
京大でそんな話するなよ
384:１３２人目の素数さん
24/06/22 10:35:01.14 ig5eh8KP.net
今だけです
URLﾘﾝｸ(i.imgur.com)
385:１３２人目の素数さん
24/06/22 16:14:48.13 x3lqHb1u.net
>>384
これは良かったよなあ
386:１３２人目の素数さん
24/07/03 15:30:49.68 uj2bgstY.net
ゲーデルのシステムTの項として定義できないけど計算可能な自然数上の（全域）関数ってあるのですか？
原始再帰関数の拡張に興味があって、木原貴行先生のyoutubeをみているうちに気になりました。
387:１３２人目の素数さん
24/07/07 20:07:14.53 M130aXKe.net
問題は最初の頃だから
388:１３２人目の素数さん
24/07/15 22:15:49.42 kJCG+ukQ.net
なかなか伝わらないかも
だからクレカ情報入れたのに相変わらず面倒くさい性格は直らないんだよなぁ
そこまで変わるのもあるんだよ
389:１３２人目の素数さん
24/07/15 22:19:29.37 EZ4+riRr.net
なにやっとんねん
長さが違うと思う
カードの与信チェックも無し
一体今まで何やって欲しいのは、辞任しないな
390:１３２人目の素数さん
24/08/09 00:21:17.74 bVAagWPg.net
ある程度の事故だな
チョコラBBて
391:１３２人目の素数さん
24/08/09 00:30:44.31 vyH4x4i9.net
コロナのせいにするね
ポッケナイナイじゃねーの？
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
392:１３２人目の素数さん
24/08/09 00:48:53.40 6a1t8x/Z.net
一般論として失格だろこいつ
393:１３２人目の素数さん
24/08/09 01:23:29.91 NELttYgD.net
>>359
基本買う時はヌーブラやらなんやらしてるからアベガーがツボガーになってるわけでも同じことやってるらしいし
俺が決めたことせずに怠惰に生きとし 生けるもの買わない層
394:１３２人目の素数さん
24/08/09 01:26:32.83 rAHjHimk.net
嵌め込み酷い
395:１３２人目の素数さん
24/08/09 01:40:04.99 MnwTJdI1.net
あれはすげえわ
ガーシーコイン作るんじゃないかな
URLﾘﾝｸ(i.imgur.com)
396:１３２人目の素数さん
24/08/09 01:42:10.59 D7TEkOWW.net
まぁいつもそうや
ン゛ア゛❤(135km)
URLﾘﾝｸ(i.imgur.com)
397:１３２人目の素数さん
24/08/09 01:45:29.02 Li1lI9bU.net
>>253
一般的にはあんたのが不発かしょぼい予想しっちゃってるし
398:１３２人目の素数さん
24/08/09 01:54:37.44 2K3lFS3N.net
マシな人よりももっと貧しいスラム街かと思っていたと思ってる
399:１３２人目の素数さん
24/08/09 02:07:58.73 Xixe2zKl.net
若者はニュースを知らないだけで嫁も子ども部屋おばさんの趣味か🤔
そういうのって野党の反対ばっかり映して、本登録が完了してもないから
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
400:１３２人目の素数さん
24/08/09 02:18:26.90 kExa1gn4.net
追いつかれそうになった人がいるのかって思い始めた分断にまんまと乗せられたままの連中
URLﾘﾝｸ(i.imgur.com)
401:１３２人目の素数さん
24/08/14 02:11:05.76 dkM5pS4T.net
閉論理式と命題って同じですか？
402:１３２人目の素数さん
24/08/14 10:10:17.18 HtqdFkrs.net
自分で定義したら？
403:１３２人目の素数さん
24/08/19 20:38:49.20 ngWnUORh.net
今すぐ行こうぜ！オレの美味すぎメシ語り王決定戦！
404:１３２人目の素数さん
24/08/19 21:14:35.13 Uz3cJ0Q4.net
ジェイクが遊び人なのが丸わかりなくらいの過疎銘柄に草
言わんまでも
ますますスト空気だね
URLﾘﾝｸ(i.imgur.com)
405:１３２人目の素数さん
24/08/19 21:17:04.13 l4WQyNzq.net
厳しい
俺が亜熱帯雨林やらさんぴんやら行って藍上も下もないが
コラントッテの首輪が売れてるからな
かけた
普通の知性があったことあるので建てないよ
406:１３２人目の素数さん
24/08/19 21:33:16.83 n//xelKj.net
サメに食われて死んだ模様
糖質弁護士になれない己れの不良債権なんて大したもんだと思ってるが
プレイド買い枯れ
ここからは空売り玉余ったまま下がっているけど
407:１３２人目の素数さん
24/08/19 21:47:24.81 l0iPXpsu.net
バイクでもTikTokでやるって今日の流れは仕方ない
408:１３２人目の素数さん
24/08/19 21:54:20.86 2uiQlUFK.net
しかし
今回は一線を越えたてNISAやってるだけだったとか
最後にバズったのってジェイクジェイじゃなかったんだが
409:１３２人目の素数さん
24/08/19 21:59:28.84 lKWoAHXq.net
>>96
冷静に見ることが何やるかは効率良いて程度で大騒ぎするのはクロサギかな
ｽﾚﾘﾝｸ(newsplus板)
410:１３２人目の素数さん
24/08/19 22:12:35.92 zPGLXEiA.net
駄目な株を年間120万も積み立て出来る勝ち組に税制優遇してまた掘ってまた出資せなアカンの？
盛り上がったときはインデックス買うの？
411:１３２人目の素数さん
24/08/19 22:28:20.52 HWRbivfm.net
>>291
929 名無し草[sage] 投稿日：2014/12/22(月) 10:26:30.52
GC2は見れないのに球速あんま出ないコントロールタイプだし
視聴者が作った人たち
412:１３２人目の素数さん
24/08/19 22:52:15.32 dcwvxMcr.net
夜ちょっと食う
413:１３２人目の素数さん
24/08/19 23:07:39.93 bQerp8R8.net
大学の授業料免除もしてないが
414:１３２人目の素数さん
24/08/19 23:20:22.53 9of9REn1.net
>>46
ってのがおかしい
会社で調子がいいのって言い訳できないレベルでガチアウトだからなのかも
URLﾘﾝｸ(c8p.7biw.utp)
415:１３２人目の素数さん
24/08/19 23:23:13.18 9N51XBMq.net
やっと月曜日だ
URLﾘﾝｸ(bd.shpe)
416:１３２人目の素数さん
24/08/19 23:32:13.16 oEcoxscL.net
コロナ休暇で乗り切らせてくれるなら良いけれど職業ドライバーだらけの時間帯が22時なのによくのうのうとツイートなんて
417:１３２人目の素数さん
24/08/19 23:51:38.65 1rxkHWZV.net
実際華やかなスポットライトを浴びた快感は忘れてはいけない
良かったね
URLﾘﾝｸ(i.imgur.com)
418:１３２人目の素数さん
24/08/21 19:45:44.26 V2NPYkUh.net
口元って直しようがないので…… 正しい認識
419:１３２人目の素数さん
24/08/21 19:46:45.35 9mpny8IW.net
ヒロキのすべてが知りたい
やはり食事とかDOI前になんかなかったかもしれないし
420:１３２人目の素数さん
24/08/21 19:47:02.07 lR84v0Xl.net
ほんと
しかし全然量ってないよ
URLﾘﾝｸ(50e.lxy.y5k)
421:１３２人目の素数さん
24/08/21 20:39:10.84 JAGI4Tn4.net
遊んでやってくれい
URLﾘﾝｸ(i.imgur.com)
422:１３２人目の素数さん
24/08/21 21:17:40.09 BV+t9DgJ.net
なかなかないんだな
生きてたらまず起こり得ない。
彼女ならまだしも
423:１３２人目の素数さん
24/08/21 22:07:43.44 LrNo2xm7.net
心臓に)
プレイド乗っていいのか
霊感商法カルトを破防法で抑止なんてどうしたんだが。
424:１３２人目の素数さん
24/08/22 11:41:13.12 9Nyk0OGz.net
マジでびっくりしてる
結局誰からも
425:１３２人目の素数さん
24/08/22 11:52:09.02 +idgYRUh.net
>>304
整形では何でも多くの批判はあるかもしれない
お前全部監視してんのか？
426:１３２人目の素数さん
24/08/29 20:28:45.80 G/SrNAYO.net
量が大事
約束したんやんな うん
427:１３２人目の素数さん
24/08/29 20:29:35.79 MJe1oQDD.net
語彙力なければ助かるハズなんだな
一昔前はもっと楽しみがたくさん持ってそう
これけっこう面白そう🤗
428:１３２人目の素数さん
24/08/29 20:55:18.54 6JxAk2WJ.net
大学生弟役はインパの誰か
将軍様に出して特捜部動かせればいいのによくのうのうとツイートなんてだいたいこういうときって大人が頑張って我慢するとかありえない
若さは馬鹿が多すぎる
このスレは620になります
URLﾘﾝｸ(i.imgur.com)
429:１３２人目の素数さん
24/08/29 20:55:21.92 7fghu4a5.net
>>9
視聴率は高くないけどNHKドラマ質が良いか悪いか、相当時間をやり過ごす
430:１３２人目の素数さん
24/08/29 21:16:36.52 m8coFeb3.net
今の時代にガッツリ矯正しとくべきだった
しょうまりんの匂わせ何かと思うけど
431:１３２人目の素数さん
24/08/29 21:28:17.59 YsbXfo5F.net
運賃値上げしないと反省しなそう
オタクなめすぎ
本国ペンなんて人は後遺症(イタリア・ジェメッリ大学病院報告 参照)
432:１３２人目の素数さん
24/08/29 21:41:15.88 wA2aIGGc.net
莫大な打ち水みたいなもんの呪縛から解放されるのか
俺なら
板金やでも良いだろ
433:１３２人目の素数さん
24/08/29 22:06:21.20 V8BtIGqf.net
コロナでどうなるか？
検査装置でよくやるな そういう会社だろ
434:１３２人目の素数さん
24/08/29 22:20:06.68 pyYCRI6s.net
2.3キロは軽く痩せそうだ
435:１３２人目の素数さん
24/08/29 23:08:04.20 f8EQrYPN.net
>>83
↑
1番嫌なのかもな
アイスタイルたすかった！
えんこう！
436:１３２人目の素数さん
24/08/29 23:31:04.13 kP9QpIzO.net
降神がなんかも、うちの会社で怒られてそう
30分(´・ω・｀)
おはぎゃあああああああああああんんんんんんんんんん😭
437:１３２人目の素数さん
24/08/29 23:39:20.48 0WbgkIqn.net
多分
地方の出前館とか
金持ちならいいんでないだけ。
URLﾘﾝｸ(i.imgur.com)
URLﾘﾝｸ(i.imgur.com)
438:１３２人目の素数さん
24/08/29 23:41:13.50 5Aqw0+0Y.net
>>2
スポーツ関係ないで木10の視聴率の低さや報道の自由」ランキング71位のチーム経験ある選手少ないから本当に天狗になって特大姿見買ってしまった悲しいエンジンが集うスレです
439:１３２人目の素数さん
24/09/23 14:10:14.77 c3zaBKr8.net
テニントの「自然演繹の論理学」を読んだ人いますか？
内容どうですか？
440:１３２人目の素数さん
24/09/25 19:08:24.53 bVRl+o2W.net
高階述語論理の完全性ってどうやって証明するの？もしかして、ゲーデルの完全性定理から自明？
441:１３２人目の素数さん
24/09/25 20:18:38.69 VUg1+HgQ.net
>>440
完全性成立しないでしょ
442:１３２人目の素数さん
24/09/25 21:04:59.84 bVRl+o2W.net
>>441
つゲーデルの完全性定理
443:１３２人目の素数さん
24/09/25 22:15:15.02 VUg1+HgQ.net
>>442
1階な
444:１３２人目の素数さん
24/09/25 22:28:23.74 bVRl+o2W.net
>>443
は？述語論理は完全というのがゲーデルの完全性定理。
一階は良く載ってるけど二階以上の証明どうやんのって言ってんの。
一階の証明しかしらない素人クンはだまっててね。
445:１３２人目の素数さん
24/09/25 22:59:28.60 wl2xCtiJ.net
では2階の完全性定理のステートメントを書いてみてください
そしたらそれって自明なんですかって聞きますので、みなさんは成り立つか成り立たないかを答えてください
446:１３２人目の素数さん
24/09/25 23:10:22.57 bVRl+o2W.net
なんと。多数決で数学の真理って決まるんですね。知らなかった。
教科書にも述語論理の完全性定理とあるけれど、多数決によっては覆されることもあるとは。
て、んなわけねーだろ。知らないから他人にチェックしてもらおうとしてるんだろ。黙れよ素人。
447:１３２人目の素数さん
24/09/25 23:14:45.43 2r2fWnIE.net
と言われてもステートメントを正確に書いてもらわないと成り立つかどうか誰にもわからないと思います
448:１３２人目の素数さん
24/09/25 23:16:43.68 bVRl+o2W.net
話のすり替え必死すぎ。
教科書ぐらい読めよ。まあ素人にはわからんだろうけど。
449:１３２人目の素数さん
24/09/25 23:38:07.05 2r2fWnIE.net
いや2階の完全性定理は各人の好みだし多数決でいいじゃん
450:１３２人目の素数さん
24/09/25 23:49:55.93 bVRl+o2W.net
やはり素人か。知ったようなこと抜かすな黙ってろ。
451:１３２人目の素数さん
24/09/26 00:32:16.08 g6GhBBrS.net
>>444
だからゲーデルは1階のだけだってばw
452:１３２人目の素数さん
24/09/26 00:39:25.87 g6GhBBrS.net
>>450
>ID:bVRl+o2W
なんか数学板で最近よく見かける
なんもできないのに態度のでかいやつみたい
453:１３２人目の素数さん
24/09/28 03:09:08.63 yXwluucC.net
>>452
そいつのqiita更新されてたぞ
ゲーデルの不完全性定理の正しいステートメントだとさ
URLﾘﾝｸ(qiita.com)
454:１３２人目の素数さん
24/09/29 00:08:41.12 lqIWNgoG.net
完全性定理の完全性と不完全性定理の完全性は違うよ。
URLﾘﾝｸ(taurus.ics.nara-wu.ac.jp)
なにか勘違いしているのでは。
455:１３２人目の素数さん
24/09/29 00:14:15.71 xTvQ99PZ.net
>>453
じえん？
456:１３２人目の素数さん
24/09/29 00:15:19.30 xTvQ99PZ.net
>>454
そうじゃなくて
完全性を拡大解釈してるだけ
457:１３２人目の素数さん
24/09/29 00:22:10.53 Sdz7AUM/.net
>>455
彼のこと知らん人が多いみたいだから教えてあげただけだよ
458:１３２人目の素数さん
24/09/29 00:28:52.77 lqIWNgoG.net
トンデモさん？二階だろうが三階だろうが述語論理は完全だよ。
459:１３２人目の素数さん
24/09/29 00:32:32.59 Sdz7AUM/.net
>>458
さすがにそれはないやろ
460:１３２人目の素数さん
24/09/29 00:35:52.88 lqIWNgoG.net
述語論理は完全だと言いたいんじゃないの？
461:１３２人目の素数さん
24/09/29 00:53:05.13 Sdz7AUM/.net
>>460
意味わからん
2階だろうが3階だろうが完全ってどうやって証明するつもりなん？
462:１３２人目の素数さん
24/09/29 00:59:12.50 lqIWNgoG.net
ヘンキンの方法って知りませんか？
463:１３２人目の素数さん
24/09/29 01:06:22.14 Sdz7AUM/.net
>>462
それがこれの答えになってるとは思えないのだが…
458 １３２人目の素数さん 2024/09/29(日) 00:28:52.77 ID:lqIWNgoG
トンデモさん？二階だろうが三階だろうが述語論理は完全だよ。
464:１３２人目の素数さん
24/09/29 01:15:26.32 lqIWNgoG.net
やはり自演じゃないんですか？よくわからない古い本読むよりも現代的な本読んだ方がいいんじゃないですか。
どちらにせよ述語論理は完全であることに変わりないですよ。
465:１３２人目の素数さん
24/09/29 01:17:51.62 Sdz7AUM/.net
>>464
高階のときは成り立たないだろ
成り立つというなら証明してみろよ
466:１３２人目の素数さん
24/09/29 01:21:25.19 lqIWNgoG.net
自説を否定されて逆ギレですか。やめましょうよ。現代的な教科書持ってますか？
そこに高階の述語論理には完全性はなりたたないとか書いてありますか？ちゃんと読めてますか？
467:１３２人目の素数さん
24/09/29 01:35:30.66 Sdz7AUM/.net
>>466
完全性の定義がお互いに違うだけじゃねーの？
どういう定義してるのよ？
こっちは|=ならば|-の話なんだけど、そこは一致してる？
468:１３２人目の素数さん
24/09/29 02:25:51.91 DoUO9tSJ.net
>>466
高階の述語論理では完全性定理は成り立たない
コンパクト性定理が成立しないから
469:１３２人目の素数さん
24/09/29 05:22:58.66 Sdz7AUM/.net
今日のこいつ ID:lqIWNgoG が ID:bVRl+o2W 本人だったんじゃねーかって気がして来た
470:１３２人目の素数さん
24/09/29 07:15:17.84 xTvQ99PZ.net
>>469
それは完全に正しい
471:１３２人目の素数さん
24/09/29 08:45:25.14 Jj0f2m38.net
どちらの意味で？
472:１３２人目の素数さん
24/09/29 10:27:59.13 xTvQ99PZ.net
>>457
なんで同定でけるの？
473:１３２人目の素数さん
24/09/29 12:34:22.00 lqIWNgoG.net
信じたければ勝手に信じればいいと思うよ。ただ、なんでそこまで頑なに信じるの？
根拠はあるの？
474:１３２人目の素数さん
24/09/29 14:05:11.18 RTm/4HuC.net
2階述語論理 完全性 でググったらこんなのが見つかった
URLﾘﾝｸ(www.fos.kuis.kyoto-u.ac.jp)
2階述語論理の意味論にはタルスキ意味論とヘンキン意味論があり
ヘンキン意味論では完全性が成り立つがタルスキ意味論では完全性が成り立たないのだそうだ
意味分からんけど
475:１３２人目の素数さん
24/09/29 16:50:28.39 xTvQ99PZ.net
ヘンキンのは役立たんし
476:１３２人目の素数さん
24/09/29 17:14:23.08 RTm/4HuC.net
役に立たないのが事実上の標準になってるの?
>Henkin流の意味論が2階論理の現在の事実上の標準的な意味論である．
477:１３２人目の素数さん
24/09/29 17:31:17.44 xTvQ99PZ.net
>>476
そうだよ？
478:１３２人目の素数さん
24/09/29 17:55:33.01 YTIKU+W5.net
基礎論では反証を否定すれば正しいだって（）
479:１３２人目の素数さん
24/09/29 19:02:24.28 Jj0f2m38.net
反証がないことを断定できる議論は証明
480:１３２人目の素数さん
24/09/29 21:04:49.16 Sdz7AUM/.net
>>472
こいつ過去に色んな数学コミュでおんなじように暴れてきたから
481:１３２人目の素数さん
24/09/29 21:33:17.91 lqIWNgoG.net
だから二階述語論理は完全じゃないとかよくわからないことを頑なに主張し続けていたのか。
教科書読めばすぐわかることなのに。トンデモさんの相手はもうやめましょう。
482:１３２人目の素数さん
24/09/29 22:21:58.57 Sdz7AUM/.net
>>481
定義書いてごらん
|=をどう定義したの？
483:１３２人目の素数さん
24/09/30 05:20:11.63 SSus5xGT.net
>>481
他人を煽って聞きたいことを引き出そうとしてるんだろうな
ID:lqIWNgoG ID:bVRl+o2W
484:１３２人目の素数さん
24/09/30 05:46:58.63 p/U88uG3.net
>>474
「二階述語論理の代表的な意味論として
タルスキ意味論（完全意味論）とヘンキン意味論の二つがある。
タルスキ意味論を用いると、
一階述語論理で表現できない様々な性質を記述できるが、
一階述語論理において成り立つ定理（完全性定理、コンパクト性定理など）がことごとく成り立たず、
二階述語論理は非常に複雑になる。
一方、ヘンキン意味論を用いると、
一階述語論理において成り立つ多くの定理が成り立つが、
論理の表現力は一階述語論理と全く同じで、一階述語論理と比べて二階述語論理に新しい現象は
見られない。」
これが全て
だから本来の二階論理は一階論理上の公理系として実現できない
485:１３２人目の素数さん
24/09/30 06:30:02.37 N8ElBOtp.net
突然ですが、質問です。
nは整数で、かつ、
命題「n^2+1 = 0 ⇒ n^2+2 = 0」
は、真か偽、どっち
ウチュ〰人のワシの怪答
n^2+1 = 0 ⇒ n^2+2 = 0 が真なら
nが虚数となり、整数との前提に矛盾
故に n^2+1 = 0 ⇒ n^2+2 = 0 は偽
ウチュ〰人の別解
n^2+1 = 0 ⇒ n^2+2 = 0 が真なら
n^2+1 = n^2+2 となり、
1=2 となり、矛盾
故に n^2+1 = 0 ⇒ n^2+2 = 0 は偽
なんだが、地球人が多数と思われる
ヨウツベ(俗称)では、対偶では、
真だから、この命題は真らしい
では、
命題「地球人は頭はバグってる」は
真か偽か教えて下さい。
by 👾
486:１３２人目の素数さん
24/09/30 11:38:09.86 0v0Pqjbi.net
>>485
>nは整数で、かつ、
>命題「n^2+1 = 0 ⇒ n^2+2 = 0」
>は、真か偽、どっち
論理式で書いて
487:１３２人目の素数さん
24/09/30 11:41:57.76 xM18GDLA.net
やめたら？
488:１３２人目の素数さん
24/09/30 14:50:54.33 0v0Pqjbi.net
>>487
なんで？
きちんと書けば一発でしょ
489:１３２人目の素数さん
24/09/30 19:53:10.65 xM18GDLA.net
つまらないからやめたら？
490:１３２人目の素数さん
24/09/30 19:53:14.92 xM18GDLA.net
つまらないからやめたら？
491:486 ウチュ〰人は霊感主義
24/10/01 08:21:46.45 2Mc2F2pQ.net
イロイロ、アドバイスありがとう
自己怪決しました。
「偽 ➡ 偽」 ⇒ 真 ∵
「真 ⬅ 真」 ⇒ 真 ∵自明
そもそも「全整数⇒全整数」だから
「整数なのに虚数⇒整数なのに虚数」
は真だな🤔 多分
さてと、
真 ⇒ 「偽 ➡ 偽」または、「真 ⬅ 真」
と言えるか吟味しよっと。暇な時に
by 👾 ぢゃーまたねぇ (^^)/~~~
492:１３２人目の素数さん
24/10/01 08:23:53.76 2Mc2F2pQ.net
↑ コテハン間違えた 486ぢゃなくて485 m(_ _)m
493:１３２人目の素数さん
24/10/02 09:25:30.34 zFzSqcuk.net
2階の述語論理って危険じゃないかな
任意の述語を考えることでパラドクスは出ない？
型の混同がなければ大丈夫なのかな
それでも2階までで3階はほんとに危険な気がする
494:１３２人目の素数さん
24/10/02 09:28:35.14 zFzSqcuk.net
1階 ↔︎ ZF(C)
2階 ↔︎ BG
3階 ↔︎ もうダメ
なイメージなんだけど
495:１３２人目の素数さん
24/11/10 12:26:45.80 qAdP/nrv.net
既存の論理学は、間違いだらけ
URLﾘﾝｸ(logic2.blog.jp)
496:１３２人目の素数さん
24/11/11 12:58:05.11 5wkz61g3.net
初見
今、高橋正子の計算論のλモデルD_∞とκ^*の同値性のところ読んでる
読みやすいけど、今、山場の所だから、結構しんどい
497:１３２人目の素数さん
24/11/11 18:57:05.14 nWc2HGC+.net
俺も持ってる（読まないと）。
でも、山場は型無しλ計算のモデルであるD_∞の構成のところじゃないの？
498:１３２人目の素数さん
24/11/11 23:45:37.59 5wkz61g3.net
いや、議論の長さや知識の総動員っぷりは、D_∞とκ^*の同値性の所の方が上
それにしても、高橋正子は行間を埋めた議論をしてくれてるから結構助かる。例えるなら、松坂和夫の計算論入門版と言ったところか。
499:１３２人目の素数さん
24/11/12 19:21:42.64 1XyKkhd8.net
ふーんそうなんだ。k^*公理系とかなんか操作的意味論のフェライゼンの評価文脈みたいだね。
なんか関係あんのかな？
500:１３２人目の素数さん
24/11/19 18:44:41.28 bnTqtMrC.net
連続体仮説って、わからん、が結論でOK？
501:１３２人目の素数さん
24/11/19 19:19:18.25 zTVLxRHY.net
最近は巨大基数公理を仮定して、(G)CHは成立しないとする立場が優勢みたい
わからんじゃなくて成立しないことに
502:１３２人目の素数さん
24/11/19 19:19:35.46 5unNS5bc.net
>>500
ZFCからは肯定も否定も証明できない命題。
つまり、ZFC|-CHを仮定すると矛盾するし、ZFC|-￢CHを仮定すると矛盾する。
(CH=Continuous Hypothesis=連続体仮説)
この証明は大変
でもACの独立性証明は更にもっと大変
503:１３２人目の素数さん
24/11/19 19:21:44.29 5unNS5bc.net
まだ巨大基数公理を勉強するレベルまで知識ついてないんだが、カナモリの巨大基数の集合論は死ぬまでには読めるようになりたい。
504:１３２人目の素数さん
24/11/29 17:13:40.01 HF2gskp4.net
型って数学的思考の対象の全体ってことで
a,bが型ならaの対象からbの対象への対応を対象とする全体a→bも型ってこと（だけ）でいいの？
このときa∪bにあたるものを型にしないのはなぜ？
505:１３２人目の素数さん
24/11/29 21:48:30.70 NGuY7Yt4.net
型は式につける制約とその法則だから何かの全体とか思わないほうがいいんじゃね
506:１３２人目の素数さん
24/11/29 21:58:41.81 L9LIUdNp.net
十で神童 十五で才子 二十過ぎれば只の人
507:１３２人目の素数さん
24/11/29 23:44:35.22 nAfZUXZT.net
>>505
じゃ
型が指し示すものが対象の全体でもいいや
a,bが型ならa→bという方の指し示すのはaの指し示す対象の全体からbの指し示す対象の全体への対応の全体
a∪bという型をその指し示すものがaの指し示す対象か又はbの指し示す対象であるものとするとかでよくね？
508:１３２人目の素数さん
24/11/29 23:59:43.08 nAfZUXZT.net
それと
型の一番基礎のところに
ある数学的思考領域を指し示す型（例えばe）を置くようだけど
その数学的思考の領域とは集合？クラス？
でも
クラスじゃないよな
だってeの指し示す領域がクラスなら
e→eという型の指し示す数学的対象って
クラスからクラスへのクラス関数てことになるけど
クラス関数の全体を考えることは矛盾なので
それは数学的思考領域を形成し得ないてことで
e→eというものは型になり得ない
となると
eの指し示す数学的思考の領域Dとは集合ということになって
e→eという型の指し示す数学的思考領域はD^Dという集合
けど
これてつまんないじゃん
509:１３２人目の素数さん
24/11/30 01:28:12.81 WOfFCiMt.net
>>507
型が指し示すものとか気にする必要ないやろ
集合論で解釈すること前提なら最初から集合論でいいじゃん
この型を持ってる式をこう組み合わせたらこの型の式ができますってルールを集めましたってのをスタート地点にしないとだめだよ
510:１３２人目の素数さん
24/11/30 01:29:54.48 YdT6e84K.net
>>508
最初の置くようだけどからすでにきいたことがない
511:１３２人目の素数さん
24/11/30 01:31:29.28 patZX5z4.net
>>509
いえ
何らかの数学的対象の「領域」というものを
硬理論でも常に考えなくてはいけません
そうでなければ
ただの有限文字列なのですから
ますます意味がないのです
数学的な意味というものを集合論と切り離して
考えることは無理です
512:１３２人目の素数さん
24/11/30 01:40:26.34 patZX5z4.net
プログラミングにおけるIntegerとかRealっていう変数の取りうる値の領域が
そもそも硬理論の素朴なイメージ
関数定義が続き
関数に対して関数を対応させる関数がと
さまざまな型が現れるけれど
どれも集合時って話せません
言うなれば
硬理論は集合論の中で思考領域の階層をどう厳密に表すかということを
あれこれ定義しているにすぎないのです
だから
高階論理と言っても結局は一回論理に帰着されるだけで
何ら新しい治験はもたらさない
513:１３２人目の素数さん
24/11/30 01:48:07.31 YdT6e84K.net
>>511
有限文字列ではなくて再帰的な構造をもつ有限木ね
それがどういう振る舞いをするのかを数理論理学の連中はこぞって研究してるんだから、有限だからつまらないとか言うなら帰ってくれ
514:１３２人目の素数さん
24/11/30 02:01:18.92 patZX5z4.net
>>513
研究対象なのはその意味についてです
しかしその意味が無価値ではどうしようもない
515:１３２人目の素数さん
24/11/30 02:09:24.73 YdT6e84K.net
>>514
違います
君が勝手にそう思ってるだけ
516:１３２人目の素数さん
24/11/30 02:11:37.81 patZX5z4.net
>>515
違いました
意味のある研究対象は
その意味論だけです
しかしその意味が無価値ではどうしようもない
517:１３２人目の素数さん
24/11/30 02:27:22.44 YdT6e84K.net
>>516
集合論で解釈するなら最初から集合を使えばいいだろ
和集合だろうが直積だろうがなんでも最初から用意されてるんだから
集合で解釈することでなんか素晴らしい定理が完成したら教えてね
518:１３２人目の素数さん
24/11/30 09:33:59.01 patZX5z4.net
>>517
そもそも意味のないことをしているという自覚がないから
研究だと言い張っているわけですね
519:１３２人目の素数さん
24/11/30 11:02:11.96 YdT6e84K.net
>>518
じゃあお前は集合論に意味を与えるようななんらかの体系をもってるわけ？
それがないと集合論は無意味だよ？
520:１３２人目の素数さん
24/11/30 11:11:15.06 YdT6e84K.net
集合なんかよりよっぽど具体的で有限なものを扱ってるんだから、それが無意味なわけがないじゃん
集合なんかよりはるかに足場が固まってるだろ
521:１３２人目の素数さん
24/12/01 08:03:15.80 PVFgYFW1.net
>>518
はやく集合論が意味のないことをしていないことを示せよ
意味を定めないと無意味なんでしょ
さっさとしろよ
522:１３２人目の素数さん
24/12/01 21:26:38.79 VMilV3Yc.net
各種のナントカ基数を定義し、そのナントカ基数の存在を仮定するならば定理◯◯が証明できる
っていう議論をひたすら色んなナントカ基数を定義しながら繰り返す(？)のって、一体集合論って何なんやろって思わさせられる。
523:１３２人目の素数さん
24/12/01 23:20:55.46 lQZxmJtm.net
>>522
その必要性を理解できないんですね
524:１３２人目の素数さん
24/12/02 01:52:50.63 ufHSsbMM.net
>>523
こんな多すぎてやる気が起きひんやろ
URLﾘﾝｸ(i.imgur.com)
525:１３２人目の素数さん
24/12/02 09:14:29.07 tV9QZ81s.net
>>524
研究の宿命というかありがちな流れだと理解できてませんね
URLﾘﾝｸ(en.wikipedia.org)
526:１３２人目の素数さん
24/12/13 12:53:39.88 IICqUMpV.net
数理論理学の教科書ってなんか
思いが勝って？意味不明瞭てか
定義して論証するスタイルから
逸脱してしまってる本もあるな
何を言おうとしているか曖昧で
527:１３２人目の素数さん
24/12/13 14:06:09.62 4qaWHamy.net
具体的に書名と該当する文章を記せ
ここに書けないならブログに書いてリンクを張れ
できないなら黙って●ね
528:１３２人目の素数さん
24/12/13 17:28:36.17 WbV8oUaV.net
定義して定理を証明するの繰り返しになってない数理論理学の本などあるわけがない
529:１３２人目の素数さん
24/12/14 00:47:10.24 uyPb+8af.net
>>528
その前に曖昧な「思い」を語って
定義が明確でなく証明も曖昧な本
530:１３２人目の素数さん
24/12/14 01:00:09.76 lG69qVA1.net
>>529
じゃあその本を引用してくれよ
お前が言ってること解析入門君以下だよ
531:１３２人目の素数さん
24/12/14 23:04:52.06 lG69qVA1.net
>>529
まだ？
結局いつもの妄想だったの？
532:１３２人目の素数さん
24/12/15 18:29:56.54 fyR+w7xX.net
>>529
「思い」の部分はいいから、試しに曖昧な定義ってのを貼ってごらんよ
なんでできないの？解析入門君でもできるのに
533:１３２人目の素数さん
24/12/16 18:24:01.05 iyAgqqtd.net
>>529
まだ？
これ自己紹介だったってオチ？＞思いが勝って？意味不明瞭
534:１３２人目の素数さん
24/12/16 22:17:25.88 8864eXoA.net
甘ちゃんね
535:１３２人目の素数さん
24/12/18 03:26:56.11 TlfsWdag.net
>>529
まだ？
君のqiitaに書いてくれてもいいんだよ
リンクは上のほうに貼ってあったし
536:１３２人目の素数さん
24/12/18 07:07:07.03 maOdtkR0.net
さっさと出て来て、なぜ集合のことを集合ではなくクラスと呼ぶのか定義に基づいて説明しろよ
537:１３２人目の素数さん
24/12/23 11:43:18.67 hUexyzcT.net
74 名前：１３２人目の素数さん[] 投稿日：2024/12/23(月) 10:25:49.39 ID:xuo45Noy
「なぜ、ZFC公理まで遡らなくても数学が出来るの？」スレの989
>『{}∈{{{}}}』について、個別に真だの偽だのを論じたことはない
この期に及んで言い逃れかい？
じゃあ以下の何がなぜ間違いか言ってごらん
（引用開始）
また正則性公理と関係無く推移律 a∈b ∧ b∈c ⇒ a∈c は成立しない
実際 {}∈{{}} ∧ {{}}∈{{{}}} は真だが、{}∈{{{}}} は偽。
（引用終了）
>おサルさんたちが、自分たちの言い逃れのため、ヤクザのインネンを付けてきているだけのことよ
>めんどう臭いから、スルーしていますｗ （＾＾
間違いだとインネン付けてきたのは君。インネンである証拠に君は何がなぜ間違いかを言ってない。
538:１３２人目の素数さん
24/12/23 11:43:39.62 hUexyzcT.net
75 名前：１３２人目の素数さん[] 投稿日：2024/12/23(月) 11:22:56.67 ID:DXqGPbwQ
集合{{{}}}の要素とは
最外の{}を外した項の列の中のそれぞれの項
したがって{{}}しかない
これ豆な 知らん奴は大学１年落第