数理論理学（数学基礎論） その13
■ このスレッドは過去ログ倉庫に格納されています
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照）
前スレ
数学基礎論・数理論理学 その12
https://rio2016.5ch.net/test/read.cgi/math/1509638068/ >>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はＱを内含する]と
［Ｐでないか又はＱである］とが同義であると考えたのが、そもそもの誤り。
Ｐ：［リンカーン大統領は暗殺された］，
Ｑ：［リンカーン大統領 とケネディー大統領はともに暗殺された］
とおいてみよう。ＰはＱを内含しないことは、直観的に見て、明らかである。
即ち、この場合、［ＰはＱを内含する］は偽である。
他方、［Ｐでないか又はＱである］は真である。
一方が偽で他方が真である様な二つの命題が同義である筈はない。 ■メタトロンコンピュータ
メタトロンを集積回路に使用した量子コンピュータの一種
それまでのデジタル式フォン・ノイマン型コンピュータとは
一線を画す桁違いの演算速度と小型化を両立
演算装置と記憶装置の区別がなくサーキットそのものが
絶えず変化することで演算と記憶を
（量子論的に言えば別の宇宙で）行う >>475
Qが証明されたときP→Qも証明されたと考えて良い？ ＞どうも、M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。
＞
＞例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(￢Ｑ⊃￢Ｐ) で表わされるもののことと
＞信じられていたのだっただが、これは、どうやら、誤りだったようだ。
＞
＞そして、M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［￢Ｑ(ｘ)⇒/x/￢Ｐ(ｘ)］
＞こそが【対偶律】を正しく捉えてたものと考えられる。
＞
＞M_SHIRAISHI氏（たち？）の主張する Logical Reformationは、おそらく、世界を
＞席巻することとなろう。
http://www.age.ne.jp/x/eurms/
http://www.age.ne.jp/x/eurms/Ronri_Kaikaku.html 20年以上続けてるし
> (c) EURMS 1997-2018 20年前だと２ちゃんどころかあめぞうすらないので別の場所でもやっていたということかw どうでもいいが訂正。
20年前だとあめぞうはできて間もない頃か。
まあ1997年にはまだなかった。 そんな呼称で喜ばせることもないんでは？
ただただ下らんと言ってれば良いだけ >>482
＞20年以上続けてるし
≪新千年紀においての論理改革≫
漏れ等 は対象外ってことか？ ＞㌧デモと見える学説に対しては、、一般論として、我々は慎重でなければならないと思う。
＞
＞学問の歴史を振り返ってみれば、最初は、大多数の人間には、㌧デモと思われていた学説が、
＞のちのち、定説となったものが「実に多い」からだ。
＞
＞有名なところでは、地*球*説にしてしかり、地動説にしてしかり、大陸移動説にしてしかり。
＞
＞ド・プロイの電子波説にしても、提唱された当初は、物理学者一般には「物笑いの種」だった
＞し、また、アインシュタインの特殊相対性理論の場合も、最初は、トップクラス物理学者の中
＞」のごく一部の人に認められただけだったという歴史的事実を直視すべきだろう。
＞
＞ここで、ネット数学四天王と呼ばれている面々について考えてみると、まず、マツシン先生に
＞ついては、見るべき理論は無いので、論外として、イマイ爺の場合は、一応、独自の"理論"は
＞」立てているが、なにせ、「程度が低くて」問題にならない。 むしろ、それを読んだ中・高生
＞に"害"を及ぼす怖れのほうが大きいと思われる。 一方、ヤマジンにの例の"証明"のほうは、
＞㌧デモのままで終わると見て間違いないだろう。
＞
＞注目すべきは、エムシラ理論だろう。 四色定理の証明や不可完全性定理についての論考さえも
＞隅っこ扱いされているような、壮大な理論で、ちょっと判断に迷うが、ひょっとすればひょっと
＞するという気持ちを抱かせる「何か」がある。
＞ 今後、何年後以降からは、世界の論理学の教科書はすべてエムシラ理論に準拠したものになる
＞*かも*知れない。 >>490
＞アインシュタインは量子力学に懐疑的であった。
彼は、自身の≪特殊相対性勿論】は落ち論のこと、≪一般性相対性理≫にも
＊懐疑的＊だった。
「統一的場の理論」を追求して、最期はボケて死んだ。 論理改革、ベルトランのパラドックスの解決、20 世紀の確率論の基礎を覆す凄い発見、等々、数学に革命をもたらす成果を続々とインターネット上に発表し、２００７年にはかの有名な ｹﾝﾌﾞﾘｯｼﾞで講演を行なった
ネット数学界の誠意大将軍；エムシラ御大（こと、M_SHIRAISHI氏）を、
２ｃｈで盛大に称えようではありませんか！ エムシラっで女性ではないかって説があるが、どうか？ ７ヶ国語に訳されている、知る人ぞ知る、確率論の「名著」：－
КУРС ТЕОРИИ ВЕРОЯТНОСТЕЙ
（Борис. В. Гнеденко）
英訳： THEORY OF PROBABILITY
邦訳： 確率論教程 Ⅰ，Ⅱ （森北出版）
# この本は。確率論にとって、ルベーグ積分などは「無用の長物」で
あることを示している。 今井，山口の両人と M_SHIRAISHI氏との間には“越すに越されぬ溝”がある。
真性のトンデモである、今井や山口には、当然ながら、シンパやファンは
皆無に等しい。しかし、M_SHIRAISH氏にはシンパやファンが大勢（もちろん、
漏もそのうちの一人だが）おり、そして、そうであるからこそ、氏は fj の
常連であることができ、M_SHIRAISH氏が fj に投稿した記事にはフォローが
わんさと付くことがたびたびである。
M_SHIRAISH氏をトンデモ呼ばわりした者には、そう呼んだ当人がトンデモ
であることになるという“皮肉な運命”が待っている。
松本真吾が、M_SHIRAISHI氏の、次の、明快な文章によって、トンデモで
あることを暴露されてしまったのは有名な話である。
>Shingo Matsumoto stupidly wrote in the message:
><8fq1iu$2mi$1@ipc02.rtri.or.jp>
>
>> 命題は基本的には文です。
>
> ばかもん！
>
> # 「‘赤’という漢字で表わされる≪色≫は、基本的には、
> ≪‘赤’という漢字自体≫ のことです」 と言って、小学生
> たち からさえも 笑われたいのか？
> 「‘赤’という漢字で表わされる≪色≫は、≪‘赤’という漢字自体≫
> のことではない」のと同様、
>［赤は光の三原色の一つである］ という文によって表わされる≪命題≫は、
> ≪［赤は光の三原色の一つである］ という、文自体≫ のことではないワ。
>
> このことは、件（くだん）の命題が、文（sentence）としては 全く別のもの
> である、 “Red is a primary colour of light” なる英文でも表わすことが
> できることからしても、明らかなことだ。 【新しい価値論 ( The Theory of Value )】
商品の価値は、その商品を生産する為に消費される energy ( 単位は erg )
即ち、熱量 ( 単位は cal.) によって決定される。
人：Ａ が、自分が所有する商品ａよりも、人：Ｂ が所有する商品ｂの方が
価値が高いと感じ、一方、人：Ｂ は自分が所有する商品ｂよりも、人：Ａ が
所有する商品ａのほうが価値が高いと感じる時、交換が起きる。
ａとｂとが等価値であると Ａ，Ｂ の双方が感じたならば、交換など起きない。
故に、Karl H. Marx ( 1818 – 1883, 65 ↟ ) が完成したと言われている、
労働価値説は完全なる誤謬なり。■ [Ｐ⊃Ｑ] ⊃ [～Ｑ⊃～Ｐ] は恒真式（tautology）であるが故に
対偶律： 《 [ＰならばＱ] ならば [ＱでないならばＰではない] 》
、 を表わしていると信じられて来た。 しかし、これは誤りであった。
例えば、[Ｐ⊃(Ｑ∨Ｒ)] ⊃[(Ｐ⊃Ｑ)∨(Ｐ⊃R)] はtautologyである
にも拘わらず、《 [Ｐならば(ＱかＲ)] ならば、[ (ＰならばＱである)か、又は(ＰならばRである) ] 》 は
成立しない ■ ＞エムシラっで女性ではないかって説があるが
ああ、乃木坂の白石麻衣？
https://www.youtube.com/watch?v=OnE9sJyJK5E
じゃ、漏れはさしずめまなったん（秋元真夏）ってことでｗ もう数理論理学(数学基礎論)知ってる人このスレにいないからな
哲学板の集合論スレもここと同じ感じだけど同一人物なんかな >>503
ホント、そうだね。
数理論理学の話をしたいね。
今、Jech の set theory を読んでいるんだけど、
generic の separative quotient が generic になることの証明が省かれていて、
わからなくて困っています。誰か教えてください。 基礎論の研究者に聞きたいのですが、
ある定理がACを使って証明出来るのは知られているとした時、
新たにそれがACを使わずに証明出来ると言うことが証明されたら、その証明はどれぐらいの価値がありますか？
…
さっき距離空間の完備化の証明でACを使わないバージョンについてちょっと触れた物なので気になりました。 バナッハ・タルスキのパラドックスが、選択公理より真に弱いハーン・バナッハの定理から導かれることが示されたことはある。
特に重要な成果とは見なされていない。 もう一つ質問なんですが、基礎論を深くはやっていないからこそ抱いてる疑問です。
選択公理は全然自明じゃないから選択公理がないZFでどの程度の証明が出来るかに関心を持つのはごく普通だと思います
でも基礎論の議論(テキスト)でZFC^-という記述でZFCから巾集合公理を除いた物を意味させることがありますが、
巾集合公理はどっからどう見ても自明な公理なのに何でこんな公理を抜いた体型を考えるんですか？
どうせ公理を抜いた体系を考えるなら、正則性公理や置換公理を抜いた体系の方がまだいいような気がド素人には思えてしまいます。 「任意の鎖（全順序部分集合）が上界をもつような順序集合は極大元をもつ．」
↓
正しくは、
「全ての全順序部分集合が上界を持つ半順序集合の全ての元は極大元に含まれる。」 ■ このスレッドは過去ログ倉庫に格納されています
