数学基礎論・数理論理学　その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/12(日) 07:11:53.14

全ての🎁の中に🍎🍎🍎🍎🍎　ある。
そして🎁🎁🎁だ。🍎はいくつあるかというと
地球人は、3+3+3+3+3って計算するのかな❓
ポクは、5+5+5で計算します。ピミ達はどっちで計算するの❓

**１３２人目の素数さん** · 2024/05/12(日) 08:09:15.62

🎁🎁🎁からそれぞれ１コ🍎を取り出すなら3+3+3+3+3ですが何か？

**１３２人目の素数さん** · 2024/05/12(日) 13:33:26.66

直観主義論理で西村巌という人が重要な仕事をしているらしい
ネットで調べてみても岐阜大にいたこと以外何の情報もない

**１３２人目の素数さん** · 2024/05/13(月) 08:48:36.38

>かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる

0)値が同じなら式も同じ(式に意味はない)
1)定義はない (半環など未定義演算
2)アレイ図を数える (直積濃度
3) (いくつ分)x (ひとつ分)の両方が成立
4) (いくつ分)x (ひとつ分)との不定状態

やっぱりこいつ真性の馬鹿なんだな

**１３２人目の素数さん** · 2024/05/13(月) 09:22:13.78

>>247　レスバしたい人を相手すると時間空費するからやめとき

**１３２人目の素数さん** · 2024/05/13(月) 11:36:06.03

論理学において、「矛盾」の扱いが雑なように感じる。
数理論理学では「矛盾」をどう扱っているのだろう。
単純に排除されるべきものとして扱われているのだろうか、
という疑問。
矛盾は数学的対象なのか？

**１３２人目の素数さん** · 2024/05/13(月) 11:47:53.15

Pと￢Pの両方が導かれることを矛盾という
矛盾からはいかなる命題も導かれることになっている
これは空集合がいかなる集合の部分集合でもあることに対応している

**１３２人目の素数さん** · 2024/05/13(月) 14:55:09.67

ありがとう

**１３２人目の素数さん** · 2024/05/13(月) 18:57:51.61

Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
さらに、Pが自己同一性をもっていないとすれば、命題ではない。
それなのに爆発律があるかのように扱われているのは矛盾する。
爆発律は、妥当でない推論の例なのではないか？
爆発律が存在する（形式）論理体系なんてものは存在するのだろうか、という疑問。

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

＞Pと￢Pの両方が導かれる場合、排中律は成り立っていない。
実際は排中律もその否定も導かれる
＞爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
排中律も導かれるという意味では成り立つ
＞Pが自己同一性をもっていないとすれば、命題ではない。
自己同一性とは？意味がわからんが
＞それなのに爆発律があるかのように扱われているのは矛盾する。
だから矛盾してるっていってるんだが　記憶能力ゼロ？
＞爆発律は、妥当でない推論の例なのではないか？
そもそも矛盾してない場合、爆発律を使うことはない
＞爆発律が存在する（形式）論理体系なんてものは存在するのだろうか
いかなる命題を前提してもトートロジーは導ける
この対偶が、矛盾からいかなる命題も結論できるという爆発律

**１３２人目の素数さん** · 2024/05/13(月) 22:21:33.13

爆発率てのは人→Pのことだけど
これをそう呼ぶのはいかがなものか
P→Qとは単にモデルによる真理値割り当てにおいて
P≦Qであるということを言っているにすぎない
つまり人の真理値がボトムだという主張が人→Pの意味であり
人がどういうものであるべきかを意味している公理と言える
矛盾を定義しているという意味から
この公理は矛盾律と呼ばれるべきかと思うけどね

**１３２人目の素数さん** · 2024/05/13(月) 22:23:54.69

うーん、理解されなかったか。
Pがなんらかのタイプの矛盾であるとき、
P ⊢ Pは妥当なのか。

**１３２人目の素数さん** · 2024/05/13(月) 22:27:25.58

>>255
自分が理解していないから問題点を明確に書けない

**１３２人目の素数さん** · 2024/05/13(月) 22:34:02.21

