数理論理学（数学基礎論） その12
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化
などを参照）
前スレ
数学基礎論・数理論理学 その11
http://rio2016.2ch.net/test/read.cgi/math/1325247440/ 前スレ 999
直観主義論理では二重否定の除去
¬¬B → B
は出来ないけど三重否定から否定を二つ除去
¬¬¬B → ¬B
するのは出来るんだよな
「「「Bが成り立つなら矛盾が導き出される」が成り立つなら矛盾が導き出される」
が成り立つなら矛盾が導き出される」
から「Bが成り立つなら矛盾が導き出される」が導き出されるという… 直観主義では(¬(A∧B))→((¬A)∨(¬B))は示せないですが、その対偶の
(¬((¬A)∨(¬B)))→(¬¬(A∧B))を示すことは出来ました。
でも(¬∃x¬A)→(¬¬∀xA)は示せないようです。（もし直観主義で
示せる人がいるなら証明を教えてくれるとうれしいです。）
直観主義では本当に(¬∃x¬A)→(¬¬∀xA)が示せないのなら、
直観主義では∀x¬¬Aと¬∀xAを同時に仮定しても矛盾しない
ことになりますが、なんか不思議な気がします。ここらへんを
うまく説明できる人はいるでしょうか。 >>2
それは一般的な定理で
古典論理が直感論理に埋め込めるって奴 >>4
量化子は無限に関わって来るので
その扱いが古典と直感とで異なるんだろうと思ってるんだけど
詳しい人の見解を聞きたいところだ >>4
直観論理の位相空間による解釈を知ってるとおかしく感じない。 >>4
丁度直観主義の意味論をかじったところなので回答します
直観主義における論理式の解釈を、以下のクリプキモデルによって定義します
世界Wiの集まり{Wi|i∈I}をクリプキモデルと呼びます
各世界Wiは通常の古典論理における構造に対応します
また、世界Wiには到達可能関係→が定義され、以下が成り立ちます
反射律 Wi→Wi
推移律 Wi→WjかつWj→Wkならば、Wi→Wk
また、Wi→Wjのとき、以下に従います
Dom(Wi)⊂Dom(Wj)
P^Wiが真ならばP^Wjも真
P^Wi(a1,..,an)が真ならばP^Wj(a1,...,an)も真(a1,...,an∈Dom(Wi))
すなわち、クリプキモデルとは、通常の古典的な意味での構造=世界をいくつも持つものであり、それぞれの世界は我々の持つ知識量に対応している、と解釈できます
すなわち、Wi→Wjのとき、Wjの世界においては、Wiの世界よりも我々の知識量が多いため、より多くの事柄に関する真偽を決定できる、というわけです ある原子命題Pが真であるというのは、「世界Wiにおいて」Pが正しいと判断できる、ということを意味して、Wi|=Pと表します
逆にPが偽であるということは、「世界Wiにおいて」Pが正しいと判断できないということ、を意味して、Wi|≠Pと表します
命題¬Pが真であるとは、Wi→Wjなるすべての世界Wjに対して、Wj|≠Pとなることを意味します
言い換えれば、その世界より後ろは全部偽なわけです
今、Wi|≠P、とわかったとします
このとき、Wi|=¬Pと言えるわけではありません
Wiに関して言えば、真ではない、とわかっただけですから
Pは本当にWi|=¬Pとなるかもしれませんし、到達可能な世界を巡っていけば真だとわかることがあるかもしれません
前者を、Pは真に偽である、後者をPは保留状態にある、と言うことにしましょう
このようにすると、Pが偽、すなわちWi|≠Pであるとは、真に偽である状態であるか保留状態にあるかのどちらかだ、と言いかえることができます
直感主義における偽とは、確証のなさを表していると言えるでしょう
本当は偽なんだけど自信がないときは真の偽、本当は真なんだけど自信がないときは保留状態であり、どちらの場合も断定ができないので、真ではないという意味で、偽を与えるのです
命題∀xP(x)が真であるとは、Wi→Wjなるすべての世界Wjに対して、全てのa∈Dom(Wj)に対してWj|=P(a)となること、を意味します
その世界より後の世界の対象をどれだけ持ってきても真になる、というわけです ¬¬Aの意味を考えましょう
Wi|=¬¬A、Wi→Wjとします
Wj|≠¬A、すなわち、「Wj|=¬A」ではない、となっています
これは、任意のWjに対して『「Wjより後ろは全部偽」ではない』、ということですから、WiにおけるAは真であるか保留状態になっている、ということを意味しています
Wi|=¬¬AとWi|=Aは異なるわけです
Wi|=∀x¬¬A
これは、全てのWjの全ての対象xに対して、Aは真であるか保留状態となっていることを表しています
Wi|=¬∀xA
これは、任意のWjに対して、『「その世界より後の世界の対象をどれだけ持ってきても真になる」わけではない』ことを意味しています
Wjより後の世界には、必ず偽となるような対象が存在する、というわけです
別に矛盾はしていませんよね クリプキモデルもいいんだけど必然的に時間の概念というかモデルの順序関係に依存するので
静的な単独なモデル(位相空間でもイイよ)による意味論の方が何かしっくりくる感じが >>11
>>8
＞各世界Wiは通常の古典論理における構造に対応します 古典命題論理＋様相記号 の体系において演繹定理ってどういう形で成り立つんですか？
参考になるURLあれば教えて下さい
私個人でチェックした限りでは
Γ,□A |- □B ならば Γ |- □(A→B)
が成り立ちそうな気がするんですが？ 前スレ http://rio2016.2ch.net/test/read.cgi/math/1325247440/897
でもいいましたが直観主義命題論理学は前原昭二の｢復刊 数理論理学序説｣で初歩を扱っています
>>2,4の話も出てきてたと思います 高橋洋一（嘉悦大）
@YoichiTakahashi
統数研。70年代にちょっといて赤池さんと話したことを思い出した。いい概念（AIC）は応用も広いし、道筋の見通しもよくなる。AICについて、AkaikeではなくAn Information Criteria と控えめに言っていたのが印象的
統計数理研究所
@tousuuken
本日は統計数理研究所第8代所長 赤池弘次先生の生誕90周年です。
https://www.google.com/doodles/hirotugu-akaikes-90th-birthday Aを公理とするとき、A|-BもA|-¬Bも証明可能ではないですから、Bは決定不能命題ですか？ 有限の立場からの質問です
普通、(公理的集合論で？)超限帰納法の定理を証明する時って背理法によって証明しますよね？
これを直接(構成的に？)証明することって出来るんですか？ 質問
自然数論の無矛盾性証明の下準備として、その証明に関係することになる順序数の定義を行うじゃ無いですか？
で、そこで定義される順序数って、その証明に必要なことを便宜的に駆け足で定義しているせいか、公理的集合論(ZFC)で議論される順序数の定義とは違ったものじゃ無いですか？
そこで気になったんですが、この順序数の定義と公理的集合論における順序数の定義って同値ですか？
なんとなく 有限の立場から(ZFCを仮定せずに定義されている？)順序数の定義から帰結される命題集合 ⊆ ZFCでの順序数の定義から帰結される命題集合
な感じはするんですが、⊇の主張には何か他の仮定がいるんですかね？
ZFCで習った順序数と違う定義を学んだものでしたので疑問を持ちました ZFにおける議論において、
順序数がカントール標準形を持つこと、
特にε_0未満の順序数については自然数とωだけを用いた標準形を持つことを示せる。
したがって、有限の立場においても、
自然数と新しく導入した記号ωを用いればカントール標準形と外見上全く同じ有限長の記号列を定義できる。
この記号列に対して順序を入れることもできる。
再びZFにおいて議論すると、
有限の立場で定義されたこの記号列全体は（順序まで含めて）ε_0未満の順序数全体と一対一対応することが示せる。
特に、この記号列全体は整列集合であることが示せる。
この記号列全体がZFでは整列集合であることがわかったので、
「この記号列全体は整列集合である」という仮定を追加して有限の立場を拡張しようと思う。
もちろん「」内の命題は自然数論では証明できない。もしできたら第二不完全性定理に反する。
無矛盾性証明では（自然数に関する）数学的帰納法を拡張した体系で議論することを基本方針としよう。 細かいことだけど以下のように訂正
× この記号列全体は整列集合である
○ この記号列からなる無限下降列は存在しない >>42
ジャストミートな回答ありがとうございます
モヤモヤ感が何となく解けました 以前、直観主義論理で証明可能では無い論理式についてのレスがありましたが、それに関係する記述を見つけたので書いておきますと、
竹内外史「数学基礎論」共立出版株式会社 の68ページの記述がそのまんまそれですね
ゲンツェン流の体系LJにおいて以下の式はprovableではない(一部抜粋)
１） ⇒A∨¬A
２） A⊃B ⇒¬A∨B
５） ¬∃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
あなたが無職だと言うことですよ、東大生さん [Ｐ⊃Ｑ] ⊃ [〜Ｑ⊃〜Ｐ] は恒真式（tautology）であるが故に
対偶律： 《 [ＰならばＱ] ならば [ＱでないならばＰではない] 》
、 を表わしていると信じられて来た。 しかし、これは誤りであった。
例えば、[Ｐ⊃(Ｑ∨Ｒ)] ⊃[(Ｐ⊃Ｑ)∨(Ｐ⊃R)] はtautologyである
にも拘わらず、《 [Ｐならば(ＱかＲ)] ならば、[ (ＰならばＱである)か、又は(Ｐならば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
ｆ(P,Q)⊃g(P,Q) だからと言って、ｆ(P,Q)|=g(P,Q) とは限らないってことさ。 |=ｆ(P,Q)⊃g(P,Q) だからと言って、ｆ(P,Q)|=g(P,Q) とは限らないってことさ。 >>54
＞にも拘わらず、《 [Ｐならば(ＱかＲ)] ならば、[ (ＰならばＱである)か、又は(Ｐならば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
[ (ＰならばＱである)か、又は(ＰならばRである) ] は偽であって、「現実と矛盾している」。
＞全ての現実に当てはまる公理が存在するとでも？
ある命題が真ならば、その否定は偽である、は恒久的な真である公理の一つ。 >>98
論理学における「ならば」は因果関係を意味するものではない、ということは理解できますか？ ■ このスレッドは過去ログ倉庫に格納されています
