数理論理学(数学基礎論) その13

1132人目の素数さん2018/07/28(土) 04:58:13.63ID:cuNdeNig
数学基礎論は、数学の基礎づけを目的として誕生したが
現在では、数理論理学として、証明論、再帰的関数論、
構成的数学、モデル理論、公理的集合論など、 多くの分野
に分かれ、極めて高度な純粋数学として発展を続けています。
(「数学基礎論」という言葉の使い方には、専門家でも
若干の個人差があるようです。)
応用、ないし交流のある分野は、計算機科学の諸分野や、
代数幾何学、英米系哲学の一部などを含み、多岐にわたります。
(数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照)

前スレ
数学基礎論・数理論理学 その12
https://rio2016.5ch.net/test/read.cgi/math/1509638068/

424学術2018/10/26(金) 15:29:14.57ID:QQT4Zu9Q
等号は時間の流れも表現されているのかなあ。

425132人目の素数さん2018/10/27(土) 18:59:51.23ID:OAQWCVH9
ヒルベルト空間でユニタリ変換するとどうなりますか

426132人目の素数さん2018/10/31(水) 10:11:11.49ID:QQVQ79oj
今、正規様相論理の有限フレーム性を勉強し始めたんですが、
様相論理って命題論理に結構割いてますね
俺は一階述語論理と様相記号が混じった様相論理をやりたいんだが

427132人目の素数さん2018/10/31(水) 15:12:50.41ID:6XQHYcTU
じゃあ頑張ってFitting & Mendelsohnの"First-Order Modal Logic"でも読んだら

一階述語論理で思い出したが、North-Holland/Elsevierから出てた例の黄色い論理と基礎論シリーズで
Gabbayらが出した"Quantification in Nonclassical Logic"が第1巻だけ出て第2巻は出ず終いだなあ
あのElsevierの黄色のシリーズはもう10年近く新しい巻は出版されずで実質的には既に終わったシリーズと化してるし
(どうも、上のGabbayらの巻がシリーズ第153巻で最も新しく出版された巻みたいだ)

Gabbayって恐ろしい数の専門書やシリーズ等の著者として名を連ねて色々と手をつけるのは良いけれど
続巻をアナウンスしておきながらいつまで経っても出さないのが少なくないから困る
Oxfordの論理ガイドシリーズでもTemporal Logicの第3巻は暫定目次までアナウンスしておきながら出さず終いだし

428132人目の素数さん2018/10/31(水) 21:02:36.31ID:APEXx/Lm
>>427
どうも
一応入手していつか読もうと思います

429132人目の素数さん2018/11/02(金) 03:29:13.35ID:91PxBCJX
形式的体系についての議論を進める時でも、一部、形式的体系の言語Lを明確に明示的に定める事無く、
ぼんやりとした感じで言語Lを前提としたかのような感じになって、議論を進める人って居ますよね

こういうのは好きじゃない
くどくても言語Lの所からきちんとやって欲しいね

430132人目の素数さん2018/11/02(金) 03:31:49.91ID:91PxBCJX
形式的体系の言語Lの変数記号のリストは
a_0,a_1,a_2,...,a_n,...
である。

として一旦は定めてから、
  以後、見やすさの都合上変数記号としてx、y、z、u、、、等も使って良いとする
と断っていくスタイルの方がすんげぇ頭の中にスルッと入ってくる

431132人目の素数さん2018/11/02(金) 08:24:27.41ID:xb7GbTqB
>>430
すまん、
0,1,…,n,…とはなんだ?

432132人目の素数さん2018/11/02(金) 08:27:55.54ID:oA9f+JQU
>>431
番号

433132人目の素数さん2018/11/02(金) 09:35:27.25ID:QXzJaN/A
番号づけって自然数の集合Nからある集合Aへの写像aで、a(0)をa_0などと呼ぶってことだよな
形式体系を定義する段階で集合とか写像って扱えるのか?

434132人目の素数さん2018/11/02(金) 09:42:17.81ID:oA9f+JQU
>>433
別に問題じゃない

435132人目の素数さん2018/11/02(金) 10:49:07.35ID:JvjPlO0/
メタと対象ですね

436132人目の素数さん2018/11/02(金) 11:34:37.26ID:ha8RQU4X
>>434
kwsk

437132人目の素数さん2018/11/02(金) 12:05:52.90ID:JvjPlO0/
それらはメタだからです

438132人目の素数さん2018/11/05(月) 16:55:04.63ID:YXMj6qLJ
実にメタメタだな

439132人目の素数さん2018/11/05(月) 18:38:18.28ID:6Tv9bMav
>>437
くっさ

440学術2018/11/05(月) 19:48:13.88ID:L/ZbDetp
宇宙んジル

441132人目の素数さん2018/11/06(火) 16:26:43.55ID:BCtXnUvk
漠然として思ってるんだけど、
ゲンツェン流の形式的体系でシーケントを使うのあるじゃないですか
で、カット除去定理の証明に見られるように証明図をグラフ理論でいうところの「木」に見立てることってあるじゃないですか
じゃあ、いっそのこと、証明図をグラフ理論の知識を使って解析してほしいなって思うんですよ

