数理論理学(数学基礎論) その12
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
(「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。)
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。
(数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化
などを参照)
前スレ
数学基礎論・数理論理学 その11
http://rio2016.2ch.net/test/read.cgi/math/1325247440/ Aを公理とするとき、A|-BもA|-¬Bも証明可能ではないですから、Bは決定不能命題ですか? 有限の立場からの質問です
普通、(公理的集合論で?)超限帰納法の定理を証明する時って背理法によって証明しますよね?
これを直接(構成的に?)証明することって出来るんですか? 質問
自然数論の無矛盾性証明の下準備として、その証明に関係することになる順序数の定義を行うじゃ無いですか?
で、そこで定義される順序数って、その証明に必要なことを便宜的に駆け足で定義しているせいか、公理的集合論(ZFC)で議論される順序数の定義とは違ったものじゃ無いですか?
そこで気になったんですが、この順序数の定義と公理的集合論における順序数の定義って同値ですか?
なんとなく 有限の立場から(ZFCを仮定せずに定義されている?)順序数の定義から帰結される命題集合 ⊆ ZFCでの順序数の定義から帰結される命題集合
な感じはするんですが、⊇の主張には何か他の仮定がいるんですかね?
ZFCで習った順序数と違う定義を学んだものでしたので疑問を持ちました ZFにおける議論において、
順序数がカントール標準形を持つこと、
特にε_0未満の順序数については自然数とωだけを用いた標準形を持つことを示せる。
したがって、有限の立場においても、
自然数と新しく導入した記号ωを用いればカントール標準形と外見上全く同じ有限長の記号列を定義できる。
この記号列に対して順序を入れることもできる。
再びZFにおいて議論すると、
有限の立場で定義されたこの記号列全体は(順序まで含めて)ε_0未満の順序数全体と一対一対応することが示せる。
特に、この記号列全体は整列集合であることが示せる。
この記号列全体がZFでは整列集合であることがわかったので、
「この記号列全体は整列集合である」という仮定を追加して有限の立場を拡張しようと思う。
もちろん「」内の命題は自然数論では証明できない。もしできたら第二不完全性定理に反する。
無矛盾性証明では(自然数に関する)数学的帰納法を拡張した体系で議論することを基本方針としよう。 細かいことだけど以下のように訂正
× この記号列全体は整列集合である
○ この記号列からなる無限下降列は存在しない >>42
ジャストミートな回答ありがとうございます
モヤモヤ感が何となく解けました 以前、直観主義論理で証明可能では無い論理式についてのレスがありましたが、それに関係する記述を見つけたので書いておきますと、
竹内外史「数学基礎論」共立出版株式会社 の68ページの記述がそのまんまそれですね
ゲンツェン流の体系LJにおいて以下の式はprovableではない(一部抜粋)
1) ⇒A∨¬A
2) A⊃B ⇒¬A∨B
5) ¬∃x¬A(x) ⇒ ∀xA(x)
provableでない事の証明も載っています。カット除去定理を使った系としての証明ですね。 UAB := ¬∃(Ax∧Bx)
なる U があれば NAND だけで命題論理が作れるようにそれだけで一階述語論理が作れるってマジ? >>46
もう少し具体的に教えてもらえますか?どこでそんなこと聞いたのかも含めて >>46
面白い記述を見つけました
竹内外史の「数学基礎論」101ページ
Γ_0^~の下では、∃xA(x)とA(Min(x)A(x))とは同等である
(この意味でMinを用いれば、∀とか∃とかを取り除くことが出来る)
という記述がありますね。 >>47
コンビネータ論理を考案したシェーンフィンケリが示したけど、あまり知られていないらしい。
コンビネータ論理についてネット検索してた時に見かけた記事で読んだんだけど、今探したらちょっと見つけられなかった。
束縛変項に関する公理がなんか姑息というか、美しくないように感じるので、これを消せないかと思ってコンビネータ論理について色々調べてたんだが、コンビネータ論理って inconsistent らしいのね。
>>48
違うアプローチみたいだけど面白そう。その本は持ってないけど買ってみるわ。でも自分みたいなドシロウトには難しそう… >>49
>>48ですが、これは昔に出版された時の書籍名です
現在はこの増補版(改題された)として「証明論入門」竹内外史(ともう一人の女性)著 が市場に出回っています。
>>48の記述ですがこれは、自然数論の無矛盾性証明の議論において脇道に逸れた話題として出てきた話です
この本は本格的な数学基礎論の書籍です。入門書を終えないとまず理解出来ないでしょう。 直観主義 と 有限の立場 ってどこが違うんですか? >>52
あなたが無職だと言うことですよ、東大生さん [P⊃Q] ⊃ [〜Q⊃〜P] は恒真式(tautology)であるが故に
対偶律: 《 [PならばQ] ならば [QでないならばPではない] 》
、 を表わしていると信じられて来た。 しかし、これは誤りであった。
例えば、[P⊃(Q∨R)] ⊃[(P⊃Q)∨(P⊃R)] はtautologyである
にも拘わらず、《 [Pならば(QかR)] ならば、[ (PならばQである)か、又は(PならばRである) ] 》 は
成立しない ■ z>>5
F(P,Q) ⊃ g ( p, p) が tautology だからって、「F(P,Q) ならば g ( p, p) 」が
必ずしも成立するわけではないってことさ。 z>>5
F(P,Q) ⊃ g (P,Q) が tautology だからって、「F(P,Q) ならば g (P,Q」が
必ずしも成立するわけではないってことさ。 >>58
何言ってるか分からないんですが、
P,Qが存在して、
|=F(P,Q)⊃g(P,Q) かつ |=F(P,Q) かつ |=¬g(P,Q)
が成り立つ
と言いたいのですか? Jech の「Set theory」の sillver's theorem の証明がわかりません。
間違っているということはありますか? >>59
f(P,Q)⊃g(P,Q) だからと言って、f(P,Q)|=g(P,Q) とは限らないってことさ。 |=f(P,Q)⊃g(P,Q) だからと言って、f(P,Q)|=g(P,Q) とは限らないってことさ。 >>54
>にも拘わらず、《 [Pならば(QかR)] ならば、[ (PならばQである)か、又は(PならばRである) ] 》 は
ああ、これですか
「ならば」を高校数学的に考えてる限りわかりませんよ
まずは命題論理と述語論理の区別から始めましょうね >>52
> 直観主義 と 有限の立場 ってどこが違うんですか?
直観主義にしても有限の立場にしても明確な記号論理の体系で公理化されているわけでない
研究者によって同じ「直観主義」という言葉で表しているものが違う、「有限の立場」についても同様
だから誰のなのかを明記した「××さんの直観主義(または有限の立場)」とか
場合によっては「××さんが○○という時期に(あるいは△△論文等で)主張している直観主義(または有限の立場)」と指定しなければ
異同の議論はできない
例えば直観主義論理を客観的な公理系として最初に提示したのはBrouwerの弟子のHeytingだが
師匠のBrouwerは「あんなものは俺の直観主義じゃない!」とその公理化の意義を認めなかったそうだ
その辺りの混乱に関しては先日亡くなられたばかりの竹内外史先生が彼のエッセイの幾つかで書いていて著書にも収録されているから
探せば今でも容易に読めると思うが、その竹内先生御自身も有限の立場について哲学的というか教条的というか非教育的だったので
竹内先生の証明論のアプローチを直接に継ぐ弟子は育たなかった(継ごうとした人達はみな討ち死にして挫折した)というような話を
確か八杉先生だったと思うがどこかに書いていた記憶がある
なので上の問は漠然としていて解答不能 >>69
ありがとうございます。
ざっくりと分かりました。
竹内&八杉のコンビといえば「証明論入門」が思いついた。 式SからGodel Interpretation S^Gを作るまでは割と形式的に出来るけど
そこからquantier-freeなreductionを作るのがホント紛らわしい 大学院生が太刀打ち出来るレベルの未解決な問題ってなんかありますか?(発展的専門書の章末問題レベル)
ステップアップにちょうどいい論文も教えて欲しいです そんなもん知ってたらこんなところに書かず、自分で論文書くか指導学生にテーマとして与えるわ [PならばQ]を[Pでないか又はQ]と同値であると考えたのが、そもそもの誤り。 ラッセル・ヒルベルト流にしろ、ゲンツェン流にしろ、[PならばQ]を[Pでないか又はQ]と同値であると考えたのが、そもそもの誤り。 >>77
直観主義論理というその同値性を認めない論理体系も存在しますよ
まあ、あなたのように命題と述語の区別をつけていない人には関係ない話ですけど >>77
別の規則の体系もある。矛盾していない限り数学上は誤りもクソも無い。 数学セミナー
2018年2月号(2018年1月12日発売)予価1090円+税
特集=「竹内外史と数学基礎論(仮)」
解析学の基礎付けをはじめ、数学基礎論の分野で偉大な足跡を残し,2017年5月に逝去した竹内外史氏。
今回は思い出も振り返りながら、氏が切り拓いた道を紹介する。
“竹内の証明論”における有限の立場(仮題)八杉満利子(京都産業大学名誉教授)
竹内先生の思い出(仮題)難波完爾(東京大学名誉教授)
竹内外史氏の思い出(仮題)一松信(京都大学名誉教授)
竹内先生の証明論(仮題)新井敏康(千葉大学) 待ちに待ってた様相論理学入門が届いた。分厚い奴ね
テンション上がったわ 有限の立場とは、具体的な図形の与えられた列、または具体的な図形の列についての具体的な操作の与えられた列、… についての思考実験を許す立場である。
by竹内外史
(科学基礎論研究39号、1972.Vol10, No.4)
だってさ その定義なら確かに超限帰納法を用いた背理法を含んでるな >>81
>矛盾していない限り数学上は誤りもクソも無い。
現実と矛盾したのでは話にならない。 論理とは主観的なものです
どのような推論を推論として認めるのか、というのは絶対的なものではないんですね >>87
現実と矛盾する、とは何を指すのか?
全ての現実に当てはまる公理が存在するとでも? 様相論理の和書は古いもの以外はほぼ無いけど
黒い本の第1章は割と纏まってて良い感じだったと思う 量子力学が定説となった現代において、数学理論が現実と矛盾するかどうか検証するのは極めて困難 >>85
ところが竹内外史はinductive definitionを有限の立場の根幹とするFefermanの考え(哲学)は完全に反対していた
どうも竹内外史は、predicativeであることが有限の立場では本質的に重要だと考えていたみたいだね >>94訂正
ごめん、日本語が少し変だった
誤>ところが竹内外史はinductive definitionを有限の立場の根幹とするFefermanの考え(哲学)は完全に反対していた
正>ところが竹内外史はinductive definitionを有限の立場の根幹とするFefermanの考え(哲学)については完全に否定的だった >>90
[ (PならばQである)か、又は(PならばRである) ] は偽であって、「現実と矛盾している」。
>全ての現実に当てはまる公理が存在するとでも?
ある命題が真ならば、その否定は偽である、は恒久的な真である公理の一つ。 >>98
論理学における「ならば」は因果関係を意味するものではない、ということは理解できますか? 自然数論の無矛盾性証明では証明図に順序数を与えて、その下で超限帰納法で証明してるじゃないですか。
なんで証明図に順序数を対応させなきゃいけないんですか?
ゲーデル数のアイデア流用して証明図に自然数を対応させるんじゃダメなんですか?
ゲーデル数の定義を巧妙にしたら、
記号列(論理式)の有限列(=シーケント) の有限列(=”糸”みたいな奴←カット除去定理の時に定義されてた奴)
の有限列(=証明図)
を一意に自然数に対応させることって出来るような気がするんですが?(漠然とした感想) >>!00
>論理学における「ならば」は因果関係を意味するものではない、ということは理解できますか?
Russellb Hilbert, Genzen も「ならば」の解釈を間違えた。 >>90
[ (PならばQである)か、又は(PならばQでない) ] は偽であって、「現実と矛盾している」。 >>90
[Pであり (PならばQである)かつ(PならばQでない) ] は偽であって、「現実と矛盾している」。 >>101
立場の問題かと思います、多分
有限の立場に立つならば、むしろ自然数と対応付けができなければそれは証明とはみなされません
>>103
あなたの考える「ならば」と論理学における「ならば」は異なるものだというだけですね >>103
論理結合子「☆」(スター)を次で定義します
T☆T=T
T☆F=F
F☆T=T
F☆F=T
このとき
《 [P☆(QかR)] ☆[ (P☆Qである)か、又は(P☆Rである) ] 》 は正しいです
これは現実と矛盾してるんでしょうか? >>101
自然数に対応させることはもちろん可能だが、証明図を変形したとき、対応する自然数が小さくなるような対応でなければ意味がない
もしそのような対応が存在すれば一階の数学的帰納法でペアノ算術の無矛盾性を証明できることになるが、
これは第二不完全性定理と矛盾する R.Shoenfield, Mathematical Logic, Addison-Wesley 1967は、基礎論の専門化を目指す人が必ず1度は手にする最高級の教科書
(田中一之「数学基礎論講義」 64ページ)
↑これって本当ですか? 第一不完全性定理についてちょっと理解不足があるんで質問なんですが、
この定理は、ある論理式ψが存在して、
PA|-ψでない
かつ
PA|-¬ψでない
だと思います。(PAはペアノ算術です)
この時PAのモデルMを任意に取るとM|=ψなのですか? M|=Ψの場合もあるし、M|≠Ψの場合もどちらもあり得ます PAともなるともはや一階述語論理の完全性定理が成り立たなくなる?と思ったので質問したのです。
算術の標準モデルNについてだけ、N|=ψなのだろうか あれ?
第一不完全性定理について、たまに「この定理は正しいにもかかわらず証明出来ない命題が存在することを主張するモノだ」
という説明を見るんですが、ここでいう"正しい"が何を指しているのか気になったので質問したんですが ありがとうございます
第一不完全性定理を扱っている議論の最中にモデルの話が出てくるところは見たことが無かったもので、
ついつい、この"正しさ"をモデル論における真ではなく、何らかの直観的な正しさなるものを指していたものとばかり思い込んでいました 前から何となく思っていたんですがロッサーの不完全性定理があるのに何でわざわざゲーデルの第一不完全性定理をテキストに載せるんですか?
ゲーデルに敬意でも払ってるんですかね?
テーラー展開があるのにわざわざx=0の時だけマクローリン展開と言ってるような違和感を感じますw 第二不完全性定理はGodel文と無矛盾性CONの
同値を言うことで示すでしょ。
Rosser文だとこれが出来ない。
第二は第一の単なる応用ではなくて、それとは全く
独立に重要な定理なので、Rosser文だけでは困る。
Hilbertプログラム云々の歴史的な話は措いといて
単純に数学としての応用としてみても、
集合論や算術のモデル論とかとの関連で
出てくるのは多くは第二の方だしね。
前者が対角線論法ズバリという感じなのに対して
後者はテクニカルな修正を加えて小手先の改良をしている。だから応用には乏しい。
Godel文とRosser文の実際の構成を知ってれば分かると思う。 「恒久的な真理」なんて言うのはオカシイ。
真理とは、すべて。恒久的なものだからだ。 第二不完全性定理の詳細な証明は学んだことが無いんですが、「第一不完全性定理の証明までの議論を形式化すればいい」みたいな文句はよく見かけますよね
じゃあロッサーの不完全性定理はゲーデルの第一不完全性定理に比べて前提とする条件が弱い(ω無矛盾ではなく単なる無矛盾性だけ)だけに
そのロッサーの不完全性定理の証明までの議論を形式化することによって、ゲーデルの第二不完全性定理よりも"ちょっとだけ一般化されたロッサーの第二不完全性定理"みたいなものが出てきはしないんですかね?
もし出てこないのであれば、ω無矛盾性・無矛盾性の違いが形式化への流れの中でどのように消えてしまっているのかが気になります >>123
>真理は相対的なもの
そう信じるのは誤り。
異なる3個のものから2個選ぶ選び方の数は3通り。これは絶対的な真理。 >>124
三段論法や排中律を使わずに証明できて居るかどうか確認できてる?
ルイスキャロルの無限後退法やブラウワーの直観主義というのもあるんだがね >>124
「異なる3個のものから2個選ぶ選び方の数は3通り
」
あるモデルにおける解釈として、「異なる」を「同じ」という意味だと解釈しましょう
このとき、この論理式は偽となりますね
同じ3つのものから2つ取り出す選び方は1通りしかありませんから >>124
「真理は全て恒久的なもの」ではない、ということ
「条件付き」の条件が空であることも許される 等号の公理を差し置いて
「異なる」を「同じ」という意味だと解釈
手の付けられない馬鹿だな >>128
そういう公理が含まれないかもしれませんね
気にくわないなら、3を4と解釈する、でもいいですよ、 >>129
そういう記号の約束事みたいな話は本質的ではない 直観主義云々は証明論とか統語的な話ですよね
真理云々は意味論、すなわちモデル理論の範疇です ・我田引水
・ああいえばこう言う
・そういうお前をわしゃ食った
論理の通じない相手を相手するだけ徒労 >>131
それ以前の日本語の話
そもそも等号の公理を使わないなら、「同じ」とか「異なる」という日本語も使うべきではない
おまえは上の文中の「日本語」や「使う」をモデルでどう解釈するか考えたりしないだろう
それと同じだ >>134
でも、理論的には間違ってはないですよ?
自分がからないからって屁理屈言うのはやめたらどうですか? 勘違いした哲学バカだな
おまえは全ての言語にモデルの解釈が可能だとでも思っているのか
無限後退に陥るだけだ ここは数理論理のスレなんですから、全ての命題は形式言語により書き直して考えるというのは何もおかしくないですよね? だったら試しに日本語の「同じ」にモデルを当てはめてみな ■ このスレッドは過去ログ倉庫に格納されています