数理論理学（数学基礎論） その13
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照）
前スレ
数学基礎論・数理論理学 その12
https://rio2016.5ch.net/test/read.cgi/math/1509638068/ 中高生の頃の俺なら、余裕で読解力()で東ロボくんに負ける自信あるけど、今は新井紀子より数理論理学を理解してるしな
何か具体的な成果とかあるんか？ 思うんだけど、東大ロボって単なる工学・情報技術の"つぎはぎ"なだけでしょ？
機械アームで紙をめくって、
紙をスキャンして書いてる内容を文字として認識して、
認識された文字の意味解釈をして適切な出力をして、
その出力に基づき、機械アームで鉛筆でマークする
これは順に見て、ロボット工学→なんとか工学→AI→ロボット工学ってな感じの”つぎはぎ”でしょ？
こんな東大ロボが東大入学出来るレベルまで実力あったとか言われた所で何も凄さを感じない >>724
どこが成果だ？
>>726さんが指摘している通り、様々な工学（情報も含め）技術のツギハギに過ぎない
そして本来なら、この東大ロボ計画で新たに開発されるべきだったAI技術の部分は何も新たなものを出せていない
その挙句に、新井の言い訳は「日本語の理解が難しい」だった
日本語処理・理解が不可欠なのは「現実の入試問題を解く」という課題設定の時点で明らかだったのに
その大前提の部分が「難しくて出来ませんでした」とは納税者を舐めるにも程がある
この東ロボの本来の研究課題はその次の段階、つまり日本語で書かれた問題（の情報）を適切なフォーマルな内部形式に変換した次の段階にあったのだ
そのフォーマルな内部形式として表現された問題を様々な知識を連携させることで如何にして速やかに解くか、という段階だよ
日本語の処理が難しかったです、というのは問題をフォーマルに変換するという本来の課題に至る前段階そのものがちゃんとできなかったということだ
こんなのを「大きな成果」と呼んで良いなら、何をやっても何もできなくても、「科研費による研究は全て大きな成果を産み出している」と言えてしまうぞ 新井紀子についてはスレチ（数理論理学の学者とは認められない）
専用スレがあるのでそちらでどうぞ 質問があります
ZFCのあるモデルが存在するとしても、一階述語論理を適当にエンコードし集合論の言語L∈をシミュレートして、その中でフォンノイマン宇宙Vというクラス(は正式には存在しないのでそれを表すL∈の論理式)がZFCのモデルであることは不完全性定理から証明できないですよね
「ZFCのモデルV」とは何者なのでしょうか？ >>728
> 問題意識のない奴には成果が見えない
そういう否定的で非構成的な表現による反論は何の意味もない
「超能力を信じない奴には超能力は使えない」と言ってるようなもの
成果があると主張する以上、肯定的で構成的な説明…つまり成果の内容を具体的な説明…を与える義務がある
成果の内容を具体的に説明しないのならば、成果があるという主張は偽（つまり単なるホラ）と判断される、これが世の中の常識だ >>726
そういう文章の自動認識すらやってない。
以前、東ロボくんが数学の問題を
Tarski-Seidenbergの量化子除去を使って解いたのが
ちょっと話題になってたけど、あれも示すべき式を
研究者が実閉体の理論の論理式として
書くまでやってあげて、それを解かせただけなので
まあ割と残念なチートではある。
記述式の解答にしたのも、人間が出力を読み取って
文章として起草して整えてるはずで、あれを
「機械が大学入試問題を解いた」
と言って宣伝するのは誇大広告にも程がある。
というか、そういう誇大広告が得意なのが
新井紀子という人なので。
数学としての実質で勝負してる夫とはえらい違い >>730
不完全性定理から出来ない、と言っているところでは
実際には完全性定理も使ってると思うけど、
そこで言っている「モデル」という言葉の意味と
V（つまり{x|x=x}）がZFCの（クラスとしての）
モデルであるという時の「モデル」という言葉の意味は
メタ数学的にちょっと違う。
そこら辺私も以前引っかかった事があってこのスレに
似たような事をこのスレに書いた事がある >>735
ご回答ありがとうございます
疑問が晴れずもう少しお付きあいいただければと思います
モデルとは一階述語論理で定義される領域と構造の対だと思っていたのですが、その例のどちらもこの定義ではないということなのでしょうか？
違いや、それが記述されてる本などでも構わないので教えていただけると有りがたいです >>736
クラスとしてのモデル M は、そもそも
∃M〜〜みたいな論理式を作る事も
（一階論理上のZFCでは）出来ないので。
メタ理論のレベルでの略記に過ぎないので。
Kunenのどっかには一応そこら辺のことは
書いてあります。2011年に出たKunenのSet Theoryなら
第一章の後ろの方か第二章の最初の方、
たぶんI.16 Models of Set Theoryのどこか。
和訳されてるKunenの本でもどこかに書いてあるとは
思いますが僕は読んでいません。
実は僕も2014年に数学基礎論サマースクールに向けて
勉強してた時に同じところで引っ掛かった記憶があって、
「数学基礎論・数理論理学スレ その14」の561辺りで
ほぼ同じ質問してるんですよね（笑） 集合論のモデルって
メタ的に考えて
普通の意味でのモデルみたいなモノと認識できるってだけでは？
たとえば順序数の全体Ordが順序数としての性質を持っているってメタ的には認識できるってのと同じような ZFCの上で普通に解釈すると、モデルというのは
ある集合mとその上の演算や述語の組になりますけど
Vはそういう意味でのモデルではないですよね
「VはZFCのモデルである」を一つの論理式で書く事自体
よく考えたら容易にはいかないですね
V自体は{x|x=x}という単なる記号列だとみなす立場も、
二階のZFCとかNBGとかMKみたいに或る実体だと
考える体系もありますが、いずれにしろ矛盾が
出てこないようにはなってるはずです。
ただ具体的にNBGとかMKとかでどうなってるかは、
ちょうどそれぞれの定式化が異なっている部分と
関係してくる上にあまりきちんとした文献に
アクセスするのも容易でないので
あまり真面目に考えた事ないです
Kunenの古い方の本の第一章の演習問題の
最後の方の問題がちょうどそこら辺に関する問題ですね >>737
それはそもそも一階述語論理では自由変数しか量化出来ないので、上の領域と構造の対としてのモデルでも同じではないでしょうか？
キューネンの集合論に関しては和訳版があるので後で読んでみます 自然数論の数項と自然数の違いがよく分からない
例えばωだと
1={φ}=suc(0)=｢1｣
ってなるよな？ 要するに1とかはメタ理論の自然数なんだけれども、ZFCのωとか古典二階PAでは区別がないが、
一階PAそのものを研究するメタ理論を限定しない立場では1とかと内部の数項を区別する必要があるんかな
ややこしいな numeralはただの記号列でしょ。
言葉によって名指されるものと、
ものを名指す言葉の関係。
命題と論理式の区別と同様かと。
閉項と定義可能元も適切に定数記号加えて
保存拡大すれば同様になる。 aとbの濃度が等しい事をa ⤄ bと表す事とすると、
ℝ ⤄ [0, 1) ⤄ 2進数列 ⤄ ℕ
推移律よりℝ ⤄ ℕ
実数と自然数の濃度が一緒になっちゃった。
どこがおかしい？ 2進数列 ⤄ 自然数列 ⤄ ℕ
これじゃダメかな？素因数分解列の一意性を使う。
以下自然数列とℕの対応付け
素数列をPとする
P(1)=2, P(2)=3, P(3)=5 ...
自然数nを素因数分解した列をF_nとする
F_600(1) = 3, F_10(2) = 1, F_10(3) = 2 ...
つまり、任意の自然数nに対し以下が成り立つ
n = Σ(m=0~∞)F_n(m)*P(m)
自然数nと素因数分解列F_nは1対1対応なので自然数列 ⤄ ℕ
なんか集合の濃度とかよく分からんくて頭おかしくなりそう
nからF_nの単射しか示せてへんなこれやと
考えたら一意なだけで一対一なんか全然示せんし
全射か逆の単射を示さへんと
でも数列が永遠に1とか続いってった時nが発散してまうわな
てかそりゃそうやろ当たり前やん
すまん自己解決や >>751
>自然数nを素因数分解した列をF_nとする
>F_600(1) = 3, F_10(2) = 1, F_10(3) = 2 ...
どんな定義よ ってか、N<2^N なんだから一々そんな回りくどい事しなくて良いだろ Xを任意の集合とするときYを「X∉X」を満たすXの集まり
Y＝{X|X∉X}
と定義する
つまりYは自分自身が自分自身に属さない集合全体の集まり
仮にYが集合だとしてY∈YとするとYは性質「Y∉Y」を満たさないといけないからY∉YとなりY∈Yであることに矛盾する
再びYが集合だとしてY∉YとするとYの定義から「Y∈Y」だからY∉Yと矛盾
いずれにしても矛盾が生じるからYは集合ではない
このような集合Yを考える背景には
「集合全体の集まり」
がある
Aを集合全体の集まりとすると
A∈A または A∉A
A∈Aとすると集まりYを排除する正則公理に反しA∉AとなるA全体の集まりYは集合にならない
A∈AであることはAが「物の集まりであること」に反する
A∉AとしてもこのようなAの集まりが集合にならない
集合全体の集まりは添え字付けられた集合族{S_λ|λ∈Λ}の共通部分
{x|∀λ∈Λ, x∈S_λ}
で添え字集合Λを空集合とした場合や圏を定義する際にも現れる
全ての集合の集まりAは
A∈A
を満たすがこれはAが物の集まりであることに反する
A∉Aとしてもこのような物Aの集まりが集合にならない
またAが集合になるとしたらAの部分集合全体の集まりPはP∈Aを満たさねばならぬがこれはA∈Pに反する
公理的集合論のZFC公理を学んでみるとおもしろいのでぜひ >>754
今まで何度も聴いてきたネタだな。
でもそれって毎回毎回自然言語で説明するからウザいよな
それって要するに
¬∃Y∀X(X∈Y⇔¬X∈X) は証明可能
ってだけに過ぎないのにな
こういう風に端的に言われたら、いざ証明しようとなったときに
∃Y∀X(X∈Y⇔¬X∈X)を仮定したとき
∀X(X∈Y⇔¬X∈X)だからXにYを代入して、
Y∈Y⇔¬Y∈Yであり
一方排中律により、Y∈Y∨¬Y∈Yであるから、
これら2式より矛盾が導かれる
よって¬∃Y∀X(X∈Y⇔¬X∈X)である
って感じに証明すればスッキリと分かり易いのにな >>755
> 一方排中律により、Y∈Y∨¬Y∈Yであるから、
無矛盾律に排中律いらんしょ？ 全ての集合の集合
という自然言語の概念を形式化するのは上手く行かないよねって話なんだから一階述語論理だけでは説明できないだろ
タルスキの真理的意味論における真理を説明するのに、Tスキーマだけ取り上げて形式化できないよねで終わらせるようなもの >>756
Y∈Y⇔¬Y∈Y
これだけからどうやって矛盾導くの？ >>757
＞＞全ての集合の集合という自然言語の概念を形式化する
ZFCではYを自由変数とする述語｢∀X(X∈Y)｣が対応してるんじゃ無いの？ 数学は部分集合しか扱えないということか
全体集合だと、全体の全体で形容矛盾になる 要素かどうか決められないと集合じゃないってだけだろ >>758
P P→¬P |- ¬P
P ¬P |- 人
P→¬P |- ¬P
¬P ¬P→P |- P
¬P P |- 人
以上より
P⇔¬P |- 人
だけど？ >>762
｢P→¬P |- ¬P｣が分からん
｢以上より｣が分からん >>764
ってか、｢P→¬P |- ¬P｣の主張そのものが排中律と同じやんけ
ってか>>762の演繹グダグダやろ？
どういう議論の流れになってんのか全く意味不明だわ >>764,765
まあよく考えてみたら？
じゃあもう少し間入れると
P P→¬P |- ¬P
P ¬P |- 人
P P→¬P |- 人
P→¬P |- ¬P
¬P ¬P→P |- P
¬P P |- 人
¬P ¬P→P |- 人
P⇔¬P |- 人
これでどう >>759
ZFCではそうなだけで公理系にはNBGとかもあるし、一階述語論理に限定する理由もない
それでもある程度困難が生じることはZFCだけでは語れないから自然言語で説明されてもしょうがない >>766
やっとどういう証明になってるか分かったけど、完全にお前の頭の中だけのことをメモ帳に書き殴って｢ハイ証明｣って他人に押しつけるタイプだな
カット規則使うにしても断りもないし、どのシーケントからどのシーケントに繋がってるかの説明もないし最悪のタイプ
何でお前みたいなクソ証明を読まされなきゃならんのだってイライラしてくるわ
で結局回り道みたいな議論した所で｢P→¬P |- ¬P｣の主張そのものが排中律と同じ。
>>766の証明は始式から推論規則を厳格に一々やってるわけでもないし、"何の意味も無い" 分けないと分からんかも？
P P→¬P |- ¬P
P ¬P |- 人
P P→¬P |- 人
P→¬P |- ¬P
¬P ¬P→P |- P
¬P P |- 人
¬P ¬P→P |- 人
P⇔¬P |- 人 >>769
>で結局回り道みたいな議論した所で｢P→¬P |- ¬P｣の主張そのものが排中律と同じ。
P P→¬P |- ¬P
P ¬P |- 人
P P→¬P |- 人
P→¬P |- ¬P
どこに排中律使ってる？ 排中律はP∨¬Pが真つまり前提なしに使って良いという主張で
>>771のどこにそれが使われてるの？
二重否定の除去¬¬P|-Pも使ってないのに >>769
>で結局回り道みたいな議論した所で｢P→¬P |- ¬P｣の主張そのものが排中律と同じ。
面白いから
P→¬P |- ¬P
から
|- P∨¬P
導いてごらんよ >>ID:YSRNi+IZ
で、結局｢無矛盾律に排中律いらんしょ？｣っていお前のレスに戻ってくるけど、
これはお前が無矛盾律からシーケントをスタートさせてるだけの話やろ
>>755で言ってるZFCでの議論において一々形式的体系をシーケントで考えて無矛盾律を使う所からスタートするかどうかはどうでもいいこと
あぁ〜他人の何の説明も無いクソな計算メモを見せられて一々どういう思考過程なのかなんでこっちが補ってあげなきゃいけないんだよ
死ねよ
マジでイライラする >>770
はぁ〜〜〜お前通じてないな
んじゃ、始式から始めて各行に使った推論規則書いてみ 同じと言うならできるんでしょ？
ちなみに
|- P∨¬P
から
P→¬P |- ¬P
は
|- P∨¬P
P P→¬P |- ¬P
¬P P→¬P |- ¬P
P→¬P |- ¬P
かな >>774
>これはお前が無矛盾律からシーケントをスタートさせてるだけの話やろ
はぁ
無矛盾律は認めないという立場なの？
これは最小論理の
P ¬P |- 人
なんだけど
使わないのはキビシイなぁw お前クソアスペ脳だからシンプルに応えてやるわ
Y∈Y⇔¬Y∈Yであり
一方排中律により、Y∈Y∨¬Y∈Yであるから、
これら2式より矛盾が導かれる
って議論にお前のアスペ脳が反応してるけど、どういう議論かというと
Y∈Y⇔¬Y∈Yであり (1)
一方排中律により、Y∈Y∨¬Y∈Yである。 (2)
Y∈Yならば(1)の→より¬Y∈Yで矛盾する
¬Y∈Yならば(1)の←よりY∈Yで矛盾する
従って(2)よりいづれの場合でも矛盾する
と言えばお前みたいなクソ証明をウダウダ言わなくても一瞬で終わるって事を>>755は言ってんだよ >>775
イライラしないで考えたらすぐわかるよ
それと>>773よろしく >>778
別にどうでも良いけど
普通P⇔¬Pが矛盾であることに排中律は使わないから
変に排中律にこだわる人かと思ったんだよ >>780
お前人に読んで貰いたいんならまず>>775の通りに書け。な？
それと、
＞＞別にどうでも良いけど
もうその時点でお前のアスペっぷりが現れてんの
＞＞普通P⇔¬Pが矛盾であることに排中律は使わないから
その証明に排中律を使わないゲンツェン流の体系での証明を与えるってのはお前のアスペ脳が勝手に言い始めたこと
分かってる？
＞＞変に排中律にこだわる人か
全く関係の無い文脈なのにお前が勝手に思い込んでシーケントの話を持ち出してんの
頭大丈夫か？ お前｢数学の本｣スレの"松坂君"レベルの人の話聞かないアスペッぷりだな
お前みたいな頭おかしい奴の相手するとマジでイライラする
割りとマジで普通に死ね >>781
変にめんどくさい人だな
俺は
>>758
>>>756
>Y∈Y⇔¬Y∈Y
>
>これだけからどうやって矛盾導くの？
と聞かれたから証明して見せただけ
P⇔¬P
が矛盾だってのは排中律要らないからさ ID:YSRNi+IZさん
おかしな人の相手をしない方がいいよ >>783
＞＞と聞かれたから証明して見せただけ
そもそも>>755では直観的な議論で証明してたから体系は明示してない
だから>>758の時点で俺が聞いてたのは直観的な議論での証明なんだよ
それをお前が"説明も無く"今まで土俵に上がってないシーケントを用いた話にしたからお前のシーケントの話につき合わざるを得なくなったんだろうが
で、今になっても体系も用いた推論規則も公理も説明無しなのがお前のアスペレス。 フィボナッチ数列の最初の2項を
2, 1 に置き換えた数列の項をリュカ数という
2, 1, 3, 4, 7, 11, 18, 29, 47, 76, 123, 199, 322, 521, 843,
1364, 2207, 3571, 5778, …
この数列の一般項は
Ln=((1+sqrt(5))/2)^n+((1-sqrt(5))/2)^n ついこの前から新井の｢数学基礎論｣を読み始めたんですけど、
Henkinの定理みたいなので一々言語Lを拡張するって議論が一瞬ややこしくなって面倒だわ 1階述語論理の完全性定理って証明法が複数種類あるけど、実際どれぐらいあるもんなのかな？
俺が見てきただけでも4パターンぐらいあるような気がする 普通順序数の和･積･冪って超限帰納法で定義すると思うんだけど、
Jechのだったっけ？、一旦和･積･冪に対応した整列集合を作ってから、その順序型としての順序数で和･積･冪を定義してたよな
この時の整列集合の見た目がゴチャゴチャしてるッぷりは目障りだった
何でこんな事するんだよ Kunenのset theoryもJechと同じ方法だしそっちの方が普通だと思われる
で、同じくset theoryでは後にクラス上の超限帰納法でも順序数の和などを定義できることを確認しているが、恐らくクラス上の超限帰納法の方が更にややこしいから後に回してるんだろう 冪はともかく、和と積は別に
ごちゃごちゃしてないと思うけど……
視覚的イメージをもって把握した方が、
結合法則とかが明らかだし
単に集合論に慣れてないだけだと思います Kunen二冊の和訳を担当した藤田さんが、公理的集合論の初歩からCHの独立性までの教科書を書いてるようですね
強制法は集合論で必要不可欠の知識ですし、それこそKunenのset theoryでは補えない現代的な内容や、より深い説明を期待したいところですね このスレの住民なら｢数学基礎論講義―不完全性定理とその発展｣これに目を通したことはあるだろうけど
これって証明が行間だらけで腹立つよな
全然教科書じゃ無い
単に各トピックスをツアーみたいにさぁーって流していくだけ Henkin法で言語を「完備化」するやり方は議論の整合性の確認が大変に面倒臭い。
発想は極めてシンプルで素晴らしいのだが…
証明を完遂するのが困難。
その細部の確認は演習にして読者丸投げの本ばっかだし。 >>796
東京での集会に出てたから
大体どういう内容か知ってるんだけど、
その本はCHとその否定の強制法による
（相対）無矛盾性証明くらいまでの本になるはず。
Jechとかで適当に書いてあるところをきちんと書いて
強制法の勉強でありがちな「気持ちが分からん」
という事が無いように解説する本。
世界一丁寧な強制法の教科書、という感じになるはず >>797
まあ実際、教科書じゃないしね。
四人の著者によるオムニバス形式の本だし。
当時、その本で扱ってるような内容の本は
ほぼ無かったので、基礎的な事から解説を初めて
ロジックの面白い所まで一冊の本の中で
到達しようとすると、当然ああいう本になるかと、
基礎論の本は証明を行間が無いようにガチガチに
書くべきだというのは、基礎論に興味を持つ
タイプの人の或る種の思い込みみたいなもので、
別に必ずしも正当な考えでもない訳だし。 >>801
>基礎論の本は証明を行間が無いようにガチガチに
そんなの無理
証明は
読者にある程度のレベルを期待して書くもの >>800
>世界一丁寧な強制法の教科書、という感じになるはず
大いに期待するなあ >>801-802
文学部出身でなおかつ数学コンプ丸出しなので数学の土俵に乗れない知能と努力量で土俵ごと突き崩してやろうと基礎論齧り出す輩どもに教えようという態度よりも
計算機に実装できる厳密性として議論するほうが無難だよねえ。
我の肥大した連中のおもちゃにされるのは避けるべきというのはかなり一般的な規範だ。 証明･記述に於いて或る程度の数学的読解力を読者に要求するのは当然だが
だからといって行間すっ飛ばしで自分の理解や頭の中の数学的議論を自分だけの目線で押しつけるのも間違ってる
｢俺がこれこれを理解してるんだから、お前らにはこれだけ言ってれば分かるだろ｣という上からの押しつけは最悪
個人的には数学科3,4年生の読解力を想定して書いて欲しい。
でも読解力という言葉って意味の幅があるんだよな
理解力自体は低いけど、当該分野についての基礎知識をある程度溜めてるからその多い知識を援用させて高度な議論を理解する人も居れば
逆に当該分野の知識は少ないけど、理解力は高いから、その高さで高度な議論を理解する人も居る
大体数学なんかやってプライドを高めてる人ってどちらかというと後者の方に比重置いてるような気がする 河合文化研究所の 倉田令二朗「数学基礎論入門」良いよ 基礎論の勉強で問題となりがちなのは、演繹体系にどのシステムを使うかだな。
楽で簡単そうだからとHilbert形式選んだけど、やっぱGentzenが良いかと右往左往して中々学習が進まん。
また、各流儀決めてもこれまた方言がいっぱいある。
後々の応用考えて十分一般的な枠組みの論理体系でお勉強したいのだが… 俺、数理論理学厨が喉から手が出るほど欲しい？本持ってるよ
ヒューズ･クレスウェルの｢様相論理入門｣
アンドリュースの｢数理論理学とタイプ理論｣ >>810
Hilbert 方式の定式化と Gentzen 方式の定式化の同値性が、
>>808 で紹介された、河合文化研究所の 倉田令二朗「数学基礎論入門」
に証明付きで載っていますよ。 >>806
>個人的には数学科3,4年生の読解力を想定して書いて欲しい。
それほぼほぼ無理 >>810
一般的って言うなら論理演算4つと量化子2つ出てくる方がいいしょ
ゲンちゃんの自然演繹からシーケントへ ラッセル著の数理哲学序説は難しくないですか。まだ3章までしか読めてませんが後裔、祖先、遺伝的、帰納的、N-遺伝的、R-遺伝的、R-祖先、後者など定義を理解することが難しいです。自然数とは直接の前者という関係に関する0の後裔であると書かれています。 中高生に自然数とは何ですか？と聞かれたら「自然数とは直接の前者という関係に関する0の後裔です。」と答えれば完璧ですねwwwww 集合論勉強しててあまりヒルベルト式かシークエントかとかって意識したことないんだけれど、
普通はやるものなのかな >>819
論理や証明を形式化する必要があるときだけだよ 証明を簡単にするために、論理記号は¬と⇒だけみたいな感じで少なめにして欲しいわ ■ このスレッドは過去ログ倉庫に格納されています