442132人目の素数さん2018/11/06(火) 18:23:12.41ID:+diz5PBl
>>441
グラフ理論とか大したことしてないンすけど?

443132人目の素数さん2018/11/06(火) 18:40:41.85ID:vah1Z03K
集合論のメタ理論にグラフ理論を使ってるのは見たことあるけど、
まああんまり役に立たないんだろうな

444132人目の素数さん2018/11/06(火) 18:46:24.25ID:jOazYBXJ
555

445132人目の素数さん2018/11/07(水) 01:35:44.13ID:hNmG+7MR
>>443
って事は実はグラフ理論と集合論・証明論の関係の研究は未開拓分野って事かな

446132人目の素数さん2018/11/07(水) 02:28:41.57ID:oRO0cRNI
>>445
未開拓というよりか
開拓しても仕方ないって感じ

447132人目の素数さん2018/11/07(水) 02:39:44.90ID:DXrrwGJH

448132人目の素数さん2018/11/07(水) 02:40:58.09ID:hNmG+7MR
>>446
なんで?

449132人目の素数さん2018/11/07(水) 06:41:56.55ID:hNmG+7MR
順序数の話だってグラフ理論と関係あるかなって思った事もあります

順序数って位取り記数法みたいな書き方で一意に展開できるじゃないですか
で、このように展開された順序数と有限な木が一対一に対応してるらしいじゃないですか
じゃあ例えば、自然数の無矛盾性証明では証明図と順序数を対応させて、証明図の書き換えが順序数の変化?に対応してるから超限帰納法を使えるって話だったと思いますが、
有限な木との対応があるなら、グラフ理論の観点からの証明もあっても良いのかなってな気にはなります

450132人目の素数さん2018/11/07(水) 06:43:32.90ID:hNmG+7MR
補足
[数学基礎論講義 不完全性定理とその発展]
の125ページ当たりに順序数と木との対応について一言二言触れていました

451132人目の素数さん2018/11/07(水) 06:45:52.16ID:hNmG+7MR
やっぱ、証明図と有限な木ってめちゃくちゃ対応してる気がするんだけどなぁ〜
ゲンツェン流の形式的体系での証明図を見てるといつも思う

452132人目の素数さん2018/11/07(水) 06:49:44.52ID:hNmG+7MR
カット除去定理の証明では最下式を変えないまま、それより上にある証明図を書き換えて、二重帰納法の仮定を使えるようにする
っていう論法でやってますけど、これが何と言うか…グラフ理論では木の何らかの意味での同型な変換に対応してるんじゃないのかなぁ〜っていう感じです。

453132人目の素数さん2018/11/07(水) 06:50:46.15ID:hNmG+7MR
俺は全然詳しくないから証明図or順序数 と 有限な木 との関係の話知ってる人居たら教えて欲しいです

454132人目の素数さん2018/11/07(水) 09:09:08.67ID:oRO0cRNI
>>448
だからグラフ理論で解明しなくちゃならないほど大したことしてないからだよって

455132人目の素数さん2018/11/07(水) 09:47:16.68ID:WM+Yo4cw
証明図はある意味ではグラフですけど、それぞれのノードは意味を持ってるから、グラフ理論みたいなノードを統一的に扱うようなの使っても難しいんじゃないですかね

場合分けが多くなって結局やってること変わらなくなりそうです
まあよくは知らないですけど

456132人目の素数さん2018/11/07(水) 09:51:47.43ID:L0+9zJeL
仮にグラフのメタデータと言えるノードの重み付けの行列みたいに整理するとすると、
メタデータのボリュームが異常に大きくなって、逆に複雑になる。

457132人目の素数さん2018/11/07(水) 11:31:19.45ID:hNmG+7MR
1つの証明図が与えられた時に、各シーケントを1つのノードにすればいいんじゃないんですか?
定理(最下式)が「根」で、始式が「葉」というわけですね。つまり、普通にイメージされる木を逆さまにした木を考えます。
例えば、推論規則”カット”に対しては、カットの下式が親ノードで上式の左側のシーケントと右側のシーケントがそれぞれ子ノードに対応する、と。
カット除去定理の証明における二重帰納法は、部分木を帰納法によって「再整理」してるようなもんです

458132人目の素数さん2018/11/07(水) 11:38:12.36ID:L0+9zJeL
>>457
それで、最低限いくつのノードを定義すれば応用できるの?

459132人目の素数さん2018/11/07(水) 11:40:40.73ID:L0+9zJeL
結論を導き出す論理的な文章を木構造にまとめることができるってだけの主張にしかなってない。

460132人目の素数さん2018/11/07(水) 11:56:10.06ID:hNmG+7MR
>>458
>>457では1つの証明図に現れるシーケントの個数=ノードの個数になるね

