数学基礎論・数理論理学のスレッド その7
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2010/11/11(木) 22:13:5719世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学のスレッド その6
http://kamome.2ch.net/test/read.cgi/math/1265884076/
0496１３２人目の素数さん
2011/03/26(土) 20:33:19.56それが日本最高峰の教科書と言っちゃうくらいだからな>>188
0497368 ◆jkwVJMjC32
2011/03/26(土) 22:32:27.30正確にははじめてではないですね。
知識と信念の論理という本がはじめてですね。
この本で命題論理・述語論理から
様相論理、デフォルト論理やメンタル・スペース理論まで
まとめて学習しました。
理解できない部分は論理と計算のしくみという本で補填しました。
またこの本で完全性定理や不完全性定理を学習しました。
0498368 ◆jkwVJMjC32
2011/03/27(日) 08:26:17.10動的認識論理DEL（Dynamic Epistemic Logic）の一種で、
公開告知やプライベートなどの多種の言語伝達に依存して
エージェントたちの認識状態が変化するというアイデアによる。
様相論理を基礎にしている。
例
APLにおける文φの意味の公開告知の型がφ！であるとき、
様相演算子を[φ！]、<φ！>と置く。さらに命題ξに対して、
公開告知の後、[φ！]ξが真する。
ξが「K_aχ：エージェントaがχを知っている」で定義されるとき、
公開告知によって[φ！]K_aχが真。
これは公開告知による知識の変化を記述している。
おっしゃられる通り、common knowledge やmutual
knowledge への拡張もされています。
また認識論理の代わりに義務論理を選択することで、
指令論理ECL（Eliminative Command Logic）なども作られました。
関連
DEUL (Dynamic Epistemic Upgrade Logic）
DDEPL（Dynamic Deontic Epistemic Preference
Logic）
Arbitrary Public Announcement Logic (APAL)
Future Event Logic（FEL）
カテゴリ
数理論理学｜計算機科学
0499368 ◆jkwVJMjC32
2011/03/27(日) 09:08:57.64証明可能性論理GLを拡張したもので、さまざま種類があります。
算術的に完全なILMやモンターギュの公理を加えた最小論理IL、
持続公理をILに加えたILPなど。
p、q...は束、
∧、∨、→、⇒は様相論理のオペレータ
定義1
d(p)＝1
d(⊥)＝0
d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1
公理2
略
自分よりも弱い理論の文を自分の中に置き換えて
数学的な性質を比較するという感じでしょうか。
0500368 ◆jkwVJMjC32
2011/03/29(火) 23:09:07.72GL＋述語記号△
二項様相演算子△を以下のように定義する。
理論Tにおける、A△Bの算術的な実現は
TにBの実現を加えたものは、TにAの実現を加えたものを解釈可能である。
つまり、Tの言語の論理式で、
T＋B |― C implies T＋A |― f(C)
となるような比較解釈可能関数ｆが存在する。
定義１
式Aの次数d(A)を次を満たす。
・d(p)＝1
・d(⊥)＝0
・d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1
定義２
ILの公理
K:□(p→q)→(□p→□q)
L:□(p→p)→□p
J1:□(p→q)→(p△q)
J2：(p△q)∧(q△r)→(p△r)
J3:(p△r)∧(q△r)→((p∨q)△r)
J5:(◇p)△p
ILの推論規則
MP
0501368 ◆jkwVJMjC32
2011/03/29(火) 23:09:26.37ILPの公理
ILの公理に以下の公理を加えたもの
P:(p△q)→□((p△q) (永続公理)
定義４
論理式Aと論理Lについて、L+Aとは、
L∪{A}を含む論理式の最小の集合で、
様相論理のMP、置換、必然性の3つの規則において閉じている論理。
定義５
IK4とは、
K、J1、J2、J3、J5に、
4：□p→□□p
を加えた6つの公理とすべてのトートロジーを含む最小の論理式の集合で、
様相論理のMP、置換、必然性の3つの規則において閉じている論理。
定理１
IK4 ⇔ △-free fragment が様相論理K4となるILの部分論理。
定理２
IK4＋PはILPの部分論理。
定理３
IL＝IK4＋L
ILP＝IL＋P＝IK4＋P＋L
定理４
IL、ILPはクリプキ構造で完全。
0502368 ◆jkwVJMjC32
2011/03/30(水) 19:18:55.66Γ_A≡Γ－{A}を論理式の集合、
◎∈{□,◇,￢}を接頭辞としたとき、
◎Γ≡{◎A｜A∈Γ}
Γ△⊥≡{A△⊥｜A∈Γ}
と表現し、推件式は以下のように表現する。
Γ→⊿
定義７
推件式GIK4Pの公理
A→A
⊥→
0503368 ◆jkwVJMjC32
2011/03/30(水) 21:24:29.35論理式Aの部分論理式の集合をSub(A)
Γ∪∆の各論理式の部分論理式の集合をSub(Γ → ∆)で表す。
定義９
GIK4Pの推論規則。
(T→)Γ→∆：A,Γ→∆
(→T)Γ→∆：Γ→∆,A
(cut)Γ→∆,A、A,Π→Λ:Γ,ΠA→ ∆A,Λ
(∧→i)Ai,Γ→∆：A1∧A2,Γ→∆
(→∧)Γ→∆,A、Γ→∆,B：Γ→∆,A∧B
(∨→)A,Γ→∆、B,Γ→∆：A∨B,Γ→∆
(→∨i)Γ→∆,Ai：Γ→∆,A1∨A2
(⊃→)Γ→∆,A、B,Γ→∆：A⊃B,Γ→∆
(→⊃)A,Γ→∆,B：Γ→∆,A⊃B
(△K4P)A,{B,X1,···,Xn}△⊥,Σ→B,X1,···,Xn、Σ→Y1△B、…、Σ→Yn△B：
X1△Y1,···,Xn△Yn,Σ→A△B
0504368 ◆jkwVJMjC32
2011/03/30(水) 21:29:12.26シーケンス計算は、
証明図が奇抜な形をしているため
掲示板に書くことはできませんでした。
0505１３２人目の素数さん
2011/04/03(日) 01:45:35.55これのメリットって何があるの？
0506論理体系の表現能力
2011/04/03(日) 12:08:08.76↑
様相論理（時相論理・認識論理・信念論理...）
↑
中間論理
↑
超直観主義述語論理
↑
超直観主義命題論理
↑
直観主義述語論理
↑
直観主義命題論理
↑
部分構造論理(ランベック計算・線形論理、矛盾許容論理、ウシュカヴィッチ多値論理、ファジー論理、適切論理...)
↑
↑ひくい
大体こんな関係じゃないでしょうか？>>487
0507１３２人目の素数さん
2011/04/05(火) 19:08:36.22今夜からΩ-論理の説明をはじめましょう。
0508１３２人目の素数さん
2011/04/05(火) 20:39:42.43勉強したら答えられるようになりますって意味だったの？
勉強したての人間の説明は何が本質的なのか全然分かんないから勘弁してほしい
0509１３２人目の素数さん
2011/04/05(火) 21:28:09.34上記のリストにΩ-論理はない。
0510１３２人目の素数さん
2011/04/06(水) 10:18:46.30http://hatsukari.2ch.net/test/read.cgi/news/1302019119/l50
0511１３２人目の素数さん
2011/04/06(水) 11:09:08.03凄い発見だな！僕は自分の人生さえ割り切りが付かないぞ！
0512１３２人目の素数さん
2011/04/06(水) 22:33:49.350513１３２人目の素数さん
2011/04/06(水) 23:42:36.65現在仏教論理は主流ではないですね。
量化が特殊なので非常に研究が難しい。
イスラエルでマルグリス（超剛性定理で有名な）らにより
研究されているキリスト教的論理学との関連が指摘されています。
キリスト教的論理学の推論規則ではほとんどの仮定が落ちません。
0514１３２人目の素数さん
2011/04/07(木) 08:01:16.270515１３２人目の素数さん
2011/04/07(木) 08:03:17.550516１３２人目の素数さん
2011/04/07(木) 13:06:25.300517１３２人目の素数さん
2011/04/08(金) 20:06:05.60> Taoのblogに載ってたようなcommon knowledge的な話とかかな？
え？
テレンス・タオってロジックにも進出しているの？
天才に来られると萎縮するわ...
0518１３２人目の素数さん
2011/04/09(土) 19:12:13.38N型推論図（フレーゲ流）はNKなどの公理を持たない体系で、
仮定を落とすのを記述するのに使われることが多いです。
L型推論図はシーケント計算など仮定がない体系で使われます。
一般的な数学はNKのN型推論図などを用いると表現しやすいです。
シーケント計算のL型推論図は様々な論理式を
証明するのに下から辿れるので使いやすいです。
本によっては → が |― と書かれていたりしてまちまち。
またHKは仮定がないのでL型で書かれることが多いです。
（HKは公理の変形が複雑だが部分構造論理で使われるそうな）
それから論理式の左側にtermと呼ばれるものをつけて、
証明の経路を辿れるようにしたものもありますね。
この際、NKの仮定をラムダ項に対応させることが出来、
カリー・ハワード対応と呼ばれることもあります。
仮定の落ちる回数に制限を設ける論理もあったと思います。
0519１３２人目の素数さん
2011/04/09(土) 19:16:06.90答えられるので何でも聞いて良いですよ。
0520１３２人目の素数さん
2011/04/10(日) 21:52:24.80これを知らないから無駄な努力をしてしまう。
0521１３２人目の素数さん
2011/04/13(水) 23:51:38.10岩波書店5月 『数学基礎論』新井敏康 著
ttp://www.iwanami.co.jp/hensyu/science/next.html
気合入ってるなあ 楽しみ
みすずから出たトルケル・フランセーンの本もかなり良いよ。
ロジック専攻というレベルじゃなくて不完全性周りが
まさに著者の専門だからかなり細かいことまで徹底的に書いている。
但し著者独自の主張じゃないか、と思うようなことも無いではないけどね。
訳者の田中先生って今どうしてるんだろうか。
今年春に東工大で講演会やるみたいな話あった気がするけどどうなってるのかな。
0522１３２人目の素数さん
2011/04/14(木) 07:08:42.36メドベージェフ次数が日本に紹介されるまではまだかかるでしょうね。
0523１３２人目の素数さん
2011/04/14(木) 08:18:58.100524１３２人目の素数さん
2011/04/14(木) 19:12:25.74後は英語の世界。
0525１３２人目の素数さん
2011/04/14(木) 19:20:30.70内容は Shoenfield のと同じようなもん？
0526１３２人目の素数さん
2011/04/14(木) 20:55:12.37Shoenfield は証明論がなかったですよ。
それから計算理論が何を指しているのかが分かりません。
ページ数が気になりますね。
解説を読む限り強制法にも触れてそうですね。
ただメドベージェフ還元まではいかないと思いますね。
0527１３２人目の素数さん
2011/04/14(木) 21:34:06.560528１３２人目の素数さん
2011/04/14(木) 21:39:51.30ゲーデルが証明したのに近い不完全性定理を導入するってことですか。
算術的階層やペアノ算術までいくShoenfieldよりは進まないということかな。
0529１３２人目の素数さん
2011/04/14(木) 22:15:29.27入門篇で原始帰納関数、基礎編で超限帰納法やるんじゃないだろうか。
0530１３２人目の素数さん
2011/04/15(金) 00:58:48.51新井先生の専門とかから考えるなら、
再帰的Mahlo順序数とかを使うKP（ZFの断片）に対する順序数解析とかに
触れたりして現代の証明論を紹介したいのかな、とか思ってるんだけど。
PohlersのProof Theory: The First Step into Impredicativity（11章）とか
RathjenのThe art of ordinal analysis
www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf
とかの後半（2.2. Set theories.以降）とか。
新井先生のhttp://arxiv.org/abs/1102.0596で言うなら4 Jäger以降の内容。
ちょっと希望的観測過ぎるか。
0531１３２人目の素数さん
2011/04/15(金) 20:27:40.850532１３２人目の素数さん
2011/04/16(土) 01:08:11.68モデル理論とはどのようなものなんでしょうか
ゲーデルあたりの研究成果を元に生まれたとは聞いたんですが
0533１３２人目の素数さん
2011/04/16(土) 07:46:53.790534１３２人目の素数さん
2011/04/16(土) 17:24:57.55タルスキが最初だよ。
ゲーデルと並行して研究されてた。
0535１３２人目の素数さん
2011/04/16(土) 22:55:12.90>>534
なるほど
「モデル」がどういう意味なのか分からなくて困ってましたが
要は意味論のことなんですかね
ありがとうございました
0536１３２人目の素数さん
2011/04/16(土) 23:57:38.441階述語論理の意味論は構造と呼ばれており、
この構造である理論のどんな論理式を解釈しても、
真になれば構造が理論のモデルになるとされますね。
つまりある理論を「まともに」解釈できる構造のことですね。
無矛盾な理論はモデルをもつ。
という完全性定理がモデル理論の初期の研究成果です。
それからコンパクト定理とレーベンハイム・スコーレムの定理は
どんな本にも載っていますね。
例えば、
可能世界で有名なクリプキ構造は様相論理のモデル、
チューリング・マシンはある計算理論のモデル、
2^ωが型なしラムダ計算のモデルになったりしますね。
ハインティング代数やブール代数などの代数的構造を
モデルにすることで、論理学を代数にする手法もあります。
モデル間の同型写像を考えて構造同士の関係・分類もできます。
連続体仮説のZFCからの独立性を証明する強制法のアイデアも
提供しておりますし、モデル自体をZFC上で形式化する研究もあります。
また様々な階数の述語論理を計算の複雑さの階層
（EXPとかPSPACEとかNPとか...）に対応させ、
算術的階層などと組み合わせて現代数学の全体像を浮かび上がらせる
記述計算量理論というものにもアイデアを提供してます。
大雑把にいって証明論に対して存在しているようにも思われます。
0537１３２人目の素数さん
2011/04/17(日) 00:03:25.54つまりある理論を「まともに」解釈できる構造のことですね。
↓
つまりある理論を「正当に」解釈できる構造のことですね。
まともでない解釈も存在しますからね。
0538１３２人目の素数さん
2011/04/17(日) 11:25:13.19面白そうですね
丁寧にありがとうございました！
0539１３２人目の素数さん
2011/04/22(金) 21:46:08.83これっていくつ位存在するんですか？
リストみたいなものってありますか？
それから今使われてる公理はなぜ使われるようになったんですか？
0540１３２人目の素数さん
2011/04/23(土) 08:16:45.01たぶん自分で独自に選んで本書く人も多いんじゃないかな
0541１３２人目の素数さん
2011/04/23(土) 11:40:28.66http://yuzuru.2ch.net/test/read.cgi/edu/1291023518/l50
0542１３２人目の素数さん
2011/04/24(日) 00:15:26.75含意断片論理（論理記号が'→'だけのもの）で、
大抵の教科書に出てくる公理のように
メタ変数が3個で論理記号4個でカッコの付け方が正常な論理式の総数だけでも、
ざっと概算したところ100万個を超えた。
一般の命題論理の￢や∧、∨など5種類ほど加えると数十億に到達するらしい。
公理選択で重要なのは、「独立」を調べること。
MPを推論規則にもつとき、
A→A
A→A→A
A→A→A→A
の3つで上の2つの文は下の文から証明可能なので公理に不要。
「完全性」「健全性」「独立」などの条件が重要で、
定理自動証明機械なども研究された。
歴史的にほとんどの証明体系が意味から出発している。
にもかかわらずそのほとんどが上記条件を満たすのである。
0543１３２人目の素数さん
2011/04/24(日) 07:10:00.79カッコの付け方が位相みたいに、
シンプルに計算できないので正確ではないですが。
0544１３２人目の素数さん
2011/04/24(日) 13:39:01.16おまいは、命題論理の公理系学んだとき、その独立性チェックしたか？
多くの教科書同様、完全性と違ってしてないはずだ。
0545１３２人目の素数さん
2011/04/24(日) 13:57:23.110546１３２人目の素数さん
2011/04/24(日) 20:39:31.01ある程度意味のあるもの、
例えばLKとの同等性が示せるものだとかに
絞られているわけです。
つまり独立性を示す努力は本の著者というか、
「論理の歴史」が勝手に代替してくれているわけですね。
私が言いたかったヒルベルト流とは推論がMPだけという意味です。
そして独立性の証明は完全性よりはるかに煩雑です。
確かに必須ではありませんが、
無から公理を創造する場合は独立に近くする努力はするべきですね。
0547１３２人目の素数さん
2011/04/24(日) 22:41:45.58少し解りにくいことも解っていて当然なような口ぶりだ。
0548１３２人目の素数さん
2011/04/24(日) 22:53:10.92分かったふりをする人は難解な文を書く
0549１３２人目の素数さん
2011/04/25(月) 01:06:51.10重要でなければ強制法とかの技法も要らない気がするけど。
0550１３２人目の素数さん
2011/04/25(月) 07:12:08.71Principia Mathemticaの公理なんか
独立じゃないことが数十年後に判ったんだぞ
0551１３２人目の素数さん
2011/04/25(月) 11:42:06.24しかし証明が必要になることはまず無い。
0552１３２人目の素数さん
2011/04/25(月) 16:59:17.12公理系そのものの独立性の話の話は区別しないと。
前者は気にするのが普通だし、重要な問題であることも多い。
後者はよほど特別なことがない限り、気にすることはない。
0553546
2011/04/25(月) 20:50:54.18それは私のレスポンスに関するものでしょうか。
そうであるとしたら具体的どこに高等趣味があるのかを、
該当箇所の引用したうえで述べてください。
>>551
詳しそうなので質問します。
独立の証明の有益な方法はありますか？
それから証明する必要がないとはいえ、
テキスト中のHKは大抵独立だったり完全だったり
無矛盾だったりして、
「子供が安全に遊べるように人為的に作ったアスレチック」で
あることが多いとは思いませんか？
>>548>>550>>552
同感です。
0554１３２人目の素数さん
2011/04/25(月) 21:04:40.480555１３２人目の素数さん
2011/04/25(月) 21:22:09.770556546
2011/04/25(月) 21:23:12.91ローマに入ればローマに従えというか、
論理学を語る時だけ独特の文体になることは確かだと思います。
しかし、文章の中に含まれる専門用語は他の数学に比べれば
かなり少ないと思いますが？
（まさか専門スレッドでテクニカルターム禁止だというわけでもないだろうし。）
それに難解なことなんか言ってないんですよ。
普通に1階述語論理までやっていれば言いたいことは
分かると思うんですが。
0557１３２人目の素数さん
2011/04/25(月) 21:34:54.22英語のことわざとごっちゃにするなよ、半可通
0558546
2011/04/25(月) 21:45:09.44>郷に入っては郷に従えだ
あえてローマに入ればローマに従え
といったんですが。
意図的に日常さはんじをちゃめしごとと読んだり、
既出をガイシュツと呼んだりする、
当たり前だのクラッカーみたいなノリで言ったんですよ。
これに関して本気で突っ込むそちらの方が半可通なのでは？
0559１３２人目の素数さん
2011/04/25(月) 21:58:46.820560１３２人目の素数さん
2011/04/25(月) 23:02:07.210561１３２人目の素数さん
2011/04/26(火) 00:10:16.55ばーか
0562１３２人目の素数さん
2011/04/26(火) 07:15:02.06Shoenfieldの第一章の演習問題は独立性を公理それぞれに対して証明しているよね
著者がそういう細かいことにこだわる人だったのかもしれない
0563１３２人目の素数さん
2011/04/26(火) 11:09:34.17> 与えられた体系の中での命題の独立性と、
> 公理系そのものの独立性の話の話は区別しないと。
前者はどういう意味?
ある形式系で命題が形式系の他の公理から独立なら
それは公理として認めないと真には成り得ないけど?
後者の「公理系そのものの独立性」って公理系が何対して独立なの?
0564１３２人目の素数さん
2011/04/26(火) 11:11:21.23独立でない公理があるなら、それは公理としては不必要なんだから、
基礎論的な意識の強い学者は当然こだわるわな。
0565１３２人目の素数さん
2011/04/26(火) 18:31:40.30そういう根本的なことから理解出来てないと、ビックリする
0566１３２人目の素数さん
2011/04/26(火) 20:05:38.43それから証明可能なすべての論理式の集合をS、T、
ある公理または推論規則をA、
S＝T∪{A}
としたとき、
TでAが証明できない。⇒SでAは独立。
Aが任意⇒Sは独立。
独立性証明のテクニック⇒3値論理。
0567１３２人目の素数さん
2011/04/26(火) 20:22:28.23正直もう二度と見たくなかったが。
0568１３２人目の素数さん
2011/04/26(火) 20:25:18.26誤
Aが任意⇒Sは独立。
正
上記条件プラスAが任意⇒Sは独立。
計算機科学とかでは体系が
独立じゃないと一般的に色々複雑になるらしい。
0569１３２人目の素数さん
2011/04/26(火) 21:04:15.53集合論のZFとかだと各公理は独立じゃなかったりするでしょ。
独立性が大事かどうかというと、あまり大事じゃない場合も多い。
少なくとも完全性に比べると些事。
>>566
一般的にはAも￢Aも証明できないときに「独立」という気がするけど。
反証可能な場合は普通は含めない。
あとAが任意って何が言いたいのか分からない。
任意の式Aが証明不可能だということはあり得ない。
三値の真偽値の割り当てで証明不可能性が証明できることもあるけど
証明できないことも多いと思う。
0570１３２人目の素数さん
2011/04/26(火) 21:07:16.28ここはエレキな人が多過ぎて困りますなあw
0571566
2011/04/26(火) 22:10:07.14「ある公理系Sの中の公理（推論規則）Aが「独立」である。」
というのは、その公理系SからAを取り除いた
公理系Tの公理・推論規則とそれから証明可能な式だけで
Aを証明できないことをいう。
さらにその公理系Sの中のすべての公理と推論規則が独立なら
公理系Sは独立。
という主張をうまく書こうとしたところ変な文章になっただけです。
なぜ、「Aも￢Aも証明できないときに「独立」」という定義に
しないかといえば、
￢という記号が公理系で必ずしも定義されているか不明だからです。
（公理的集合論やるなら気にしなくてもいいかもしれませんが。）
例えば￢AがA→⊥のメタ理論的な略記だとしても、
⊥が公理・推論規則に含まれていないために、
単なる命題変数になっている場合もあるかもしれません。
それから3値論理はそういう方法もありますよ、位に行っただけです。
一般的に独立を証明する巧い手段は知りません。
0572１３２人目の素数さん
2011/04/27(水) 00:21:21.26どうすれば良いのか想像もつかないけど……
0573１３２人目の素数さん
2011/04/29(金) 08:43:43.06上の論理式の総数みたいなやつです。
0574１３２人目の素数さん
2011/04/29(金) 09:47:53.770575１３２人目の素数さん
2011/04/29(金) 23:10:35.52＞意図的に日常さはんじをちゃめしごとと読んだり、
＞既出をガイシュツと呼んだりする、
＞当たり前だのクラッカーみたいなノリで言ったんですよ。
若者＝バカモノっていうのはホントだね。
ホルモンが無駄に出てるせいかな？
0576１３２人目の素数さん
2011/04/29(金) 23:29:08.45仮に若かったって若者が皆バカって訳じゃないと思うけどなあ
0577１３２人目の素数さん
2011/04/29(金) 23:44:05.25それ「独立 independent」じゃなくて普通に「証明不可能 unprovable」で良い話だよね
0578１３２人目の素数さん
2011/04/30(土) 10:50:22.25大抵の論理学の本に書かれている定義に準拠しているなら、
独立は証明不可能より条件が強いと思います。
独立性は「公理と推論規則に無駄がない」という主張です。
証明不可能は理論の持つ公理と推論規則だけで
特定の論理式の証明図が書けないという主張です。
0579謝罪
2011/04/30(土) 10:56:05.79を読み返してみたところ間違っていました。
「ある公理系Sの中の公理（推論規則）Aが「独立」である。」
というのは、その公理系SからAを取り除いた
公理系Tの公理・推論規則とそれから証明可能な式だけで
Sで証明可能な式でTでは証明できないものが存在すること。
でした。
0580１３２人目の素数さん
2011/04/30(土) 11:18:11.62謝罪を受理しました。
では続きまして、『賠償』を求めます。
宜しくお願い致します。
0581１３２人目の素数さん
2011/04/30(土) 12:13:51.50単に公理と推論規則に無駄がないって言えばいいんだと思う。
加えて言うと、独立性はもちろんのこと、
完全性や無矛盾性さえ体系には必要ない。
0582１３２人目の素数さん
2011/04/30(土) 16:41:03.73公理系に肯定を付け加えても、否定を付け加えても矛盾しないってことです。
無駄がないとかアホか。
0583１３２人目の素数さん
2011/04/30(土) 19:01:36.700584１３２人目の素数さん
2011/04/30(土) 19:56:17.91これと>>582は同値だけど、こっちの方が良く見かける。
0585１３２人目の素数さん
2011/04/30(土) 20:34:00.85意図を明示しないでもってまわった記述をするから高踏的って言われるんだよ。
0586１３２人目の素数さん
2011/04/30(土) 22:05:18.03揚げ足ですが、
普通公理系って閉論理式の集合だから
推論規則は入らないと思いますよ。
形式体系とか言った方が無難だと思います。
0587１３２人目の素数さん
2011/04/30(土) 22:08:55.34>>582より弱くなるはずだけど。
0588１３２人目の素数さん
2011/04/30(土) 22:19:28.530589１３２人目の素数さん
2011/04/30(土) 22:21:07.74様相論理みたいにS3とS5は証明できる式が違うとか
そういうことをやりたい場合の独立性の話をしてた訳ね
ヒルベルト式の述語論理に限って言えば、
ああいう体系の独立性を調べる作業は
ただの面倒くさいだけのパズルに過ぎないと思う
あと、カット除去定理があるからsequent計算のカット規則は「独立」ではないわけだけど
だからといって無駄がある、というような見方が如何に浅薄かというのも
証明論の本によく書いてあると思うけどね
カットを使わないと証明の長さが指数関数的に長くなる
>>581
無矛盾性は大抵の場合は必要だけどね
0590１３２人目の素数さん
2011/05/01(日) 07:36:51.86> 現代数理論理学序説みたいに部分構造論理とかBCK論理の話とか、
> 様相論理みたいにS3とS5は証明できる式が違うとか
> そういうことをやりたい場合の独立性の話をしてた訳ね
この場合の独立性以外ってのは例えばどういったものがあるのでしょうか？
0591１３２人目の素数さん
2011/05/01(日) 09:26:47.68結果自体の意義としては、独立だと分かったからどうなの？
ということになっちゃうので、あくまで独立性を示すためには
新しい真偽値もどきを定義したりしてこういうことをやるんだよ、
というテクニックの習得のためだけに設けられた演習問題だと思う
0592１３２人目の素数さん
2011/05/01(日) 22:58:39.80体系の強さが相対的に比較できれば良いだけ。
ある論理式が証明できるかどうかに着目しているため、
体系自体の独立性が問題になることはない。
また否定のない体系ではすべての論理式が証明可能であるため、
あまり意味のない体系になる、零環やX/=みたいな
数学的に面白みのない構築物になる。
根源まで戻れば論理学も所詮組み合わせ論的構造の産物でしかないし、
意味のない構造が無数に作られる。
こういった主張をするのならばそれは、
「すべての数学はグラフ理論（または数論、2進数）で書きかえられる。」
といった、「数学は記号で書かれている。」といった主張と
同レベルの無意味な議論になってしまう。
もちろん根源はバベルの図書館的宇宙における
カオス的情報の広がりへと到達してしまい
人類は自ら数学という精神活動を停止させることになる。
0593１３２人目の素数さん
2011/05/01(日) 23:00:30.52誤：また否定のない体系ではすべての論理式が証明可能であるため、
正：また否定のない体系ではすべての論理式が定理であるため、
0594１３２人目の素数さん
2011/05/02(月) 01:39:50.54書いていることに気づかないのかなあ。
0595１３２人目の素数さん
2011/05/03(火) 12:31:38.14ススリン線を加えたZFでも
ストリクト・ヴァイハードの定理は成り立つのでしょうか？
0596１３２人目の素数さん
2011/05/03(火) 22:00:08.65￢SHならGCHやdiamondを加えたものでも成り立つ。
■ このスレッドは過去ログ倉庫に格納されています