10/11/12 20:59:31
小耳に挟んだことくらいはある方が普通だと思うけど。
23:１３２人目の素数さん
10/11/12 21:21:15
乞食が殺到する程の有効性が無いのだろう
24:１３２人目の素数さん
10/11/12 21:32:12
極小モデル理論とは関係ないの？
25:１３２人目の素数さん
10/11/12 21:59:41
以前書いたが例えば
ヒルベルトの既約性定理をモデル理論で証明
するより、Puiseux級数を使ったりして、
具体的な構造を見る方が重要なんだって。
26:１３２人目の素数さん
10/11/12 22:01:16
基礎論を学ばない言い訳w
27:１３２人目の素数さん
10/11/13 00:33:40
>>22
同意
日本でだって、『幾何的モデル理論入門』 by 板井昌典 （日本評論社）なんて教科書まで一応は出てるんだし
その本にも出てるHrushovskiの仕事ぐらいは知ってる代数幾何屋は少なくないんじゃないの？
少なくともモデル理論は基礎論極右というか基礎論原理主義者の巣窟の証明論よりは
普通の数学者(Mac Lane風に言えば working mathematicians、「現場の数学者」とでも訳すのが正解かな？)にも
「数学の分野として存在意義アリ」と認知されてるんじゃないの？
その点、証明論はなあ
最近は "Applied Proof Theory"なんて本も出てるみたいだけど、コンピュータサイエンスの理論屋にはともかくとして
普通の数学者からはどこまで存在意義を認められてる事やら
28:１３２人目の素数さん
10/11/13 00:53:51
working mathematician は職業数学者じゃねーの？
29:１３２人目の素数さん
10/11/13 02:23:02
今読んでる本にλ計算というのが出てきたんだが、何だこの記号…すげえ見辛い…
30:１３２人目の素数さん
10/11/13 02:51:33
λカリキュラスなんて、あんなもんやってもなあ・・・
31:１３２人目の素数さん
10/11/13 14:38:01
こんちには みさなん おんげき ですか？ わしたは げんき です。
この ぶんょしう は いりぎす の ケブンッリジ だがいく の けゅきんう の けっか
にんんげ は もじ を にしんき する とき その さしいょ と さいご の もさじえ あいてっれば
じばんゅん は めくちちゃゃ でも ちんゃと よめる という けゅきんう に もづいとて
わざと もじの じんばゅん を いかれえて あまりす。
どでうす？ ちんゃと よゃちめう でしょ？
ちんゃと よためら はのんう よしろく
32:１３２人目の素数さん
10/11/13 16:34:39
>>25
一般的には具体的な計算が困難（実際的には不可能）だから非構成的な証明が考案されるわけでしょ。
ゴルダンに戻るわけ？
33:１３２人目の素数さん
10/11/13 17:01:18
ヒルベルトの神学、なんて言われた時代もあったんだってねえ
34:１３２人目の素数さん
10/11/13 17:18:02
数学を形式的に記述していって、例えば実際に微積分まで形式化した人はいるんでしょうか
プリンキピア・マテマティカでさえ実数論までだと聞いていますが
35:１３２人目の素数さん
10/11/13 17:39:00
>>34
ツァリス（ツァリス・エントロピーの考案者）が、
多重線形積分まで形式化した。
トラック・サンジャイロ構成や第3層制限解釈によって
分裂しやすい論理学を生成してからカリー・ハワード対応を与えることで。
36:１３２人目の素数さん
10/11/13 19:43:32
Coq URLﾘﾝｸ(coq.inria.fr) などのアプローチは
>>34 に該当するだろうか
ライブラリには derivative の文字も見えるが
37:１３２人目の素数さん
10/11/28 22:50:53
バートランド・ラッセルのプリンキピア・マテマティカと
ヒルベルトの形式系はどの点で違うんでしょうか？
素人向きの解説書、どなたかご存じありませんか？
38:１３２人目の素数さん
10/11/28 23:03:46
プリンキピア・マテマティカは型付きの体系なのが一番の違い
解説書としては「確かさを求めて」とか
39:１３２人目の素数さん
10/12/17 05:16:50
超数学と数学基礎論の違いを教えてください。
全く異なる分野なのですか,
それとも片方が他方の一分野の関係になっているのでしょうか?
40:１３２人目の素数さん
10/12/18 01:16:09
『算術的命題、すなわち一階算術で記述可能な命題に関しては、
選択公理を使った証明があればそれを使わなくても証明できる。』
この定理の証明が載っている文献をどなたか御存知ありませんか？
41:１３２人目の素数さん
10/12/20 16:53:54
多くの公理的集合論の本に載っている有名な基本的な定理の系。
オリジナルに近いものを読みたいならば、Goedel の本をどうぞ。
Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory.
Princeton University Press
42:１３２人目の素数さん
10/12/20 17:59:37
>>41
ありがとうございます。
趣味で基礎論を勉強している身ですが、やっと公理的集合論に取り掛かる決心がつきました。
43:１３２人目の素数さん
10/12/23 15:45:33
俺もやるよ。
44:１３２人目の素数さん
10/12/29 10:14:23
初歩的な質問で申し訳有りませんが2つ質問させてください
1.
命題論理や一階述語論理よりも基本的な公理系はありますか？
あるのでしたら教えてくださいませんか？
2.
公理的集合論は一階述語論理の上に定義されるから
"公理系"の"系"って公理的集合の一種にはなりませんよね？
だとすると"系"っていったい何なんですか？
"系"を組み立てるための"公理系"が存在してしまったら循環論法になりませんか？
あるいは「まず素朴に定義しておいて、後に公理的集合論を定義したあと、
その素朴な定義が、公理的集合論と矛盾しないことを示す」
みたいな回避方法を取るのでしょうか
45:１３２人目の素数さん
10/12/29 13:25:40
形式化というのは飽くまでも無矛盾性を示したり
或る命題が独立であることを示したり、或いは
証明が厳密に行われることを保障するために行うものなので、
別に循環論法だとかそういうことは無いと思う。
集合論やら述語論理やらを記号列に関する形式的なルールの集まりとして表現した時に、
そのルール自体は、元の理論で直接扱うようなものでは無いんです。
46:１３２人目の素数さん
10/12/29 13:38:38
「より基本的」というのが「証明できる論理式がより少ない」という意味なら
最小論理、直観主義論理、etc...があるけども
47:１３２人目の素数さん
10/12/29 15:47:20
公理系ってのは
あるパラダイムの中でしか
意味を為さない
48:１３２人目の素数さん
10/12/29 15:51:01
そりゃそうだ
49:１３２人目の素数さん
10/12/29 16:04:50
哲学に憧れて厨二的誇大解釈をしてしまう人も稀にいるのかもしれない
50:44
10/12/29 17:08:00
>>45
なるほど・・・
では間接的になら扱うことが可能なのでしょうか
>>46
二階述語論理に対する一階述語論理、
一階述語論理に対する命題論理のような意味での基本的という意味です
論理ではなくて単なる記号の規則でも良いです
51:１３２人目の素数さん
10/12/29 18:25:32
間接的にで良いなら、自己言及「的な」現象が起こることがあって、
その良い例が不完全性定理。
基本的と言うか、より一般的な記号列の機械的な書き換えということになると
オートマトンだとかチューリングマシンだとかの話になるけど、
だんだん数理論理というより計算機科学よりの話になる。
52:１３２人目の素数さん
10/12/30 00:31:12
>>45
完全性定理の証明に選択公理が使われてても問題ないのか？
納得できん
53:１３２人目の素数さん
10/12/30 03:05:37
ゲーデルによる不完全性定理の証明に中国剰余定理が使われているようなもの。
計算量理論の観点からすると問題になるらしく、この定理を使わない改良版もあるそうだ。
54:１３２人目の素数さん
10/12/30 08:05:03
確か前スレに完全性定理と選択公理の話あったぞ
55:１３２人目の素数さん
10/12/30 22:01:05
選択公理を無くせ
56:１３２人目の素数さん
10/12/31 17:24:04
>>54
前スレ見たけどいまいち。
「式の集合」がZFCのモデルになっているとは考えにくいし。
57:１３２人目の素数さん
10/12/31 17:28:09
「式の集合」がZFCのモデルになっているなんて話あったかなあ、
58:１３２人目の素数さん
10/12/31 19:08:16
>>57
あ、そこまでは言ってないや。
でもZornの補題とほぼ同じような論拠で極大理論をもってきてるでしょ。
理論＝公理の集合。つまりは式、というか文字列の集合だし、そんなものが
ZFC（の一部かな？）のモデルになってるわけないや、と。
59:１３２人目の素数さん
10/12/31 20:58:41
ごめん前スレよく見たら131あたりで議論してるね。
有限な立場では完全性定理の証明はできないってところまでは合意済み（？）のようだ。
それと上記の疑問はまた別物と言うことで。
60:１３２人目の素数さん
10/12/31 21:16:55
人間や計算機が実際に扱うような理論は、有限個の記号しか扱わないから
論理式を整列できるし、選択公理も別に要らない。
だから認識論的なことを話題にする限りは別に問題にはならなくて、
選択公理が問題になるのは、そもそも理論で使う基本的な記号の集まり自体が
基数を持たない、みたいな場合なので、別に問題ないんじゃないかと。
61:１３２人目の素数さん
10/12/31 22:54:53
>>60
そうなのか？
記号が有限、個々の論理式の長さは有限、全体としては可算無限まで。
その中から矛盾にならないよう論理式を選んでいって極大理論に至る。
これが論理式が整列できるなら選択公理いらない？
62:１３２人目の素数さん
10/12/31 23:20:03
ところで完全性「定理」っていうけど何理論の定理？
一階述語論理における真理ではあるんだろうけど、「定理」って？
63:１３２人目の素数さん
10/12/31 23:38:16
A1 A2 A3 …：閉論理式の枚挙
①Γ_0 ：無矛盾集合
②Γ_i まで得られたとして、Γ_i+1 を次のように定める
Γ_i │─ ￢A_i+1 ならば Γ_i+1 ＝ Γ_i
Γ_i │─ ￢A_i+1 でないならばΓ_i+1 ＝ Γ_i ∪ { A_i+1 }
Γ_∞ ＝ Γ_0 ∪ Γ_1 ∪ Γ_2 ∪ … と定めると、これは無矛盾かつ完全（どの閉論理式も証明可能or反証可能）
記号が可算個なら閉論理式は可算個なので、
選択公理の替わりに上の事実を用いて極大無矛盾集合を作ればよい
64:１３２人目の素数さん
11/01/01 01:00:12
2011明けましたおめでとう
>>63
各 A_i+1 または ￢A_i+1 を追加する箇所でどっちが無矛盾か判定する手続きはないから作ることはできないよね。
「作ることができる」じゃなくて「存在するよ」だったら言えるのか。
枚挙された閉論理式の集合の冪集合の中に「すべてをうまく選んだ例」が一つは存在するよ、って主張だろうか。
選択公理の使用だけじゃなく他にもいろいろ気になるなあ。
65:１３２人目の素数さん
11/01/01 08:02:53
ゲーデル解釈っぽく考えたら心理的な違和感はだいぶ解消する
つまりＡという命題を「Ａでないということはない」、
「Ｇ（ｘ）となるｘが存在する」を「全てのｘに対してＧ（ｘ）でない、ということはない」と解釈する
66:１３２人目の素数さん
11/01/01 16:16:48
>>65が流れと関係あるのかどうかわからんね。
完全性定理への選択公理の使用有無は>>63にもう一度聞きたいな。
67:１３２人目の素数さん
11/01/01 22:23:43
存在という言葉にこだわるのは楕円曲線を考えるとき楕円をイメージするくらい意味のない行為
68:１３２人目の素数さん
11/01/01 22:31:41
だって素手でやっていい範囲でって言われても、その範囲がわかりにくいじゃん。
楕円曲線とかは抽象的存在と割り切って議論進めてるんでしょ？使っていい道具も決まってるんだろうし。
論理式の集合だと実在してるものを相手にしてる感じだし～
69:東大生
11/01/01 23:13:34
おまえら馬鹿なんだから、蘊蓄はいいよw
70:１３２人目の素数さん
11/01/01 23:18:02
> 蘊蓄
へー、なんて読むんですか～？
71:１３２人目の素数さん
11/01/02 00:32:47
うんち
72:１３２人目の素数さん
11/01/02 01:16:41
くいたい
73:１３２人目の素数さん
11/01/02 02:37:57
eのe乗、πのπ乗、πのe乗が有理数でないことの証明をお願いします。
ウィキのゲルフォントの証明のページで、eのπ乗しか証明されておらず驚きました。
できないものなのでしょうか？
74:１３２人目の素数さん
11/01/02 11:19:17
ここ数論のスレじゃないから。
>>69-72みたいな話するところでもないけど。
75:68
11/01/02 11:45:49
集合論とかの道具を使っていいのかってよりも、成り立たない場合をどう考えればいいのか、とか
正直よくわからないんだよねー。
あれから少しぐぐったところ完全性定理への選択公理の使用有無については
>>63と同じ様なこと書いてあるサイト見つけたんだけど、
URLﾘﾝｸ(ysserve.int-univ.com)
やっぱり冪集合公理や選択公理を使用してるのかしてないのか、成り立つとしていいのか
ダメなのかについて理解が進展しないや。
76:１３２人目の素数さん
11/01/02 15:27:50
そもそも無限公理は使って良いの？
外延性公理は？
77:１３２人目の素数さん
11/01/02 19:44:58
論理式を「実在するもの」と考えるのなら、構文論的に考察することにならない？
述語論理の「意味」なんて考え出したら超越的議論が必要になるのは、感覚的に自然
78:１３２人目の素数さん
11/01/02 22:32:30
>>76
少なくとも無矛盾性を問題にしているときに無限公理を疑うってのは極悪過ぎない？
>>77
論理式を実在物として構文論的に考察しているときのことを言ってるんだが。
「理論」の拡張時に無矛盾性を保ちながら極大集合を得る話でしょ。構文論だと認識してるが。
79:１３２人目の素数さん
11/01/03 00:44:17
>>44
＞公理的集合論は一階述語論理の上に定義されるから
＞"公理系"の"系"って公理的集合の一種にはなりませんよね？
俺も初心者だけど
まさに>>78の言うように「構文論的」に考察しているからこそ
たとえ集合論が一階述語論理を用いて定義されていようが
「一階述語論理で記述された公理系の性質」について調べるときは
公理系を論理式の集合と考えて、集合論という道具を使って調べるんじゃないかな
80:79
11/01/03 00:59:47
>>79の最後が抜けてた
だから公理系は公理的集合の一種になると思う
81:79
11/01/03 01:37:26
ごめん>>80はちょっといろいろ言い切りすぎてるか
「一階述語論理の公理系がなにがしかの性質をもつことを、厳密に示す場合」には
公理系を集合とみなして、集合論を道具として使って議論を進めて
その集合論に基づく議論によって得られた結果をもってして
「一階述語論理の公理系はこれこれの性質をもつことが示された」
と考えるんだと思う。
あと、もちろん、その超数学的議論の中では
その発想のおおもとや意味が有限的なものではない
集合論のいろいろな公理とか、モデルや解釈や
それを集めるとか一つ選ぶとかいった概念が登場するけど
それは普通は問題とは考えない。
・・・あれ、なんだろ
なんか今になって急に恥ずかしくなってきた
もしかして俺、場違い？
82:79
11/01/03 02:11:44
ありゃ
>>52からの流れで
>>56みたいな疑問が出てきて
さらに>>64の論点も追加で出てきて
本当に集合論？という話になってるのか
すいません場違いでした
83:１３２人目の素数さん
11/01/03 02:18:47
極大イデアルの存在を言うために選択公理を使うのは抵抗ないのに
極大無矛盾理論のときはなんかひっかかる
考えてみればおかしな話だ
84:１３２人目の素数さん
11/01/03 02:32:38
公理的集合論を組み立てていくときに
述語論理の完全性だとか、極大無矛盾理論の存在だとかは
無関係、必要ない情報なんじゃないかと思うのだけど
そうして、既に組み立てられた公理的集合論を用いて、
「論理式からなる集合」について一層詳しい性質を調べることは
別におかしくない
85:１３２人目の素数さん
11/01/03 09:50:46
おはよう。
誰が誰やらわからんけど、>>82の言うとおりの流れだと思ってる。
>>84の
>公理的集合論を組み立てていくときに・・・必要ない情報
も、必要な部分だけつまみ食いすればいいだけという意味であってると思うが、
論理式の集合がZFCのモデルになっていると素直には認められないんで、その点で
いろんな立場があり得るんじゃないかと考えてる。
またその流れで>>62の疑問も出てきてる。
86:１３２人目の素数さん
11/01/03 13:04:25
無限公理を疑うのは極悪過ぎる（？）、だから認めて良い、とか
理屈になってないと思うんだけど……
だいたい「論理式の集合がZFCのモデルになっている」
ってどういう意味で言ってるんだろうか。普通こういう言い方はしないと思うけどなあ。
論理式の集合が即理論のモデルになるわけじゃなくて
論理式の無矛盾な極大集合を一つ取って、そいつが持ってる情報から
モデルを組み立てる、ということをやってるだけなんだけど。
87:１３２人目の素数さん
11/01/03 13:48:48
>>86
無限集合の存在を認めて初めて理論の無矛盾性を問題にできるんだから、
理論の無矛盾性を問題にしておきながら無限集合の存在は認めません、という態度は
話にならないと思ったんだが。
論理式の無矛盾な極大集合を一つ取るってことがどうして可能になるの？
論理式の集合がZFCのモデルになってると考えてるからでは？
88:１３２人目の素数さん
11/01/03 13:52:14
＞「論理式の集合がZFCのモデルになっている」
完全性定理の証明の過程で、
一階理論（これはZFCを特別な場合として含む）のモデルの存在を示す
ことを指していると推測
>>86に加えて言うと、
モデルを組み立てられるのは、元々の理論が無矛盾という仮定の下での話
ZFCが本当に無矛盾かどうかは未だに不明
＞論理式の集合がZFCのモデルになっていると素直には認められないんで
これを認めるのは、ZFCが無矛盾であると認めるのと同じこと
89:１３２人目の素数さん
11/01/03 15:31:10
無矛盾ってのはφ ∧ not φがどちらとも証明できてしまうようなことが起きない、
ということなのだから、構文論的にはある記号変形手続きが存在しないことで、
すべての自然数が～～を満たさない、程度のことは扱える必要があるけど
無限集合を扱う必要はないと思うけど。
だいたい完全性定理を前提にしない限り、モデルと無矛盾性は直接関係無い。
とりあえず完全性定理の証明を良く読んで
自分で証明を再構成できるようになるのが一番の近道な気が
90:イスラエルの数学
11/01/03 16:23:33
サラハやシュピロなどによる、
数理論理学・集合論的位相空間論・無限組み合わせ論や保型関数論などの発達が近年目覚しいが、
なぜかまったく話題にならない数学世界。
91:１３２人目の素数さん
11/01/03 16:42:29
保型関数論がどうしてそこに付いてるのか良く分からん
92:イスラエルの数学
11/01/03 17:02:56
シュピロの保型関数研究は有名ですが。
いずれにしろシェラハに全く言及できていない時点で
日本数学界の世界数学からの取り残され感がするのですが。
93:イスラエルの数学
11/01/03 17:08:14
そもそもシェラハのやっている数学を理解できている人間が日本にいるのだろうか。
いまだにグロタンディークで盛り上がるような世界では
Ω-logicもpcf-thoryも知られていないでしょうが・・・。
94:１３２人目の素数さん
11/01/03 17:58:45
>>89
論理式の長さやその総数に制約を付けないという前提で
A ∧ not Aの証明があるか、ないか
を問題にしてるんですよね？
論理式や証明というものが無限にある、という主張などいちいちせずとも構文論的な考察はできる
というのが「無限集合を扱う必要はない」という意味でしょうか？
>>88
中段と後段はわかります。なので
「論理式の集合がZFCのモデルになってると証明できない（←当然だが）だけでなく、
モデルになっていないと感じている」
ぐらいの言い方に変更します。
95:79
11/01/03 19:57:46
すいません
流れが読めてないついでにもうちょっと聞いてみたいんですけど
>>56 = >>88 さんの主張は
「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」
あるいは
「極大無矛盾集合の構成には，ZFCでは許されていない操作が含まれている」
ということなんでしょうか？
それとも
「完全性定理の証明にはなんらかの超越的な公理が必要だが
それはかくかくしかじかの点で問題がある」
ということなんでしょうか？
96:１３２人目の素数さん
11/01/03 21:44:30
>>95
まず>>56 ≠ >>88 なんだけど、自分の主張は
「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」
が一番近いと思う。>>85もそういう気持ちで書いている。
だけど、逆（モデルになっている）の捉え方をされていたかも。（>>86とか>>88とか）
97:79
11/01/03 22:34:08
>>96
56 = 87 と書くつもりが間違えました．ごめんなさい．
＞「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」
＞が一番近いと思う。>>85もそういう気持ちで書いている。
近い，とは・・・？
98:１３２人目の素数さん
11/01/04 00:10:09
＞「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」
ZFCの枠組みの中で、帰納的に定義された集合について調べよう。その集合はたまたまZFCの公理系と読めるものだ。
というだけの話では？
ZFCに用意された記号、論理式をZFCの考察の対象とすることに
自己言及のような気持ち悪さを感じているのだろうか。
はたまた、さらにそこから新しい記号を導入して、元のZFCから拡張されてしまうことになるから、
拡張された体系は一体何物なんだ、ということか。
そうではなくて、例えば…
自然数1を￢ 自然数3を⇒ 自然数5を∀
自然数8n+7を関数記号f_n
等とみなして、これら自然数の（帰納的に定義された）特定の列からなる集合を考える。
ということ。
自己言及ではない。
見当違いの指摘だったらｽﾏｿ
99:１３２人目の素数さん
11/01/04 00:11:55
>>97
とは・・・？ って聞かれても．．．
ただ素朴なモノの集まりとしてみた場合に、集合論が成り立ってる気が全然しないというだけ。
ベキ集合の公理とか、選択公理とか。
100:99
11/01/04 00:21:11
>>98
すれ違いになっちゃったけど・・・
> 記号、論理式をZFCの考察の対象とすること
これ自体は何の違和感も感じてないつもり。
ZFCを拡張してるなんてことも思ってないです。
ごめんなさい。何か決定的な勘違いしてるんじゃないかと不安になってきた。
101:１３２人目の素数さん
11/01/04 03:46:53
>>93
何年か前の数セミでも、PCFは紹介されてた。
102:１３２人目の素数さん
11/01/04 09:17:07
論理式の集まり F があったときにその冪集合の元は別に論理式じゃないんだから
論理式の全体の中でいくら探してもその中に F の冪集合なんか無い訳だけど、
当然の話だし、何も問題ないと思うけどなあ。
論理式の集まりがZFCのモデルになるんじゃなくて
ZFC（のモデル）が論理式を扱える、というだけでしょ。
だからZFCの方に論理式を素朴に扱う上で必要の無い余計な公理
がちょっと位付いててもそんなに大きな問題は無いと思うんだけど。
103:ノニ
11/01/04 17:49:14
>>101
そうでしたか。
日本でシェラハがここまで無視されているのは、
なぜなんでしょうか。
104:ノニ
11/01/04 17:57:07
>>102
一見したところ、それが正しい理解のようでした。
自身をもって結構ですよ。
確かにZFCのモデルは論理式を扱えますが、
それが２階の述語論理に基づくものだということを確かめてくださいね。
バベルの図書館的宇宙はモデルより先にあるのですから。
105:１３２人目の素数さん
11/01/04 19:10:45
うっせ帰れ
106:猫は作業 ◆MuKUnGPXAY
11/01/04 19:42:51
>>105
まあエエがな。ソレともワシがアンタの相手をスルかァ！
猫
107:99
11/01/04 21:53:52
>>102
もともとは完全性定理の証明に超越的な方法が使われているかどうかが
問題だったのに、ZFCのモデルなどという話にしちゃったのは申し訳ないです。
冪集合のこともおっしゃる通り。
で、>ZFC（のモデル）が論理式を扱える ってとこだけど、論理式を素朴に扱う上で
必要の「ある」公理って何を指してますか？
冪集合公理は関係ないとしても、選択公理がそこに含まれるかどうかが最初の疑問
だったわけですが、そこらへんは>>64あたりから前に進めていない気がする。
>>83
環とかは最初から（集合論でいうところの）"集合"として考えるわけで、構成手続きを経て文字から
組み立てられる具体的な論理式は同次元に捉えられないです。
それに極大イデアルの存在は選択公理に依存している、と言うとみんな「その通り」と返してくると思うけど、
極大無矛盾理論のときはそういうすっきりした回答が無いのでは？
108:１３２人目の素数さん
11/01/04 22:52:08
どうしても理論のモデルが欲しいんだい！などと我侭を言わずに
あくまで構文論的に論理式を扱う限りでは
ペアノ算術で充分過ぎるくらいで、実際はもっと弱い算術でも大丈夫。
選択公理ACが無くてもZFはペアノ算術を解釈できますから
論理式の操作も充分扱うことが出来ます。
というか置換公理も基礎の公理も要らないから、
順序数とか使って複雑なことをしたりしない限りZ-とかでも大丈夫。
で、どうしてもモデルとかそれに類する超越的対象が欲しいといったときに
極大無矛盾理論の存在がどの程度超越的なのかについては、
前スレで話が出た通りです。
逆数学的な方向じゃなくてもっと大雑把にZFの上でどうなのかは
あまり調べる気がしませんが、Löwenheim-Skolemの定理が
ACと同値なのは昔から知られているので、仮に完全性定理が
ACと同値だと分かったとして、そりゃあそういう結果が出るだろうなあ、という感じです。
109:１３２人目の素数さん
11/01/04 23:09:36
ストーンの定理、ブール主イデアル、完全性定理が同値でなかったっけ。
110:１３２人目の素数さん
11/01/05 13:01:24
ヒューズの様相論理入門』に
●が定理であるなら□●が定理 必然性規則
●→□● 公理（ここで、●は定理） は駄目
というくだりがあったと思うんですが
反例が思い浮かばずに（思い出せずに、今、手元に本ありません）苦しんでます
なんで駄目なんでしたっけ？
111:１３２人目の素数さん
11/01/05 20:19:48
偶然に真だけど必然的に正しい訳じゃないみたいな例を挙げれば良いんじゃないの？
112:１３２人目の素数さん
11/01/05 21:24:26
A→∀xA がダメなのと同様に考えればいいんじゃないの？
113:１３２人目の素数さん
11/01/05 21:39:33
>>108-109
了解しました。というか何となくすっきりしました。
まあACがない場合どうなるか、という仮定だと面白い結果が無いんでしょうね。
wikipediaでは「一階述語論理における意味論的真理と統語論的立証性の対応を確立した」とか
いかにも絶対に成立する結果のように書いてるけどｗ
114:１３２人目の素数さん
11/01/05 22:49:52
そりゃあ普通、選択公理は認めるものですし…
115:１３２人目の素数さん
11/01/06 20:31:31
田中尚夫の公理的集合論
どこにも売ってねえ（ノД｀）゜。゜。
116:１３２人目の素数さん
11/01/06 20:55:06
もう絶版でしょ
古本で買うしかないけど、今はKunenの訳書あるからなあ
117:１３２人目の素数さん
11/01/07 17:00:07
質問です。アレフって極限基数なんですか? それとも直前の基数が存在するんですか?
証明付きでおながいします。
118:１３２人目の素数さん
11/01/07 17:27:52
Introduction to Cardinal Arithmetic でgoogleブック検索せよ
119:１３２人目の素数さん
11/01/07 20:28:07
なぜにその本
120:１３２人目の素数さん
11/01/08 18:15:24
集合論はPDFがネット上にたくさん転がってるでしょ。
121:猫は作業 ◇MuKUnGPXAY
11/01/08 18:42:30
もうエエかァ？ ほしたらや：
■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■
■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■
■■■■■■■ このスレは他板・他スレ運営妨害の非常に悪質糞スレの為に ■■■■■■
■■■■■■■反感を買って終了しました。 皆様のご愛顧有難う御座いました■■■■■■
■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■
■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■
猫
122:117
11/01/09 21:30:03
>>117
答えは解っているのですか？それとも未解決なんですか？
123:１３２人目の素数さん
11/01/10 00:35:54
どっちも（ZFCから）示せないはず。
2^(aleph 0) が後続基数 aleph(n+1) だと仮定しても
矛盾しないことは昔から分かってる。
（n=0のときGo¨del、nが正の整数のときCohen）
極限基数でも良いんだけど、ただしaleph_ω とかaleph_ω^2とかと
等しくなることは出来ない、というのは簡単に証明できて、
よく一、二年の集合論の期末試験で証明問題として出されたりする。
じゃあどういう極限基数 κ なら良いんだということになると、
少なくとも共終数cf(κ)がωよりも大きくないといけないことは
同様に証明できるんだけど確かこのようなκの存在は証明不可能だったと思う。
つまり敢えて難しく言うと
「「連続体濃度が後続基数であることは証明できない」ということは証明できない」
ということが証明できるということです。
そうは言っても皆「連続体濃度が後続基数であることは証明できない」のは
ほとんど確実だと思ってるんですけどね。
124:１３２人目の素数さん
11/01/10 00:37:45
最後らへん本当にそうなのか不安になって来た。
もっと詳しい人フォローお願いします。
125:１３２人目の素数さん
11/01/10 07:27:12
すみません。どこで質問していいのか判らないのでここかもと思って書いてみました。
親切な方がいたら教えてくれたら嬉しいです。
また、もし「スレチだ、ここに書くな」という人がいましたら、出て行きますが
もしできたら適切なスレを教えて貰えたりすると嬉しいです。
では、質問です。
この問題に詳しい人はこんな質問をすること事態が疑問かもしれませんが
お願いします。
テレビのドラマを見ていて４色定理というものをみました。
URLﾘﾝｸ(ja.wikipedia.org)
これなのですが、以下のような地図の時はどうするのだろうか？ということです。
-------------------------------------------
│ 土地A │
--------------------------------------------
│土地B │土地C │土地D │ 土地E │
--------------------------------------------
こんな形なのですが・・・・
土地B・C・D・Eは飛び地ということなのでしょうか？
宜しくお願いします。
126:１３２人目の素数さん
11/01/10 07:28:31
あっ、ごめんなさい。
-------------------------------------------
│ 土地A │
--------------------------------------------
│土地B │土地C │土地D │ 土地E │
--------------------------------------------
こうです。
127:１３２人目の素数さん
11/01/10 07:32:03
宮崎の口蹄疫、実は韓国産
韓国の口蹄疫ウイルス、宮崎とほぼ一致 水際対策を強化
URLﾘﾝｸ(www.asahi.com)
農林水産省は７日、韓国で大流行している家畜伝染病・口蹄疫（こうていえき）のウイルスを分析した結果、昨年に宮崎県で広がったものと遺伝子配列がほぼ一致したと発表した。農水省は国内への侵入を防ごうと、
空港や港など水際での防疫対策を強めている。
農水省によると、韓国では昨年１１月に東部の慶尚北道・安東で確認されたのを皮切りに、５道１市とほぼ全土に拡大した。今月７日までに９９例が発生し、牛や豚約１０７万頭が殺処分の対象になった。このほか
約１２０万頭にワクチンを接種中だ。
このウイルスを韓国政府が分析した結果、宮崎のウイルスと遺伝子配列が９９％以上一致したという。韓国では昨年４月にも発生していた。
128:１３２人目の素数さん
11/01/10 07:56:01
-------------------------------------------
│ 土地A 赤 │
--------------------------------------------
│土地B 青│土地C 黄 │土地D 青│ 土地E 黄│
--------------------------------------------
でこの場合は３色でOK
129:１３２人目の素数さん
11/01/10 08:45:46
BCK論理ではラッセルのパラドクスが発生しない。
BCK論理を中心とする部分構造論理は数学のすべてを記述するだろう。
130:１３２人目の素数さん
11/01/10 16:13:01
>>128
あっ、そうか。
俺、あほだな。
ありがとね。
131:１３２人目の素数さん
11/01/13 00:32:45
自然数の0のことを 0: = Ø = { } と定義しちゃったら
空集合と0を区別して使いたい場合に困るじゃないか、
仮に0を退避させてもその先で用途が今後被るかも知れないじゃないか、
っていうことは公理的集合論を勉強し始めたときに気持ち悪い点の一つだと思う。
順序対の定義とかもそうだけど、最初に集合論を勉強し始めたら
結構な人が違和感を持つんじゃないだろうか。
これは、これこれの対象と関数と述語が存在して
自然数論の公理を満たす構造になっている、
という公理系 T を別に考えて理論の合併 ZFC ∪ T を考えれば良くて、
ZFC ∪ T では0=Øみたいな式が証明されることは絶対無いので
実際に数論とかの数学をやるときはこっちのほうが自然。
でも集合論の公理系のことを主に考えている場合は
T の∃z ～～ とかは実はZFCの公理から普通に証明できるので、
敢えて公理にする必要無いよねって話だと思うと良い。
人間が読めば文脈で区別できます、みたいな返答はあんまりじゃないかなあ。
そりゃそうだがそんなこと言ってるんじゃないだろうよ。
132:１３２人目の素数さん
11/01/13 06:20:19
>>131
ツイッターから出てくるなよゴミカス
133:１３２人目の素数さん
11/01/14 22:30:41
「数学のロジックと集合論」によると
完全性定理は選択公理よりもちょっと弱いらしいよ
こないだ立ち読みしてたら書いてあった
134:１３２人目の素数さん
11/01/15 01:41:29
ゲンツェンによる自然数論の無矛盾性証明における
証明図の簡略化は有限回で終わるのか。
言い換えれば、対応する順序数は整礎なのか。
正しいような正しくないような…モヤモヤする…
135:１３２人目の素数さん
11/01/15 06:04:33
最近、数学するときに不完全性定理のことを
もっと真剣に考えないといけないと思うようになりました
真とも偽とも判断が付かない命題があるなら
真か偽かを考えると同時に証明できない可能性も考えるべきだと思います
そこで、ある命題が「真とも偽とも証明できない」ことを
証明するような手段を知りたいのですが、
何か手順・プログラムなどがあったら教えてください
136:１３２人目の素数さん
11/01/15 08:31:57
簡単なところでは反例を作るとか。
集合論的な独立命題なら強制法使って独立性示したり
他の良く分かっている命題に帰着させたりとか。
137:135
11/01/15 18:53:51
レスサンクスです
強制法とか参考になります
自分はそれほど論理学をマスターしていないので
もう少し詳しく教えていただけるとありがたいです
> 反例を作るとか。
これはどのような反例を作ればよいのでしょう？
真または偽と証明できたと仮定して反例を導くのでしょうか？
しかし不完全性の例だと、真であっても偽であっても
矛盾しないような気がします。
> 集合論的な独立命題なら強制法使って独立性示したり
強制法をいまチラ見しただけでまだよく分かってないのですが
任意の命題（集合論的な独立命題でないもの）に対しては
適用できない手法ですか？
よろしくお願いいたします
138:１３２人目の素数さん
11/01/15 19:58:30
例えば、～～という前提のもとでAとnot Aのどちらが正しいのか？
とか言った場合にAを満たす例とnot Aの例の両方を作るとか。
強制法が適用できないような独立命題もあって良さそうなものだけど、
現実問題としてはあまりそういうものは知られてないんじゃないかと思う。
だから独立性のことが気になるなら強制法が一番強力な武器なのは間違いないと思う。
ロジックでは強制法が使えないほど弱い理論（たとえば限定算術）から或る定理が
独立かどうかとかが問題になることもあるのだけど、
普通の数学ではZFCから証明出来たら、証明できたものと見做す。
だいたいAもnot Aも証明できないというのが真実だとしても、
「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。
139:１３２人目の素数さん
11/01/15 20:31:18
ありがとうございます！大変参考になります。
> だいたいAもnot Aも証明できないというのが真実だとしても、
> 「Aもnot Aも証明できない」ということが必ずしも証明できるとも限らない。
そうですね。証明可能性を分類していくと
A (が証明できる）
not A (が証明できる）
「A か not A か証明できない」（ことが証明できる）
『「A か not A か証明できない」ことが証明できない』（ことが証明できる）
と続けて n 段階目を
「A か not A かという」 [ことが証明できない]^n (ことが証明できる）
と書ける。これを n 段階証明不可と呼ぶと、
n はいくらでも続けることができてω段階証明不可という命題を妄想します。
さらにω段階証明不可が証明不可であることを（ω+1）段階証明不可として
、nω段階、ω^n段階、ω^ω段階のようなことを妄想します。
これらの可能性を包括的に走査するプログラムなどを当方は妄想していますが
不完全性からは無謀な試みでしょうか？
140:１３２人目の素数さん
11/01/15 21:46:21
そんなつまみ食いで何かできるとしたらよほどの天才
141:１３２人目の素数さん
11/01/15 21:53:19
しっかり栄養をつけて食べるにはどう学習したらよいでしょう？
いまのところ戸田先生の『論理学をつくる』をざっと眺めました。
他の論理学の本は、なんだか頭に入ってこないというか、
書き方が難しいです。哲学よりの本も多いし…
数理論理学をやるのによい中級の本はないでしょうか？
142:１３２人目の素数さん
11/01/15 21:55:34
全く無謀な試みです。
……なぜかと言うと、矛盾からは任意の命題が出て来るので、
Tから証明できない或る命題が存在する⇔Tが無矛盾
よって、たとえばZFCで考えているとして、ZFCが無矛盾であることが証明できない限り
三段目以降は全部自動的に無理になってしまう。
これも前のスレにあった話だけど。
やっぱ皆考えることは同じだよね。
143:１３２人目の素数さん
11/01/15 22:02:29
>>141
自分は『論理学をつくる』の次に
前原昭二『数学基礎論入門』を読みました。
論理計算を実践しつつ（かなり丁寧）、不完全性定理の厳密な証明が学べます。
命題論理の公理系から始まるので、シンタクスとセマンティクスの区別さえできていれば、
他に予備知識は不要な本です。
144:１３２人目の素数さん
11/01/15 22:32:41
>>141
たぶんその栄養が身になるころにはなんのために論理学を身に着けようとしたのか
もう忘れてしまっているのに十分な時間が経過していることでしょう。
三途の川の向こうに答えがあるかもしれませんね。
145:１３２人目の素数さん
11/01/15 22:48:53
>>142
そうですか…
しかしZFCからは連続体仮説が証明できない、という結果があったと思いますが
これはZFCが無矛盾であることを示したことにならないでしょうか？
もっと込み入った事情がありますか？
146:１３２人目の素数さん
11/01/15 22:51:39
>>143
ありがとうございます
その本も手元に持っていたので読み込んでみます
>>144
まあ数学やる以上は答えが出るか分からない旅…
147:１３２人目の素数さん
11/01/16 00:43:48
>>145
> これはZFCが無矛盾であることを示したことにならないでしょうか？
そうするとZFCは無矛盾でないことになりますので、大発見だと思います。
148:１３２人目の素数さん
11/01/16 10:30:53
>>145
単純に、ZFCが無矛盾だとすれば、の前提つきでの話。
もちろん、矛盾していても証明できるけど。
149:139
11/01/16 18:36:25
>>147 >>148
なるほど。
よく言われる「連続体仮説は証明も反証もできない命題である」
ということの証明には前提条件があったのですね。
しかしZFCが矛盾するとすると集合論が崩壊するので
数学は致命的なダメージを受けますね。
数学という船にのっている以上、ZFCは無矛盾、と仮定するのは
自然な成り行きだと思います。
言い方は悪いですが、沈むときは一緒だ、みないな。
そこでZFCは無矛盾と仮定した上で、>>139 のような
考えはどうなのでしょうか？
どのみち独立性を示すためには基の論理体系が無矛盾であると
仮定しなければならないようなので。
150:１３２人目の素数さん
11/01/17 00:01:06
渕野昌先生、『ゲーデルと20世紀の論理学』で
御本人が執筆された公理的集合論の解説を丸々upされてるんですね。
太っ腹な御人だ。
151:１３２人目の素数さん
11/01/17 18:09:18
>>149
ZFC集合論が矛盾していたとしても集合論は崩壊しないよ。
別の定式化をすれば良いだけだ。
152:１３２人目の素数さん
11/01/17 19:08:31
朝倉数学ハンドブックという本の飯高茂先生の章に
「P(N)の濃度をアレフ1と書く」
「アレフ0とアレフ1の間の濃度はないという主張を連続体仮説という」
（アレフは実際にはヘブライ文字で表記されています）
と書いてあります。
連続体仮説が成り立たない場合にはアレフ0の次に
アレフ(1/2)とかアレフεみたいな基数があるのだと思うのですが
これは実数の集合で言うとどういったものになるんでしょうか？
153:１３２人目の素数さん
11/01/17 19:16:19
>>152
何世紀も引用されまくるような偉大な論文ができる。
154:１３２人目の素数さん
11/01/17 19:53:22
>>151
しかし最定式化の段階で一旦ZFCに基づいていた証明を捨てなければなりませんよね。
そうなると数学全体をスクラップ＆ビルドしなおす必要が出てくると思います。
ある意味、集合論（数学の基礎）の崩壊かなと。
また、同等の機能を持った別の定式化というのは存在するでしょうか？
同等の機能を持つなら同じ論理式が同じように証明できるわけで
また矛盾してしまうのではと思います。
155:１３２人目の素数さん
11/01/17 19:56:06
え？
156:１３２人目の素数さん
11/01/17 19:58:20
カントール以前には数学がなかったかのような言い分
157:１３２人目の素数さん
11/01/17 19:59:01
×言い分
○言い様
158:１３２人目の素数さん
11/01/17 20:01:46
>>154
その台詞自体があなたが基礎論のことを何もわかってないことを如実に示している
ということを理解したほうが良い。
159:１３２人目の素数さん
11/01/17 20:11:26
>>158
う～ん。確かに基礎論難しくて良く分かってないけど
台詞のどの辺がだめなのか指摘してもらえたらいいな
160:１３２人目の素数さん
11/01/17 20:12:19
現代数学がZFCに基づいている、とはいっても
実際はZFCの表現力の一部しか使っていない。
再定式化する際には、数学に必要なだけの表現力を持つ体系であれば
（ZFCをはじめとする集合論とは見た目が全然違っていても）何でもいい。
161:１３２人目の素数さん
11/01/17 20:15:58
>>159
全部。学校のことを説明しているつもりで消防士の説明をしてるくらい根本的にオカシイ。
162:１３２人目の素数さん
11/01/17 20:23:01
>>160
なるほど。サンクス。
崩壊は言い過ぎだったか。
既存の定理Ａと定理Ｂが衝突してどちらか捨てなければならない
という事態なら生じるだろうか？
その場合でも、高校の様に（？）、数学Ａと数学Ｂに分かれて
どちらも生き残るのだろうか…
163:１３２人目の素数さん
11/01/17 20:42:35
せっかくの>>160も、バカを前に真意は伝わらずか。
164:１３２人目の素数さん
11/01/17 20:47:37
>>162
既存の数学ってのはツーバイフォーの家みたいなもので、
その規格に合う基本部品さえ作れれば、
作る道具には依らないで同じ家ができるんだよ。
165:１３２人目の素数さん
11/01/17 20:50:43
実際の数学の"証明"は形式化されていないけど
形式化されていないからこそ融通が利く
166:１３２人目の素数さん
11/01/17 21:08:23
すいませんが公理的集合論について詳しい和書ありますか？
できれば強制法や2階算術まで載っているのが良いんですが。
（キューネン以外で。
167:162
11/01/17 21:12:48
>>164
その代替部品って簡単に作れる（存在する）ものですか？
>>165
定理Ａと定理Ｂから矛盾が導けるとき
もとの公理系から矛盾が導けるということだから
矛盾から任意の定理が導けるのは当たり前（？）で
単にもとの論理体系が矛盾するというだけか
もとの論理体系を無矛盾なものに取り替えれば
定理Ａと定理Ｂがまた矛盾するかどうかは分からないわけか
現代の数学から見て明らかに矛盾するような
理論を作ったとしても、将来に論理の枠組みを変更して
無矛盾にできる可能性がずっと残されるのかな
168:１３２人目の素数さん
11/01/17 21:17:55
>>166
こんなんありますよ
URLﾘﾝｸ(kurt.scitec.kobe-u.ac.jp)
169:１３２人目の素数さん
11/01/17 21:28:05
論理学にガロア理論（の類似物）ってありませんか？
170:１３２人目の素数さん
11/01/17 21:29:08
>>167
実数の話をしたいなら実数の公理を記述できるものを出せばいいけど
それは別にZFCよりもずっと弱い系から出てくる理論なので余裕。
171:１３２人目の素数さん
11/01/17 21:30:17
>>167
ゼロからきちんと勉強する気がないならあきらめろ、お前の考えは休むにも劣る。
172:１３２人目の素数さん
11/01/17 22:13:09
難波完爾の集合論があまりにもコンパクトに纏まってて泣ける
安いから損はしないけどね
173:１３２人目の素数さん
11/01/17 22:38:38
>>170
>>171
先走りたがりなものでスミマセン
ゼロから勉強する気はあります
ありがとうございました
また何かあったらよろしくお願いします
174:１３２人目の素数さん
11/01/21 22:23:26
命題論理の抽象の定義って何種類位知られているんでしょうか？
175:１３２人目の素数さん
11/01/21 22:50:24
(´･ω･)?
176:１３２人目の素数さん
11/01/21 23:04:15
メレディスの公理系
A1 （（（（A→B）→（￢C→￢D））→C）→E）→（（E→A）→（D→A））
R1 A A→B├ B
177:１３２人目の素数さん
11/01/21 23:31:57
ゲーデルによる高階論理を用いた自然数論の無矛盾性証明
が読める文献を御存知ありませんか？
178:１３２人目の素数さん
11/01/22 09:36:53
ウィキぺでぃあの証明論ひどすぎ
URLﾘﾝｸ(ja.wikipedia.org)
哲学系の人間が書いたに違いない
179:１３２人目の素数さん
11/01/22 11:16:00
>>178
データ構造や自動定理証明や型理論など、
数学視点ではなく計算機科学視点が多いですが、
哲学視点はほとんどありません。
ひどいと感じたのはどこですか？
なぜ哲学系の人間が書いたと思ったのですか？
Proof theory (証明論の原文)
URLﾘﾝｸ(en.wikipedia.org)
180:１３２人目の素数さん
11/01/22 12:20:23
俺もどこが酷いと思ったのか分からん
他のロジックの記事の方がよほど酷い
181:１３２人目の素数さん
11/01/22 18:14:26
チャーチ・ロッサーの合流定理の証明ってどこかに載ってませんか？
182:１３２人目の素数さん
11/01/22 20:45:37
Barendregt嫁
183:１３２人目の素数さん
11/01/22 22:59:33
小野寛晰さんの本読んでんだけど、
テクニカルな議論と"意味"の解説の配分が絶妙だね
ムラムラしてきたからオナヌして寝るわ
184:１３２人目の素数さん
11/01/22 23:24:35
>>183
私もそれ今読んでます。
演習問題の質もちょうど良い。
国内の論理学入門書でも画期的なものだと思いますね。
今日明日で読了するつもりです。
185:１３２人目の素数さん
11/01/23 00:03:22
>>183-184
この本ですか？
現代数理論理学序説 (古森雄一・小野寛晰 著)
URLﾘﾝｸ(www.amazon.co.jp)
URLﾘﾝｸ(www.nippyo.co.jp)
URLﾘﾝｸ(d.hatena.ne.jp)
186:１３２人目の素数さん
11/01/23 01:35:03
その本は三章までは古森さんが書いてる
四章はあまり入門と言うような内容でもないし
「情報科学における論理」の方かと思った
187:184
11/01/23 10:10:24
述語論理の意味論から急に難しくなってきた。
188:184
11/01/23 12:30:11
>>185
それだね。
日本の数理論理学の最高峰だと思う。
189:183
11/01/23 13:44:18
ありゃ、自分が今読んでるのは『情報科学のための論理』の方です
もう一つの方もチェックしてみます
190:１３２人目の素数さん
11/01/23 14:37:33
＞『情報科学のための論理』
手触りが良くて、角ばってて、ガッシリしてて…
とても良い本ですよね
191:１３２人目の素数さん
11/01/23 15:22:51
>>189-190
『情報科学における論理』ですよね？
情報科学における論理 (小野寛晰 著)
URLﾘﾝｸ(www.amazon.co.jp)
URLﾘﾝｸ(www.nippyo.co.jp)
URLﾘﾝｸ(www10.atwiki.jp)
192:183
11/01/23 15:37:19
>>191
あ、そうです。失礼しました。
193:１３２人目の素数さん
11/01/23 21:04:17
健全性と完全性を満たさない体系はどうなるの？
194:１３２人目の素数さん
11/01/23 21:14:53
pcf理論を哲でもわかる様に説明してちょんまげ。
195:１３２人目の素数さん
11/01/23 22:44:08
もしも量化演算子に語られるものが
人間の脳の機能になければ、
あらゆるものは分類できず、すべてがバラバラであったであろう。
196:１３２人目の素数さん
11/01/23 22:54:51
竹内外史の実数論の無矛盾証明って『Proof Theory』以外
に載ってませんか？
197:184
11/01/23 23:19:17
コンパクト性定理証明終了。
ようやくラムダ計算に突入。
198:１３２人目の素数さん
11/01/24 00:00:36
ZFが無矛盾なのか気になって夜も眠れない・・・ぐぅ・・・
199:１３２人目の素数さん
11/01/24 03:19:30
>>196
"two application"になかったかなあ？
200:184
11/01/24 07:08:31
>>198
ラムダ計算が矛盾したんだ。
ZFのだめだろう。
201:１３２人目の素数さん
11/01/24 07:12:13
モノイド空間を定義して
そこで健全性定理をイーストンの定理で導入すればZFが矛盾する。
202:１３２人目の素数さん
11/01/24 12:04:44
>>199
あった
203:１３２人目の素数さん
11/01/24 20:48:38
>>201
はいはいわろすわろす
204:201
11/01/24 23:07:59
>>203
> >>201
> はいはいわろすわろす
バカにするわけじゃないけど、
これ俺の近所の小学生の会話の中にもあった（笑い
205:201
11/01/24 23:08:49
まぁ実際健全性定理が成立する体系なんてごくわずかな例外的な存在だけどなぁー。
206:１３２人目の素数さん
11/01/24 23:33:57
健全なんて幻想、セカイは不健全なものなのです。
207:201
11/01/25 23:54:05
健全性定理と完全性定理が同時に成立しないということが、
２階述語論理の第２不完全性定理の意味論。
208:１３２人目の素数さん
11/01/26 19:40:32
現代数理論理学序説の９３ページの
古典述語論理の体系が決定不可能であることの証明って、
不完全性定理と同等のものですよね？
209:１３２人目の素数さん
11/01/26 22:15:06
おもしろい講義ノートがあったので貼り貼り
様相論理と不完全性定理
URLﾘﾝｸ(www.shizuoka.ac.jp)
210:１３２人目の素数さん
11/01/26 22:16:02
あ、>>208さんの疑問とは特に関係ありません
211:１３２人目の素数さん
11/01/26 22:25:06
既に収集済みだった
>>208
同等というと語弊がある気がするけど
不完全性定理を使って示すよね
212:１３２人目の素数さん
11/01/26 22:30:34
>>211
定理3.1.13が不完全性定理でしょうか？
この本は不完全性定理という記述をあえて避けているんでしょうか。
とすると、論理学の古典や歴史的文脈は完ぺきに排除した、
天下り的現代論理学入門書ということになるのでしょうか。
213:１３２人目の素数さん
11/01/26 22:42:26
>>212
その定理3.1.13 のステイトメントをここに書いた方が早い気がする
214:１３２人目の素数さん
11/01/26 22:48:27
>>213
定理3.1.13
空でないCL-項の集合AがCL-項全体ではなく、
Weak-equalityについて閉じているならば、
CL-項が集合Aに入っているかを判定する決定手続きは存在しない。
215:１３２人目の素数さん
11/01/26 22:53:35
それだいぶ緩くネ？下痢しそう……
216:１３２人目の素数さん
11/01/27 11:39:27
>>208
> 古典述語論理の体系が決定不可能であることの証明って、
> 不完全性定理と同等のものですよね？
全く違います
217:１３２人目の素数さん
11/01/27 19:06:24
そういえば、ε-δ論法がわからない人って何がわからないのだろう
概念？ 論理の記号操作？
218:１３２人目の素数さん
11/01/27 19:07:05
誤爆
219:１３２人目の素数さん
11/01/27 20:06:47
荒れてるな。
イングランド出身の傭兵で中世イタリアの伝説的英雄、
ジョン・ホークウッドによると、占領地で女達を輪姦し続けると、
だいたい30人くらいで必ず死んでしまうらしい。
商売ならなんでもなくても命がどうなるかわからない状況で、
輪姦され続けると興奮し過ぎで必ず死ぬらしい。
これ、豆知識な。
220:１３２人目の素数さん
11/01/27 20:08:38
誤爆しすぎ
221:１３２人目の素数さん
11/01/27 20:11:04
>>216
違うなら何だというのだ？
222:１３２人目の素数さん
11/01/27 20:12:51
良いこと聞いた
明日、塾の生徒に教えてやろうっと
223:１３２人目の素数さん
11/01/27 22:29:06
超限算術
直観主義命題論理
超直観主義命題論理
：
：
中間論理
：
：
古典命題論理
224:１３２人目の素数さん
11/01/28 00:56:41
>>221
それも解らないんなら数理論理学の基本から勉強し直せ
225:１３２人目の素数さん
11/01/28 07:25:34
>>224
だから今数理論理学の入門書を読んでいる。
私は不完全性定理については全く知らないが、
名前だけは聞いたことがある。
だからこそ定理3.1.13が不完全性定理というものなのかと聞いている。
226:１３２人目の素数さん
11/01/28 08:49:39
ああ、じゃあ違う定理だと思っといた方が良い
チホノフの定理とツォルンの補題が違うのと同じくらいには違う
同等だと言えば同等だけど違うと言えば違う
不完全性定理のステートメントも知らんのに
>>212みたいなこと言うと誤解呼ぶと思うなあ
別にそんなに天下り的じゃないよ
ロジックはシンタックスだけ先にあって後から意味論が考えられるようなことが良くある
組合せ論理はそうじゃないと思うけど、これは初学者がシンタックスと意味論を
混同するようなことがあるから敢えてそれがないようにこういう導入の仕方を取っているだけ
227:１３２人目の素数さん
11/01/28 14:18:32
述語論理の形式的体系の演繹定理：
Γ, A├ B ⇒ Γ├ A→B
（一般化規則 「A から ∀xA を導いてよい」 を適用する際、
x は A が依存する仮定に自由変数として現れないものとする）
なんですけど、
Γの元や A が閉論理式である、
といったような仮定無しに無条件に成り立ちますよね？
228:１３２人目の素数さん
11/01/28 21:29:52
>>226
シンタックスだけで意味論が見つかっていない
論理学って何があるの？
229:ノニ
11/01/28 21:33:09
代数的論理学の良い入門書ってありますか？
230:１３２人目の素数さん
11/01/28 22:09:16
型無しラムダ計算の意味論はかなり後になって
Scottが考えたんだったと思う
>>229
無い
231:ノニ
11/01/28 23:17:10
ラムダ計算は研究途中に矛盾が発見された体系だっけ？
232:１３２人目の素数さん
11/01/29 00:10:10
>>229
代数的論理学は入門書どころか
基本的文献が1冊しかないのでは？
代数的方法による論理学の新たな展開
URLﾘﾝｸ(kaken.nii.ac.jp)
>代表者 2005年度～2007年度 小野 寛晰
代数的視点からの論理へのアプローチ (小野寛晰)
URLﾘﾝｸ(www.jaist.ac.jp)
>また、部分構造論理に対する代数的研究におけるこれまでの成果を共著としてまとめ、
>この春に"Residuated Lattices: an algebraic glimpse at substructural logics"として出版する。
>ここではこのような研究のことを、従来のabstract algebraic logicよりは
>広い意味に解釈して代数的論理学とよぶことにする。
Residuated Lattices: An Algebraic Glimpse at Substructural Logics
URLﾘﾝｸ(www.amazon.co.jp)
233:１３２人目の素数さん
11/01/29 00:34:30
演繹定理の前提条件はformulationの違いに依存するとか聞いたような
234:ノニ
11/01/29 13:39:27
現在の数理論理学の主流は、
世界的に abstract algebraic logic と modal logic の
2本柱なのに、大丈夫なのかね、この国は。
意味論もウィトゲンシュタイン流の2値論理は終焉を迎えて、
真理値がノルム空間に拡張された fuzzy logic の
萌芽も見え始めているというのに・・・。
235:１３２人目の素数さん
11/01/29 17:22:02
formulationって？論理式の構成の仕方？
236:１３２人目の素数さん
11/01/29 19:05:15
>>227 仮定無しでは成立しません。
Γ を空, A を px, B を ∀x px とする。条件がないとき, ⇒ の左側は正しい
が, 右側は正しくない。
237:１３２人目の素数さん
11/01/30 00:48:36
px に一般化規則を適用して ∀x px を導こうとしても、
px は一般には仮定「Г, px」に依存するから、実は一般化規則は使えなくて、
左辺も正しくない気がする。
238:１３２人目の素数さん
11/01/30 00:55:10
仮定というのは変数条件ですよ。それをなくしてしまえば
⇒ の左側は正しい。
239:１３２人目の素数さん
11/01/30 01:09:39
ただし，227 の 「A が依存する仮定...」は間違いで, 「仮定の...」と
現代数理論理学序説に書いてある。
240:１３２人目の素数さん
11/01/30 03:32:49
>>234
主流がどうのこうのと言ってる内は永遠の2番手ですよ
241:１３２人目の素数さん
11/01/30 21:24:01
>>227 にはわざわざ「A の依存する仮定」と書いてあるのだから、
証明のツリーを１つ定めた上で、仮定の集合の元のうち、一般化規則の上式A が依存するものだけを問題にしていると思われ。
実際そう考えると、与えられたツリーを書きかえることで無条件に演繹定理は成り立つ。
ヒント：「Г, A ├ B」のツリーにおいて一般化規則を適用する際、
上式がAに依存する場合としない場合にわける。
依存する場合は「Aが閉論理式」と仮定したときと同様、
しない場合はツリーの上式から上の部分をそのまま利用して書きかえ。
242:１３２人目の素数さん
11/01/30 21:24:08
なあ、5月にやる司法試験予備試験のサンプル問題なんだが、
第1問って4番も正解でよくね？
URLﾘﾝｸ(www.moj.go.jp)
243:１３２人目の素数さん
11/01/30 21:26:41
5は真理を探求する哲学者が1人もいない場合を含むが、4は含まない。まったく別物。
244:１３２人目の素数さん
11/01/31 00:07:41
>>227 は「現代数理論理学序説」を誤解して書き間違えただけ。
そもそも Г, A ├ B で A は仮定だよ。「A の依存する仮定」というの
がおかしいということいが分からないのかな。
245:１３２人目の素数さん
11/01/31 00:42:10
初心者のための演繹定理の解説
演繹定理はヒルベルト流の体系についての定理である。ヒルベルト流の体系は
公理から定理を導くとき modus ponens と普遍化規則の二つの推論規則を使
う。証明図の頂上には公理しかないので普遍化規則には変数条件は必要ない。
しかし, 演繹定理を述べるためには頂上に公理以外のものを認める必要があ
る。頂上には公理以外のものを認め二つの推論規則を使って得られる図形
を「現代数理論理学序説」では証明図と区別して推論図と呼んでいる。
推論図においては証明図とは違って普遍化規則には変数条件が必要であると
「現代数理論理学序説」で述べられている。227 は変数条件は必要ないので
はないかと疑問を述べている。236 で述べたように変数条件をなくしてしま
うと演繹定理は成立しない。
「Г├ A」の意味は Г を頂上(頂上にある公理はГ に入れないでもよい )
とする A に至るヒルベルト流体系の推論図が存在する。頓珍漢なレスをし
ている人はこれが分かっていないのではないかな。
246:１３２人目の素数さん
11/01/31 03:08:25
古臭くて不親切本引くなよ爺さん。
247:ノニ
11/01/31 07:58:24
前原の本と間違えてないか？
248:１３２人目の素数さん
11/01/31 12:21:50
数日前からやたらと現代数理論理学序説にこだわる痛い人がいるな…
「A が依存する仮定」の「A」は「Г, A├ B」の「A」ではなく、
一般の状況での普遍化規則の上式のことだろう。
249:１３２人目の素数さん
11/01/31 12:31:15
付言すると、演繹定理はヒルベルト流の論理計算を補助するための定理なので、
その目的が達成される限りにおいて、「仮定からの推論」には異なる定義があり得るということも覚えておくといいよ。
君の読んでる本では、
「個々の上式が依存する仮定」ではなく、
「あらかじめ与えられた集合の元すべてを仮定として考える」ようだけど、
それは議論を簡単にするためであり、
また、その程度の縛りがあっても十分有用な定理となるからだろう。
250:１３２人目の素数さん
11/01/31 12:45:07
227 が現代数理論理学序説についての演繹定理について質問している
のだから, その本にしたがって答えるのが当然だろう。
251:１３２人目の素数さん
11/01/31 13:12:59
前の流れから 227 が現代数理論理学序説についての演繹定理に質問している
ものと早とちりをしてしまったようだ。248 の指摘で早とちりに気づいた。
だとすると 227 での条件とは閉論理式という条件だけだ。そのような条件は
演繹定理にはないのが普通なので, 早とちりを引きずってしまった。
もちろん, 閉論理式という条件は必要ない。
252:１３２人目の素数さん
11/01/31 13:51:57
248 を書いた方, どうもありがとうございます。
253:１３２人目の素数さん
11/02/01 13:14:26
>>242
4が駄目なのは、
問題文が「両立しないものを選べ」ではなく「否定を選べ」だから
254:１３２人目の素数さん
11/02/03 21:43:53
日本語で読める様相論理の本って
ヒューズ／クレスウェル以外でなんかありませんか？
255:ノニ
11/02/03 22:36:23
一番載ってるのは
小野 寛晰
情報科学における論理 (情報数学セミナー)
256:１３２人目の素数さん
11/02/05 12:12:10
なんで数理論理学系のPDFって
ネット上にいっぱい転がってんの？
他の分野より多いよね
257:１３２人目の素数さん
11/02/05 19:37:12
そうでもないと思う
他分野のpdfファイルをあまり知らないだけでは
258:１３２人目の素数さん
11/02/05 21:05:40
集合論と数理論理学って別々に研究されてんの？
数理論理学って計算機科学の人のが詳しいってホント？
259:１３２人目の素数さん
11/02/07 20:59:15
帰納的関数の本で、コレ！ってのはある？
260:１３２人目の素数さん
11/02/07 21:38:59
大抵のrecursion theoryの教科書に参考文献として載ってるようなのがあるでしょ
あとCooperのcomputability theoryの新しい版が今度出るみたいよ
261:１３２人目の素数さん
11/02/09 19:58:22
ブール代数とかハイティング代数とか、
代数的な意味論って、完全性が成り立つように
無理矢理作った感じがするんですが、何か効用はあるんでしょうか。
262:１３２人目の素数さん
11/02/09 20:42:39
ブール代数は述語論理が出来る前に真理値の代数として
作られたものなんで別に無理矢理じゃないと思うけど。
ハイティング代数の方は知らん
263:１３２人目の素数さん
11/02/09 22:22:00
mixiid=8878429
264:１３２人目の素数さん
11/02/09 23:28:35
インチキの最たるもん数学基礎論。
265:１３２人目の素数さん
11/02/11 01:26:29
>>261
URLﾘﾝｸ(en.wikipedia.org) とか
266:１３２人目の素数さん
11/02/12 02:18:22
再帰的（recursive）と帰納的（inductive）って同じ意味ですか？
267:１３２人目の素数さん
11/02/12 19:54:57
>>264
無知乙。
インチキ扱いされるのは、
無限、宇宙、数学の基礎というワードに電波が群がっているから。
268:１３２人目の素数さん
11/02/12 22:15:21
(A⇒B)⇒((A⇒￢B)⇒￢A)
突然ですいませんがこれなんですか。
∀とか∃とかなんですか
テストなんです。助けて下さい
269:１３２人目の素数さん
11/02/12 22:57:02
URLﾘﾝｸ(ja.wikipedia.org)
URLﾘﾝｸ(ja.wikipedia.org)
教科書読め。
270:１３２人目の素数さん
11/02/13 03:57:53
ヒルベルト方式命題論理の公理図式だろ
271:１３２人目の素数さん
11/02/13 04:32:23
(￢A⇒B)⇒((￢A⇒￢B)⇒A) じゃね？
272:１３２人目の素数さん
11/02/13 15:16:36
A⇒(B⇒A)
[A]B⇒A
[B]A
この流れが全く分かりません。多分法則とか公式分かればとんでもなく簡単なんだろうけど。
明日本屋で勉強しようと思うんだが、なんかオススメの本ありますか？
273:１３２人目の素数さん
11/02/13 17:26:21
>>272
「恒真式、真理表」を速攻理解しろ。
274:１３２人目の素数さん
11/02/13 19:03:51
俺も依然ヒルベルトの証明形式HKをやったことあるけど
公理型に￢なんて含まれてたっけ？
275:１３２人目の素数さん
11/02/13 19:18:05
>>274
公理図式の組にはバリエーションがあって、￢を含むタイプのもある。例えば
ルカシェヴィツの公理系L
公理１ A⊃（B⊃A）
公理２ （A⊃（B⊃C））⊃（（A⊃B）⊃（A⊃C））
公理３ （￢A⊃￢B）⊃（B⊃A）
推論規則１ A, A⊃B → B （MP）
276:１３２人目の素数さん
11/02/13 19:21:52
自分が習った体系しか無いと思うとは、おめでたいやつだ。
277:１３２人目の素数さん
11/02/13 19:22:07
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
(￢B→￢A)→((￢B→A)→B) 背理法
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
(￢B→￢A)→(A→B) 対偶律
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
￢￢A→A 二重否定除去（ただし￢AはA→⊥の略記）
A→(B→A)
(A→(B→C))→((A→B)→(A→C))
⊥→A
((A→B)→A)→A パースの法則
etc...
278:追加
11/02/13 19:26:04
>>176
279:１３２人目の素数さん
11/02/13 19:31:39
シェーファーの棒を使う変態的なシステムもあるな。
280:１３２人目の素数さん
11/02/13 20:20:54
Nand でしょう？
281:１３２人目の素数さん
11/02/13 21:05:06
論理学ではnandとは言わない
282:１３２人目の素数さん
11/02/13 21:38:41
え、じゃあnandはどこの用語なんだ
283:１３２人目の素数さん
11/02/13 21:41:48
電子工学
284:１３２人目の素数さん
11/02/13 21:44:02
ググったら「NAND型フラッシュメモリ」というのが出てきた
285:１３２人目の素数さん
11/02/13 21:44:57
論理回路も知らんのか・・・
286:１３２人目の素数さん
11/02/13 21:48:39
>>283
あ、そうか。サンクス。
287:１３２人目の素数さん
11/02/13 22:22:27
>>276
> 自分が習った体系しか無いと思うとは、おめでたいやつだ。
他にあるってこと自体は知っていた。
ただ俺はHKといった。
HKは普通、
公理１ A→B→A
公理２ (A→B→C)→(A→B)→A→C
公理３ ((A→B)→A)→A
公理４ ￢→A
推論規則１ A, A⊃B → B （MP）
だろう？
今はBCIとかBCKとかBCKW...とか言われてるのを知らのか？
288:１３２人目の素数さん
11/02/13 22:27:43
今、論理学で若手の有力株と言えば？
数学畑の人と哲学畑の人と両方教えて
289:１３２人目の素数さん
11/02/13 22:44:54
聞いたことないな。
集合論ならいるけど。
290:１３２人目の素数さん
11/02/13 22:49:33
集合論か・・・
一応教えてください
291:１３２人目の素数さん
11/02/13 22:59:25
>>290
URLﾘﾝｸ(twitter.com)
292:１３２人目の素数さん
11/02/13 23:59:22
すみません、スレ違いなのは承知しているのですが質問させてください。人間のクリアランスが倍になったら薬物の半減期はどれだけになるか教えてください。
293:１３２人目の素数さん
11/02/14 00:07:39
スレ違いどころか板違いだろ。
294:１３２人目の素数さん
11/02/14 00:09:13
わろたｗ
295:１３２人目の素数さん
11/02/14 00:18:58
すいませんが、
DIAMOND: A PARADOX LOGIC (2ND EDITION) (Series on Knots & Everything)
URLﾘﾝｸ(www.amazon.co.uk)
この本で扱ってるDiamondって様相論理の可能性演算子と、
連続体仮説の一般化の方のとどちらでしょうか？
296:１３２人目の素数さん
11/02/14 01:14:20
HKってそういう意味じゃなくてたぶんHilbert式のcalculusのことを
ドイツ語の頭文字をとって一部の教科書がそう読んでるだけじゃないの？
BCKとかのBとかCとかはそれぞれ一つの公理図式の名前だけどHKはそうじゃないでしょ。
松本和夫の本とかにもHKとか名付けてあるけど当時BCK論理とかがあったはずもないし。
一般的には、ほとんどの規則を推論規則として定式化する
Gentzenの自然演繹とかシーケント計算とかに対して
modus ponensとか汎化規則とかしか推論規則が無くて、
あとは公理として規則を立てるような体系のことをHilbertスタイルというように思う。
というか
＞公理４ ￢→A
これ意味分からんのだが。論理式になってないし。
297:１３２人目の素数さん
11/02/14 02:14:03
> ＞公理４ ￢→A
> これ意味分からんのだが。論理式になってないし。
否定ではなくて、矛盾のつもりなのでしょう。
298:１３２人目の素数さん
11/02/14 23:24:24
集合論て難しいですか？
299:１３２人目の素数さん
11/02/15 07:29:29
公理的集合論に最低限必要な武器は、
・素朴集合論
・線形代数学
・位相空間論
・一階述語論理学
・グラフ理論
・群/体
・ルベーグ積分
・公理的な確率/統計
・関数論
などだ。難しいと感じるかは当人のセンス次第だ。
300:１３２人目の素数さん
11/02/15 09:25:54
>>298
「難しい」と書いて「たのしい」と読むんだぞ
301:１３２人目の素数さん
11/02/15 09:27:02
ごめんsage入れ忘れた
302:１３２人目の素数さん
11/02/15 09:28:30
再度すまんorz
303:１３２人目の素数さん
11/02/15 11:44:47
>>298
シェラハというイスラエルの爺さんの頭脳レベルを調べてみなされ。
304:１３２人目の素数さん
11/02/15 12:09:53
どうやって調べるんですか？
305:１３２人目の素数さん
11/02/15 12:14:05
シェラハを貶めるつもりは毛頭ないが、
この文脈では、論文を量産できるほど簡単な分野であるかのようではないか
306:１３２人目の素数さん
11/02/15 12:15:20
>>304
URLﾘﾝｸ(ja.m.wikipedia.org)サハロン・シェラハ?wasRedirected=true
307:１３２人目の素数さん
11/02/15 17:45:24
高校生のための質問スレからこちらに誘導されてきました。
「ラッセルのパラドックス」を解決した「グロタンディーク宇宙」とはどんなものなんですか？
ウィキ読んでもさっぱりわかりませんでした(笑)
308:１３２人目の素数さん
11/02/15 21:02:17
別にGrothendieck universeとRusselのパラドックスはほとんど関係ないけども。
どこで読んだのそれ？
309:１３２人目の素数さん
11/02/15 21:09:38
ウィキペディアの数学基礎論あたりにそんな変な記述があって笑った記憶があるｗｗ
310:１３２人目の素数さん
11/02/15 21:11:35
>>307
普通のZFでもラッセルのパラドクスは構成できないよ。
311:１３２人目の素数さん
11/02/15 21:24:20
>>299
今ではそれに付け加えて、
・数論
・代数的トポロジー
・モデル理論
・チューリング/メドベージェフ還元
・計算量複雑性・再起理論
・不完全性定理（四則演算並みの頻度で多用）
・論理学の代数化定理周辺
までが求められる。
シェラーとかいう人は確か特異基数仮説周辺で有名な人じゃなかったっけ？
（私も全然ついていけてないです...
312:１３２人目の素数さん
11/02/15 21:29:10
またメドベージェフ君のレスか
313:１３２人目の素数さん
11/02/15 21:43:42
>>299
なんで集合論に確率が必要なん？
てきとうに挙げただけちゃう？
314:１３２人目の素数さん
11/02/15 21:46:32
>>313
カントール空間とかポーランド空間とか使うからでしょ。
メドヴェージェフ還元に＾＾
315:１３２人目の素数さん
11/02/15 21:57:46
メドヴェージェフって言いたいだけちゃう？
316:１３２人目の素数さん
11/02/15 22:02:03
チューリング次数におけるポストの定理が
メドベージェフ次数のおけるプールエルクリプキの定理に該当！
317:１３２人目の素数さん
11/02/15 22:19:31
トリンドルちゃんて言いたいだけちゃう？
318:１３２人目の素数さん
11/02/15 23:23:44
ミッチェル次数もあるよ＞＜
319:１３２人目の素数さん
11/02/15 23:27:25
メドベージェフ次数とかは、どの本で勉強すればいいのでしょうか？
320:１３２人目の素数さん
11/02/16 07:20:38
電子版では
シュプリンガーから
Kripke Models, Distributive Lattices, and Medvedev Degrees
Sebastiaan A. Terwijn
が出てる。
紙媒体は多分まだない。
321:１３２人目の素数さん
11/02/16 10:59:40
>>320
ありがとうございます！
322:１３２人目の素数さん
11/02/17 17:43:46
LKのcut除去定理の証明で、証明図を変形していき、
rankとdegreeについての二重帰納法を用いるものがありますよね？
証明図の変形によるrankとdegreeの減少を精密に評価することで、
何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、
どうも無理な気がしてきました。
実際どうなんでしょうか？
よろしければお知恵をお貸し下さい。
323:１３２人目の素数さん
11/02/17 19:03:27
できます。
Girard の Proof theory and Logical comlpexity には
その方法で評価がされています。
また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の
自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ
ωを 3 に置き換えればよいというようなことが書いてあったと思います。
324:１３２人目の素数さん
11/02/17 20:36:27
>>323
ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。
325:１３２人目の素数さん
11/02/17 23:25:04
＞数学的帰納法がなければωを 3 に置き換えればよい
あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ？
326:１３２人目の素数さん
11/02/18 13:37:43
ペアノの公理で、
なんでx=y→x'=y'じゃなくて
x'=y'→x=yなのか教えてください
327:１３２人目の素数さん
11/02/18 13:57:58
前者はあらゆる関数に成り立つべき性質(等しいものの代入法則)で自明とも言えるが、後者は違う。
328:１３２人目の素数さん
11/02/18 15:47:05
>>326が自然数の公理に必要な理由を教えてください。
329:１３２人目の素数さん
11/02/18 15:54:02
x+1=y+1 ならば x=y でないと困るでしょ。
演繹するか公理で仮定することになる。
330:１３２人目の素数さん
11/02/18 15:58:30
x=y → x'=y' じゃだめなの？
331:１３２人目の素数さん
11/02/18 16:28:40
>>330
なにがいいの？
332:１３２人目の素数さん
11/02/18 16:43:54
>>331
？
333:１３２人目の素数さん
11/02/18 16:47:14
A かつ ￢Aが良い
334:１３２人目の素数さん
11/02/18 17:22:53
>>332
～じゃだめなの？＝～でいいだろ。
ということだから、いいってのはどういう意味でいいっていってんのかってこと。
335:１３２人目の素数さん
11/02/18 19:20:42
自然数の公理として機能しないのかどうかってこと
336:１３２人目の素数さん
11/02/18 19:34:06
だからどう自然数の公理として機能してると主張してるのかってこと。
337:１３２人目の素数さん
11/02/18 19:39:50
しらんがな
そんなうまく質問できるくらいなら質問してない
初めてペアノの公理見たんだよ
なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください
338:１３２人目の素数さん
11/02/18 19:47:26
君の現在の理解力を越えてるようだね。
339:１３２人目の素数さん
11/02/18 19:48:08
x'=y'→x=y
これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。
0→1→2→3→1→2→3→1→2→3→…
形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。
上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。
340:１３２人目の素数さん
11/02/18 20:00:42
>>339
x=y → x'=y'
ならば、
0→1→2→3→4
となるんじゃない？3の次は3'(=4)だけでしょ？
341:１３２人目の素数さん
11/02/18 20:06:45
>>340
x'=y'→x=yを仮定しないと、3' が 1 になり得るという話
342:１３２人目の素数さん
11/02/18 20:12:23
>>340
それだけだと、
3'のまえが3じゃないとこから複数本繋がってきてもいい。
343:１３２人目の素数さん
11/02/18 20:13:21
感覚としては、後者関数を使って自然数を次々と生成していくわけだが、
新しく生まれる自然数が、先に生まれた自然数のいずれとも異なるように、
言い換えれば、自然数を一直線に並べるために必要な公理なんだよ
もし単射でなかったら、直前の世代にあたる自然数が一通りに決まらない
例えば、1の直前が 0 と 0''' ということもあり得る。
344:１３２人目の素数さん
11/02/18 20:22:27
x=y → x'=y' なのになぜ3の前が複数になりうるの？
345:１３２人目の素数さん
11/02/18 20:22:34
今の場合反例モデルが作れるからそれで説明するけど
x'=y'→x=yがなくてその逆だと
Z/nZでも条件満たしちゃうでしょ。
Z/nZが何なのか分からないなら先に初等整数論を勉強してね。
346:１３２人目の素数さん
11/02/18 20:51:38
ごめんボケてた>>345はx'≠0が必要だって話だｗ
やっぱり皆の言うようにやらないとダメだ
ただどっちも似たような話で、
0'=1，1'=2，2'=3，……，～'=n、n'=1みたいな状況が生じちゃうってこと
347:１３２人目の素数さん
11/02/18 20:57:05
>>344
x≠yのときについては何の制約も掛けて無いから。
348:１３２人目の素数さん
11/02/18 20:58:58
>>344
a=b だからって、a と b が「記号列として同じ」であるとは限らない
等号の公理：反射律および代入可能性を満たす限りにおいて、a と b が異なる記号列であってもよい
だから、1の直前が 0 と 0''' である、つまり論理式 0=0''' が証明可能、という状況もある（かもしれない）
349:１３２人目の素数さん
11/02/18 20:59:18
>>344
まず「単射」という概念を理解した方がいい。
ググればいくらでも出てくるだろう。予備知識は必要ない。
それでも分からなかったらここで聞いても無駄。
350:１３２人目の素数さん
11/02/18 21:03:00
>>344
その条件は3の後はかならず3'にしかいかないということを言ってるだけで
3'の前がかならず3になってるとは言ってないからだよ。
後者の条件はお前がどうしても外したがってるx'=y'→x=yのほう。
351:１３２人目の素数さん
11/02/18 21:24:25
久しぶりにスレが伸びていると思ったら
またこの流れか。
352:１３２人目の素数さん
11/02/18 21:28:40
竹内・八杉の『証明論入門』
芯の通った思想を感じる本だね。楽しくなってくる。
353:１３２人目の素数さん
11/02/18 21:53:00
和書しか読まないから
竹内の本がありがたく感じる。
もちろん良い本だけど。
354:１３２人目の素数さん
11/02/18 21:54:39
何か他の条件から後続関数の単射性が言えれば仮定しなくても良い。
どのみち、分からん君が置き換えたがってる等号公理からは出ないが。
355:１３２人目の素数さん
11/02/18 21:57:11
>>350
それだったら同じ理屈で、x'=y'→x=y だと
1の次が2だったり3だったりしてしまうのでは？
356:１３２人目の素数さん
11/02/18 22:04:20
>>355
∀x x'≠0という公理があるから特に0≠0'=1。
ところが1'=1'' だとすると1'=(1')'→1=1'だから1=1'、
つまり0'=(0')'となって同様にして0=0'となって矛盾する。
357:１３２人目の素数さん
11/02/18 22:14:38
>>356
まじで？
358:１３２人目の素数さん
11/02/19 05:24:22
x≠y → x'≠y'
359:１３２人目の素数さん
11/02/21 00:33:29.67
基本的なこと分からない人は、
島内さんの「数学の基礎」をよめばどうかな。
基礎論の初歩的なところを手取り足取り進めてくれるから。
中学生でも理解できるような歩みで。
360:１３２人目の素数さん
11/02/21 01:00:24.59
あれε記号使ってたような
361:１３２人目の素数さん
11/02/21 07:25:58.31
shenfieldのmathematical logic1冊で充分だろ。
362:１３２人目の素数さん
11/02/21 08:21:03.83
>>326にShoenfield薦めるとか頭おかしいとしか思えん。
p→qとその逆のq→pを混同してるかもしれないレベルなのに。
363:１３２人目の素数さん
11/02/21 17:07:35.54
>>360
いや、それどころか自然数の公理系まで入ってるけど。
364:１３２人目の素数さん
11/02/21 17:19:04.08
>>359
その本の目的がいまいちぴんと来ない。
読みてはどんな人がターゲット？
365:１３２人目の素数さん
11/02/21 23:51:21.86
広く浅く学びたい趣味人だろう。
366:１３２人目の素数さん
11/02/22 17:07:57.67
>>364
>>326に勧めてるじゃんw
367:１３２人目の素数さん
11/02/22 23:35:42.32
有限の立場では、背理法の無制限な使用は認められますか？
368:１３２人目の素数さん
11/02/23 08:02:56.58
有限の立場ってのは有限公理化可能ってことだとするなら、
ZFCやMKは有限でないが、NGBは有限。
排中律を公理にするかは１階述語論理での話で、
むしろ背理法なしで無矛盾な集合論を展開できるかということ。
答えはYes。
369:１３２人目の素数さん
11/02/23 08:14:46.30
こりゃまた斬新な答えだ
370:１３２人目の素数さん
11/02/23 10:13:34.91
有限の立場は人の数だけあるとは言うが…
371:１３２人目の素数さん
11/02/23 12:09:40.31
少ない脳味噌を如何に活用するかってことなんですね。
372:368
11/02/23 19:56:25.65
>>369>>371
文句があるなら論破してみろ。
373:１３２人目の素数さん
11/02/23 20:04:38.06
どこから手をつけろと言うんだｗ
374:368
11/02/23 20:22:42.56
>>373
言い訳乙＾＾
375:368
11/02/23 21:10:09.87
全員まとめてかかってこい！
ジャクソンとショーアのlow basic theoremより
recursive degreeを下げることで不完全性定理は成り立たないようにできる！
376:１３２人目の素数さん
11/02/23 21:15:08.73
basicってことはadvancedとかもあるの？
377:１３２人目の素数さん
11/02/23 21:27:56.54
結局、有限の立場で背理法はOKなの？
378:368
11/02/23 22:13:03.52
>>376
basicってのは日本語では恐らく基底とか基数に該当するので基本とかではないです。
379:368
11/02/23 22:19:23.25
>>377
有限の立場の立場を明確にせよ
380:１３２人目の素数さん
11/02/23 22:21:36.12
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers.
It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist.
381:368
11/02/23 22:59:50.96
>>377
述語の数を増やせばできます。
382:１３２人目の素数さん
11/02/23 23:43:01.36
>>378
いやlow basis theoremのはずなのにスペル間違ってたから
きっと内容分かってないんだろなと思ってからかっただけだよ
というかジャクソンってもしかしてJockuschのことじゃないだろうな？
383:１３２人目の素数さん
11/02/23 23:52:38.94
>>367
ヒルベルト達の言う有限の立場で示せる命題と言うのは、
或る特定の自然数に対する命題（Δ0式）とか、
或いは変数 x を使って x に対して成り立つ命題を証明することで
「任意の x に対して～～」を示す、とか、つまりかなり直截的に証明できるものなので、
∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、
そういう凝った証明は出て来ないんじゃないかと思います。
従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、
背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。
だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。
384:１３２人目の素数さん
11/02/24 00:02:15.70
訂正
∀x P(x)を仮定して背理法によって∃x ￢P(x)を示すとか
385:368
11/02/24 00:14:58.16
>>384
∃x ￢P(x)は∀x P(x)の略記じゃないんですか？
386:368
11/02/24 00:21:42.85
>>382
ああそうだよ、内容なんてわかってないよ。
俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、
最近shoenfieldを読み始めたばかりだよ。
low basis theorem についてはある人のブログで知ったんだよ、問題あるか？
387:１３２人目の素数さん
11/02/24 00:26:29.37
議論・喧嘩してるわけでもないのに、なんで名前固定してんのこの人
388:１３２人目の素数さん
11/02/24 00:26:46.53
仮に∀x P(x)を仮定して～～みたいな議論がそもそも無いので
￢∀x～～という論理式がそもそも出て来ない。
だから￢∀x￢が出て来ないからその略記としての∃xもそもそも出て来ない。
あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
389:１３２人目の素数さん
11/02/24 00:28:01.31
くあんてぃふぁいあふりー
390:１３２人目の素数さん
11/02/24 16:44:00.27
素人でこの方面興味持つ奴は概ね基地外
391:１３２人目の素数さん
11/02/24 20:11:19.86
>>387
話の展開をわかりやすくするためだろ。
392:１３２人目の素数さん
11/02/24 20:28:22.40
というかロジックの場合、他分野では優秀な数学者が
往々にしてトンデモだったりするから困る
393:１３２人目の素数さん
11/02/24 21:04:17.78
>>392
www 本当杉て困る。
394:368
11/02/24 22:45:14.87
まともに勉強していないからに決まっている。
395:368
11/02/24 23:12:50.35
集合論研究者でさえ
論理学をやったことない人がいる。
396:１３２人目の素数さん
11/02/25 12:41:58.62
いまどき素朴集合論のみで食ってる研究者なぞおらんわ
寝言は寝てから言え
397:１３２人目の素数さん
11/02/25 12:44:27.44
いや、普通の数学の専門家は可算濃度と連続濃度の算法しか分からんのが結構いる。
398:１３２人目の素数さん
11/02/25 13:40:21.63
>>397の「いや」へ
>>395-396の流れを読め。
399:368
11/02/25 19:53:26.53
>>396
公理的集合論やモデル理論の研究者で
ロジックをやったことがないといのは
結構あるぞ。
400:１３２人目の素数さん
11/02/25 20:18:53.14
いやモデル理論はロジックの一部だし。
あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。
非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
401:368
11/02/25 22:19:27.88
知識あれば良いけど、
キューネンとかウッディンとかの本読んでるけど、
論理学のテキストまったく読んだことない人間でも
読めると思うけど？
実際に自分が読めてる。
論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。
実際に直感的に明らかな論理学の結果しか使わないし。
何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
402:１３２人目の素数さん
11/02/25 23:35:13.21
Woodinって何読んでんの
403:368
11/02/25 23:57:02.29
The Axiom of determinacy,
forcing axiom, and the non-stationary ideal
404:１３２人目の素数さん
11/02/27 01:20:35.00
>>399
> 公理的集合論(略)の研究者で
実際に何やってる人?
組合せ論的な構成可能集合の研究とか?
405:１３２人目の素数さん
11/02/27 21:35:27.99
基礎論を勉強し始めたど素人ですが、どなたか教えてください。
前原「数学基礎論入門」で、「等号の基本性質」の節の冒頭にある、
次の記述意味が分かりません。
>sとtがn階の対象式である場合には、s=tは、
>∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1})
>という論理式の略記法であった。
ここで、_{n+1}により下付き文字をあらわしました。
この定義ですと、t∈ξ_{n+1}でかつ、￢(s∈ξ_{n+1})となるξ_{n+1}が
存在した場合でも、論理式s=tが成立し得るというふうにとれます。
その意味で正しいのでしょうか？
普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、
思えるんですが。
406:１３２人目の素数さん
11/02/27 21:42:08.97
ξ_{n+1} の前に ∀ があるので、適切な内包公理の下で、
∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から
∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。
ちょっと読み進めばそのことが書いてあるはず。
407:１３２人目の素数さん
11/02/27 21:43:42.25
>>405
"集合" ξ_{n+1} の補集合を考えれば、
s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
408:１３２人目の素数さん
11/02/27 21:53:53.94
>>406
>>407
ありがとうございます。
ちゃんとした理屈があることが分かり、安心しました。
内包公理や補集合をヒントに理解してみます。
409:１３２人目の素数さん
11/03/03 15:09:48.69
知ったかぶりのバカが集まるすれですね
何の役にもたたないのにｗ
410:１３２人目の素数さん
11/03/03 16:30:05.36
自己紹介ご苦労
411:368
11/03/03 21:57:25.77
>>404
点集合トポロジーだったかなんだったか。
>>409
俺もそうだけど、別にいいじゃん知ったか。
知ったかでも博士とれちゃう国あるんだよ、世界には＾＾
412:１３２人目の素数さん
11/03/03 22:08:12.18
だったら無駄に名乗らないでください
邪魔なんで
413:368
11/03/03 22:34:23.08
>>412
こんな俺でも
ここじゃちょっとは役に立つと思って助言してる。
なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる
人間みるとつい助けたくなっちゃう。
414:１３２人目の素数さん
11/03/03 22:55:43.28
>>413
じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？
415:368
11/03/03 23:09:52.65
>>414
pcfはJechに載ってるだろう。
予備知識などいらん！
416:368
11/03/05 23:12:13.84
志賀の無限からの光芒って面白いね。
知らなかった定理が結構ある。
417:１３２人目の素数さん
11/03/06 06:14:59.41
証明抜きが多かった記憶
418:368
11/03/07 21:37:05.07
>>417
まぁ本来啓蒙書なんで。
その割には証明がある丁寧な本程度と考えた方が。
419:１３２人目の素数さん
11/03/16 18:44:12.04
東北大学のサイト落ちてますねえ。
まあ仕方ないかな。
420:１３２人目の素数さん
11/03/16 18:46:10.16
被災地域の大学生、教員でアボーンした人どれだけ居るのやら。
421:１３２人目の素数さん
11/03/16 19:09:28.70
田中一之さん、東北大学だよね。心配ですねえ。
422:１３２人目の素数さん
11/03/17 13:19:17.80
今東北にロジックの学生どれくらいいるの？
423:１３２人目の素数さん
11/03/17 13:24:44.90
学徒動員。福島原発に突入せよ。
424:１３２人目の素数さん
11/03/18 22:11:10.98
質問です。
命題論理のごく初歩的なところをやっているんですが、
replacement theoremとstrong replacement theoremの違いがわかりません。
wff Aを何回か含むwffをC[A]とし、C[A]の中のいくつかのAをwff Bで置き換えた結果をC[B]とする。このとき、
replacement theorem：AとBが論理的同値ならばC[A]とC[B]も論理的同値
strong replacement theorem：(A←→B)→(C[A]←→C[B])はトートロジー
なぜ、後者のほうが「強い」のでしょうか？
425:368
11/03/18 22:19:34.59
strong replacement theorem
なんて初めて聞いた。
426:１３２人目の素数さん
11/03/18 22:22:50.44
それはお前が無知なだけ
427:368
11/03/18 22:45:13.30
>>426
そんなら425をサクッと説明しちゃってくださいよ。
428:１３２人目の素数さん
11/03/18 22:50:59.58
なにこの糞数字コテ
429:１３２人目の素数さん
11/03/18 22:56:57.07
「A→Bが証明可能」 ⇒ 「Aが証明可能⇒Bが証明可能」
だけど、逆は一般には成り立たないことに
なぞらえてるのでは？
430:１３２人目の素数さん
11/03/18 23:05:57.04
だって、replacement theoremとstrong replacement theoremは同値じゃん。
なんでstrongなのかわからん
431:１３２人目の素数さん
11/03/19 00:31:55.49
そういうときは
wff、置換、論理的同値、トートロジー
の定義を書いてみよう。
書いているうちにわかる場合が多いよ。
432:１３２人目の素数さん
11/03/19 00:33:29.97
なにその万能な回答
433:１３２人目の素数さん
11/03/19 00:44:12.36
万能文化猫娘
434:431
11/03/19 00:50:10.47
え、割と有効なやり方だと思うんだけど
435:368
11/03/19 08:09:26.45
まぁ確かに定義を書くことで
頭が整理されるってことは結構あると思う。
436:１３２人目の素数さん
11/03/19 09:44:19.26
strong replacement theoremというのは一般的な呼び方じゃないと思う。
別の名前が付いている訳でもないけど。
AならばBというのとA→Bはトートロジーだというのでは
後者の方が強い気はするよね。
トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。
437:１３２人目の素数さん
11/03/19 11:07:58.09
ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
どなたか、お教えください
よろしくおねがいします
438:368
11/03/19 11:58:48.45
>>437
> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
言葉の定義とかも書かないとわからないと思いますよ。
普通の数理論理学のテキストにない用語が多いですから。