>>459
だから証明図を木構造で捉える事が出来るんなら、グラフ理論の各種定理や議論を援用して証明図の構造や性質について分析ができるんじゃないの?
だからそんな議論があるなら教えて欲しいって>>453で聞いてる

461132人目の素数さん2018/11/07(水) 12:03:32.17ID:L0+9zJeL
>>460
証明図のシーケントに頼ると応用が効かないだろ、事前に定義しておかないといけない。
整理するだけが目的なら形式化された証明図をテキストマイニングしてグラフ構造に出せばいい。
でもそんな事すると膨大になるのは容易に分かるから議論にならない。
なぜ議論にならないかといえば、膨大なノードを前にして効果的な木構造を分析するアルゴリズムがない。
量子コンピューターの出現を待って。

462132人目の素数さん2018/11/07(水) 12:16:33.23ID:hNmG+7MR
>>461
俺はただ純粋数学的な議論として証明図とグラフの関係を知りたいだけであって効率やアルゴリズムといった側面には関心を持っていないし、
そういう意図でこの話をレスしたわけじゃない

数理論理学の議論では証明図の書き換えによる議論が見られる事があるから、グラフ理論側からの理解が出来るなら知りたいだけ

463132人目の素数さん2018/11/07(水) 12:27:59.76ID:L0+9zJeL
PC使えば純粋数学じゃないっていうのか?証明図は手順(アルゴリズム)に従わないのか?
バカじゃないのか?一般のグラフじゃなくて木構造使う大きな意味は経路が単純化されるからだ。
グラフ理論持ち出してくるなら最低限のものを仕入れてから書き込め。無知すぎる。

464132人目の素数さん2018/11/07(水) 12:46:43.51ID:hNmG+7MR
>>463
何一人で熱くなってんのか知らんが、根本的に話が噛み合ってない
>>461で膨大なノードやら効率的やらアルゴリズムやら言ってるけど、そもそもそんな話してない
PC使うから純粋数学かそうでないかとかそんな話もしてない
証明図を使うからアルゴリズムがなんやらかんやらってのもそんな話してない
経路が単純化されるってのがどういうことか知らんが、俺は理論に興味あるだけで量子コンピューターとかのワードが出てくる時点で完全な筋違いだし、俺が言ってる事理解してない

例えて言うなら、ゲーデルの不完全性定理の証明のために形式的体系の各種概念をゲーデル数化して自然数論における議論に持ち込んでるけど、
お前が言ってるのは「そんなゲーデル数化してもあまりにも膨大な数過ぎる〜」っていうようなもん
俺はそんな事聞いてない
もういい、答えなくて言い。お前に聞いても期待した答えは返ってこない事が分かった

465132人目の素数さん2018/11/07(水) 12:54:10.44ID:L0+9zJeL
>>464
いや、だからグラフ理論で分析できることはせいぜいがこれぐらいだと言ってるんだが。

466132人目の素数さん2018/11/07(水) 18:33:45.86ID:Mu9DzDzn
>>415
>>413
>直観主義でも
>Q→(P→Q)
>は恒真なんだけど?

「恒真式」即「論理法則」と考えるのは間違い。

467132人目の素数さん2018/11/07(水) 21:19:46.36ID:oRO0cRNI
>>459
だよねー

468132人目の素数さん2018/11/07(水) 21:20:16.09ID:oRO0cRNI
>>460
>だから証明図を木構造で捉える事が出来るんなら、グラフ理論の各種定理や議論を援用して証明図の構造や性質について分析ができるんじゃないの?
そんな大したことしてないって

469132人目の素数さん2018/11/07(水) 21:22:19.77ID:oRO0cRNI
>>466
は?
Q→(P→Q)
が真であると認めるのかってことを聞いてるだけだよ
そんなことすら言えないの?

470132人目の素数さん2018/11/07(水) 21:24:23.90ID:oRO0cRNI
>>466
もうちょっとかみ砕くと
Qが真であると証明されたとしましょうと
そのとき
P→Qも証明されると考えるのかを聞いてます

471132人目の素数さん2018/11/08(木) 11:38:14.97ID:pf4U07Z+
ロープの結び方って色々あって、各結び方によって強度があります。
勿論そこで言う強度は力のかかる方向や摩擦という物理的側面からの強度っていう意味ですが、

2つの線がお互いに結び、絡まり合う事によるその複雑さに着目した、元の2つの線に分離しにくさを表す位相的な強度っていう概念はありますか?

472132人目の素数さん2018/11/08(木) 11:38:31.82ID:pf4U07Z+
聞く場所間違えました

473132人目の素数さん2018/11/10(土) 09:45:07.20ID:pTcwVLLJ
>>441
線型論理の proof net とかはそういう方向を目指してたね

474132人目の素数さん2018/11/10(土) 10:13:35.24ID:VH0xGtn3
>>473
http://perso.ens-lyon.fr/olivier.laurent/pn.pdf
が初心者にも読みやすそうなのでいづれ読んでみます

新着レスの表示
レスを投稿する