数理論理学(数学基礎論) その13
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
(「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。)
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
(数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照)
前スレ
数学基礎論・数理論理学 その12
https://rio2016.5ch.net/test/read.cgi/math/1509638068/ それは論理の推論規則です
ZFCは公理系です
推論規則は論理式の変換規則であり、公理系は無矛盾な論理式の集まりです
「公理系」の意味を曖昧にしているから起こる勘違いですね
あなたの言葉で言えば、いかなる数学をする上での共通な公理系はその6つだけです 俺は 1. 5. 6. は推論規則で 2. 3. 4. は公理だと解釈してたのだけど違うんか?
そんで推論規則と公理をいくつかまとめて公理系と呼ぶんだと解釈してたんやけどそれも違うんか?
さらに言うと、ZFの置換公理は一階述語論理の中では論理式として記述できないから推論規則として置いてるらしいじゃん。それ以外は公理だけど。よく知らんけど。
つまり何が言いたいのかと言うとさ、俺が上で挙げた公理系(ヒルベルト流公理系と呼ぶことにしよう)と、ZFC公理系にはあなたの言ってるような明確な違いが俺には分からんのよ。
推論規則とは?公理とは?公理系とは?論理式とは?俺の言ってる事は一般論とそんなにずれとるん?俺は独学だから間違ってる事があるんなら教えて欲しいんやけど。 直観主義論理だと4.を認めないよね、というのはおいといて
グッドスタインの定理みたいなのがあるから、ペアノ算術では十分ではないことがあって、
これは無限集合を扱う能力の有無によって生じていると認識してる
無限集合を使いたかったら#include <ZFC>しときましょう、みたいなイメージ >>272
今どこにいるのでしょうか?
あなたを殺したいのですがどうすれば良いですか? >>無限集合を扱う能力の有無によって生じている
ZFCで構成される自然数は少なくともペアノシステムの1つな訳で、制約はZFCの方がキツイはずでしょ。
それでも問題が生じているんだから俺にはその辺はもう分からん。
でもどちらにせよそれならペアノシステムに問題があるのであってモデルのそもそもの定義がどうとかの話になるでしょ。
その理由でZFCを使うことにしようと言うのは納得できないな。 ZFCでペアノシステムが作れる
ゆえに、ペアノ算術で証明可能な命題はZFCでも証明可能
逆に、ZFCで証明可能でもペアノ算術で証明不可能な命題が存在する
つまりZFCのほうが「強い」 >制約はZFCの方がキツイはずでしょ。
制約がキツイって何だ?
公理が少なければ、いろいろな操作が自由にできて何でも証明可能だが、
公理が多くなるほど不自由になって、証明できることが少なくなっていく
と勘違いしてるのかな? >>276
それは何となく分かる。
俺がZFCを否定したい理由がそこにもあって、「ZFCで証明可能でペアノ算術で証明不可能な命題」というのがあったとしたらそれはペアノシステムの中で成り立たないものがあるわけじゃん。
ペアノシステムは自然数の性質である訳だからそれは自然数に対して必ず成り立つ命題ではない訳。
つまり弱い性質のもので議論した方が広義的な議論になるでしょ。
ちなみにさ、「ZFCで証明可能でペアノ算術で証明不可能な命題」ってのはやっぱり273で言われてた定理みたいなものの事なんかな。んー。 >>277
そりゃそうだね。勘違いしてた。
でも275で主張したかったのは後半部分だよ。 >>278
>つまり弱い性質のもので議論した方が広義的な議論になるでしょ。
広義的な議論って何?
公理が少ないほど広義的な議論になるので、いろいろな操作が自由にできて何でも証明可能だが、
公理が多くなるほど「狭義的」になっていき、証明できることが少なくなっていく
と勘違いしてるのかな? はい、ZFCで証明可能でペアノ算術で証明不可能な命題として代表的なのがグッドスタインの定理 >>280
いやいやその逆だよ。
広義的な議論ってのはZFCだけでなく他の自然数も全てひっくるめて話をしようって事。
広い意味での議論って事。
で、狭義的な方が証明できることが多くなることも分かってる。
ペアノシステムで成り立つ事はZFCでも確実に成り立つけど、
でもZFCで言える事がペアノシステム全体で言えるかどうかは分からない訳じゃん。
だから、ZFCで言える事が自然数に対しても言えるとは限らないわけじゃん。
だから自然数の話をしたいならZFCではなくペアノシステムを用いて議論をするべきじゃない?って事。 弱い性質のもののほうが、というなら268の4.も取り除くべきでは >>283
それ本気で言ってる?揚げ足取りにしか思えないんだけど >>284
Minimal logicとして知られていて、これはこれで面白い体系だと思うよ ZFCが何の役に立ってるかと言えば、カントールのように、ZFCから独立な命題に生涯を費やす数学者を減らすのに役立ってる >>2681 most shamefuly wrote :-
>
>俺はさ、ZFCの内容を認めなくても議論を進める事は出来ると思ったのよ。
>
>ZFCを認めた後具体的にどう進めて行くかってのを自然数を構成して、整数、有理数の順で構成していってってのを見たんだけどさ。
>
>でもその議論はペアノシステムを満たす何らかの系があるとして... といきなり始めてしまって良いと思ったわけ。
>それは自然数の存在を認めてる訳じゃないから特に公理体系を汚す事なく議論を続けられる訳さ。
?
>だから、これくらいは認めて欲しいって内容はZFCを認める以前に認められているような述語論理、それから論理学における基本的な公理系だけを認めればそれで十分だと思った訳。
>1. A, A⇒B ├ B
>2. B ⇒ (A ⇒ B)
>3. ( A ⇒ (B ⇒ C) ) ⇒ ( (A ⇒ B) ⇒ (A ⇒ C) )
>4. (¬A ⇒ ¬B) ⇒ (B ⇒ A)
>5. ∀x[P(x)] ⇒ P(a)
>6. P(a) ⇒ ∃x[P(x)]
>
>公理系の規則はこの6つで十分だろうと。
こん bakatare が !!!
俺は数学科ではなく情報系の人間だからこういったZFCのようなものはグローバル変数を汚しているような感覚があって好まないのだが。 >>287
「こん bakatare が !!! 」
なんでそんな変な書き方するの?
単にバカタレでいいじゃん 【天文台閉鎖、FBI】 アポロ捏造のキューブリックも真っ青、太陽に映ったのはマ@トレーヤのUFO
http://rosie.5ch.net/test/read.cgi/liveplus/1537840672/l50
おまいらが注目しないから宇宙人は出てこれない、その結果、地球の放射能危機がどんどん進んでしまう! 犬は動物である
ゆえに、犬の耳は動物の耳である
この論証を形式化して下さい 矛盾とは公理系からφ∧¬φが証明されることなので、素朴集合論は矛盾を含んでいないのでしょうか? >>291 132人目の素数さん2018/09/27(木) 11:41:30.09ID:DqESno6t
>
>矛盾とは公理系からφ∧¬φが証明されること
いいや違う! >>290 132人目の素数さん2018/09/27(木) 07:34:26.54ID:Eb9GPj1U7)
>
>犬は動物である
>ゆえに、犬の耳は動物の耳である
>
>この論証を形式化して下さい
{ [ x は動物である] ⇒/x/ [ x の耳は動物の耳である] } & <x:犬> >>292
素朴集合論に公理系はないので公理系の上の概念である矛盾もないということです >>290
自信がないが興味があるので、答練。批判は受ける。
d : Dog とする。
つまりd : Dog trueと主張できる。
Dog ⊆ Animal であるから
d : Animal
Dogの証明 d はAnimal の証明にもなるという意味で
d : Animal trueと主張できる。
かな?
耳云々はわからない。
勘違いしているなって時は逆にはっきり言ってもらえる方がありがたい。 今年のサマースクールも竹内シンポジウムも
書籍化するみたいだね。
夏休み取れなくて行けなかったのでありがたい。
神戸の人達はいい仕事するなあ。 すでにだいぶ完全な人間の心理モデル持っているんじゃないか? 僕は、君らは内容の重要性に比して世の中から正当に評価されていないと
ずっと思い込んでいた。一体何がしたいんだ?することが何も無くなってしまった? >>290
犬は動物である
動物の耳は動物の一部である
ゆえに、犬の耳は犬の一部である >>296
じゃあ素朴集合論というもの自体がないってことだな ∀a,b[ a⊆b ⇔ ∀c[c∈a ⇒ c∈b] ]
こう言ったのは素朴集合論の公理ではないの?
この場合「定義」って事になる? 定義といった方が正確じゃないの?
別に定義でも公理でも間違い時ないけど、
略記としての新しい記号の定義には、
必ず元の理論の保存拡大になるという顕著な特徴がある。
この場合はそれに該当する。 何かの理論Tの上で定義をするときのTのこと。
Peano算術でも良いしZFCでも良いしRCAとかの
二階の体系でも良いだろうし、
普通の述語論理上の理論ならなんでも良い。
古典論理は強過ぎるから部分構造論理を採用するとか
線形論理を考えるとか言われたら困るかも知らんけど なるほどねー。
ちょっと思ったんだけどさ、定義と公理の明確な違いってあるんかな? >>311
思ってないけど何で?
「定義」「公理」自体にそもそも定義なんかないよって言いたいの? >>312
なら
定義は定義
公理は公理
分かってんの? 怒らないで欲しいんだけど、結局日本語不自由なんじゃない? 「各成分が離散位相の入った有限集合の直積集合はコンパクト」からチコノフの定理が選択公理無しで導けるはずなんですが、うまくいきません。
どなたか証明または証明の書いてあるリンクをお教え頂けないでしょうか? >>318
もちろん「…」の証明には選択公理を用います。
「「…」→チコノフ」がZFで証明できるかどうかという話です。 >>276
>ZFCでペアノシステムが作れる
>ゆえに、ペアノ算術で証明可能な命題はZFCでも証明可能
論理が飛躍している! >>320
厳密に言うとペアノ算術で証明できる命題は、
それをZFCで定式化するとZFCで証明できる。
まあ別にそれくらいの略記はいいと思うが。 >>320
あなたの指摘もおかしくはなく、
「非ユークリッド幾何のモデルがユークリッド幾何で作れる。
ゆえに平行線公理の否定がユークリッド幾何で証明できる。」
だと、言葉の濫用という感じになる >>321-322
横レスですが非常に分かり易くポイントを突いた説明ですね、勉強になりました、ありがとう >>288
>>287
>「こん bakatare が !!! 」
>
>なんでそんな変な書き方するの?
>単にバカタレでいいじゃん
Бакамон! >>322
物質としての脳は3次元空間内に存在するが、ニューロン構造は最大で“11次元”にまで拡がっている。3次元空間内で11次元のモデルを作れるからこそ、動物は高度な時空認識が可能で鳥類の渡りや魚類の回遊が出来ることが解明されている。
これは脳に限った話ではなく一般に言えることで、異なった幾何モデルだけでなく、より高次のモデルも作れる。
実際、情報幾何の発展でニューラルネットワークを説明できるようになったように、ニューロン構造を情報幾何の多様体として捉えることでさらに高速な学習が実現されつつある。 2つのことを比較するときに
片方にしか思考が及んでいない(共通事項すべてを自分が肩入れする片方にしかないものだとして語る)状態のことを指す言葉って何かあったっけ? >>325
なんか脳内完結しているオントロジーみたいな概念も導入されているんですかね?
明文化にせずにさらに主張することも回避してなんか物事進めているんですけど、
正直ついていけないですよ。 >>330
真っ先にそれが思い浮かんだんだけど、ピンとはこないんだよね
でも他に適当な言葉が浮かばないしそれが最適なのかもしれない 明文化してないからあれこれ考えて、参照するべきではないものまで参照して話を
進めようとしているから整理するべきなんだけれど、情報が多すぎて基軸を見つけられない。
こういう時ってどうするべきですか? Бакамон!
物質としての脳は、4次元時空間に存在する。 脳内の空間認知システムって2014年のノーベル生理学・医学賞のネタだろ。 i>>328 Stupidly wrote:-
>物質としての脳は3次元空間内に存在する
Бакамон!
物質としての脳は、3次元空間内ではなくて、4次元時空間内に存在する。 人工知能についての世界で最初の国際会議である「ダートマス会議」
の中で、ラッセルの「プリンキピア・マテマティカ」の中の定理を
自動証明する人工知能プログラム「Logic Theorist」が公開された。
「Logic Theorist」 は、1955年から1956年にかけてアレン・ニューウェル、
ハーバート・サイモン、J・C・ショーが開発したコンピュータプログラム。
人間の問題解決能力を真似するよう意図的に設計された世界初のプログラムで、
「世界初の人工知能プログラム」と称された。ホワイトヘッドとラッセルの
『プリンキピア・マテマティカ』の冒頭の52の定理のうち38を証明してみせ、
一部については新たなもっと洗練された証明方法を発見している。
ハーバート・サイモンは「限定合理性」の理論でノーベル経済学賞をのちに
受賞した。 数理論理学は、論理的思考の過程を演算化できるようなシステムだと
みなせるので、現在のディープラーニングや人工知能の発展の歴史の
原点となっているものだと考えられる。ライプニッツはすでに当時から
「思考の演算化」を提唱していたようだし、フレーゲやラッセル、
ヒルベルト、チューリングやノイマンも、思考の演算化や機械化、
自動化かが可能だと想定していたのではないかな。
人工知能には人間と違って自我や心はないので、疲れたり、他人を
憎んだりすることはない。ストレスフリーな存在だ。逆に人間は
ストレスの塊で鬱にもなる。だから、人間と人工知能は正反対な存在
なので、相互の欠落や弱点を補完しうる。
ハーバート・サイモンは「限定合理性」は、人工知能が陥る局所最適解
に似ていないだろうか。 現在のアマゾンではステマレビューが多いということに
気づいた。☆5つがやたら並び、レビューの日付の間隔も
小さかったりす。レビューアーの他のレビューをチェック
してみると類似商品を似たような日付で☆5つでレビュー
している。
こういうステアレビューをある程度、自動的に推論させて、
それらを不正なものとして排除するシステムを作れば、
アマゾンを利用する顧客の利益に資すると思うのだけど、
どうだろう。推論規則をいくつか作って、それで自動判定
させるだけなので、技術的には簡単なはずなのだが、何か
別の理由で制限がかかっているのだろうか。中国系の製品が
翻訳のおかしな日本語レビューも含めて、そういうステマ
要員を動員しているようだが。 ラッセル・ヒルベルト流にしろ、ゲンツェン流にしろ、[PならばQ]を[Pでないか又はQ]と同値であると考えたのが、そもそもの誤り。
その昔、イマニュエル・カントは『純正理性批判』(第二版・序文)で
「論理学はどう見ても、アリストテレスの著作でもって完成している
ように見える」と書いたが、その見解が誤りであったことは、その後の
記号論理学の著しい発展を見れば明らかである。では、今日の記号論理学
は、一応なりとも、完成したと言えるのだろうか? 大多数の人々は、
ゲーデルのいわゆる“(述語論理の)完全性定理”を引き合いに出してして、
イエスと答えるであろう。しかし。これも又、カントの轍を踏んで、誤り
なのである。
諸君は、(P⊃Q)v(Q⊃P)などと言った「奇怪な“定理”」をもつ
「現行の論理学理論」を正しいものと信じて疑いないのか? www
論理学を、“命題論理”と“述語論理”とに分けるのがそもそもの間違いだ。
例えば、p⊃(PvQ)は恒真式(tautology)だと言うが、それは取りも
直さず、∀p,q{p⊃(PvQ)} ってことであって、“命題論理”の段階で、
全称概念を「密輸入」しているからだ。 今、Jechの set theoryを読んでいます。
absoluteness of constructibilityの辺りがよくわかりません。
この辺りが丁寧に書いてある本があれば教えていただけないでしょうか。 諸君は、(P⊃Q)v(Q⊃P)などと言った「奇怪な“定理”」をもつ
「現行の論理学理論」を正しいものと信じて疑いないのか? www >>342
それはお前が述語論理でしか考えようとしてないから >>344
全然奇怪ではない
真理値が2値だから
当たり前の恒真式
ならばを神秘化しすぎのようね 現行の論理学理論は、少なくとも、「ならば」の解釈の点で間違っている。 ラッセル−ヒルベルト流にしろ、ゲンツェン流にしろ、[PはQを内含する]と
[Pでないか又はQである]とが同値であると考えたのが、そもそもの誤り。
P:[リンカーン大統領は暗殺された],
Q:[リンカーン大統領 とケネディー大統領はともに暗殺された]
とおいてみよう。PはQを内含しないことは、直観的に見て、明らかである。
即ち、この場合、[PはQを内含する]は偽である。
他方、[Pでないか又はQである]は真である。
一方が偽で他方が真である様な二つの命題が同値である筈はない。 >>348
リンカーンは生きてるかもしれないじゃん、アホか。 >>348
PもQも真偽のはっきりした命題と考えなければ、いつまでたってもわかるようになりませんよ
P,Q考えた時点で真偽は既に決まってるのです
あなたはP→Qを分解せずに、P→Qという新しい命題を解釈しようとしてるからおかしくなるんです
数理論理においては、ならばとは、既に真偽の定まった命題から新しい命題を作る操作のことです
あなたのならばの解釈は、上の前提から外れているんです
そういう新しい論理を作りたいなら勝手にすれば良いですが、既存のものを批判してはダメですよ
既存の論理とあなたの論理は前提からして違うんですから >>348
ラッセル−ヒルベルト流とか、ゲンツェン流とかの領域に閉じたルールとすりゃいいだろ。
この領域内で[PはQを内含する]と[Pでないか又はQである]が同値にならないことはあるのかね? >>351
だめだめ
あの人が言っているのは
自分の実感に合わないってことだけで
じゃあ
自分の実感に合う理論を示せって言っても
ごにょごにょするだけなんだよ 内含するとかでカテゴリーにしてしまうのはどうかなあ。PとQは独立体
いつもね、アルファベットはと考えてみるとか。 どうも、M_SHIRAISHI氏(つーか、EURMS)の理論」のほうが正しいようだな。
例えば、対偶律は、従来は、 (P⊃Q)⊃(¬Q⊃¬P) で表わされるもののこと
と考えられていたのだっただが、これは、どうやら、誤りだったようだ。
そして、M_SHIRAISHI氏の言う[P(x)⇒/x/Q(x)]⇒/p,q/[¬Q(x)⇒/x/¬P(x)]
こそが【対偶律】を正しく捉えてたものと考えられる。
M_SHIRAISHI氏(たち?)の主張する Logical Reformationは、おそらく、世界を
席巻することとなろう。
http://www.age.ne.jp/x/eurms/
http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html ■■■■■■■■■■■■■
□□□□□□□□□□□□■
■■■■■■■■■■■□■
■□□□□□□□□□■□■
■□■■■■■■■□■□■
■□■□□□□□■□■□■
■□■□■■■□■□■□■
■□■□■□□□■□■□■
■□■□■■■■■□■□■
■□■□□□□□□□■□■
■□■■■■■■■■■□■
■□□□□□□□□□□□■
■■■■■■■■■■■■■ >>346 stupidly wrote
>>344
>全然奇怪ではない
Бакамон!
おまえの頭がどうかしているだけの話だ・ >>357
お前がだよw
一体どんだけの人に同じこと言われてる?
とにかく理論体系構築してから書いてね >>349
リンカーンは生きてるかもしれないじゃん
おまえの空想のなかではな。(^o^) 20世紀の論理学は、Russell, Hilbert および Goedel によってミスリードされた、
暗愚な100年であったということになろう。 どうも、M_SHIRAISHI氏(つーか、EURMS)の理論」のほうが正しいようだな。
例えば、対偶律は、従来は、 (P⊃Q)⊃(¬Q⊃¬P) で表わされるもののこと
と考えられていたのだっただが、これは、どうやら、誤りだったようだ。
そして、M_SHIRAISHI氏の言う[P(x)⇒/x/Q(x)]⇒/p,q/[¬Q(x)⇒/x/¬P(x)]
こそが【対偶律】を正しく捉えてたものと考えられる。
M_SHIRAISHI氏(たち?)の主張する Logical Reformationは、おそらく、世界を
席巻することとなろう。
http://www.age.ne.jp/x/eurms/
http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html こんにちは。a4と申します。数学基礎論から数論の大問題を解こうと思っている者
です。いつもはプログラム技術板にいるのですが、その問題を解くために論理計算を
行う人工知能開発環境「T」というものを創っています。数学の問題だけでなく、
喋る、すなわち、自然言語処理もやってます。開発中ですが、とりあえず、公に
出せるところまで行きました。ダウンロードはこちらです。
http://www.01ken.com/art1.html
これから、仲間を集めてP2Pコード共有などを行って、人工知能の神経構造を交叉
させて成長させようと思っています。このソフトは無償で好きに使っていただいて
構いません。ご意見、要望があれば、
http://www.01ken.com/contact.html
こちらの松本に連絡を。このスレでもしばらくは返信を行います。 検索してみた
01研
www.01ken.com/
01研. ホーム, 作品 · 連絡先. 私達は量子コンピュータで1番の大域最適解を探索して作曲等を行おうと考えている研究会です。
次のものも研究しています。 ・人工知能・タイムマシン・UFO. 論理学というとリズムがあって、数理といっても楽しそうな学問だなあ。 何でこんな真面目なやつが皆無なスレになってしまったんだろう 廣瀬健、帰納的関数 95ページ 定義4.18
定義4.18 定義4.16のD^{ψ_1,ψ_2,…,ψ_l}の定義に現れるψ_i(w)を(v_i)_wで
おきかえた述語、ψ_iがm_i変数の関数(i=1,2,…,l)の場合には、ψ_i(w_1,w_2,…,w_{m_i})を
(v_i)_{w_1,w_2,…,w_{m_i}}で置き換えた述語をD^{m_1,m_2,…,m_l}(v_1,v_2,…,v_l,z,y)と書く
とありますが、日本語的に言っている意味が分かりません
「(v_i)_wでおきかえた述語、」で切れてますがここをどう理解すればいいのでしょうか? >>362
>数学基礎論から数論の大問題を解こうと思っている者
まず無理 >>366
詳しくないけど見た感じ最初の述語と最後の述語がandで繋がってるように見える ■ このスレッドは過去ログ倉庫に格納されています