数理論理学（数学基礎論） その13
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照）
前スレ
数学基礎論・数理論理学 その12
https://rio2016.5ch.net/test/read.cgi/math/1509638068/ 何で数理論理学も数学基礎論もまるでできない奴が集まるようになってしまったんだろうな 永遠にバグ取り作業を強いられる宿命がゲーデルの主業績なんだから
ITドカタ程度の扱いが妥当だな >>373
統合失調症の薬を飲んで落ち着きました。
うん？書いた通り、数学基礎論の公理をCPUのように作って、みんなでリーマン予想の
ような問題をWindowsを作るようにP2Pコード共有で解決。 もし、懸賞金かかってる問題が解けたら、ですが、僕がお金いっぱい欲しいという訳
ではなく、話し合いなどで、主要部分を書いた人に多めに分散させようと思っています。 1000までたどり着くか知らんけど次スレからは数学基礎論外すか
実質含意のパラドックスは仕方ないとして、
糖質プログラマーと不完全性定理大好きさんは来なくなるだろ >>377
「メタ数学」のほうがいいよね。「記号論理」という名称ももはや適切なのかよくわからない
「形式体系」を議論するという意味ではまあ記号論理なんだろうけど、意味論的な議論もするのだからちょっとおかしい >>384
> 「メタ数学」のほうがいいよね。「記号論理」という名称ももはや適切なのかよくわからない
記号論理学あるいは数理論理学の目的としてはメタ数学（数学基礎論）つまり数学理論を形式化して分析（し数学の基礎を考察）することだけとは限らずもっと様々な目的がある 廣瀬健の｢帰納的関数｣ 111ページの S_n^m定理 の証明を読んでるんですが、
{ S_n^m(y1,...,ym) } (x1,...,xn) ってなんですか？
どう解釈したらいいのかが分かりません
何らかのｎ変数関数のゲーデル数がS_n^m(y1,...,ym) なんでしょうが、
そのn変数関数が何か分からない…
証明は構成的にしているようなので具体的に明示できるはずなんですが、イマイチ分かりません 質問です
廣瀬健の｢帰納的関数｣の134ページ定理6.6の証明です
任意の次数fに対し、 f<f' の証明ですが、f≦f'は明らか
と言っていますが、この理由が分かりません。 帰納的関数論についてのpdfってあんまりヒットしないから探しにくいですね 質問です
廣瀬健の｢帰納的関数｣の137ページの帰納的加算な次数についてです。
R^f(x,y)をfで帰納的な述語とし、fの次数をf~とすれば、述語∃y R^f(x,y) の次数d~は、f~で帰納的加算な次数である。
とありますが、これを定義に沿って理解する事が出来ません
A:={x|∃y R^f(x,y)}とすれば、確かにAの次数はd~となる事は分かりますが、f~で帰納的な関数gで、
gの像がAとなるようなものをどうやって見つければいいのかが分かりません ゲーデルの不完全性定理を素スペクトルを用いて表現できるらしいのですが(wikipediaより)
詳しく書かれている本があれば教えてください P→Q∨Q→P
に難癖の人は
Qが真である時P→Qが必ず真になることを認めないのね 「Aでないと立証できないならばAである」
あるいは
「Aであると立証できないならAではない」
と主張する誤りです 嘘かどうかはわからない
「肯定する証拠がない」から「ゆえに否定される」は導けません
「否定する証拠がない」から「ゆえに肯定される」は導けません
論理構造 証拠の定義から頑張らないといけない。
証拠が存在そのものを指してるのか、発見された事実を指しているのかでぜんぜん違う。 >>404
何に付いてあなたが「誤りです」って言ってるか聞いてるんだけど？ >>404
もしかして>>402の人じゃなかった？
にしても下らなさすぎ とにかくさ
Qが真であるときP →Qが真であることはヒルベルトの論理公理の一つなんだけど
これを認めない立場なのね？ P『P →Qが真である』 Q『Qが真である』
P ならば Q である（前提 -- 実質含意）
Q でないならば P でない（その対偶）
Q でない（前提）
従って、P でない（モーダスポネンスによる帰結） >>410
また当たり前なこと書いてる
無意味すぎて笑えるわ 哲学板の論理学スレでやれ
ここは"数理"論理学のスレだ 証拠があるかどうか云々は直観主義と深い関係がありますから仕方ないです まず、善と悪といった相対的な価値を排斥することで
絶対的なシステムが確立されます
必要なのは完璧にして無謬のシステムそのものであり
それを誰がどのように運営するかは問題ではありません
真に完成されたシステムであれば運用者の意志は問われないのです >>413
直観主義でも
Q→(P→Q)
は恒真なんだけど？ 【数学】〈最小超置換問題〉「涼宮ハルヒの憂鬱」のおかげで25年解けなかった数学の難問が解決されるかもしれない［10/25］
https://egg.5ch.net/test/read.cgi/scienceplus/1540441618/ 群の定義ってさ、組(G,c)が ~~ を満たす時 (G,c)を群と呼ぶって感じやん。
ペアノシステムの定義はさ、組(N,f,s)が ~~ を満たす時(N,f,s)をペアノシステムと呼ぶって感じやん。
これってさ、この組の中に等しいを表す関係「=」は要らないのはなぜなん？
これだけで群とかが定義できた事になったとは思わんのだ。 >>417
(恐らく)ZFCを前提とした定義だから
だから、｢∈｣についても言及してないでしょ？
fによるxの行き先である｢f(x)｣についても言及してないでしょ？ いや、通常はZFCなんて強いものは前提にせず等号つき一階述語論理で展開する。 なるほどね そうゆう事だったのか
等号つき一階述語論理ってのはzfcより弱い公理系って認識で合ってる？
「=」の反射率・対象律・推移律だけを定めてるって感じ？ 抽象代数といって確かに一階述語論理の直下で考えることもできるけど、
群を勉強する際に普通に自然数とか使うからZFCの下でも良い 等号はただの同値関係ではなくて、
もう少し特別な性質を持ってるのでそれを含めて公理にしないとダメだよ 今、正規様相論理の有限フレーム性を勉強し始めたんですが、
様相論理って命題論理に結構割いてますね
俺は一階述語論理と様相記号が混じった様相論理をやりたいんだが じゃあ頑張ってFitting & Mendelsohnの"First-Order Modal Logic"でも読んだら
一階述語論理で思い出したが、North-Holland/Elsevierから出てた例の黄色い論理と基礎論シリーズで
Gabbayらが出した"Quantification in Nonclassical Logic"が第１巻だけ出て第２巻は出ず終いだなあ
あのElsevierの黄色のシリーズはもう10年近く新しい巻は出版されずで実質的には既に終わったシリーズと化してるし
（どうも、上のGabbayらの巻がシリーズ第153巻で最も新しく出版された巻みたいだ）
Gabbayって恐ろしい数の専門書やシリーズ等の著者として名を連ねて色々と手をつけるのは良いけれど
続巻をアナウンスしておきながらいつまで経っても出さないのが少なくないから困る
Oxfordの論理ガイドシリーズでもTemporal Logicの第３巻は暫定目次までアナウンスしておきながら出さず終いだし >>427
どうも
一応入手していつか読もうと思います 形式的体系についての議論を進める時でも、一部、形式的体系の言語Lを明確に明示的に定める事無く、
ぼんやりとした感じで言語Lを前提としたかのような感じになって、議論を進める人って居ますよね
こういうのは好きじゃない
くどくても言語Lの所からきちんとやって欲しいね 形式的体系の言語Lの変数記号のリストは
a_0,a_1,a_2,...,a_n,...
である。
として一旦は定めてから、
以後、見やすさの都合上変数記号としてx、y、ｚ、u、、、等も使って良いとする
と断っていくスタイルの方がすんげぇ頭の中にスルッと入ってくる >>430
すまん、
0,1,…,n,…とはなんだ？ 番号づけって自然数の集合Nからある集合Aへの写像aで、a(0)をa_0などと呼ぶってことだよな
形式体系を定義する段階で集合とか写像って扱えるのか？ 漠然として思ってるんだけど、
ゲンツェン流の形式的体系でシーケントを使うのあるじゃないですか
で、カット除去定理の証明に見られるように証明図をグラフ理論でいうところの｢木｣に見立てることってあるじゃないですか
じゃあ、いっそのこと、証明図をグラフ理論の知識を使って解析してほしいなって思うんですよ >>441
グラフ理論とか大したことしてないンすけど？ 集合論のメタ理論にグラフ理論を使ってるのは見たことあるけど、
まああんまり役に立たないんだろうな >>443
って事は実はグラフ理論と集合論･証明論の関係の研究は未開拓分野って事かな >>445
未開拓というよりか
開拓しても仕方ないって感じ 順序数の話だってグラフ理論と関係あるかなって思った事もあります
順序数って位取り記数法みたいな書き方で一意に展開できるじゃないですか
で、このように展開された順序数と有限な木が一対一に対応してるらしいじゃないですか
じゃあ例えば、自然数の無矛盾性証明では証明図と順序数を対応させて、証明図の書き換えが順序数の変化？に対応してるから超限帰納法を使えるって話だったと思いますが、
有限な木との対応があるなら、グラフ理論の観点からの証明もあっても良いのかなってな気にはなります 補足
[数学基礎論講義 不完全性定理とその発展]
の125ページ当たりに順序数と木との対応について一言二言触れていました やっぱ、証明図と有限な木ってめちゃくちゃ対応してる気がするんだけどなぁ〜
ゲンツェン流の形式的体系での証明図を見てるといつも思う カット除去定理の証明では最下式を変えないまま、それより上にある証明図を書き換えて、二重帰納法の仮定を使えるようにする
っていう論法でやってますけど、これが何と言うか…グラフ理論では木の何らかの意味での同型な変換に対応してるんじゃないのかなぁ〜っていう感じです。 俺は全然詳しくないから証明図or順序数 と 有限な木 との関係の話知ってる人居たら教えて欲しいです >>448
だからグラフ理論で解明しなくちゃならないほど大したことしてないからだよって 証明図はある意味ではグラフですけど、それぞれのノードは意味を持ってるから、グラフ理論みたいなノードを統一的に扱うようなの使っても難しいんじゃないですかね
場合分けが多くなって結局やってること変わらなくなりそうです
まあよくは知らないですけど 仮にグラフのメタデータと言えるノードの重み付けの行列みたいに整理するとすると、
メタデータのボリュームが異常に大きくなって、逆に複雑になる。 1つの証明図が与えられた時に、各シーケントを1つのノードにすればいいんじゃないんですか？
定理(最下式)が｢根｣で、始式が｢葉｣というわけですね。つまり、普通にイメージされる木を逆さまにした木を考えます。
例えば、推論規則”カット”に対しては、カットの下式が親ノードで上式の左側のシーケントと右側のシーケントがそれぞれ子ノードに対応する、と。
カット除去定理の証明における二重帰納法は、部分木を帰納法によって｢再整理｣してるようなもんです >>457
それで、最低限いくつのノードを定義すれば応用できるの？ 結論を導き出す論理的な文章を木構造にまとめることができるってだけの主張にしかなってない。 >>458
>>457では1つの証明図に現れるシーケントの個数=ノードの個数になるね
>>459
だから証明図を木構造で捉える事が出来るんなら、グラフ理論の各種定理や議論を援用して証明図の構造や性質について分析ができるんじゃないの？
だからそんな議論があるなら教えて欲しいって>>453で聞いてる >>460
証明図のシーケントに頼ると応用が効かないだろ、事前に定義しておかないといけない。
整理するだけが目的なら形式化された証明図をテキストマイニングしてグラフ構造に出せばいい。
でもそんな事すると膨大になるのは容易に分かるから議論にならない。
なぜ議論にならないかといえば、膨大なノードを前にして効果的な木構造を分析するアルゴリズムがない。
量子コンピューターの出現を待って。 >>461
俺はただ純粋数学的な議論として証明図とグラフの関係を知りたいだけであって効率やアルゴリズムといった側面には関心を持っていないし、
そういう意図でこの話をレスしたわけじゃない
数理論理学の議論では証明図の書き換えによる議論が見られる事があるから、グラフ理論側からの理解が出来るなら知りたいだけ PC使えば純粋数学じゃないっていうのか？証明図は手順（アルゴリズム）に従わないのか？
バカじゃないのか？一般のグラフじゃなくて木構造使う大きな意味は経路が単純化されるからだ。
グラフ理論持ち出してくるなら最低限のものを仕入れてから書き込め。無知すぎる。 >>463
何一人で熱くなってんのか知らんが、根本的に話が噛み合ってない
>>461で膨大なノードやら効率的やらアルゴリズムやら言ってるけど、そもそもそんな話してない
PC使うから純粋数学かそうでないかとかそんな話もしてない
証明図を使うからアルゴリズムがなんやらかんやらってのもそんな話してない
経路が単純化されるってのがどういうことか知らんが、俺は理論に興味あるだけで量子コンピューターとかのワードが出てくる時点で完全な筋違いだし、俺が言ってる事理解してない
例えて言うなら、ゲーデルの不完全性定理の証明のために形式的体系の各種概念をゲーデル数化して自然数論における議論に持ち込んでるけど、
お前が言ってるのは｢そんなゲーデル数化してもあまりにも膨大な数過ぎる〜｣っていうようなもん
俺はそんな事聞いてない
もういい、答えなくて言い。お前に聞いても期待した答えは返ってこない事が分かった >>464
いや、だからグラフ理論で分析できることはせいぜいがこれぐらいだと言ってるんだが。 >>415
＞>>413
＞直観主義でも
＞Q→(P→Q)
＞は恒真なんだけど？
「恒真式」即「論理法則」と考えるのは間違い。 >>460
>だから証明図を木構造で捉える事が出来るんなら、グラフ理論の各種定理や議論を援用して証明図の構造や性質について分析ができるんじゃないの？
そんな大したことしてないって >>466
は？
Q→(P→Q)
が真であると認めるのかってことを聞いてるだけだよ
そんなことすら言えないの？ >>466
もうちょっとかみ砕くと
Qが真であると証明されたとしましょうと
そのとき
P→Qも証明されると考えるのかを聞いてます ロープの結び方って色々あって、各結び方によって強度があります。
勿論そこで言う強度は力のかかる方向や摩擦という物理的側面からの強度っていう意味ですが、
2つの線がお互いに結び、絡まり合う事によるその複雑さに着目した、元の2つの線に分離しにくさを表す位相的な強度っていう概念はありますか？ >>441
線型論理の proof net とかはそういう方向を目指してたね ラッセル−ヒルベルト流にしろ、ゲンツェン流にしろ、[PはＱを内含する]と
［Ｐでないか又はＱである］とが同義であると考えたのが、そもそもの誤り。
Ｐ：［リンカーン大統領は暗殺された］，
Ｑ：［リンカーン大統領 とケネディー大統領はともに暗殺された］
とおいてみよう。ＰはＱを内含しないことは、直観的に見て、明らかである。
即ち、この場合、［ＰはＱを内含する］は偽である。
他方、［Ｐでないか又はＱである］は真である。
一方が偽で他方が真である様な二つの命題が同義である筈はない。 ■メタトロンコンピュータ
メタトロンを集積回路に使用した量子コンピュータの一種
それまでのデジタル式フォン・ノイマン型コンピュータとは
一線を画す桁違いの演算速度と小型化を両立
演算装置と記憶装置の区別がなくサーキットそのものが
絶えず変化することで演算と記憶を
（量子論的に言えば別の宇宙で）行う ■ このスレッドは過去ログ倉庫に格納されています
