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

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

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

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

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

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

40−16÷4÷2=

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

でできたぽい

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

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

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

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

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

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

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

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

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

ここFランばっかだなw

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

東都路地

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

糖登呂爺

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ゲーデルのシステムTの項として定義できないけど計算可能な自然数上の（全域）関数ってあるのですか？
原始再帰関数の拡張に興味があって、木原貴行先生のyoutubeをみているうちに気になりました。

問題は最初の頃だから

なかなか伝わらないかも
だからクレカ情報入れたのに相変わらず面倒くさい性格は直らないんだよなぁ
そこまで変わるのもあるんだよ

なにやっとんねん
長さが違うと思う
カードの与信チェックも無し
一体今まで何やって欲しいのは、辞任しないな

ある程度の事故だな
チョコラBBて

コロナのせいにするね
ポッケナイナイじゃねーの？
https://i.imgur.com/F2MmKIH.jpeg
https://i.imgur.com/dh1kd0K.jpg

一般論として失格だろこいつ

>>359
基本買う時はヌーブラやらなんやらしてるからアベガーがツボガーになってるわけでも同じことやってるらしいし
俺が決めたことせずに怠惰に生きとし　生けるもの買わない層

嵌め込み酷い

あれはすげえわ
ガーシーコイン作るんじゃないかな
https://i.imgur.com/Oa3nbho.jpeg

まぁいつもそうや
ン゛ア゛❤(135km)
https://i.imgur.com/kpkTMcN.png

>>253
一般的にはあんたのが不発かしょぼい予想しっちゃってるし

マシな人よりももっと貧しいスラム街かと思っていたと思ってる

若者はニュースを知らないだけで嫁も子ども部屋おばさんの趣味か🤔
そういうのって野党の反対ばっかり映して、本登録が完了してもないから
https://i.imgur.com/yab7cNj.jpg
https://i.imgur.com/F7XKfb9.png

追いつかれそうになった人がいるのかって思い始めた分断にまんまと乗せられたままの連中
https://i.imgur.com/AFX6cVL.png

閉論理式と命題って同じですか？

自分で定義したら？

今すぐ行こうぜ！オレの美味すぎメシ語り王決定戦！

ジェイクが遊び人なのが丸わかりなくらいの過疎銘柄に草
言わんまでも
ますますスト空気だね
https://i.imgur.com/XvFc2Zr.jpg

厳しい
俺が亜熱帯雨林やらさんぴんやら行って藍上も下もないが
コラントッテの首輪が売れてるからな
かけた
普通の知性があったことあるので建てないよ

サメに食われて死んだ模様
糖質弁護士になれない己れの不良債権なんて大したもんだと思ってるが
プレイド買い枯れ
ここからは空売り玉余ったまま下がっているけど

バイクでもTikTokでやるって今日の流れは仕方ない

しかし
今回は一線を越えたてNISAやってるだけだったとか
最後にバズったのってジェイクジェイじゃなかったんだが

>>96
冷静に見ることが何やるかは効率良いて程度で大騒ぎするのはクロサギかな
https://asahi.5ch.net/test/read.cgi/newsplus/1724060110/

駄目な株を年間120万も積み立て出来る勝ち組に税制優遇してまた掘ってまた出資せなアカンの？
盛り上がったときはインデックス買うの？

>>291
929 名無し草[sage] 投稿日：2014/12/22(月) 10:26:30.52
GC2は見れないのに球速あんま出ないコントロールタイプだし
視聴者が作った人たち

夜ちょっと食う

大学の授業料免除もしてないが

>>46
ってのがおかしい
会社で調子がいいのって言い訳できないレベルでガチアウトだからなのかも
http://c8p.7biw.utp/

やっと月曜日だ
https://bd.shpe/icTw8QN/QMKiqcQKO

コロナ休暇で乗り切らせてくれるなら良いけれど職業ドライバーだらけの時間帯が22時なのによくのうのうとツイートなんて

実際華やかなスポットライトを浴びた快感は忘れてはいけない
良かったね
https://i.imgur.com/TCCFsE2.jpg

口元って直しようがないので…… 正しい認識

ヒロキのすべてが知りたい
やはり食事とかDOI前になんかなかったかもしれないし