>>252
>爆発律は、妥当でない推論の例なのではないか？
P∧￢P→人
は￢Eという推論規則を公理化したもので
矛盾律人→Pと合わせて
P∧￢Pは人と同等であることを言っている
（ここで同等とはお互いを導き合うこと
一般には同値と呼ばれるが自分は同等と呼びたい）
矛盾律を公理としない場合でも
人がある論理体系ならP∧￢P→人は公理もしくは推論規則にするだろうから
矛盾にさまざまな階層が生まれることになる
つまり人はもはやモデルによる真理値割り当てでボトムではなく
もっと低い真理値も容認されることになる

**１３２人目の素数さん** · 2024/05/13(月) 22:35:47.79

>>255
Pが矛盾でも何でもP→Pは成立するよ

**１３２人目の素数さん** · 2024/05/13(月) 23:01:13.68

P→Pが成立しないような矛盾は数理論理学では
扱えないということなら納得します。

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

大概の論理で
Pを矛盾として
P→Pは成立するよ
成立しないのは
PからQが導かれてもP→Qが成立しないとするような
相当つまらない論理だけでしょ

**１３２人目の素数さん** · 2024/05/13(月) 23:53:33.82

つまらない論理ではないと考えているから質問しています。
まあ、そこだけみて閉じてしまえばつまらない論理でしょう。
数学屋ではないのでちょっとやろうとしていることが違うのであしからず。
ありがとうございました。やくにたちました。

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

>>261
>つまらない論理ではないと考えている
PからQが論証できてもP→Qが成立しないような論理が
どうしてつまらなくないと思えるのかしれないけど
お好きにどうぞとしか

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

>いかなる命題を前提してもトートロジーは導ける
>この対偶が、矛盾からいかなる命題も結論できるという爆発律

矛盾からいかなる命題も結論できる、というのを否定するなら
いかなる命題を前提してもトートロジーが導ける、も否定される

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

トートロジーの否定は構文上はFalseではなくね？

**１３２人目の素数さん** · 2024/05/14(火) 10:07:36.20

矛盾はFalseだが

**１３２人目の素数さん** · 2024/05/14(火) 10:08:19.24

P⋁￢PがTrueなら￢P∧PはFalseだが？

**１３２人目の素数さん** · 2024/05/14(火) 11:27:24.56

￢(P∧￢P)とFalseは構文としては違うじゃん

**１３２人目の素数さん** · 2024/05/14(火) 11:41:52.90

爆発律って
P∧￢P→Q
か
False→Q
ぐらいしか流儀はないと思うのだが、
Pがトートロジーのとき
￢P→Q
なんて流儀は無理やろ

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

Pがトートロジーのときは￢PからFalseが導けるからFalse→Qから￢P→Qが云える

**１３２人目の素数さん** · 2024/05/14(火) 11:59:53.76

トートロジーかどうかを推論規則の前提にするわけにはいかんじゃろ

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

>>226
自然数の帰納的関数であるこれってどうコーディングされるの？

a,b,cは自然数
Xは0個以上の非負整数
a#bはb個のa

a{}0=a
a{}b=1+(a{}(b-1))
a{0}0=0
a{0}b=a{}(a{0}(b-1))
a{c}0=1
a{c}b=a{c-1}(a{c}(b-1))
g()=1{}1{}1
g(0)=g(){}1
g(a)=g(){g(a-1)}g()
G()=g(g(0){1}g())
G(0)=g(G())
G(a)=g(G(a-1))
G(0#c,0)=G(G()#c)
G(0#c,a)=G(G(0#c,a-1)#c)
G(X,b,0#c)=G(X,b-1,G()#c)
G(X,b,a)=G(X,b-1,G(X,b,a-1))
G(X,b,0#c,a)=G(X,b-1,G(X,b,0#c,a-1)#(c+1))
GG()=G(G()#G())
GG(0)=G(GG()#GG())
GG(a)=G(GG(a-1)#GG(a-1))

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

>>270
Pがトートロジー　⇔　￢Pから矛盾が導ける　は認めないの？　
認めないとして反例示せる？

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

>>270
そこまで書けるならできるじゃん　脳味噌あるだろ？

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

ヒント（というよりほぼ答え）
文字を数に置き換えてそこから文字列を数に置き換える方法を考える

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