数学基礎論の質問スレッド その5

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

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。

前スレ
数学基礎論の質問スレッド その4
http://science6.2ch.net/test/read.cgi/math/1207899938/

初歩の質問する奴は>>1すら読まない

いま基礎論て何やってんの?
なんか成果ある?

>>3
基礎論詐欺

基礎論はオワットル

「数学基礎論および歴史」スレッドにすべきだな

続きは前スレ埋めてからな

基礎論やってたやつは
いま何してる?
給料泥棒

もうみんな墓の中

自然数は自然数を含む全ての集合の共通部分として既定されていると聞きましたが
それが自然数以外を含まないことはどのようにして証明されますか？

内容も日本語も疑問をもつところもおかしい

基礎論の墓碑銘を考えるスレになりました。

Odifreddiのエッセイが和訳されてるね

>>11
説明が下手ですみません
自然数のみを含む集合は、無限公理によって存在が保障される、全ての自然数を含む、全ての集合の、共通部分として定義されますよね？
それが自然数以外の集合を含まないことは、どのようにして証明されますか？

自然数を定義するときに「自然数」という概念を
使っちゃ駄目なのは分かるかな。

だから自然数全体の集合の定義は
「全ての自然数を含む全ての集合の共通部分」
じゃなくて
「〜〜を満たす集合全ての共通部分」になる。
〜〜に具体的に何が入るのかは自分で勉強して下さい。
ただそれ以前に分かってないといけないのは
〜〜の中に「自然数」という言葉が入ってはいけない、ということ。

で、「ωを含む集合全ての共通部分」がどうして実際にωと等しいのかだけど、
自然数の全体というのが一つの集合を成すのならば、
「ωを含む集合」にはωも含まれるのだから、これはωよりも真に大きい集合にはなりえないよね。

ありがとうございます
＞自然数の全体というのが一つの集合を成すのならば
しかし「自然数の全体」が直接記述できない以上これを仮定できない気がするんですが・・・
たとえばある集合が共通部分集合の要素であると証明された場合
それがいずれかの自然数に必ず等しいと言えるのでしょうか

流石にトンチンカンすぎる、>>15の内容を全く理解できてないな。

＞それがいずれかの自然数に必ず等しいと言えるのでしょうか
この文章の「自然数」というのはどういう意味で使ってるのかが
そもそも良く分かんないんだよね。

例えばここで「自然数」といったときに、Peanoの算術でも何でも、
「自然数」の満たすべき性質が列挙されているのなら
ωがその全てを満たすことを示せば良い。

逆に、定義がほかに別に与えられていないときに、
この定義が妥当であることを「証明」しろというのは全く無理な話なんだよね。
定義のある言葉と定義の無い言葉が同値であることを示せって言ってるんだから。

定義を与えずに厳密な議論をすることは不可能なのだから、
>>16で書いてあるようなことはそもそも証明しようがない類の話じゃない？

極論を言えば
滑らかな函数というのを無限回微分可能な実函数と定義したときに、
滑らかなだけど無限回微分可能でないような函数が存在しないのは
どうやって証明するんですか？と言ってるのとあまり差はないような。

>>16
>>18を見てもわかるように、現在の基礎論は「自然数」という概念さえまとも扱えないんだよ。

電波が電波を呼ぶ展開

てか基礎論でいい日本語の教科書ないよね。教えてる大学も少ないし。みんなは独学なの？

それにしても、たまに来る電波は教科書のせいじゃないと思う

>>19
それは現在の解析学は滑らかな函数という概念さえ云々
とか言うのと同じじゃないだろうか

>>18
すみません、自然数は０に有限回＋１をしたもの、ということでお願いします
自然数かどうかは人間が式を眺めれば分かりますけど集合論の式ではその「有限」を定義するのに自然数が必要になって循環してしまう気がします
可算個の式を使えるなら０と等しい、または１と等しい、または２と等しい、・・・、で定義できるんですけど・・・

その「有限」が定義されてない以上同じでしょｗ

別にその「有限回」というのは無限回ではないとかいう意味で書いてるのではないよね。
　0, 0+1, 0+1+1, 0+1+1+1, 0+1+1+1+1, .........
のことを自然数と言うといいたいんだろうけど
.........なんて使った「定義」はただ直観的な把握の為にあるだけのもので、
厳密じゃないので、もっと論理式で表せるような定義をしないと。

>>24
はたから見てて思うんだけど、そろそろここで質問なんかしないで自分の力で苦しんで解決するしかないと
思うよ。ちゃんと回答されてるのにわからないって言うんだから。君の疑問は、たぶん君特有のものだよ。
自力で何とかしないと。

>>25
ありがとうございます
そうすると人間が自然数を把握してるというのは錯覚なのでしょうか・・・
少なくとも自分はどれが自然数であるかを厳密に知っている気がします

人間が知っている自然数に関する知識の総体は
再帰的だろうか？再帰的可算だろうか？
とかそういうことはたまに考えたりする。
まあ実際には有限なんだろうけど。

何か変なネタ本をつかまされたんだな

数学者が扱っている自然数と
基礎論が扱っている自然数が
総体として一致するかどうかなんてどうでもいい

初心にもどってブール代数を騙れ

有限集合の定義には自然数は必要ない。
集合Aを定義する時にA自身を用いる事は実数の部分集合では普通にある。

＞集合Aを定義する時にA自身を用いる事は実数の部分集合では普通にある。
それは、本来は論理的にダメなんだけど
well-foundedな順序に関して帰納的な定義をする限りにおいては
それでwell-definedになるという定理があるからそういう定義ができるのであって、
今の話とは関係ないような

>>27
何かを証明しようと思ったとき、定義、公理など前提とするものがなければ
証明というもののありようがない。
あなたが自然数をよくわかっているなら、何を証明しようとするのか？
また、自然数をわかっているなら、自然数に関する色々な定理は証明など
しなくてもわかるのではないのか？

んな事言ってたら解析学なんて展開出来なくなるんだが

>>35
すでにわかっていることを公理としているということだ。

>>36

>>35は>>33の

＞ それは、本来は論理的にダメなんだけど

に対して

>>37
なるほど！
どっちの書き込みに対しての反応ともよめるね (:

>>35
かなりの部分がきちんとできる。
竹内のふたつの応用とかに例がある。

レスの文脈と「集合Aを定義する時にA自身を用いる事」だから
帰納的定義のことを言ってるのかと思ったけど違うっぽいね。
>>32ってもしかして帰納的定義じゃなくて
非可術的定義のことを書いてあったのかな？

非可術的定義ってのはきちんと書くと
「対象 a を定義するときに、 a を含む集合に言及
（したり、或いは a を含む領域での量化を用いたり）すること」。
要は a ∈ b ∈ c ∈ ......... という風な所属関係があった場合、
a は必ず b より先に、また b は c よりも先に定義されていないといけない、
というのが可術的定義。

「集合Aを定義する時にA自身を用いる事」というのはちょっと違う。
A ⊆ R の上限 sup A を定義するために集合 A を文章の中で使ったりするのが
典型的な非可術的定義だけど、この場合、 (sup A) ∈ A というだけで、
別に A を定義するための文中で A とか sup A とかに言及してるわけじゃないので。
というか別に A は定義無しのただの変数で構わない。

いずれにせよ>>31よりも上のほうで質問者が使ってるのは
「P(x)をP(x')かつQであることとして定義する」みたいな
明らかにマズいだろって感じの循環論法のことなので
predicativity云々は関係が薄いと思う。

>>14
表現は稚拙だがいいたいことは判る。

> それが自然数以外の集合を含まないことは、どのようにして証明されますか？

証明不能であることが証明されている。

そういうことを言ってるのかとは考えないでもなかったが
いずれにせよ何か混乱しすぎているし買いかぶりでは

ということで>>26に戻る。

>>14とは別人ですが。

「それが自然数以外の集合を含まないこと」(?)って
フォーマルにきちんと表現したらどういう表現になるんでしょうか？

「ZFCは偽な算術の命題を証明しない」(S)とは表現できませんよね。
自然数の標準的モデル N より真に大きいが、（一階の）
自然数論の命題に関する限り全ての文で N と真偽が等しくなるような
拡大モデル M (⊃ N)みたいなのは実際に存在することが証明できますし。
つまり(?)は(S)より明らかに強いことを言っています。
（まあZFCから(S)は証明できませんから、(?)がきちんと定式化さえできれば、
ZFCから(?)が証明できないことはすぐ分かるんですが。）

それにそもそもこの際、自然数の標準的モデルとかそういう言葉遣い自体が不適切ですよね。
モデルというのはメタ理論として仮定されている集合論の中で集合を為すものですから。

なんか曖昧で混乱したまま話が進んじゃってるような。

>>44
> なんか曖昧で混乱したまま話が進んじゃってるような。
何も曖昧なところはないよ。証明不能であることが証明されているし。
混乱しているとしたら、君が混乱しているだけだろ。

0は自然数なの？

>>45
いや、だから証明不可能であることが証明できるというのだから
「それが自然数以外の集合を含まないこと」ってのは
論理式で書けるような命題なんですよね。
具体的に書くとどういった論理式なんですか？ということなんですけど。

どうしてみんなネタ本をもう少し丁寧に読まないのだろう

ネタ本じゃなくてトンデモ電波な人間が独自解釈でネタにしてしまうから
学術論文を読んですらネタ的解釈をしてしまうトンデモを止める術はない

大学出て10年ほど経っているのですが、一般教養での数学が
イプシロンデルタもやらないぬるいものだったので、
今から独学で数学やり直そうと思っています。
集合・位相の入門って微積分の前にやるものですか？後ですか？

やっぱり>>1すら読まない馬鹿が現れた
スレタイから「基礎論」は外した方が良いと思う

こうか？

「数学の質問スレッド その6」

【数学】foundations of mathematics【基礎論】

えー、
数学科って何やってんですか?

広義にはスレ違いではないと思うが。

>>http://science6.2ch.net/test/read.cgi/math/1207899938/998-999
どんな過疎板だろうが二日放置して残っているとこはない。

ゲーデル読んで思ったんだが、真の定義ってなに？
今までは真＝証明可能だと思ってたんだが単にブール関数の値が1になるって事かい？

>>57
読んだって何を読んだの?

初心者なのでよく分かってないのですが、洋書のゲーデルの不完全性定理でオックスフォードのやつです

半端な知識は害にしかならない

「真」の定義うんぬんってのは、セマンティクスの話じゃねぇの？？シンタクスとごちゃまぜにしちゃいかんよ

>>57
ゲーデル系では「真」という概念は定義されていない（し、できない）。
議論できるのは証明可能かどうかだけ。

ですが冒頭には真であるが証明できない命題を作るのが目標的な事が書かれていたのですが…
それが不完全性って事じゃないんですか？

解釈とか真とか恒真とかでググってみ

>>63
ゲーデル命題：「この命題は決定不可能である」は、証明も反証もできない以上、
系外の立場からの超越的な解釈によって（要するにその意味を考えて）真とすることができる。
系内では証明できないので真とすることができない。

ちょっとおかしいな

× 系内では証明できないので真とすることができない。
○ 系内で真偽の概念を定義する必要はない。

還元公理ってって何ですか？

基礎論の入門書で最も程度の高い本は何でしょうか？
Shoenfieldですか？

>>57
まず意味論と証明論の違いが分かって無かったら、完全性定理、あるいはその前からやり直した方が良いです。
第一不完全性定理の意味論は非形式的な自然数論(スタンダードモデル)で我々の普段扱ってるもの、証明体系は一階述語論理のペアノ算術。
第一不完全性定理を大雑把に言うと「スタンダードモデルでは真になる命題で、ペアノ算術で証明出来ない決定不能命題Gが存在する」となる。
ここで「証明体系Tが完全」≡「全ての命題φについて、φか¬φをTで証明できる」となり、完全性定理(恒真な命題は証明可能)の完全とは違う事に注意。
完全性定理と不完全性定理は両立し得、一階述語論理は典型的。
第一不完全性は非形式的な自然数論における計算可能述語というクラスと、ペアノ算術におけるΣ(Π)文というクラスを表現定理で対応させて論証を行なうから、両者の区別が出来て無いと混乱するだけだよ。

「証明も反証も出来ない」だったな。ごめん。

>>67
http://c.2ch.net/test/-/math/1207899938/141

>>71
ありがとうございます
タイプ理論特有の公理で通常の集合論には関係ないということでしょうか？

>>71
ttp://c.2ch.net/test/-/math/1207899938/141
について。

PM (Principia Mathematica) の初版は見たことがないので、憶測だけど。

還元公理は分岐した型理論の公理で実用的な観点から要請されたものである。
PM の2nd edition では、分岐した型理論ではなく単純な型理論を採用している。
現在出回っている PM は 2nd edition 以降のものに基づいているので、
還元公理は書いていないような気がする。

Quine の本に載っていた気もするけど、真面目に読んだことがない。

一階述語論理が不完全なのは当り前じゃないか……決定不能性ですね。
完全性は任意の解釈と論理体系の間、不完全性は特定の解釈(標準モデル)と算術(論理体系＋算術の公理)の間で考えてるものだから、逆に誤解を招く書き方をしてしまった。

グッドスタインの定理の証明には選択公理を必要としますか？

一階述語論理で関数と述語にはどのような違いがあるのでしょうか?
なんだか似た概念としか分からないんです
ちなみに命題論理はわりと分かってるつもりです

>>76
個体変数を受け取って、個体変数を返すのが関数、真偽値を返すのが述語。

>>77
値域が真偽値の関数が述語と言っていいですか？

>>78
意味論においてはそうです。
証明論においては真偽値なんてものは無いので、

n変数関数f:任意のタームt_1,t_2,……,t_nに対して、タームf(t_1,t_2,……,t_n)を作る
n変数述語P:任意のタームt_1,t_2,……,t_nに対して、命題P(t_1,t_2,……,t_n)を作る

と、述語は「タームの組から命題への関数」と見ることが出来ます。

ゲンツェンのカット定理ＬＫを学ぶ標準的教科書
は何でしょうか？

>>47
初心者ですか？
斎藤先生の数学の基礎218ページでも読んでください。

>>80
小野『情報科学における論理』

>>82 ありがとうございます
洋書だと何が標準的でしょうか？

>>80
Cut除去定理に関しましては、松本和夫先生の「数理論理学」と竹内外史の「証明論入門」なんかに詳しく書いてあったかと思います。
またネット上で配布されているPDFで良ければ、金子洋之先生の
http://www.isc.senshu-u.ac.jp/~thb0442/winter05.pdf
が詳しいです。LJで書いていますが、LKは場合分けの数を増やせば大丈夫だったかと。
また同じくLJに関しては鹿島亮先生が解説しているPDFもあった様な気がします。

>>83
エンダートンのマスマティカルロジックがお薦め

>>80
NKから見るという観点からは、林晋の「数理論理学」もおすすめ。

洋書だと、竹内外史の「Proof theory」なんだろうか。

>>83
MATHEMATICAL INTRO TO LOGIC のことですか？
そこにはカット除去定理はありませんが

カット除去が載ってない参考書薦めてるのはなんだかなあ、、

「情報科学における論理」は、命題論理のカット除去は前原先生の証明法が載ってるけど
述語論理に関しては証明などは省略されてて参考文献（>>84>>86あたりの本）参照という
ことになってるので、カット除去の教科書としては微妙。いや良い本なんだけどね。

>>83
カット除去定理について知りたいことがあるときに読む本となると、
たぶんTakeutiとかいうことになるけど、証明論の教科書なら大抵、
基本的なことは載ってるはず（多分）。Troelstraらの Basic Proof theory
とかSchutteとか Pohlers（最近universitext化した）とか。

>>72
普通の集合論（つまり一階述語論理上のZFCとか）には関係ないです。
型無しの述語論理の上に展開されてるので。
二階のZFC(Morse-Kelley集合論と同一視してる人(Steelとか)も居るけど
2nd order ZFCとMKは別だという人も居る)がどうのとか言い出したら、
全く関係無いとも言い切れませんけど。

http://quod.lib.umich.edu/cgi/t/text/text-idx?c=umhistmath;idno=AAT3201.0001.001
web公開されてるPM（第一版）。*12.1 (p167) からThe hierarchy of types and the axiom of reducibilityという章がある。
以下も参照。
http://en.wikipedia.org/wiki/Axiom_of_reducibility

>>81
「数学の基礎」の218頁っていうとこれですかね。
　しかし、形式的自然数がどれも直観的自然数で
　あるかどうかは、それを認識する手段がない．実際、個々の直観的自然数は
　形式的自然数であるが，<<直観的自然数の全体>>というものは集合論では捉
　えられない．
証明不能であることが「証明されている」というのはこれが根拠だったんですね。
>>41がどういうレスだったのか良く分かりました。


>>44にしろ>>47にしろ、「それを認識する手段がない」「捉えられない」のは
そもそも問題の定式化自体が出来ないからであって、それを認識する手段の無いことが
論理学的・数学的に証明できるというのは違うんじゃないか、くらいの意味のレスだったんで、
別に形式的自然数＝直観的自然数だなんて言いたかったつもりは毛頭無いんですがね。

計算可能性の定義なんかはこれと良く似た状況なんですけどね（包含関係は逆だが）。

帰納的関数はすべて計算可能な関数と見なされる。しかし
計算可能な関数がどれも帰納的関数であるかどうかは、それを認識する手段がない．
実際、個々の帰納関数的は計算可能な関数であるが，<<計算可能な関数の全体>>
というものは再帰関数論では捉えられない．

こんな記述があったときに、「計算可能関数が全て帰納的であることは
証明できない」ということが証明されている、とか言いますかね？普通。
要はHilbertのテーゼの特殊な場合だと思うんですけどね。

言葉の遊びはもういい

変項が可算無限個あり、個体定項、関数、述語が有限個であるペアノ算術は、定項(またはターム)、命題(または文)の数はそれぞれ可算無限個でしょうか？それとも不可算でしょうか？

独自解釈して勝手に怒るんだもの

変項が可算無限個あり、個体定項、関数、述語が有限個であるペアノ算術は、定項(またはターム)、命題(または文)の数はそれぞれ可算無限個でしょうか？それとも不可算でしょうか？

またペアノ算術で証明可能なる任意の文は標準モデルで真になるというわけではないですよね？

>>92は書き込みミスです。失礼しましたm(_ _)m

ペアノ算術とか関係なく記号の有限列の全体は可算個しかないので可算だと思いますが。

完全って何？
簡単に説明してくれないか

どの完全だよ

なるほど完全にも色々あるんだな
ブール代数で否定論理積はそれ一つで完全であることを証明せよ、ってな感じだったらどう言えばいいんだ

>>99
functional completeness ですね。

質問です。
次の方程式を解いてください。
√10-x^2=x+2
＜ポイント＞
グラフを用いない無理方程式
２条して√をはずす
方程式の場合　Ａ＝Ｂ→Ａ＾２＝Ｂ＾２は成り立つが逆は成り立たない…＊
√をはずして得た解が最初の方程式を満たすかどうか確認する

解説・解法
方程式の両辺を二乗して　10-x^2=(x+2)^2
整理して　(x-1)(x+3)＝０　よってｘ＝１,-3
X=-3は与えられた方程式を満たさないから　ｘ＝１

こういうことが問題集(黄チャート数３基本例題８)に書いてあるんですが
＊ の行に書いてあることが成り立つなら
＝で結ばれた式を両辺二乗して出した答えが
必ずしも正しい答えとは限らないということになって

たとえば

sinθ＋cosθ＝１／２
（sinθ＋cosθ）＾２＝１／４　　　sin^2θ＋cos^2θ＝１より
１＋２sinθcosθ＝１／４
sinθcosθ＝-3/8
この答えも両辺を２乗して出した答えだから
正しいとは限らないことになると思うんですが
僕が納得できる説明を出来る方いますか？
お願いします。

>>101
>>1

>>102
すいませんスレ違いでした。

>>101
マルチ

97,99のものだが
>>100
英語ではそういうのか

結局のところ完全であるとは何を言えばいいんだ
何を示せたら証明したことになるんだ
誰か優しく教えてください

完全な組(Not/And/Or)をnandで示せばええんじゃね

完全は概ねできてほしいこと、またはできるべきことが全てできるということ

>>106
じゃあANDとORとNOTが完全であることはどう示すんだ？

完全っていうものが、ここではどう定義をされているかっていうのがわからないと示せなくないか

>>107
およそなんてナンセンスだろ

前の>>107へのレスは無視してくれ

>>107
できるべきことが全てできるって言うのをもう少し具体的に言ってくれないか

ＬＫやカット除去定理のどこらへんに意義があるのか、よくわからないんですが。

ゲンツェンでググれ

>>110
決定可能性

>>110
証明図の変換と言う手法。これがその後の超限帰納法を用いたペアノ算術の無矛盾性証明に繋がる。

PAの無矛盾性を証明するには，健全性定理（モデルを持てば無矛盾である）を使って，
「(N,０,S,＜,＋,・)はPAのモデルだからPAは無矛盾である」というのはダメなんでしょうか？

それで示したのは
「自然数論の標準的モデル N が存在するならば、PAは無矛盾である」
であって、PAの無矛盾性じゃないし、そういうのを無矛盾性証明とは言いません。

自然数全体の集合なんてものが存在するということは
無矛盾性証明では使ってはいけないと，そういうことですか？

>>116
PAからNが証明できれば使ってもいいＹＯ！(ﾟ∀´)d

>>116
普通は前提として使ってはいけないですね。
もし議論に使った集合論が矛盾してたらどうするんですか？

集合論はPeano算術なんかより遥かにぁゃιぃ理論だから、
Peano算術は無矛盾かつ有意味なのに集合論は矛盾してる、
なんてこともあるかも知れない。

数学者：自然数なんて無矛盾に決まってだろ
論理学者：形式化された自然数論の無矛盾性は有限の立場では証明できない
哲学者：数学には矛盾があるかもしれないニダ　たいへんニダ

数学以外のことは数学の外でやってくれ

数学じゃないとかいう問題じゃなくて
循環論法に近いんだよね

>>120
この辺のスレ伸ばしてる馬鹿に言ってくれ

http://science6.2ch.net/test/read.cgi/math/1240985720/
http://science6.2ch.net/test/read.cgi/math/1234568394/
http://science6.2ch.net/test/read.cgi/math/1234967031/

十分基礎論の範囲の話だと思うけどなあ。基礎論嫌ならここにこなきゃいいのに。
どうしても基礎論をバカにしないと気がすまないのかしら。

いや、そもそもペアノ算術に対して標準モデルは健全なのか？
端的に「PA|-∃xP(x)⇒N|=∃xP(x)」何かを示すにはω無矛盾性、ひいては「全ての(勿論変数を含む)タームは数項と＝で結べる」ことが必要だと思うんだが。

言葉遊び(というか、言葉に弄ばれてる、という方が正確かも)と基礎論を
混同しちゃう人は哲板にいくほうがいいよ。

東大数理か京大理学に基礎論の研究室ができれば基礎論の地位も上がるよ、きっと

誰に言ってるんだ？

無矛盾性の証明の話が言葉遊びだというのなら
基礎論は言葉遊びから始まったことになるぞ

>>126
京大数理はなんで除外すんの？

基礎論やってる大学あるの？

なかったらこのスレの奴らはどこで基礎論を学んだと

いやまあ学部のときとか最初は独学の人も多いだろうけど
基礎論の研究者自体は結構いろいろな大学の数学科に居るよ。

どっからが工学部とか情報学科のロジックで
どっからが数学科のロジックなのかは曖昧だけど。
日本では哲学科で記号論理/数理論理研究してる人は少なそうだね。

証明論、集合論、計算論、モデル理論だっけ？
それぞれどこの大学院がいいの？

東大か京大

あったらいいのにね

>>130
学部で基礎論教えてる大学が周りで無いからほとんど無いのかと思った。
あと京大は解析、統計が強いイメージしかない。

京大は総人にそれっぽい教員がいるけどなんか違うような気もする

「どこの大学院が良い」というか、
どの先生の下で何を勉強したいのか、というように考えた方が良い気がする。
場合によっては僻地（北陸とかｗ）の大学がベストな選択肢になるかもしれない。

それに一口に証明論つっても順序数解析もそうだし逆数学もそうらしいし
非古典論理みたいなのも証明論に入るかもしれないし。

計算論はどこが良いんだろうなあ。
そもそも計算量理論じゃなくて計算論（computablility theory）の
研究者ってほんと数えるくらいしか居ない気がする。

ここ20年以上まったく成果がない分野で研究者が増えるわけがない

ま、どんな分野であれ、増えたところで・・・

日本人の名前が出てこない分野だとなおさら集まらんだろうね

>>138
そこまで、なかったのか。

>>138が知らないだけでしょ。

フィールズ賞等にふさわしいような目立った成果がないってことでは？

Mordell-Lang conjecture for function fields
というのは、目立った結果ではないということですか。

「フィールズ賞にふさわしいような目立った成果」は
代数幾何とか低次元多様体論とかじゃないと無い気がするｗ

まあ後者は今後あまり出ないかもしれないけど

144は候補にはなったな。
集合論は進歩し過ぎて、他の数学者が理解できなくなって久しい。

証明図を書くのに良いソフトって無いですか？

TeX
もしくはフォトショ

TeX使っても簡単には書けないけどね。
まあproof.styみたいなのもあるけど。

エクセルで…

エクセルか
確かにそれはちょっと便利そう

私はVisual Tabularとかいうソフトを使っています。そんなに書きやすいわけではないですが、
直接LaTeXで書くよりは楽です。

LinuxがあればxpeというソフトでTEXは描きやすくなるみたいだけど

レーベンハイム-スコーレムの定理の証明が乗った書物を教えて頂けないでしょうか。なるべく日本語が良いのですが、無ければ英語のものでも構いません。

例えばゲーデルと20世紀の論理学の
二巻の「完全性定理とモデル理論」とか。

数学基礎論とか数理論理学とかいう書名の本なら
結構載ってるので、別にこの本に拘らなくても良いだろうけど。

古典論理体系NK,
自然推論体系NJ,
直感主義述語論理LJ,
古典述語論理LK,
はメタ的にはどういう包含関係になってるのか教えてください
LJ⊃LKみたいな

>>156
どういう本読んだんだ。
自然推論体系やシーケント推論体系は論理体系の表現法。
古典論理、直観論理は論理体系の種別。
NJ=LJ,NK=LK
この間では証明図を相互に変換できる（逆関数にならないけど）

本なんかロクに読まずにとりあえず概要から入りたい人なんじゃね？
そういう人は結構多い。

和書で述語論理の完全性定理の証明が書いてある本ってあるでしょうか？
なるべく初学者にも分かりやすいやつで(´･ω･`)

清水の記号論理学が読みやすい

http://www.utp.or.jp/bd/978-4-13-012018-0.html

>>157
今手元にないのですが、松本和夫というひとの本だったと思います

知り合いから、「カット定理」の証明が載ってるから、とオススメされて買ったのですが、
ゲンツェン、シークエント計算とか、解析学では見たこともない言葉が多くて
混乱していたのです
NJとNKは基本的に別のものなのかすら、分からず
公理と推論規則のうちいくつかは共有してるだろうと勝手に推測して包含関係を尋ねてしまいました
回答いただき、ありがとうございます

分かってると思うけど>>156のNK、NJ、LK、LJの日本語が滅茶苦茶。

どんな読み方したのか知らんけど、普通にその本読んだなら
理解してて当たり前くらいのものだと思うんだけどなあ。
手元の「数理論理学」も一応確認したけど、
誤解別にしやすい書き方でもないし。
速読術を駆使して三十分で読破しましたとかそんな感じなのかな。

パラ見しただけで読んでないんだろ
おそらく>>158の言うパターンそのままだと思う

そういえばN,L,K,Jはそれぞれ何の略なの？Nはnaturalとかだろうけど、他はわからんなあ。

>>165
fjよりコピペ

u+ウムラウトを \"u と記しています。

手元に原論文がないので(英訳の論文集ならある)原論文のどこに出ているか正確なことはわかりませんが、前原先生のずいぶん前に絶版になった

数理論理学 数学的理論の論理的構造
(数理科学シリーズ６) 培風館

では以下のように記しています。

LK (logistischer klassischer Kalk\"ul)
NK (nat\"urlicher klassischer Kalk\"ul)

LJ (logistischer intuitionistischer Kalk\"ul)
NJ (nat\"urlicher intuitionistischer Kalk\"ul)

それ以前に logistischer Kalk\"ul という言い方が出てきますので LK, NK の K は klassischer か Kalk\"ul のどちらかでしょう。

intuitionistischer なのになぜ J なのかという疑問がありますが、ドイツ文字の大文字は I と J とを区別しないということと関係があるのでしょう。

原論文でのドイツ文字を英訳する際に I -> J になってしまったという怪説を見たことがありますが、残念ながら原論文でもラテン文字で LJ と記していました。

>>165
英語じゃねーよ

えふよっと

計算も古典もＫか

タルスキの不完全性定理ってなんですか？
たぶん集合論についてなんですが。

真理定義不可能性のこと？

集合算言語で決定不能命題の存在することのなんちゃらってやつです
集合算言語って何ですか？？

http://portal.mie-u.ac.jp/syllabus/?action=display&id=4997
これとかに書いてある奴のこと？
だとしたらタルスキの該当する論文で指定されている言語のこと、
としか言いようが無いけど。

「集合算言語」と言っただけでは、ああアレだという風に一つには定まらないよ。

不完全性と言うのは「Aだ」も「Aでない」も証明できないようなAが存在すること。
ただ、タルスキーのこの業績を「タルスキの不完全性定理」なんて呼ぶのは
大げさ過ぎだし、タルスキーを贔屓しすぎだと思う。

>>173
そうです、ありがとうございます。

>>173
そうです、そこのシラバスで目にして気になったもので。
解説ありがとうございます。

ゲーデルの証明できないことを証明可能って矛盾じゃない？

確かに単なる一つの公理系では証明不可能でもメタ数学ではって区別ついてるのはわかるけど。

でもどんどん構成して、全ての数学で証明が構成不可能と、証明を構成するって背理じゃない？

>>176
不完全性定理のステイトメントをきちんと書いてみれば？
＞わかるけど。
たぶん分ってないと思うよ。

>>176
林・八杉翻訳のゲーデル『不完全性定理』（岩波文庫）を読め
これを読んで理解できないんだったら不完全性定理は自分に縁がないと思って諦めろ

じゃ教えてくれよ。自然数論の公理系で公理では証明できない自然数論の命題があるとやるわけだろ？
だけど拡張していって数学全体でも証明できない命題が、
数学で構成イコール証明できるとなれば、おかしくね？

>>179
体系での話と体系をメタに扱う話の区別、
つまり、
証明できることと、真偽とも証明できないことが証明できるは違う。
ここから始まる。

おかしくない。

自分の勝手なイメージだけで用語を作って演説かますからおかしくなる。
自分で言ってる意味わかってるか？
ヘルメットかぶってたお兄さんじゃなかろうなｗ

「証明できる」とはどういうことかここに書いてみろ

思考が不鮮明な奴は言語からして不鮮明な奴が多い

>>176みたいに怒鳴り込んでくる奴って
どうしてまず自分の頭を疑わないんだろうな

>>181
ある公理系において証明できるとはその公理系と適当な推論規則で導けること

>>176>>179
普段こういう話し方してるんだと想像すると笑えるなｗ

悪い、見間違えた
質問者かと思った

その「数学全体」とやらの公理系って具体的に書き下せるもんなの？
そんな公理系は聞いたこと無いが。

>>179
> だけど拡張していって数学全体でも証明できない命題が、
> 数学で構成イコール証明できるとなれば、おかしくね？

数学全体という発想がそもそも間違い。

ゲーデルの不完全性定理が含意する事柄には様々なものがあるが、その一つとして「数学は無限であって閉じる事はない」、
つまり「これだけの公理と推論規則があれば全ての数学を表現できます」という公理系は存在し得ない、というのがある。
これは不完全性定理から直ちに導かれる事実。（少し考えれば分かる事）

だから「数学全体」などというものは最初から概念的にも存在し得ない。

>>180

＞ >>179
＞ 体系での話と体系をメタに扱う話の区別、
＞ つまり、
＞ 証明できることと、真偽とも証明できないことが証明できるは違う。
＞ ここから始まる。

いや、だから数学全部で考えれば区別がなくなるって話なんだが。

>>189
>>188

証明できる。
真または、偽、あるいは真偽決定不能に決定できる。
無矛盾性仮定すればゲーデル命題は真にも決定できない、
偽にも決定できないけど実は真だって話で真偽と決定可能性分けるって話だろ？
だけど推論規則から導ける構成できる命題全体で考えれば真偽決定不能なら真偽決定不能だろ？
決定不能だけと真とか矛盾じゃん。

>>187

ん？具体的に書き下ろせる、構成できる数学全体だろ？
何か変？

>>191

不完全性定理は証明可能性に関するものであり、真偽の概念とは全く別もの。
無論、偽なのに証明できてしまう公理系は矛盾してるから無価値だが、真だからといって証明できるとは限らない。

証明可能性と真偽概念とが区別できないのなら、不完全性定理には縁がないと思って諦めろ。お互いに時間の無駄。

>>188
論点ずれているな。
別にスーパー公理系とか求めているわけじゃないよ。
ゲーデル命題自体、真だとは思えない、数学が無矛盾とは決定しえないって話だけど。

>>193
＞ 無論、偽なのに証明できてしまう公理系は矛盾してるから無価値だが、真だからといって証明できるとは限らない。
＞
＞ 証明可能性と真偽概念とが区別できないのなら、



だからその話しかしていないっつーの。知能障害？
その区別が成り立たなくなるって話？わかる？

>>194
だから林・八杉の翻訳書を読めと言ってるんだ。
ゲーデルの不完全性定理をきちんと理解したいならば、その証明をきちんと追う以外に方法はないんだから。
不完全性定理の証明はとても技術的な話だ。その証明の当否をお話レベルで理解しようというのがそもそもの間違い。

証明の詳細を追って自分で点検するのが嫌ならば（当然ながら人類の９９．９９％以上の人間はそうだろうが）、
ゲーデルのやった証明を信じるか無視して不完全性定理そのものに近づかないようにする以外に道はない。

>>195
> >>193
> ＞ 無論、偽なのに証明できてしまう公理系は矛盾してるから無価値だが、真だからといって証明できるとは限らない。
> ＞
> ＞ 証明可能性と真偽概念とが区別できないのなら、
>
>
>
> だからその話しかしていないっつーの。知能障害？
> その区別が成り立たなくなるって話？わかる？

成り立たなくなると思うのはお前が知能障害だから。
そう言われたくなければ、ちゃんとゲーデルを読め。

>>196

なんだ説明できないのね。ならくるなよ。

>>198
> >>196
>
> なんだ説明できないのね。ならくるなよ。

お前こそ最低限の勉強もしようとせずにガタガタ意味不明な事を並べて騒ぐな。

>>191
> 実は真だって話で
そんな話は無い。

ア，真だけど決定できない証明できない命題がある。決定したら矛盾だから。

矛盾してしまうから決定不能。なら真じゃない。初めの仮定間違ってるってことだろ。
アが間違っているんだろ。

>>192
変。

>>201
統語論と意味論が別物だというところから始めないとお前の場合はダメだよ。

>>192
だーから数学全体ってのを定義しろよ
任意の無矛盾な公理系でいいのか？

>>203

それはあんたがわかってないなｗ

／ADA＼ ＜トリップの使用を提案

>>204

任意な無矛盾の公理系で証明できない命題全体含めて全て真な命題全体だな。
そこからそれでも真偽決定不能な命題あるとしてもないとしても。

えらくちっちゃいんだな、数学全体って…

>>207
＞任意な無矛盾の公理系で証明できない命題
そんなものは論理的矛盾でもない限り存在しません

>>201
> ア，真だけど決定できない証明できない命題がある。決定したら矛盾だから。

この１行目が既に意味不明。「証明できない」は良いとして「決定できない」とは「証明できない」と同義語のつもりか？
それともは「反証できない」のつもりか？

まあ良い、「決定できない」を削除してアを「真だけど証明できない命題がある」と読もう。

ゲーデルの不完全性定理の表す「内容」をアだと「説明」したのは前原昭二だが
前原自身が、後年、「あの説明は誤解を招いて良くなかった」と後悔していたのは事実だ。

ゲーデルの不完全性定理そのものは、本質的には「真」や「偽」の概念とは無関係だ。
「自然数論を含む無矛盾な公理系では、ある命題が存在し、その肯定も否定も証明できない」、そして
「そんな決定不能な命題の具体例としては、その公理系が無矛盾だという事を形式化した命題である」
これがゲーデルが不完全性定理で示した全てだ。

> 矛盾してしまうから決定不能。なら真じゃない。初めの仮定間違ってるってことだろ。

ここには、真なんて話は出てこないんだよ。

> アが間違っているんだろ。

間違ってるのはお前の脳味噌。

なんだかんだ言ってみんなの優しさに泣いた

あ

伸びてるなー
ちょっと知識があれば突っ込み所満載なのが一目瞭然だから
レスしたくなるのも分かるけどね

>>207
「任意な無矛盾の公理系で証明できない命題全体含めて全て真な命題全体」
じゃ意味不明。
（言語及び）公理系を定めないと真も偽も何も無いんだよ。

「真な命題」とかいうけど、例えば連続体仮説 CH は
その「数学の全体」に含まれるの？ not CH が含まれるの？
それとも CH も not CH も含まれないの？
207の「定義」じゃ全然分からないけど。

>>191
＞無矛盾性仮定すればゲーデル命題は真にも決定できない、
＞偽にも決定できないけど実は真だって話で真偽と決定可能性分けるって話だろ？
公理系 T からはゲーデル文 G は証明できないってだけの話で、
T に「Tは無矛盾である」を「意味」する命題 Con_T を付け加えた
T + Con(T) からは G が証明できる。

任意の無矛盾の公理系からその公理系では証明できない無数の命題があって、
それは無矛盾性の要請から真だよな。公理系で証明できるもの、証明できないけど真なもの。
そういう全体の構成、決定できるもの全体の中からゲーデル方式で決定不能な命題構成できるが、
それが真偽決定不能なのは構成証明イコール真なわけで真だとしても偽だとしても矛盾じゃん。

わかってないな。馬鹿だなｗ

>>213

わかってないｗ

>>213
げんごなんてにほんごでいいじゃねーか（ぼうよみ

>>214
> それは無矛盾性の要請から真だよな

おまえのなかの「無矛盾性」の意味が一般とは違うもののようだ。

一応注意しとくと、

「数学全体」じゃあまりに意味不明だからとりあえず
自然数論のみを考えることにして、
「自然数論における真な文全て」を T と置いたりすると
T は不完全性定理が成り立つための三つくらいある前提条件のうちの
或る一つを満たさなくなって、 T が不完全であるということは言えなくなる。

不完全性定理は「任意の無矛盾の公理系」に対して成り立つわけじゃないんだよ。
（たぶん）無矛盾だけど完全な理論の例なんて、
ロジック勉強してる人なら大抵知ってるだろうし。

>>214
＞そういう全体の構成、決定できるもの全体の中からゲーデル方式で決定不能な命題構成できるが

ダウト

>>214
＞任意の無矛盾の公理系からその公理系では証明できない無数の命題があって、それは無矛盾性の要請から真だよな。
違うよ

>>220

んなら全ては決定可能で真偽分かれてるの？

>>201
> ア，真だけど決定できない証明できない命題がある。決定したら矛盾だから。

この場合、最後の「矛盾」はどの理論を対象にしてるかな？

>>223
＞
＞ この場合、最後の「矛盾」はどの理論を対象にしてるかな？

これは自然数論の公理系だな。確かに。だけどそこで公理系分けろというのはわかるけど、
数学体系全体の無矛盾性や超数学の背理性は否定しがたいけどな。

>>221

なら、数学は始めから無矛盾で真偽決定できるわけ？
なら基礎論自体いらないし。
それがわからないから議論しているんだろ。

「そういう全体の構成、決定できるもの全体」
って何のことだか全然分からんのだけど、みんな良く理解できるな

背理背理って言うけど矛盾してるのは
お前が使ってる曖昧な用語だろと

>>222
証明も反証もできないと言う話に、真偽は出てこないよ。

>>225
違うよ。

>>225
真偽を決めるのは「解釈」と呼ばれる意味論的な「関数」で、これは一意ではなく無数にある。
ゲーデルの話は証明論、文あるいは命題と呼ばれる文字列を推論規則と呼ばれる
有限個の変形手続きで到達できるかどうかの話。

基礎論は君の言ってるような意味不明のことを議論するものではないよ。

＞任意の無矛盾の公理系からその公理系では証明できない無数の命題があって、それは無矛盾性の要請から真だよな。


完全性定理から勉強しなおせ。もし、任意の公理系で

無矛盾⇒真（モデルをもつ）

ってんだったら、どうなると思う？？

わかってない馬鹿ばかりだなｗ

だから基礎論なんて掲示板で議論するのに一番向いてないでしょ

>>230

あんた、面白い。

釣りはもういいよ、本物の207どこいったんだ？

膝小僧をかかえながら
「ボクは馬鹿じゃない、みんなの方が馬鹿なんだ」
と涙目になりながらつぶやき続けてます

妙にスレ伸びてたんだな
ざっと読んだが、何を言いたかったのか
数学全体云々に関する結論は>>219かね

不完全性定理の前提条件には帰納的公理化可能というもんがあってだな、

ある公理系から証明できない命題を可能な限り全て加えて新しい公理系とする、とやりたかったんだろうが、
そういう方式だと、一般には帰納的公理化可能になってくれないんだな

だから、仮に「数学全体」とやらを考えたかったとしても、
それが帰納的公理化可能になるという保証がないから、
数学全体とやらに、ゲーデルの不完全性定理を適用できる保証は無い

馬鹿多すぎｗ
帰納とか整列させるとかテクニカルな話はどうでもいいんだって。
その手の扱いやすいものだけでしかゲーデルの不完全性定理が通用しないなら、
ほんとどうでもいい話だし。ゲーデルでインパクトあったのそこじゃないだろ。
喚き立ててた馬鹿も消えたしｗ
数学で証明不能と真偽自体は別なわけないじゃん。
数学で証明不能と証明できる。矛盾は避けられないっつーの。

釣りはもういいよ…

せめて新しいネタを入れて書いてくれないかなあ

なんかリアルで誰にも相手されないからネットの中でだけは誰かにかまってほしいのかな

「整列させる」なんて>>237以外の誰が言ってるのか知らんが、
「帰納的公理化可能」っつうとテクニカルな感じがするけど、要するに
「ある文が公理であるかそうでないかは
機械的に判定できなければいけない」ということ。

公理かどうかは偉い人がケースバイケースで判断する、とか、
俺が決める、みたいなのはダメだ、というごく当然の話。
そういう場合にまで通用する定理を考え出せってのは
無理な話なので続きはどっか別の場所でやってて下さい

＞その手の扱いやすいものだけでしかゲーデルの不完全性定理が通用しないなら、
＞ほんとどうでもいい話だし。
たぶん207にとってはどうでもいい話なんだと思うよ

馬鹿の檻にわざわざエサ放り込むなよ

あ〜あ、燃料投下しちゃったよ。

>>241
　　　　　　＿
　 　 　 ／,.ｧ､＼
　　 　 (　ﾉo o ) ）　　空
　 　 　 )ヽ ◎/(.　 　 気
　　　 （／.(･)(･)＼　. 嫁
　　　 （／|　x　|＼）
　 　 　 ／／＼＼
　　　. （／　　　＼）

いやあ暑いのにタフだなあ

偽207の釣りはもう飽きた。新しい餌をくれ

お前ら、馬鹿すぎｗｗｗｗｗ

馬鹿がうつるからもうこのスレは見ない方が良いよ

>>241
馬鹿すぎｗｗｗ
笑える！

エンドレス

不完全性定理は直観主義論理を用いては証明出来るの？

wikiの証明を見ると
第1も第2も不完全性定理の証明で対偶を使っているけど
直観主義論理では対偶の真偽値は元の命題の真偽値と一致しないよね

> 第1も第2も不完全性定理の証明で対偶を使っているけど

なんだって？もう少し明確に事実のみを根拠に挙げて話してくれないかな。

そもそもツッコミどころはそこじゃない

>>251
> 不完全性定理は直観主義論理を用いては証明出来るの？

この質問は曖昧。

（１）古典論理に基づく形式的理論に関する不完全性定理がメタ論理として直観主義論理を用いて（つまり構成的に）証明出来るのか？

（２）直観主義論理に基づく形式的理論に関する不完全性定理がメタ論理として古典論理を用いて（つまり非構成的に）証明出来るのか？

（３）直観主義論理に基づく形式的理論に関する不完全性定理がメタ論理として直観主義論理を用いて（つまり構成的に）証明出来るのか？

の３通りの読み方が出来る。

この後の文章を見ると、（１）か（３）の意味を意図して質問しているのだろうが。

(2)は常識的に考えて明らかだよね

常識www

>>255
> (2)は常識的に考えて明らかだよね
まあね、でも元の質問が読めるという意味で列挙に含めておいたんだ。
それにあんな質問をしてるんだから「常識」がない可能性だってあるしｗ

常識的を基準にしてそこで思考停止するなら数学なんぞいらない

>>254
そう問われると(1)か(3)と答えるけど
元の理論がどういう論理を使って構築されているかは
ほとんど無関係なんじゃないの？
古典/非古典論理に関わらず
元の理論の推論規則は
ゲーデル数化するために
それぞれ自然数への関数として表せれば良いだけでしょ

推論規則が無限にあるような体系があると
制限が必要になるかもしれないが
違うならすまない

ああ、強い方の結果で証明出来るね
自己解決
ttp://r6.ca/Goedel/goedel1.html

>>256>>258は何を言ってるんだ？
(2)は自明だって言えば分かるか？

>>261
第二不完全性定理はそれほど自明ではない。

馬鹿ばっかし。笑える。

>>263
真面目に勉強しろ！ばか者！
そんな態度じゃ何も身につかないぞ！

馬鹿ばっかし。
無矛盾な形式体系の内部で証明できない命題＝数学の構成できる内部では証明できない命題がある。
と、数学で形式化し証明できる。数学では証明できないと数学で証明できる。

わかりやすいのにな。笑えるｗ

俺はさみしいんだよ！
まで読んだ

メタ数学使って完全性を証明すればいいじゃん

>>265
学会に発表しろよ。

威勢が良かった馬鹿どもも沈黙か。笑える。
数学で構成できる証明の外部に数学の証明を考える必要ないのにな。
内部に取り込まれているんだから。
数学で証明できないと数学で証明できる。何の不思議もないのに。

だから学会に発表しろよ。

259だけど207が言ってることは別に変じゃないと思うけど
ただ、「数学では証明できないと数学で証明できる」能力自体が
対象の数学になければそれは言えない

プログラミング言語でも同様のことがなりたっていて
無限ループする関数f
プログラムが停止するならばtrue,そうでなければfalseを返す述語halt
int g(x){if halt(x) then f() else 1}
この関数の引数xにgを渡すとhaltの動作は矛盾したものになるためhaltは定義出来ない
cでもjavaでもチューリング完全な言語ならhaltは定義出来ないが
文脈自由文法で定義出来る文法クラス/正規言語のクラスでも同様のことが成り立つのか
チューリング完全でないSQLではどうか

成り立たないクラスが存在するのは明らかで
HQ9+のようなプログラミング言語を考えれば自明

その最小の境目はどこなのかについては
数学の世界では研究されているの？

増えたぞ

良くわかんないけどプログラミング言語の能力を制限していくことによって
haltが定義できるようになったりはしないんじゃないの？

B が証明できるから A も証明できてしまったら矛盾、
みたいな証明の場合に、同じ議論が成り立つための条件の
下限を求めるような研究はあるけど、それはあくまで
B が成立する下限を求めているだけだと思う。

>>273
>良くわかんないけどプログラミング言語の能力を制限していくことによって
>haltが定義できるようになったりはしないんじゃないの？

極端な話、あらゆる入力に対し true を返す関数以外存在しなければ、halt は作れます。

それは「プログラムが停止するならばtrue,そうでなければfalseを返す」
という条件を満たしているの？

停止性を判定しないといけないプログラムの範囲も
狭まるから作れるとかそういうことかな。

なんだか、制限算術の方向に行きそうな感じだな。

>>275
> それは「プログラムが停止するならばtrue,そうでなければfalseを返す」
> という条件を満たしているの？
>
> 停止性を判定しないといけないプログラムの範囲も
> 狭まるから作れるとかそういうことかな。

例えば型付きλ計算のバリエーションの中でもpolymorphicな型を許す（２階命題論理相当の型システムの）GirardのＦ2の場合、
自然数や真理値といった基本データを適当な形のλ項として表し、計算はこれらのλ計算の体系でのreductionとすれば、
その計算に基づくプログラムは必ず停止するから、haltは渡されたプログラムを解析する必要さえなく、無条件にtrueを表す
データを返す１引数関数として定義すれば良い。

このやり方はずるいけどね。

つまりメタ理論上の結論（Ｆ２の強正規化性定理）を用いて停止性判定述語haltのプログラミング作業を一気に省略してしまってるんだから。

haltを地道に作ろうとした場合、つまりhaltが渡された関数（というよりも、haltが停止性を判定する為に関数の中身を分析する為には、
関数でなく、関数のソースコードあるいは理論の言葉で言えば関数のゲーデル数をhaltが受け取る必要があると思うが）をちゃんと分析して
停止性判定を行う場合にどうなるかは分からん。

Ｆ２では地道なhaltは記述できない可能性がある。

もしも仮にＦ２で地道にhaltが記述できるならば、そのhaltのコードにはfalseを返すブランチもあるんだけれど、
渡された関数のコードを色々と解析した挙句、決してfalseのブランチには分岐しないという形になるだろうね。
何しろＦ２で書けるどんな関数も必ず停止するんだから、その関数のコードを解析するhaltがfalseを返す事は有り得ない。

>>275
>それは「プログラムが停止するならばtrue,そうでなければfalseを返す」
>という条件を満たしているの？

すべてのプログラムが停止して true を返すのだからあたりまえ。

Saul A. Kripke　　“The Collapse of the Hilbert Program: Why a System Cannot Prove its Own 1-Consistency,”　Abstract, in: The Bulletin of Symbolic Logic, vol. 15, no. 2, 2009

それってここから落とせる物？まだ中身空だけど
ttp://www.math.ucla.edu/~asl/bsl/1502-toc.htm

>>260は直観主義論理ではなく古典一回述語論理での証明

計算機論やるならホーア論理くらい書けよ

>>281
> 計算機論やるならホーア論理くらい書けよ

計算機論といっても
Hoare Logicは手続き的プログラミングにしか使えないがね
しかも上の停止性判定の例で出てるｇのような関数を引数で受け取るのに対する
Hoare Logicは殆ど使い物にならないぐらい煩雑だがな

関数プログラミングならば型がある言語に対してならtype theory、
型がなけりゃλ計算に関するconversionで定義されるequational theoryだろ

ずいぶん昔にそういった言語に対して健全なHoare論理を作れないことは
2年前にチューリング賞とった人が証明済

>>283
> ずいぶん昔にそういった言語に対して健全なHoare論理を作れないことは
> 2年前にチューリング賞とった人が証明済

うろ覚えで出鱈目は書かんように。
Hoare Logicを語るならせめて林の内容ぐらいはちゃんと理解し切ってからにしろ。
「健全な」じゃない、「相対的に完全な」だ。

不完全性定理の前に完全性定理勉強しろと言いたい

完全性定理自体意味ないわな。

意味って何？

ユークリッド幾何と非ユークリッド幾何とか、
連続体仮説とか、矛盾しあう数学いくらでも展開できるんだから、
大域的には意味のないこと前提で、モデルによる無矛盾性といってもただこの内部、
ユークリッド幾何の内部は整合性とりましょって話以上でも以下でもないしな。
ゲンツェンとかの超限帰納法とかによる数論の無矛盾性証明も、
局所的に無矛盾性納得しましょうってだけだし。

数論の内部では証明できません、しかし、超限帰納法使って、
どの命題も無矛盾で真でありますと言うところにどんだけ意味があるのか。
その命題も確定してんのか。

矛盾しあう数学と言ったって
可換環論とLie環論は矛盾するとかいうのと似たような話だけどね

そりゃ公理を一緒くたにすると環が可換かつ非可換になって
矛盾するだろうが、だから何だというのが正しい反応であって
だから大域的には可換環論は意味が無いとか言い出すのはかなり妙な話

無矛盾性証明もそういう話だな。

１：ペアノ算術は完全かつ健全。(不完全性定理の意味では不完全)
２：Kirby-Parisの定理「グッドスタインの定理はペアノ算術の範囲では証明も否定の証明もできない」

無限集合の公理を使えば必ずグッドスタイン数列は収束することがわかるそうですが
そうするとグッドスタイン数列の収束性は実質、真ですよね

真偽どちらにも証明は出来ないけど実際は真であるような命題って
不完全性定理の証明におけるゲーデル文の真偽とは種類が違うように思うのですが
完全性定理はこういった特殊な命題に対しては役に立ってなくないですか？

「ペアノ算術は完全」って何？いみふ

最後の三行は何を言いたいのか全然分からんのだけど
たぶん最後のピントのズレた疑問はこういうところに
理解不足があると思う。

＞真偽どちらにも証明は出来ないけど
言葉遣いがおかしい。変。
この命題を偽に証明する、とかそういう言い方しますか？
普通はしませんよ。

一階ペアノ算術は一階述語論理上の公理系なので、完全性定理が適用できる
とWebで見たのですが間違ってますか？
真偽が〜の部分はすみませｎ
証明も反証も出来ないと読み替えてください

謝る必要はないよ。
言葉遣いから、あなたの学力を推察しただけだから。

（意味論的）完全という性質を持つのは
ペアノ算術じゃなくて一階述語論理だと考えるのが普通だけどね

任意の命題φに関して
完全:「N|=φ⇒PA|-φ」
健全:「PA|-φ⇒N|=φ」
とするなら成り立たないのでは？健全性は少なくともω無矛盾性が必要だし。
まあΣ文の中とかに限定すれば完全性は成り立つね。更にΔ文の中に限定すれば健全性も成り立つと思うけど。(間違ってたらごめん)

大学文系のペーペーですが
カントールの対角線論法について質問です。
対角線論法は、集合の形が縦軸＝横軸の正方形の形にならないと成立しないと思うんです
でも、普通、当てはまる数のパターンを描こうとすると
例えば「0と1によって表せる2桁の数」のばあい
00
01
10
11
と、２*４の長方形になってしまい、対角線などひけることはありません
結局新しい数が現れるのは、座標が正方形でない以上、当たり前なのではないでしょうか
この点について、私が無限の概念を取り違えているのだと、説明おねがいしたいです

正方形だと仮定して矛盾を導くのが対角線論法なんだから正方形っぽくなくて当たり前なの

そもそも別に対角線論法って必ずしも「新しい数を作る論法」じゃないよ
一種の不動点定理だとは言えるかもしれないけど

>>298はなんかそこらへん勘違いしてる気がする
「0と1によって表せる2桁の数」に対角線論法を適用するとか言われたって
何がしたいのか全然意味が分からん

「横が可算個で、もし縦が可算個だったら個数が同じ→長さが同じ→正方形→対角線が引ける→でもこれだと矛盾するじゃん！→実際は正方形じゃないんじゃね？」
っつー論法だから実際は正方形じゃなくて良いんだよ。横がn個だとしたら縦が2^nになるから2のアレフ乗は不可算になる。

2のアレフ0乗だなすまん

>>298
自分のイメージとか直観とかに固執するから独自解釈をしてしまう。
つまずく人に共通するのは「こうであってほしい」という願望のようなものに
とりつかれているところ。

はっきりいうとスレ違い
質問する前に>>1くらい読め、馬鹿

私大文系卒（>>298とは別）ですが、対角線論法は基礎論の範疇、あるいは関連していると思ってました。
違うんですか？

ゲーデルの不完全性定理に対角線論法ライクな手法が用いられてるけど
>>298のは完全に素朴集合論の範囲、スレ違い扱いは妥当だろう。

にしても対角線論法を新しい数を作る論法と考えるトンデモは後を絶たないな。

トンデモばっかりだからな。

足し算も基礎論の範疇、あるいは関係しているけどね

あんなに騒いでいた馬鹿も消えたな。
ゲーデルの不完全性定理の自然な拡張で、
局所的な完全性定理を修正するってごく当たり前な話なのにな。
馬鹿はしようがないからな。

>>214
＞任意の無矛盾の公理系から
＞その公理系では証明できない無数の命題があって、
＞それは無矛盾性の要請から真だよな。

いや。任意の無矛盾な公理系で証明できない命題は、定理の否定しかない。

なぜならば、ある無矛盾な公理系で、Aも¬Aも証明できない場合
その公理系にAを追加しても、¬Aを追加しても無矛盾だから。
Aを公理とすればAは証明できるし、¬Aを公理とすれば¬Aが証明できる
したがって、どの無矛盾な公理系でも証明できない命題には
Aも¬Aも含まれない。

＞数学で証明できないと数学で証明できる。

いや、証明できるのは
「矛盾が証明できないなら、
　矛盾が証明できないことも証明できない」
だが。

ちなみに
「ある命題が証明できないなら
　ある命題が証明できないことも証明できない」
というのも上記の系として証明できる。

決して、命題が証明できないこと自体は証明できない。

馬鹿はしようがないからな。

>>310
よくそんなバカなことを滔々と書いているな。

> いや。任意の無矛盾な公理系で証明できない命題は、定理の否定しかない。

この「証明できない」というのは、どこでの証明なのだ。「任意の無矛盾な
公理系をどのように無矛盾に拡張しても証明できない命題はそのもとの公理
系の定理の否定しかない」といってほしいものだ。

数板っぽくないスレだな。
揚げ足とりの応酬は哲板を彷彿とさせるものがある。

そりゃ数学基礎論なんて哲学科でやるもんだからな。

いや、基礎論は十分数学だろ。哲学要素もまだまだ濃いが。

数学も哲学の一分野だから諦めろ
基礎論が数学ならそれは基礎論は哲学と言うことだ

ハテ哲学で解析とか統計とかやるのか？

日本の哲学でやらないだけ
哲学とは本来数学や自然科学も含んでいる大きい学問

>>318
統計やりたきゃ経済系の学部逝きな

はいはい哲学最強哲学最強

結局、哲学にはすべてが含まれることになるのかw

医学法学工学は明らかに含まれない

哲学＞＞＞（越えられない壁）＞＞＞数学⊃基礎論

でいいだろｗ

哲学⊃数学⊃基礎論
だと言ってるだろが

基礎論は数学じゃないと言ってるだろうが

もうなんでもいいよ
それで気が済んだら巣に帰れよｗ

ここが俺たちの巣だ

夏休みここまで

まだ始まってすらいないんだが
お前どこの大学だよ

荒らしを相手にすんな

レベル低すぎｗ馬鹿すぎｗ

数学と哲学とが交わった結果の不幸な婚外子が基礎論だ

学問を擬人化してみました☆(ゝω・)v

砂の器ですね

無限公理は神学に属する

a

馬鹿ばっかしｗ荒らしは死んだのかなｗ

威勢が良かった馬鹿どもも沈黙か。笑える。
数学で構成できる証明の外部に数学の証明を考える必要ないのにな。
内部に取り込まれているんだから。
数学で証明できないと数学で証明できる。何の不思議もないのに。

夏休みか･･･

>>340

笑える、馬鹿しかいねえｗ

せめて正しい用語使ってくれればなんとかなるんだけどそれをする気が無い以上結局はスルーなっちゃうよねぇ・・・

人のレスを真面目に読む気が無いからいずれにせよ駄目

基礎論の通常数学への応用に興味があるんだけど、何読んだらいいのかな。

>>344
「数学基礎論の応用」

>>343
本当に馬鹿ばっかし。笑える。

述語論理のカット除去定理で、左前提(Γ⇒Δ,D)と右前提(D,Γ⇒Δ)で、カットによって消える論理式Dが、∀xφ(x)や∃xφ(x)であり、
さらに両方の前提でDが主式だった場合(ここではD＝∀xφ(x)とおきます)、両前提はL∀とR∀から出て来て、片方はφ(a)、もう片方はφ(t)
(a:固有変数,t:適当なターム)から出てきますが、これをカットで消すには、φ(a)を持ったシーケントを根とした枝全体の、固有変数aを全てtに置き換えれば良いのでしょうか？

電波がホイホイ獲れるな、この板

>>347
左前提の上式を導くまでの証明図において固有変数 a が他の推論規則 R∀やL∃ の固有変数として用いられていないときには、全てを置き換えればよい。

そうでないときは、置き換える a を適切に選ぶ必要がある。

t に含まれる自由変数についての条件も必要だった。
t に含まれる自由変数が他の箇所で固有変数として用いられている場合は、
証明図全体の書き換えが必要。

馬鹿ばっかし。頭悪すぎｗ

>>345
著者は？
検索でみつからないのですが

>>352
http://webcat.nii.ac.jp/cgi-bin/shsproc?id=BN06172489
これだろ
とっくに絶版で出版社のホームページに書かれてないくらいくらいだからたぶん入手困難
上の検索結果に出てる大学の図書館で借りてください

大学図書館って部外者も借りれるんだっけ？

大学にも寄るけど普通は無理
館内での閲覧ならOKってところもある

国公立大で館内閲覧不可ってところはまずない
貸出に関しては不可のところと国立大学等の学生のみ可というところと所属国立大学等の図書館の紹介状がある場合のみ可のところがある
現在大学生・院生なら所属大学の図書館に依頼すれば紹介状を書いてもらえたり取り寄せてくれたりすることもある

>>356＋県内など特定の地域内の学生のみ可ってところもあるね

とりあえず電話等で問い合わせだな

>>349
鎖を考えた場合、固有変数aは、L∃やR∀の適用で消える瞬間は、適用される当の論理式以外に、そのシーケント自体に含まれず、適用直後も現れないので、
まず最初に、各L∃やR∀の直前の固有変数を全て、証明図上に出て来る他の変数と異なる様に書き換えれば大丈夫なのでしょうか？

>>352
数年前に、その本買ったから内容を見てみたよ。
基礎論の基本的な事項がほとんど。
いわゆる第10問題、計算量理論のさわり、あとはランダムとはとかが少し。
手続き型プログラミング言語の論理を公理化するのがめずらしいくらい。

「数学」への応用といったら、数論幾何への応用がされてるそうだ。
板井昌典『幾何学的モデル理論入門』とかみたことがある。

難しくて、不定法定式に帰着できて、妖しい匂いがすると基礎論がからんでくるのだろうか。

包含関係と否定関係の橋渡しはけっこう難しいんだよ。さらりと扱ってる
ものって結構あるけどね。

>>359
「数学基礎論の応用」なんてタイトルの本あるの？
俺も初耳だよ。
著者と出版社を教えて。

>>361
>>353 に書誌情報が出ている。
広瀬健（編著）『数学基礎論の応用』日本評論社
数セミ増刊で1981年の出版。再版されたかは知らない。
著者は、広瀬健、足立暁生、足立恒雄、筧捷彦、笠井琢美、難波莞爾。

>>362
ありがとう。
ごめん、>>353を見落としてた。
ああ、これなら古本屋で立ち読みした事があるけど
雑誌の増刊シリーズでしかも随分と古いのだからすっかり忘れてて
タイトルから全く連想できなかった。
てっきり普通の単行本だという先入観でレスを読んでたから。

通常数学への基礎論の応用って観点で日本語だと、>>359に挙げてた板井さんの本ぐらいだろうけど、
その本の副題にもあるように、通常数学への応用があるのは基礎論の中でもモデル論が一番なんじゃないの。
（そもそも、今や確率論なんかでは当然の道具になってる超準解析もモデル論から生まれたものだし）

証明論の場合、通常数学への応用なんて絶対に出てきそうな気がしない。
そもそも通常数学やってる人ってsyntaxとsemanticsを区別しないというか
ほとんどsemanticsだけでやってるから。（λ計算のRoger Hindleyが「数学者はsyntaxを知らない」と
言ってたのを聞いた事がある）

ゲーデル命題で肯定も否定も証明できない。できたら矛盾する。
形式的証明有限の手続きで拒絶しているとかの話じゃない。
形式体系で証明できないと形式体系で証明している。
この意味考えれば負け犬みたいなことできないのにな。

未練があるならきちんと書いてみればいいのにねぇ

馬鹿ばっかしｗ

正直な話207はまず数学よりも日本語の勉強をした方がいいと思う。
「てにをは」あたりから。

だいたい最初は不完全性定理は矛盾だ間違っているとか
言っておいて、最近になると不完全性定理を拡張して
「局所的な完全性定理」とやらを修正するだけだから
ごく当然の話だとか言い出すし。
（207自身にとって）矛盾している定理を拡張してどうすんだよと。

「局所的な完全性定理」なんてものは207の脳内にしかないんだから、
それと相矛盾しているとか言われたって知ったこっちゃ無い

>>367
笑えるｗ

ヌルーしろよ

まともに議論できないからと馬鹿ばっかし。
死ねばいいと思うよｗ


形式体系で証明できないと形式体系で証明しているんだから、
逃げも隠れもできないのに。笑える。

強制法を（ ZFC なり何なりの）モデル M の存在を仮定して、
M のなかからうまい G を取ってきて
それをもとにφ（¬CHとか）を充足するような拡大 M[G] を
構成する方法だと理解するのって別に間違ってはいないよね？

当面の議論に必要なZFCの有限部分 T1 を取ってきてどうのこうのとか
書いてあることが多いけど、こういうことにこだわる意味が分からない

ZFC +Con(ZFC) |- (M[G] |= ZFC + ¬CH)
を示してるんじゃなくて、非常に弱いメタ理論を仮定して
任意の T1 に対して
T2 |- (M[G] |= T1 + ¬CH)
を示してるんだよと言いたいんだろうか

あまり実用上は違い無さそうだけどなあ

サマースクール行きますか？

行ったら報告おねがい

散々荒らしといて謝りもしない馬鹿は死んだのｗ
いいことだｗ

お前も荒らし

議論できないくせに。
証明できないと証明しているこの単純な事実理解できないのｗ馬鹿なのｗ
じゃゲーデルの外で形式体系は証明できるの？
有限の立場と無限は違うとかナンセンス。形式的証明で証明できないのは証明できないよ。
形式的証明と超数学の実質的証明は別とか馬鹿なの？
頭悪いの？死ねの？

日本語が通じない+脳内理論展開

>>376
馬鹿乙!!

馬鹿って面白いな。
形式体系で証明できないんだから、それ以外の証明なんかあるわけないのにな。
外なんかないのにな。
証明できたらそれこそ矛盾なのにな。
そんな単純なこともわからない馬鹿は死ねばいいのに。

ゲーデル命題で証明できないと証明してしまっていて、
他に解釈のしようもないのに。
無矛盾性証明とか意味ないのに。完全性定理とか意味ないのに。

壊れたレコードプレーヤーだな

名無しで書けない奴は例外なく荒らし

マジこいつどっかいってくれねえかな。

ん？負け犬謝らないの？
形式体系で証明できない命題って、限定された公理系の話じゃなく、数学全部の話だろ？
お花畑としてどこかに証明できる楽園があるってわけじゃないだろ？
公理として取り込んでもそんなの意味がなくいくらでも証明できない命題作れる。
数学自体証明できない命題導き出してしまう。一部無矛盾でも、
それ自体は証明できない命題に囲まれたどうでもいい無矛盾性。
必然的に証明できない命題導き出しその存在は証明されている。
数学は証明できないと証明できる。矛盾した存在。
なんでこんな単純なことがわからないのｗｗｗ

負け犬なんで手をついて、私がわるうございましたと土下座しないの？
馬鹿なの？死ぬの？

なんでこんな単純なこともわからず荒らしは壊れたテープレコーダーみたいに、
同じこと繰り返すのかな。馬鹿丸出し。

＞完全性定理とか意味ないのに。
完全性定理の完全性は
　φがTの任意の解釈で真ならφはTから証明できる
不完全性定理の完全性は
　任意のφに対して「φ」と「φでない」のどちらか一方は証明できる
で違う意味なんだけど。

＞形式体系で証明できない命題って、限定された公理系の話じゃなく、数学全部の話だろ？
固定された何らかの公理系の話ですが何か。
数学全部とか言ってるのはこのスレの約一名だけ。

「Sを自然数の有限集合とすれば、どんなSに対しても
Sのどの数よりも大きい自然数 n が存在する」
と
「任意の自然数よりも大きい自然数 n が存在する」
を混同してるようなもんだ。Sは、前提条件を満たせば
何でもいいわけだけど、それでも固定されている。

こう分かりやすく書いても
どうせ聞き入れずに数学全体から証明できない云々と書き散らすんだろうけどね。
207にはこの二つの違いも分からないかもしれないし。

馬鹿すぎｗｗｗ

荒らしの相手をするやつも荒らし

>>371
以下山勘。誰か突っ込みヨロ。

そもそも
>ZFC +Con(ZFC) |- (M[G] |= ZFC + ¬CH)
が多分怪しい。

Kunen の本なんかだと、Mが（可算）推移的ε-モデル、つまり推移的で
Mの中の所属関係∈が本物の所属関係∈と同じモデル、として議論を進めている。
ここで重要なのはMが推移的ε-モデルであることより、Mがwell-foundedモデルであること。
実際そこかしこでMのwell-foundednessを使っている（M[G]を作るところとか）

一方で、確かZFC +Con(ZFC) からは ZFC のモデルの存在は言えても
ＺＦＣのε-modelの存在はいえなかったと思う。

そんなわけで、
>ZFC +Con(ZFC) |- (M[G] |= ZFC + ¬CH)
は単純にはいえないと思われる。
Mが ill-founded モデルだったりすると
Ｍ［Ｇ］をそもそも作れるのか？という問題が生じるわけで。

僕が馬鹿でした

本当に僕が馬鹿でしたorz

死にます

わかればいいのよ、わかれば。
ああ、笑わせてもらったｗ

笑いすぎて窒息死した

>>387
ああ、なるほど。

崩壊補題とかで何とか作ろうと思ってもなかなか作れませんね。
やっぱ強制法の勉強には或る程度きちんとしたモデル論が必須ですね

あれれ、それじゃ渕野先生の「強制法入門」の
「generic 拡大を用いた相対的無矛盾性証明のアウトライン」
の(9')(10')→(9)(10)って（少なくとも文字通りには）正しくなくなるような。

ZFCの任意有限部分がモデルを持ってもZFC自身がモデルを持たない場合とか、
ZFCがモデルを持っても∈（集合）モデルを持たない場合にまずいですよね。

>>394
まず、そのスライドだと「モデル」で「∈モデル」を意味していることに注意（脚注３）。
それと、定理9'は正確には（半順序集合を一個固定したとして）
　ＺＦＣの任意の公理φに対して、
　ZFC|- (ZFCの任意の可算推移モデルM とジェネリックフィルターGに対して、
　　　　　　M[G] |= φ)　・・・・（＊）
と考えるべき。

それで、確かに文字通りの意味だと若干問題ある。
結局のところスライドの通りに議論進めようとすると、
「定理9', 10'の証明を眺めていれば定理9, 10も成り立つことがわかるよ」
としかいえないと思う。
実際、上の(*)の証明を眺めていると、
MがフルのZFCのモデルである必要はなく、適当な有限部分Σで
　ZFC|- (Σの任意の可算推移モデルM とジェネリックフィルターGに対して、
　　　　　　M[G] |= φ)
となることがわかる。それで後は適当に有限なΓをとれば
　　　Γ|- (Σの任意の可算推移モデルM とジェネリックフィルターGに対して、
　　　　　　M[G] |= φ)
がいえる。後はこれの繰り返し。
非常に泥臭いけど (誰かエレガントな解答求む）。

土地勘のある人には同様に証明できることがわかる、
という意味の文章だったんですね
だから正当化とか書いてたのか

最初に読んだとき「(9’) と(10’) から(9) と(10) が導ける」
の部分だけ証明が分からなかったので
自分の頭が悪いのが原因かと思ってました

なんだこのくるるさん界隈のブログで見たような既視感は……

いや、結構前から良く分からなかったのですよ

∈モデルと普通のモデル論っぽいモデルの違いを強調してる本は
（少なくとも入門レベルの本には）ほとんど無いと思う

Cohenの本（最近Dover化した奴）には
「CHの否定やACはちょっと不自然に見えるから、∈モデルを探すのは
絶望的だと思うかもしれない。それでも我々は∈モデルしか
考慮しないことに決める。これは非常にきつい制限に見えるかもしれないが、
実はまさにこの制限のおかげで新しい定理が証明できる可能性が生まれることが判る」
という記述があるらしい。たぶん当時はかなり発想の転換だったんだと思う。
KanamoriのCohen and set theoryにも標準性がどこで利くのかが結構説明してある。

>>396
ちょっと言い訳。
渕野先生のあのスライドの文章の意図は俺もよく知らない。
ひょっとすると文字通り読むものなのかもしれないけど、
俺にはあのような感じにしか正当化できない。

>>398
Cohenの本にそーゆーことが書いてあるとは初耳。
俺Cohen読んだことないんで、ちょうどい機会だし後で読んでみよう。

この講義はビデオが一般公開されてるんで
さっきその部分を聞いてみたら、最初に(9)の証明に
必要な有限部分集合を取れば〜〜みたいなことを発言されていたので
良く分からないけどたぶんほぼ同趣旨だと思います
http://fe.math.kobe-u.ac.jp/Movies/cm/2007-09-04-ls-fuchino.html

ただし、まだ実際に証明を理解してない読者に取っては全然自明じゃないですけど

あとCohenは最近（死ぬ数年前ですね）に"The Discovery of Forcing"
なんていうレクチャーもしてますね
原子論理式の強制関係とか、どうやったらあんなのを思い付くのか
不思議で仕方ないから是非読んでみたいんですが、
掲載雑誌がうちの大学に置いてないのが残念だったり
まあ他の大学に行けば良いんですが

集合論ﾑｽﾞ杉わろた。
最初から順番に取り組んで、
関係のところで苦しくなって、
商集合に入って先に進めず逆行して、
部分集合まで戻って定義がよくわからなくてｵﾜﾀ＼(＾o＾)／

部分集合はある関係で定義されてると思っていいの？
関係のおかげでなにもかもわからなくなりますた・・・

基礎論とはあんまり関係無い質問だな

>>402
すいませんでした

ありゃ、静かだと思ったらいつもの人間違いに気付いて帰っちゃったのか・・・
どうせならどう気付いたのか言って帰ってくれれば良かったのに

荒らし再来させるようなこと言ってんなよ。

>>400
おもしろそう
http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.rmjm/1181070010

そこだと最初の一ページしか読めないよね

選択公理の独立性が数学の定理・結果として現代でも重要なのは認めますが
現代において強制法を学ぶ価値はどのくらいあるのでしょうか？

別に強制法は昔は学ぶ価値があったが今は歴史的価値しか無い、
というような証明技術じゃないと思うけど。
寧ろその逆だと思う。

まあ知りたいと思ったら勉強すればいいんじゃないですかね。

選択公理の独立性？　選択公理がZFから無矛盾であることの証明だけなら強制法いらないぞ

強制法は歴史的価値云々というよりは、一部の分野で便利なツール、という代物だから、
そういう分野で新しい研究結果を出したいなら、必ず勉強しなきゃいけない必須の証明技法だし、
そういう分野に関わる気が無いなら、興味があったら勉強すればいい程度のものだな。

現代的な集合論やるなら強制法は必須。
集合論の半分は強制法で出来てます、といってもそんなにウソではない。
あと、ペアノ算術がらみの研究でもよく使われている。
それ以外だとシラネ。

>>410
>>選択公理がZFから無矛盾であることの証明だけなら強制法いらないぞ
詳しく。ひょっとして、ゲーデルがやったけど発表しなかったってやつ？

よく知られていることだが、構成的集合全体 L を構成し、これが
V=L を満たすことを示し連続体仮説を示すのは、強制法で連続体仮説
の整合性、その否定の整合性を示すよりも難しい。また、強制法から
は、選択公理の相対的無矛盾性は示せない。
強制法は、独立証明だけでなく、集合論のなかで広くつかわれているの
でこれがわからないと話にならない。
まあ、構成的集合の方も、基本的な構成だから広くつかわれているので
これもわからなければ話にならない。

無矛盾であることだけなら、(ZFC)^Lが
実際に成り立つことを確かめれば良いでしょ。
独立性なら要るけど。

ACは独立性まで型理論の上で証明したとか
どっかで読んだんだが、どこで読んだのか覚えてない

ドーソンの本によると、型付言語の上での独立性は、
・ V = L については成功した
・ACについても同様の方法で出来ると思っていたが細かいところまで研究しなかった
らしいけどね

個人的には構成的集合の話の方が強制法よりも簡単だと思う。

>>413
あ、独立性と無矛盾性を勘違いしてましたか、おれ。

>>413
ドーソンの本ってどの本？教えてちょ。

Logical Dilemmas

>>413
選択公理が　L　で成立することを証明しようと思えば、それは　L で　すべて
の集合が構成的であるということを証明することになると思います。つまり、
V=L　を証明することになると思いますが、、、。

(V = L) じゃなくて L |= (V = L)だよね。

あと>>413は>>411に対するレスだからね

>>417
ありがと！

Church-Rosserの定理を簡単な場合（型のないλ計算）でいいので、形式的
（1階の述語論理）に証明してみようかななんて思ってるんですけど、特に
文字列の置換を形式化するのって難しくないですか？関数記号とか、述語記号を
どのように定めればいいでしょうか。どなたかアドバイスしていただけませんか。

（集合論の形式化だと述語は∈とか＝くらいでよかったんだけど、もしや、かなり
たくさんの関数記号、述語記号が必要になるんでしょうか。）

自然数論の上で
不完全性定理の証明のときと同様にやれば良いんじゃないの？

>>421
どこまで形式化するかにもよるけど、ものすごくたいへんだと思うよ。

>>423
やっぱりものすごく大変なのかなあ。

422 に書いてあることは、尋常のことではない。
大体、もっと簡単な定理の形式的証明をつくるのでさえ大変なので、
原理的なことを考えるのと、形式的証明をつくることは全く異なることだ。
ゲーデルの不完全性定理の形式的証明がもうすこしでできると書いた人がいた
が、結局はできなかったのだと思う。

1. 形式的証明を生成するコンパイラを作る。
2. 出来たオブジェクトが証明であること確認する証明検査器を作る。

証明オブジェクトを人間が読める形に変換するビューア等周辺プログラムをごにょごにょ作る。

1.ってスゲエな

>>425
話はそれますが
＞ゲーデルの不完全性定理の形式的証明がもうすこしでできると書いた人がいた
に近いことしないと第2不完全性が示せないんじゃなかったっけ？

「しないと示せない」ってのは嘘で、別の証明法もあるよ

一番普通な方法は第一定理の証明の形式化だけど

チャーチとかチューリングでいいじゃん

日本近代史の真実

第二次世界大戦
http://vision.ameba.jp/watch.do?movie=214552
http://www.youtube.com/watch?v=Z1QTiKB1qzE&feature=fvst

神風
http://vision.ameba.jp/watch.do?movie=211636

なんで証明アセンブラって未だに無いの？

つMizar

つい一週間ほど前に昔の「数学」（86年一号）読んで
Kreisel予想って面白そうだなあとか思ってたんだけど、
何やら今度のJSLに証明が載ってるっぽいね

儚い夢だったｗ

ゲーデルの不完全性定理の論文読んでたら、
「順序対(a,b)は{{a},{a,b}}で定義できる」とあったのだけど、どういうことでしょうか？
こんなんで順序を表現できてるとは思えないんですが。

たとえば、順序対(a,b,c)はどう表記されるんでしょうか？

初歩的な質問すいません(´･ω･`)

>>435
論文読むレベルに無い

順序対の定義は
(a,b)=(c,d)⇔a=cかつb=d
が満たされればなんでもいいよ
その定義はこれを満たしているというだけ

>>437
長さnのリストの構成法も教えてやれや

お前が教えてやれ

>>439
予想通りすぐるレスにワロタ

>>435
じゃあ、順序対ってどう定義するつもりだ。

背伸びの厨房いじめてもしゃあないぞ

ﾒｼｱ主義の巣窟

普通の集合・位相の教科書には書いてないからなあ。

＞こんなんで順序を表現できてるとは思えないんですが。
出来てます。良く考えましょう、としか。

みなさんありがとうございます
ググったらいろいろ出てきたんで、なんとかなりそうです

順序「対」

ググらんでも(a,b)と(b,a)を比べようとか思わなかったのか

>>437
＝を定義して下さい。

お断りします

A=B⇔∀x(x∈A⇔x∈B)

＝って普通は無定義語じゃね？

普通も何も不完全性定理の原論文は
確かプリンキピア・マテマティカの体系か何かで議論されてたような

等号についてどういう公理が入ってたかは知らないけど

あとマジレスすると不完全性定理の原論文は結構難しいので
>>435は読めるレベルに達してないと思う

現代流に整理したヴァージョンって無いの？

完全性定理に依れば任意の構造に対して真である論理式は証明可能ということは、
不完全性定理というのは、任意の公理系Γに対して
「Γ⇒A」が構造によって真になったり偽になったりするようなAが
存在するということでしょうか

まあだいたいおｋ

「構造」じゃなくて「モデル」だし
「任意の公理系」でもないけど

>>450
右辺の∈が逆じゃね？
A=B⇔∀x(A∈x⇔B∈x)
では。

外延性

>>455
やっぱりそうですか・・・
自身も否定も証明できない命題があると聞いたときは単に推論規則が足りないんじゃないのとも思ったんですが
採用する演繹体系に触れずに似たようなことが言えるとなるとそういう問題じゃないんですね・・・

>>435
良心的な集合の教科書には書いてあるよ。


サイエンス社の集合位相演習がちょーオススメ。
もちろん公理的じゃないけど、それにつながる配慮がされつつ、
でもツールとしての集合論の勉強に徹している。

450からは456は出て来ないので
=を∈で定義したい場合両方必要。

高階論理の話をしているか集合論の話をしているかでも違うけど。

ああ、どうして原論文なんかに手を出してるんだろうと思ったけど
良く考えたら文庫で出てたな

お宅やニートでも文庫で原論文が読める。いい時代だよ。

時代じゃない。教育がいいんだよ。

>>458の理解は大体合ってますか？

証明を理解すれば自ずとわかる。

完全性定理の証明には選択公理を使うって聞いたんですけど本当ですか？

証明見て確かめろ

Lが整列されてたら要らないけど一般の場合は要るんじゃないかな

というかこういうのは自分で確認できないと何も意味無いよ

>>468
ありがとうございました！
できるだけ理解してみます

自然数論を含む再帰的な公理系は証明も反証もできない命題を持つということですが
自然数論の命題を全て証明か反証できるような再帰的な公理系は存在し得るのでしょうか？

それ不完全性定理のステートメントそのままじゃん

自然数論を含む体系は必ずそのどこかに証明も反証も不可能な命題を含むということですが
それらの少なくとも一つは自然数論のどこかに含まれるということですか？

472が何を言いたいのか分からん

>>472
証明を読め

選択公理や連続体仮説は証明も反証もできませんけど自然数論の命題じゃありませんよね？

述語論理のLKにおけるカット除去が示されている場合、完全性を示すのに最も楽だと思われる道筋を教えて下さい。
命題論理の完全性は示せるのですが……
またその証明が載っている書物等も教えて頂けると助かります。

>>475
そうだね
不完全性定理の方法で作った独立命題は自然数に関する命題になるね

初等的な教科書だと或る理論で別の理論を解釈できるということの
定義をちゃんと書いてる本は少ないしね

>>476
カット除去を利用する方法としては
LKのcut-free fragmentに対して、
LKの推論規則で場合分けして示す方法もあるっぽい。
Handbook of proof theoryに載ってる。

論理式をSkolem標準形に変換して
Herbrandの定理使って示す方法もあるんだっけ？

ただ個人的には、楽なのはやっぱりHenkinの証明法だと思う。

>>466
示す体系によって違うけどBPIくらいでよかったかな。
詳細は逆数学の本でも読んでみて。

>>476
古典論理だと証明図を逆にたどる方法かな。
俺がその証明を読んだ本はいま品切れ、他にもあると思う。
その他の証明法だけど竹内の証明論入門はおすすめ。

>>477
Handbook of proof theory、明日大学の図書館で読んでみます。
エルブランの定理から証明する方法も見たことがありますが、タブロー法でヒンティカ集合を構成する方法と同様に、部分決定アルゴリズムを用いて、
証明不能な命題を偽にするモデルを構築していたような記憶があります。
>>476
最初はその方法でやろうかと思ってました！命題論理の規則は同値性を保存するので証明図ひっくり返してもいいのですが、述語論理の規則でL∀やR∃の場合につまってしまいました……
この方法で出来るのならぜひ知りたいです。大学の図書館だったら絶版の本も結構置いてあると思うので、もし覚えてらっしゃったらタイトル等教えていただけませんか？

質問した後にネットで探してたらこんな方法もありました。
http://www.is.titech.ac.jp/~kashima/pub/Mar99.pdf
シーケントでヒンティカ集合を構成しているようです。

>>475
ここはよく考えるべきところだ。
選択公理が、ZF から独立であるという命題は、集合論の命題なのか？
あなたは、形式体系に自然数論とか、集合論とか名前がついているので
そう思っているということなのか？　また、選択公理といっているものは
形式的文字列を指しているのか？　
つまり、何をどうかくのか？何をどう解釈するのかということを考えて
おかないと何をいっているのかわからなくなって当然のところだ。

メタを記述する論理式と体系内の論理式の区別が出来無い
ようなやつには基礎論は理解出来無い。

アウトラインだけ知りたがるのはゆとりの特徴だろ

>>481
数理論理学のユーザだが全く同感。
数理論理学を理解するという事は、syntax対semantics、object対meta、
これら２通りの区別をきちんと出来る、その感覚を身に着ける事が何よりも基本だと思う。

まあ普通はメタレベルの言明は普通の日本語なり英語なりで
表現することが多いけどね

semanticsを考える場合、体系の内で行う場合と
メタレベルでやる場合があるから難しいよね

まあそういう人は完全性に至る基礎をすっとばしてミーハーな感じで不完全性定理やってるんじゃない。
まともに証明論や意味論の計算やってたら頭の中でそれぞれのイメージが出来て然るべきだけど。
まあ意味論の教科書が日本語であんまり無いってのもあるけど。
坪井明人先生の本以外で、まとまって意味論の成果を書いてる本ってあるのかな？

そんなミーハーな人からの質問なんですが、
算術の公理を含まない一階述語論理の公理系において、形式的完全性（≠意味論的）って成りたちますか？

行列いいですか？

1　1
1　5　

の逆行列がなんか出来ないです。
わかるひとおねがいします・

>>487
スレタイと>>1をよく読みなおしてから、自分でいいかどうか判断しなさい。

自分が間違っていることに自力で気づくにはどうすればいいですか

まず服を脱ぎます

>>479
Handbook of mathmatical logicのD2も参考に。

証明図を逆にたどる方法は
M.Davisの超準解析の翻訳の付録に難波完爾が書いていたのを読んだ。
他の本にもあるかもしれない。

グッドスタインの定理をペアノ算術の記法で書くとどうなりますか？

>>492
任意の数列の概念がないので書けない。

誰か>>486にレスを・・・

勉強すれば自然に書けるよ

>>492
まずε0以下の順序数のコーディングを決めないといけないから
面倒くさい。Prob(φ)って具体的に書いたらどうなりますか？
とか言っても面倒くさがって誰も説明したがらないのと一緒。

>>494
成り立つものも成り立たないものもある。
あとは自分で調べて。

>>495
証明可能性と蓋然性の区別も付かない?

？
定理の証明をしたいんじゃなくて
自然数論の命題として表現したいだけでしょ

β函数使えば普通に書けるよ
確かΠ2命題だったはず

>>498
Goodstein の定理は、普通に解釈すると Π_1^1 命題です。
減少列の取り方に制限を付けた特殊な Π_2^0 命題が PA で証明不能というのが、Paris-Kirby の結果。

>>484
メタレベルでのsemanticsはなんとなくわかるんだけど(モデル理論とかのですよね？)、
体系内でのsemanticsってどういうことですか？

初歩的な質問ですみません。

最初から勉強した方が早い
聞きかじりだとどうしても知識が断片的になってかえって身にならない

ある直線とX軸について線対称な直線の定義とは
ある直線とY軸について線対称な直線の定義とは
これがわかりません例えば・・・
Y=-3x-4にX軸について線対称な直線はどういった式で求められるのでしょうか？
尚、y=-3x-4のY軸について線対称な直線はどういった式で求められるのでしょうか？
僕は恥ずかしながら今現在14才でして受験に独学で挑もうとしています。
語彙能力にかけた拙い文章ですが、経験者の方お力をお貸しいただけないでしょうか。

すまんが数学基礎のスレではないんだわ

よくスレタイ変えようって色んな案が出るけどさ
数学外して基礎論質問スレにするのはどうよ

「基礎」という字面のせいで初心者ホイホイ状態になってるから
「数理論理学」の方がいいと思うけど

それだとスレッド一覧で検索掛けた人が見付けられないじゃん
一応基礎論が通りがいい名前なんだから

算術の無矛盾性ってどうやって証明するんですか

>>504
数学外すなよｗｗ

数理論理学でも良いでしょ。探してる人は候補はいくつか検索するだろうし。数理論理学(数学基礎論)にするとか。

俺基礎論か集合論までは検索しても数理論理学まで検索せんと思うわ

なんでときたま迷い込むスレタイが読めない・>>1も読まないバカのために
わざわざ分りにくいスレタイに替えなきゃならんのｗｗ

基礎的な簡単な数学と思い込んでやってくるやつより、
数理論理学を哲学的ななにかと思い込んでやってくるやつのほうがやっかい。

>>512
> 基礎的な簡単な数学と思い込んでやってくるやつより、
> 数理論理学を哲学的ななにかと思い込んでやってくるやつのほうがやっかい。

感覚が変なんじゃないの？
数学基礎論という呼び名の方が数理論理学という呼び名より哲学的なニュアンスが圧倒的に強いぞ。
何しろ数学を「基礎づける」のが目的という名前だからな。

数理論理学って呼び方だととっても哲学性皆無のとっても技術的な分野名に聞こえる。
代数幾何学とか複素関数論なんかと同じ類の響きだな。
いまどき数学基礎論という呼び方に相応しい研究態度の研究者なんてほとんどいないんじゃないの？　
ほとんどが技術屋つまり数理論理学者でしょ。

数理論理学スレにしたらしたで
「基礎論スレがないから立てました」ってのが月一で

質問スレッドさがすなら真っ先に「質問」でスレタイ検索しないか？
基礎論専攻者なら最低限「基礎論」と「論理学」くらいは検索ワードにするだろ
スレタイ変えたところで見つけられない方が馬鹿な気がする

問題は>>514みたいな輩なんだろうけど
後から立てたらそっちを初心者隔離スレとして本スレとわければ済む話

「基礎論専攻者なら」っつうことは大学院生以上限定かｗ

他の専攻の人だとプロでも「数理論理学」という
キーワードは分かんない気もするけどね

FoMとmathematical logicって確かに
かなりニュアンス違うから分けてもいいのかもね

>>515説でいくとタイトルから「質問」を取ったほうがいいってことにならないか？
「数学基礎論で禅問答」とかにしたら迷子は減るだろ。

>>516
たまに学部4年から基礎論やってる奴いるだろ

>>499
どんな制限を付けるんですか？

「禅問答」はともかく、「議論」あたりはいいかも

普通の人にはメタ数学とか禅問答にしか映らないよ

そうは言っても或る体系で証明出来るか出来ないかの
ギリギリのラインに関わってくるからなあ

別に自然数論とかの弱そうな理論じゃなくてもっと強い奴でも

足し算とは何ですか？

任意の体に代数閉包があることを示すには選択公理が必要なことは良く言及されますが、完全閉包の存在には選択公理は不要で正しいでしょうか？

ここで完全閉包とは最小の完全体となる拡大のつもりです。

構成するには、Kを標数pの体としたとき、K_n = K, K_n --> K_{n+1} を x --> x^p で決まる帰納系の帰納極限を取る、で良いと思うのですが。

>>524
もっと正確に考えれば、代数閉包をつくるときと同じ問題が起こると
思いますが、、、。

単に帰納極限を取るだけなのに？
想像がつきかねます。

帰納極限の存在証明を書いて下さい

虚数の例を教えてください
理屈じゃななく、数字をお願いします。

有理数で、自然数じゃない数字とははなんですか？

>>528-529
スレ違い

>>530
分からないんですね
ワカリマスww

荒らすな

>>531
それと数学基礎論と何の関係が？

スレチかもしれませんが賢い人お願いします。
スコーレム標準形を求めてください。
∀x∃y［P（x）→Q（x、y）］∧¬（∀x∃y［P（x）∧∀zR（z）］）

答の一部に¬R（g（y1））がでるはずなんですが答には¬がないんです。

>>527
は？
集合論的な直和を取り、同値関係で割るだけです。、

>>535
ん?

同値関係で割るだけなのです〜

>>524の「完全体」ってのはcomplete fieldのことで良いのかな。
だとしたら普通は「完全」じゃなくて「完備」と言うような。
それから集合論的な用語法では「直和」じゃなくて「直積」と言う気がする。

集合 K_i たちからそれぞれ代表元を選び出すというのは要するに
直積Π_{i} K_i から要素を一つ選ぶのと一緒なんだよね。
つまり選択公理が無い場合、各々のnに対してK_i≠Øでも
その直積がΠ_{i} K_i＝Øとなってしまう可能性さえあるわけで、
直積を同値関係で割って定義した帰納極限やら射影極限やらが
nontrivialな性質を持つことが証明できるためには、
選択公理はまず間違いなく必要なんじゃないかと思うけど。

選択公理はもう本当に至る所で知らぬ内に使ってしまっているものなので
気にしないで使うことにするか、もっと真面目にZF集合論を勉強するか
どっちかにした方が良いかと。

どなたか>>519をお願いします

パーフェクトフィールドは完全体だよ。

喪前等、専門馬鹿になる前に代数ぐらいはちゃんと勉強しような。

>>526
代数閉包だって、K 上の代数的数をつけていくだけの帰納極限ですよ。

538は出てこなくて良いです。あなたは代数の初歩はおろか集合論すら分かっていないでしょう。

542さん、完全閉包部分はフロベニウスでカノニカルに決められますが、分離閉包部分はガロア作用分の自由度があるからそれこそ選ぶところで選択公理がいるでしょう？

完全閉包の構成はいわゆる普遍写像問題で(代数閉包は違う)、このての普遍的な構成では選択公理が必要な例を思いつかない(例えば自由な代数系や加群のテンソルなど)のですが、何かありますか？

良く考えたら帰納極限を取るのに選択公理は要らないね

選択公理と両立しない公理を使って新しい定理を示すとかじゃなければ
そういうことを考える意味はあまり無いとは思いますが

よく考えたらって、そんなこと考えるまでもないのでは。
考える意味？わけのわからないボケぶりだね。

>>534
Ans.1
P(x) -> Q(x,f(x)) ∧
P(a) -> ¬R(g(y))
Ans.2（単に対偶をとって）
P(x) -> Q(x,f(x)) ∧
R(g(y)) -> ¬P(a)
Ans.3 (Rは1項述語だからこうしてもOK）
P(x) -> Q(x,f(x)) ∧
R(b) -> ¬P(a)

>>519をお願いしますー

>>547
>498 の書いていることが正しい。

498は「制限」については何も書いてないと思うが

>>549
>499 が間違っているということ。

どうして
¬(∀a)(∃b)P(a,b) = (∃b)(∀a)¬P(a,b)
になるか、教えて下さい。

自然数に関する２項関数「＋」を論理記号と∋のみを使って定義するにはどう書けばいいですか？

>>551
ならない

二階算術ってtwo-sortedな一階述語論理の理論の研究なんだね
こないだまで二階述語論理上の理論の実例だとばかり思ってた

>>552
後続関数がないと無理

>>555
ごめんなさい、やっぱり後続関数もアリでお願いします

φ(0)=a
φ(x')=φ(x)'

これがa+xの定義

φは何ですか？

Σ_1論理式、Π_1論理式、Δ_1論理式って、どんな論理式でしょうか？？

>>552
たぶん，集合論の公理のもとのことだと思う．
555の答えはおかしい．
557の帰納的定義を，論理式で書くことを，explicit な定義と
いう．後続関数も集合論の中でなにを使うかも標準的なものが
ある．こんなところで訊かないで，まともな先生にきくべき．

>>560
はい、最初はそのつもりだったんですが後続関数を用いた場合が分かれば用いない場合に翻訳できないかなーって・・・
どこかにこういったことを紹介したサイト（できれば日本語）はないでしょうか？

>>561
たとえば Kunen の本なら，超限帰納法の証明から後続関数をつかった帰納法
の書き換えがわかる．また後続関数の　x∪{x}　について，それが = あるいは
ε との組み合わせが論理式でかけることは，absoluteness の関係のところ
に書いてある．また自然数の定義も必要．ともかく，まともな先生にきくの
が早道． もっとも，わかるかどうかは保証しないが，，，．

ふと思ったんだが論理学者ってproblem solver型の人が少ないよね。
FoM主催してるSimpsonとかも典型的な理論家だし。
まあ哲学科出身の人とかも多いからそりゃそうなるよね。

たぶん数理論理学と基礎論の使い分けとかもほとんど同じで、
problem solverがやるのが数理論理学で
理論家がやるのが基礎論、みたいな感じなんじゃなかろうか。
基礎論にトンデモが多い原因にも関係してると思う。

たぶん基礎論に妙な反感を持ってる人達は
problem solver型なんじゃないかと思う。
だから「ロジック」「数理論理学」のほうが受けが良かったりするわけで。

基礎論に妙な反感を持っている人なんているのかな？
単に例えば>>538みたいな無内容な輩を軽蔑する人がいるだけじゃない？

昔のブルバキのメンバーの書き物とかを読むと
基礎論とか集合論を蔑視した意見なんかは良くある。
岡潔も基礎論屋のことをマッハボーイなんて言ってバカにしてる。

だいたい生粋の論理学者・集合論者じゃないコーヘン自体が
割とそんな感じだったことが知られている。自分が或る定理を発見したとき、
クライゼルなどの周りの論理学者に話したとき、
こんな初等的な結果も知らないのかと非常に驚いた、とか言ってるし
クライゼルも、その後自分とコーヘンとの関係は歪んだものとなった、と言ってる。
またコーヘンは、集合論から他の分野へ転向するときに、
一般的な数学者は論理学者みたいに薄っぺらな流行を追いかけたりはしないものだ、
なんて言っている。いかにもproblem solverの言いそうなことだけど。
数学通信か何かでも、探してもちょっと今見つからないけど
「〜〜先生は基礎論のようなどうでもいい分野には目もくれず」
みたいな割と酷い文章みた覚えがある。

因みに2ch上でもかなり昔から居るっぽいですよ。


数学の本 6版目。

746 名前：１３２人目の素数さん ：03/11/23 09:28
>>744
数学における基礎論の役割なんてカスみたいなものだから、基礎論の業績なんて
どうでもいいのでは?

基礎論が蔑視されてるというか
ロジックやる奴は他の分野の数学者から嫌われてるという感覚はある

変人揃いの数学者の中でも特に一癖も二癖もあるシトの集まりでしかも
内部での対立も多いからねぇ

たぶん米国だとそこまでは無いんだろうけどねえ
他の国とは研究者の数が格段に違うし

やはり、反感じゃなくて軽蔑だね。
もう少し数学を理解しなさいということ。

いやだから、こっちは数理論理も数学だと思ってるんだけど

根本的なところで齟齬があるような気がするけどｗ

具体的な対象から代数構造だけ抜き出して研究してもなにも言われないのに、
なぜ、論理構造だけ抜き出して研究するのは反感かうのかな。

>>570
そこに主義主張が入ってくる余地があるからだろ
自分に合う合わないの皮膚感覚で反感を買う事が多い

どんな人が何を軽蔑しているかについて話が噛み合ってないんじゃないですか

>>565
2ch上ならどんな人でもいますがな

　「普通の」数学をもっと知るべきだ、という意見について
数学の他分野に詳しい人がもっと増えるべきだ、くらいなら賛成なんだが、
（一般的な数学者は普通持っているような）基礎的な知識は誰でも持つべきだ、
だったらあまり賛成できない。

情報科学・計算機科学や哲学出身の人がそれなりに多い分野だし、
そういう人は、仕事に代数なり解析なりが役立ちそうな場合、
必要に応じて勉強をする能力は当然持ってるけど、
関係ない数学には疎いのが普通だと思う。そういう人を放逐したり、
或いは例えば慶應大の哲学出身の人とかにそういう知識を求めたりするのは
メリットよりデメリットの方が大きい気がする。

特定の一個人とは全然関係ない一般論ね。>>538は誰が見ても無内容だと思う。

　どんな人が何を軽蔑しているかについて
そもそも2chの本人のレスだけで、レス書いたのが
どんな人かなんて分からないと思うんだが。
例えば>>572がどんな人かなんて知らないし知りようが無い。

>>563も>>565も数学者の全体の傾向を推測した話で、
2ch数学板の人が特にどうかというのはどうでも良い話だと思うけど。
分かってるだろうが、ネット上ではsilent majorityが声の大きい一部の人間
（たぶん私はこれ）によって覆い隠されるというのは良くある話で。

で、要は長文レスは止めてどうでも良い事はレスに書くなと
言いたいだけなんだと思うけど、個人的には真面目に二度三度推敲するより、
何も考えずに長文書くほうが余程楽なんだよなあ。
短文で本質的なレスの方が受け容れられやすいのは分かるけど
2chのレス書くのにそんなに時間掛けてどうするんだよ、ってのが正直なところで。

>>574
じゃあいますぐ2chから去れ。

嫌だよ

>>576
じゃあ長文レスは止めてどうでも良い事はレスに書くな

言っとくが>573>574は相当推敲して必須でない情報は省いて書いてんだぞ
三十分くらいかけた気がする

本スレの例の話は、一般論の水掛け論だけが続いて
それこそどうでも良い議論になりかけてたと思ったから
本意が伝わるように具体例を示したまでのことで、
文章はもう少し短く出来たとは思うが、少なくとも
自分にとってどうでも良いことを書いた覚えはない

>>578
じゃあいますぐ2chから去れ。

何でだよｗ
579にとってどうでも良いことは
他の人にとっては意味があっても書くなって言いたいのか？

>>580
じゃあ死ね。

話にならないな

水掛け論も駄長文もどっちも同様に意味がないよ

何で一般論の一つの実例になってるか、
真面目にレスを読んだ人間には理解できるように
書こうと思ったらどうしても結構な語数が要るんだよ

>>584
じゃあ死ね。

いや俺が死ぬよ

いや俺が死ぬよ

どうぞどうぞ

一つ早いだろｊｋ……

>>589
じゃあ死ね。

なんつーか無内容の長文を読むのは他人の自慰行為を見せつけられるようなしょっぱい気分になるな

なにそれ、見たこと無い。
女子中学生の示威好意なら見てみた息もする。

基礎論はその名称には似つかわしくないけれど今や応用数学（普通の数学や計算機科学に対する）の最右翼という気がします。
なので外野から見たら普通の数学や計算機科学を理解していることを求めたくなるんじゃない？

>>593
っ「計算機科学は応用数学でしょ」

計算機科学はいわゆる応用数学じゃないと思う。
>>594 から同意を得ようとは思わないけど。

>>595
っ「こっちは数理論理も数学だと思ってるんだけど」

少なくとも数理論理からロジックやってる奴は普通に他の分野も教養心得はあるでしょ。
そりゃ専門でやってる人間にはかなわないけど全くの素人でチンプンカンプンってこともない。

>>538は明らかにまったくの素人で、教養心得はあると思われない。

どの分野でも馬鹿やトンデモは一部いるもんだ。

ttp://www.iis.it-hiroshima.ac.jp/~ohkawa/math/conjecture.htm
の問題１）って基礎論っぽいんだが

違うよ、全然違うよ

そうかな。計算機出身で圏には或る程度詳しいとか、
哲学科出身だけど非古典論理とか代数的セマンティクスが専門で
代数はかなりの知識があるとか、そういうことはあっても、
偏微分方程式だとか微分位相幾何だとかについて
東大京大の院生レベルの「最低限」の知識があるとも言いがたいんじゃないの。
やっぱ他の分野の人と比べて「教養」が或る程度
落ちることにはなってるんじゃないかとは思うけど。

そんなのはどの専攻でもあることだ。ロジック専攻者に顕著というわけじゃない。
逆も然りだよ。解析系の人間が全てロジックについて院レベルの知識まで持ち合わせてるわけじゃないだろ。

ま、あれだ。基礎論を軽蔑してる人が多いのは事実だな。なんか、基礎の部分で自分の知らない世界が
あるのが気に食わないのかな。教養程度の知識を素直に受け入れればいいのに。

>>604は知識＝教養な人

「〜してる人が多い」

そんなのwikipediaでもつっこまれちゃうよｗ

で、>>524に戻ると完全閉包の存在には選択公理は要らないの？

例えば「余計な特徴を持たない」という意味で
genericという用語を使うのは、実は別に
集合論やら証明論やら算術やらだけじゃないんだよね。
ロジック以外にも複数ある。

じゃあどういう例があるか？と聞かれてすぐ二つ三つ例を
挙げられる人はそう多くは無い。ただこれは少々難易度が高そうなので
ロジックの専門家じゃなくても答えられないかもしれないけど。

受け容れる受け容れないの問題じゃなくて、
時間がありゃそりゃ勉強したいが、絶対使わないので、
そういう知識を生かした研究は他の人に任せて
最も興味を持ってることの勉強に時間を使いたいというだけ。
別に否定しているわけじゃない。
高校生レベルの日本史の知識も無いけど気にしないというのと同じ。

専門の研究をほったらかして全然関係ない他分野の
初歩的な教科書を趣味で読んでる人に碌な研究者は居ないと思う。

逆に問うが、不完全性定理もコンパクト性定理も知らない一般の数学者は
幾らでも居るが、それが許されるのはなぜ？自分の仕事と関係無いからだろ。

>>608
Spec Zの上でSpec Qはgeneric

>>608-609

じゃあ長文レスは止めてどうでも良い事はレスに書くな

なんかキチガイが居るなあ

>>609
基礎論を軽蔑してる人の話となんか関係あんの？

604で受け入れがどうのって話が出てるじゃん。
それにあくまで特定の人を軽蔑してるのであって
分野を軽蔑してるという話ではなかったような。

なんかキチガイが居るなあ

718 名前： 記憶喪失した男 投稿日： 2009/09/09(水) 17:11:43 ID:gTO4wcov0
始まりもなく、終わりもないが実数とか（笑い）
実数は∞と-∞で終わりますが。
何をいっとるんかな。

>>601
モデル理論の知識がない馬鹿
極大フィルターなどこの種の極大なものはいろいろ役に立つ

そんなの別にモデル理論に限った話じゃないだろ

>>617
おにぎりを指さしてこれはパスタですかと尋ねられたら、
「ええ、おにぎりには塩を使っていてパスタや料理全般にも塩は不可欠ですから
これはパスタですよ」と答えるのかね？君は。
お前の方がよっぽど馬鹿に見える。

基礎論と言うかただの集合論の問題だと思う

極大フィルターくらいはそのサイトの著者も知ってると思う。
ただ、モデル内部での∈無限下降列とモデルの外での
無限下降列の区別が付いていないように思える記述がある。

>>619
論理展開はまんまそのままだなｗワロタよｗ
ゆとりの結実に笑ってばかりもいられない、のかな

NK，LKについて一通りのことが説明されていて，
これらが互いに（述語論理の場合も含めて）同値であることや
健全性，完全性の証明がきちんと与えられている書籍を探しているのですが，
ご存知ないでしょうか？洋書でも構いません。
よろしくお願いします。

たしか松本和夫の数理論理学にかなり載ってたと思う。

>>623
松本和夫の本では完全性の証明はヒルベルトの体系で証明されてなかったっけ？

同値性を証明してるんだから
どれで証明しても同じなような

NK,NJなら林晉がくわしい。

>>625
すいませんが、松本本のどこで同値性が証明されていますか？

松本の本には事実として載ってるだけですね、失礼

林晋の数理論理学にだいたい622の話は全部載ってるみたい

林晋さんの本ですね。
NKだけでも詳しく書かれているのなら嬉しいです。
今度見てみます。

洋書でのお薦めはありますか？
amazon.comで軽く探してみたのですが、
NK，LKについて詳しく書かれてる本があまり見当たりませんでした。

kkgeryh　Kingこそ国を乱す国賊　内乱平定
我々保安庁の討伐を試みるKingの脳を細密に解析して試みを先取りし、Kingを隠密に闇に葬り去ること
それが私に与えられた使命　kkgeryh

>>622
上江洲忠弘著「述語論理入門」

和書でオススメの公理的集合論の教科書って何でしょうか？？

>>633
図書館か古本屋で探すしかないけど
田中尚夫「公理的集合論」培風館。
それか Kunen の翻訳書。

本屋で手に入るのがそもそもキュネンと難波くらいしかないっていうね

なんで洋書が駄目なのかがわからない。

あ、あと東大出版会の四巻があったか

みなさんありがとうございます。田中さんのをとりあえず借りてくることにします。

Reply:>>631 お前の建国を示さずに国賊と書くな。

フレーゲの概念記法ちょっと見たらﾜﾛﾀw
何であんなキチガイじみた記号使ったんだ

というか、今のような記法がたいした発見だったんだよ。

そういうのは発見ではなく発明というのではないか

R.ハーツホーン「幾何学」 p.83より

　最後に，公理系は完全であるかと言う問題がある．すなわち，公理系のす
べてのモデルでなりたつ命題は，公理系から結果として証明されるか，とい
う問題である．再びゲーデルは，相応に豊富な任意の公理系が，完全ではあり
得ないことを示している．

これは……（笑

で、>>524に戻ると完全閉包の存在には選択公理は要らないの？

543が答えてるから参考にしたら？

ていうか、>>543は基礎論の素養など全然ない私自身が書いたものなのですが。
まぁ、いいや。

自分で聞いて自分で答えてるなんて奇特な人だな

自分で聞いて自分で答えるって、どちらも聞いてるだけですが。
単なる馬鹿は反応しなくていいよ。

自分がその馬鹿の仲間じゃないと思うなら自分で勉強したらいいじゃない

ははは。
勉強したらってほどのことじゃないよ。
完全閉包の構成に選択公理が不要なのは私には自明に感じるの。
だけど任意の体の代数閉包の構成に選択公理が必要なことはよく見かけるのに、完全閉包についての言及は見かけたことがないので、何か見落しがないかと思って基礎論のことを知っている方にお尋ねしたかっただけです。
無内容な反応をするあなたが不可解です。

あ、そうか。
あなたが>>538なのか。違ってたらゴメン。
違ってなければ、それこそもう出てこないで。

選択公理いらんだろ
不要な場合は、単にわざわざ不要とは明言しないだけじゃないのか？

ふーん。
こういう頓珍漢が複数いるの？
それともただ1人が何度も現れてるだけ？
完全閉包の構成を代数閉包の構成に先立ってすること滅多にないよ。
（ひょっとして基礎論だとそういうのが普通なの？ここのレスを見てる限りとてもそうとは思えない。）
代数閉包の部分拡大として作っちゃうなら必要になるでしょう。
良くあるArtinの代数閉包の構成（超限帰納法風？）も妙な感じだし。

完全閉包の存在に選択公理が必要かどうか聞きたかったんじゃなかったの？
完全閉包の構成を代数閉包の構成に先立ってすること滅多になかろうが、
完全体に拡大するだけにするなら選択公理はいらんだろ。

お前が何を聞きたいのかよく分からん。
代数閉包の構成を前提にするんだったら、既に選択公理が必要なのは知ってるんだろ？

選択公理が必要がどうかってのは、うまくやれば選択公理の使用を回避できるかって質問じゃないのか
うまくやれば選択公理を回避できるって答えても、普通はそんな方法を使わないって却下されるんだなｗ
そら選択公理が必要な構成を経由することを前提としたら、選択公理は絶対に必要になるわなｗ
自明でしたｗ

>>654, >>655
なんか変な人。
常識的な論理のレベルで破綻してる。

単に
> 不要な場合は、単にわざわざ不要とは明言しないだけじゃないのか？
に反応しただけだよ。

可能なら、選択公理んなて忘れてしまいたい。
可能なら、選択公理んなて捨ててしまいたい。

ついにポエムが始まったか

>>652のどこが頓珍漢なのか分からんのだが
>>653の方がよほど頓珍漢だろう

うゎ。
複数いるの？

X：任意の集合　Y：Xの任意の部分集合　のとき
ord(X)≦ord(Y)+ord(X-Y)

を証明したいのですがやり方がわかりません
お願いします

うざいんでコテハンでやってくれないか？

ord(X)って何

>>663
Xの順序型です
Xは任意の整列集合の間違いでした

>>664
X=ω+1, Y={ω} とすると、
ord(X)=ω+1>ω=1+ω=ord(Y)+ord(X-Y)
なので、反例がある。

>>665
反例がありましたか
ありがとうございました

>>665
ord(X)が極限順序数のときなら成り立ちますか？

ω^2+ωは極限順序数だけど>>665とほぼ同じことが起きる

>>668
ありがとうございました

確率の求め方が分かりません…orz

クジは一回に一枚しか引けない
A: 3/8　で当たりが出るが、引けるのは１回
B 3/11 で当たりが出るが、引けるのは３回
この場合、Bの当たりの確率の求め方は
3/11 + 3/11 + 3/11 = 9/11 でいいんでしょうか

シーケント計算の所謂G3の体系って述語論理ではcontraction外せないんですかね？

基礎論って何がおもしろいんですか？
プロパーな方に訊いてみたい。

そのなんだ、あれだから、面白いんだよ。

自己解決しましたというやつですか
よかったですね

個人的には数学的証明自体の構造を調べたりする
或る種の「証明工学」っぽい側面なんかが好きなんだが
人によるかと。

もうダメぽ

>>675
多分ポイントをついていない質問だと思いますが、数学を実効的に形式化できると考えますか？
以前、これを見かけたとき（特にBourbakiの1のくだり）
http://www.radiumsoftware.com/0606.html#060630
笑ってしまいました。

最近インターネット上で次のようなものを拝見しました。
ttp://oshiete1.goo.ne.jp/qa217225.html?from=navi_ranking
とりあえず、stomachmanさんの回答を見て一応は納得したのですが、
まだ分からないところがあります。上のページの回答が締め切られていたので、
こちらで質問させていただきます。
自然数の定義に集合を使う必然性が感じられなかったのですが、これは
現代数学の基礎が集合論でできているからでしょうか。たとえば、
まず、１を定義する。
２を１＋１で定義する。３を２＋１で定義する。ここでｎ＋１はｎの次の数である。
一般のプラスはｍ＋ｎ＝(ｍ＋(n-1)+1と定義する。
こうすれば、＋１から一般の加法について帰納的に定義できる。
ただし、-はプラスの逆関数である。
という風に定義します。
私がなぜそう思ったかというと、上記のページの証明で使われている
s(n)という関数が＋１と全く同じものだと感じたからです。
それなら、そもそもの関数s(n)を＋１と定義してしまえば、１＋１＝２を
は定義そのままで証明する必要がないように感じました。
つまり、わざわざ、上の証明が+1と全く同値な関数をわざわざ別に
定義して、証明する必要のないものを証明しているように思えたからです。
もしチンプンカンプンなことを言っていたらごめんなさい。
お願いします

こういう根本でつまずいている人、しかもそれに全然気が付いていない人の相手するのってもう飽きたなあ。
第一
＞まず、１を定義する。
ってなに？
それに
＞２を１＋１で定義する
って、まだ自然数も存在してない段階で、＋を使うってどういうこと？

好意的に解釈してもいいんだけど、もう疲れた。もう少し自分で本読んでよ。

くだらないマルチポストにいちいち反応するから疲れちゃうんだと思うよ。

>>678
あなたの理解で正しい。

そのリンク先の説明は、プリンキピア・マテマティカの「１＋１＝２」に関する命題を簡単に書き直したものですが、
これは実際にはプラス記号を関数で定義しなおしただけのものであって、「証明」ではありません。
その関数を使えば、我々が普通に行っている「足し算」が実現できるというだけの話。
「証明」と言っているのは、実際には「この関数は、普通の足し算と同一の値を返します」と説明しているだけ。

モデル理論についての質問です。(ゲーデルと20世紀の論理学第2巻、P177「各自然数nに対してn個の変数列xをもつTでのn変数タイプが有限個しかないとき、全てのタイプは孤立的である」の証明の一部より)
「例えば1変数に絞って考えた時、有限個のタイプ全体をP_1(x),P_2(x)……P_m(x)とすると、
それらを違いに区別する論理式φ_i(x)∈P_i(x)が存在する。」
という部分がわかりません。これはどの様に証明するんでしょうか？

>>677
何がおかしいのかちっとも分からんが。
基礎論で大事なのは、>>678のような問題。
分かったらあっち逝け！

>>682
i≠j ならば 「φ_ij(x) ∈ P_i(x)」 かつ 「φ_ij(x) ∈ P_j(x) でない」を満たす φ_ij(x) がある。

φ_i(x)=φ_i1(x) ∧...∧φ_ij(x)∧...∧φ_in(x) (j≠i) とおけばよい。

>>679 >>680
それはすいませんでした。
>>681
奥歯に詰まってたものが取れたような気がするよ。
ありがとう

>>677
証明してみようとできるものが数学だというなら形式化できる。
信仰みたいなものならできない。
そのように信じてる。（笑）
そのリンク先を読んだが、ソフトウエアの人みたいだね。
その笑ったところは機械語でいまも直接プログラミングしますかと逆にたずねたいことかな。

>>684
こんなに早く返信頂けるとは。本当に有り難う御座います！助かりました。

Shelah, et al.
http://arxiv.org/PS_cache/math/pdf/0702/0702294v1.pdf
には何が書いてあるのですか？

最近は集合論よりも、圏とか何とかの関数的な考え方の方が、
より数学全体をまとめるのに有効であるという話があるらしいんだけど、本当なの？

最近？

数学全体をまとめるというか、
数学の一部の分野で有効な手法、くらいが適当だと思うけど

圏論は集合論に替わるものではない

Hilbertの第二問題で無矛盾性を示すことが問題とされた体系って
二階算術で良いんでしょうか？
それとも適当な体系（例えば二階論理）における
極大アルキメデス順序体の理論みたいなもの？

代数学総合スレが面白いことになってるなあ

低レベルすぎる罵りあいになってるな
ここもあまり変わらないけどね

いっつも思うんだけど、あーゆー奴らって先にレスをやめた方が負けだとでも思ってるのかな

今見てきたがおもろすぎるｗｗｗｗ
ID出ない板で何やってんだ

Handbook of categorical algebraという本の2ページ目に
定義1.1.2 universe U とは以下の性質を満たすような集合である
(1) x∈yかつy∈U⇒x∈U
(2) I∈Uかつ∀i∈I x_i∈U⇒∪_{i∈I} xi∈U
(3) x∈U⇒P(x)∈U
(4) x∈Uかつf:x→yが上への関数⇒y∈U
(5) N∈U

と書いてあったんですけど、(4)に変な条件があるせいで
こんなUは存在しないことが証明できてしまうように思うのですが。。

すいません、今日一日良く考えたらただの勘違いだったみたいです
お騒がせしました

うんこ

最近盛り上がってないですな。
巷では『数学ガール』の話題が多いけど、ここの住人的にはどうなのよ

ここの住人のレベルにはジャストフィットなのでは。

やっぱ不完全性定理は中高生や抽象数学を使わない人には
説明が難しいんだなあと言う印象
あの難易度あの複雑さがぎりぎりのラインだと思う

理解できるできない以前に中高生の理解できる知識で日本語で書かれたテキストが存在しない

>>703
日本語に問題があるな。

不完全性定理は田中さんの数学基礎論講義が、証明論だけじゃなくて意味論からもアプローチしてる良書だったけど絶版になってしまった。
超凖モデル自体は河合の基礎論シリーズにあるんだけどね……

基礎論に関して、個人的には「ゲーデルと20世紀の〜」と河合の基礎論シリーズが綺麗に纏まってて、中級者の標準的な参考書としては最適だと思うんだけど、それ以上となると和書では中々無いんじゃないかねぇ。

圏論は集合論のモデルでもあるので、原理的には集合論を
置き換えることは可能

>>706
＞圏論は集合論のモデルでもある
それを説明してくれている本や文献を紹介してもらえませんか。できれば英語か日本語で。

topoiに無かったかな？今Doverが安売り中だな。

>>708
ありがとう。さっそく注文したよ。

一階述語論理の完全性あたりを趣味で（日本語の教科書で）勉強している初心者の質問です。

形式的証明の説明の途中で、論理式の「（可算）集合」とか、あと、
モデルの定義において「集合」という言葉がいきなり出てきたのですが、
この「集合」が意味するものが何なのかよく分かりません。

いま考えている形式体系（たとえば古典述語論理）とは別に、形式化された集合論（たとえばZFなど）
をすでに構成し終わっていることを仮定している、ということでしょうか？

いろいろ初歩的な勘違いをしているとは思いますが、ご教示いただければ幸いです。

そこらへんは公理的集合論で、ZF内でZF+CHとかを考えるときとか
証明論の一部みたいに出来るだけ有限的な対象しか考えないことにしたい場合とか
いろいろあるのでわざと両方の場合に通用するような書き方にしてあるんじゃないかな

必ずしもそうしないといけないということはないけど、
>>710みたいに構文論的な対象としては最小限の有限的なものしか認めず
そこから形式的な数学を構築するという立場に立つのなら
式などの集まりに関する何らかの理論が構築されている必要はあるんだろう。
別にそれが論理式とかのレベルでちゃっかり形式化されてる必要は無いと思うけど。

> この「集合」が意味するものが何なのかよく分かりません。

集合がどういうものであるかについては述べているが、何であるかについては述べていないので
それは正しい感想

たとえば幾何学で「直線」「点」についてどう言っているか調べてみれば
事情は納得がいくかと

>>710
>いま考えている形式体系（たとえば古典述語論理）とは別に、形式化された集合論（たとえばZFなど）
>をすでに構成し終わっていることを仮定している、ということでしょうか？

そういうこと。そうでないと完全性定理が証明できない。

>711, >712, >713

ありがとうございました。
独学なのでゆっくりですが勉強を続けたいと思います。
また何かありましたら、お願いいたします。

>>711

たびたびすみません。
私は、>711さんが仰るとおりの立場のものです。
（ただし、厳格な有限主義者ではありませんが。）

一応、スマートではないと思いますが、以下の手順を踏めばよいということでしょうか？

１）形式化された集合論を、述語論理として以下の２）に必要な最小限の構文論的にだけ構成しておく。

２）上の１）を使って、改めて述語論理の意味論（と構文論との関係）を構築する。

３）上の２）を１）に適用して、形式化された集合論の意味論（と構文論との関係）を構築する。

恥を忍んで、告白しますと、このようなことを質問したのは、最初、公理的集合論を勉強し始めていて、教科書に
「公理的集合論は述語論理の一種である」とか「述語論理のいくつかの結果は使う」とあったので、
先に論理を勉強しようとしたところ、私の最初の質問にもありましたように、いきなり「集合」が現れたので、
集合論と論理学の関係が分からなくなった、という次第です。

対象としての理論とメタ理論の違いとかについて
書いたものを何か読めば良いんじゃないかな。
きちんと正確に書かれたものを読まないと余計混乱するかもしれないけど。

集合論は、ZFCの中で論理式とかをコード化する場合もあれば
理論の外にあって体系内で言及できないメタな論理式だと思って
話を進める場合もあってちょっと複雑なので
実際に完全性とかコンパクト性とかを実際に使う段にならないと
具体的にどういうことをやっているか分からないと思う。

学び始めの段階だと公理的な集合論を学ぶ前には
述語論理をしっかり勉強する必要がある、と考えがちだけど、
実際は集合論で出てくる議論はほぼ全て意味論的議論だから
述語論理の構文的な定式化とかを気合入れて勉強する必要はあまり無いと思う。
プロの集合論者でもそこらへんは結構疎い人が多そう。使わないしね。

集合論を勉強する上での
「対象としての理論とメタ理論の違いとか」は
キューネンが一番親切に書いてると思う。

第一章の大部分（特に1・2・3・4・5・8講と補遺）と
第四章の補遺あたり読めばたぶんそれでOK。

>716, >717

まだまだ、自分は仰られている事項を理解できるレベルには遠そうですが、
とりあえず、キューネンを見てみることにします。
ありがとうございました。

>>710さんとは違う者ですが、私も独学で勉強してます。本スレのやりとりがとても勉強になりました。私もキューネン本で勉強してみます。

恥のかきついでに。

もうひとつ疑問に思っていることがあるのですが、
たとえば、対象理論としてNJ（直観主義論理）を扱う際に、メタ理論において
排中律（やその他の強力な手法）を使ってメタ定理を証明することは、「何か」によって禁じられているのでしょうか？

（上で上げられたキューネン本は手元に無いのでまだ未見です。
もし、その中にこういうことも書いてあれば申し訳ありません。）

いや普通の集合論の本だから
直観主義論理とか欠片も載ってないよ。

「何か」によって禁じられているというか、
メタ理論のレベルで二値原理（排中律）を用いない主義の人は使わない、
というだけかと。これは対象としての理論の排中律とは別。
尤も現在そういう主義の人はごくごく稀だけどね。

八十年前ならともかく現代では、直観的に明らかでない概念は
メタ数学では使うべきではないだとか、
あまりそういうことには拘らない方が本当は得策だと思う。

>>721

ご返事ありがとうございます。
直観主義は例えで出しただけです。
メタ理論の選択になにか（ロジック研究者に共通の）原理があるのかどうか知りたかったのもので…。

やはり、初心者にはロジックは難しく感じられるというのが正直な感想です。
また、ROMに戻ります。

和積標準形　因数分解
積和標準形　展開

数は人の心から独立した客観的実在なのでしょうか？
教えてください　よろしくお願いいたします

答えはＹＥＳ
ピタゴラスの定理が人類が絶滅したら偽になることはありえない

>>725
「ありえない」の根拠は？
すべての可能性を検証したのか？

>>725
答えはno
ピタゴラスの定理は人類が絶滅したら無になる

人類がいてもピタゴラスの定理が
理解できない人ばかりなら同じ

ある種の機械がピタゴラスの定理を利用した
作業を行っている場合はどうなんだろう

例えば？

>>729
ピタゴラスの定理なんて考えなくても、宇宙は存在したし存在し続ける。

>>726
前提を増やしても真偽は変わらないから
>>727
無になることを証明せよ

>>731
宇宙が存在し続ける保証は何もない。

ビッグバンてピタゴラス以降だっけ？

>>724->>734
数学基礎論はごみ箱じゃないから

大した意味は無いのかもしれないが
数学認識論みたいなあればいいのかもね

モデル萌え

数学の哲学という分野で、数の存在論やら認識論をごりごりやってるけど、たぶんここの板の人には至極つまらないと思われる。

スレチだしな

>>710 長いので分けて載せます。

私も似たような１階述語論理と集合論の関係に対して疑問を持つ者です。
一応の意見はあるのですが、未だに確信が持てずにいます。この機会に
皆さんにそれを披露することで意見を頂戴したいと思っています。

用語が本によって微妙に違うことがありますから
ウィキペディア（１階述語論理、議論領域）の文面を前提として私見を明示
させて頂きます。以下「である」調に替えます。

　�@１階述語論理では変項の値は既知の議論領域から選ばれる。
　�A議論領域は、量化子で扱われる実体の適切な集合を指す。
従って、１階述語論理を定義するためには「議論領域」（「数学基礎論
講義」（田中一之）P24ではこの用語は使わず「空でない集合」とある）が必要。

ところが、「ゲーデルと２０世紀のロッジク　４」P49によるとつぎのような
説明がある。

　�B集合論の古典的な結果の多くは、素朴集合論的立場からでも十分理解可能
　�Cしかし、構成的集合の理論や強制法の理論の正確な記述や理解には、
　　１階述語論理による集合論の公理化が必要不可欠

と云うことは「議論領域」は公理化された集合では有り得ないと考えられる。
これを裏付けるべつの記述が「ゲーデルの世界」（広瀬健・横田一正）P50に
ある。

　�D述語論理について問題になるのは、変数のとり得る値が無限集合の元で
　　あることを考慮しなければならないことである。すでに、公理的集合
　　論を見てきたが、それは述語論理をもとにしているから、これを用いる
　　訳にはいかない。

ではどのような集合なのか素朴集合論による集合か？と突っ込みたくなる所
である。これについて同書では次のような興味深い記述がある。

　�E従って、われわれが議論で用いるのは古典的な集合論理とならざるを得
　　ない。そのため完全性などを問題にするときは、有限の立場を逸脱した
　　超越的なものになってしまうのである。

この意味は私見では、以下の通りである。
議論領域は公理化されていない集合だし、１階述語
論理の構築に使われる論理も古典的な公理化されていない論理である。
それ故、１階述語論理の完全性（ゲーデルの完全性定理）はヒルベルトの有限
の立場（直観的に確かめられる対象とそれらに対する有限の操作の過程と云う
ものに方法を限定する立場）では、超数学として、証明出来ない。

しかし、素朴集合ではラッセルの背理をはじめとするパラドックスが発生した
らどうするのか？と云う疑問が湧いてくる。�Aで「実体の適切な集合」と書い
ているのはそのようなパラドックスがおきないような健全なものにかぎるよと
言いたいのであろう。では、そのような適切な集合を公理的集合論を使わずに
どのように構築するのか？これに対する私の回答は「『公理主義による集合論』
を使用すれば良い。」である。公理的集合論とは形式主義（論証に使用される
言語も記号化し、使用される論理も特定して、数学の理論を単なる記号の羅列
としてみようと言う立場）に基づく集合論であり、「公理主義による集合論」
とはヒルベルトによって公理かされたユークリッド幾何のように数学的対象は
公理によって無意味化されたが理論展開する言語、論理は自然言語にとどまっ
た集合論のことである。「数　体系と歴史」（足立恒雄）P47

以上のように手法は若干違いますが　７１５　さんの発想と似ていると思って
います。
ただ、私は素人なので嘘を言ってるかもしれません。
詳しい方で間違ったところが判ったら教えて下さい。

７４２　で混乱した書き方をしてしまったので訂正・補足をしておきます。

議論領域は公理化されていない集合だし、
⇒議論領域は形式化されていない集合だし、

しかし、素朴集合ではラッセルの背理をはじめとするパラドックスが発生した
らどうするのか？
（注）ここでの素朴集合の意味はカントールが作り上げた、公理で定義されていない
集合論を指す。しかし、�Bの素朴集合論は「公理主義による集合論」を意味する。

前段の話題と少し関係のありそうなことなのですが、
話題がそれるかもしれませんがお聞きします。
710さんの疑問は、集合論を展開する前に論理式の「集合」
といった用語の使用はおかしいのではないかという疑問かと思います。
　私は、数学の基礎として、自然数をどう扱うかについてまだよく
理解ができていません。いろいろ本を見てみたのですが、
どれも納得がいかなくて専門的に携わっている人の意見を聞きたいと思います。

　数学の基礎は、１階述語論理といくつかの公理と推論規則から
成り立っているものと考えます。
　自然数の扱いですが、自然数やごく基礎的な数学的帰納法は、１階述語論理を
展開する前に自明のものとして仮定すべきなのかということが疑問です。
私の見た限りの本では、自然数の定義を行う前に、自然数の存在が前提
とされているようです。
たとえば、変数の添え字に自然数を宛てて、可算個の変数を用意したり、
（そもそも、可算だとか無限だとかの概念は、自然数の存在を前提としなけれ
ば意味をなさないと思います）、本によっては、論理式のある性質を証明する
ために数学的帰納法を使用しているものもあります。
　自然数の存在を前提とするならば、その自然数はどのようなものなので
しょうか、それどころかその後、集合論（の公理）により、再び定義される
自然数とどんな関係にあるのでしょうか？

１階述語論理では、自然数の存在を前提とすべきなのでしょうか？
そうであれば、それを使用した集合論で自然数の 再構築を行う意義はなんなの
でしょうか？もちろん集合という概念に ついても同じだと思ってます。

というわけで、基礎論の冒頭で躓いています。

>>744
私も>744さんが第二段落にかかれたこととまったく同じ疑問を持っています。
このようなことは、基礎論専門家の方には何らかの共通認識があるのかもしれませんが、
少なくとも初級の日本語のテキストで説明してあるものを知りません。

今は、何となくうやむやに自分に納得させている状態です。
数理哲学などの妙な？方向に行かない、何らかの説明を知りたいと思っています。

私は上の方でキューネン本をすすめられたので少し読んだのですが、はっきりと
>744さんと同じ疑問に答えてある箇所はいまだ見出せていません。
（私の読解力不足が大いに関係しますが。）

メタ論理（あるいはそれを語るときの「地の文の論理」）というのは、
「人間の日常経験から帰納的に得られた、ある共同体に受容されている共通言語」
という以上にきちんと説明できるのでしょうか？

上手く説明できないので、誤解を生じさせたらすみません。

（つまらない続き）

基礎論とか集合論を、位相幾何学とか、環論、微分方程式論などと同じような数学の1セクションとして考えれば、
そのようなつまらないことを考えても仕方がないのかもしれませんが、
専門家でなく、基礎論とか集合論に興味を持って独学で勉強したいという（私のような）人は、
どちらかというと、（プロの方には100年前の問題意識だといわれましたが）「数学の基礎」としての役割を、
基礎論なり集合論に期待しているのではないかと思います。

そういうわけで、数学の構築が出来る最小元の「何か」を求めるのかもしれません。
（少なくとも私はそうです。）

それが、たとえ、「人間の思考」とか「日本語」とか何でもいいので、答えがほしいというのが正直なところです。

（追記）
>>744さんと同じ方かどうか分かりませんが、上の>>740考える人さんもあわせて、
このような疑問を抱いている方が、自分だけでないと分かり、ちょっと安心（笑）しました。

まとめて、どなたかにご指南頂けるとよいのですが。

744の書き込みを行った者です。
（740の考える人さんとは別の者です。）

そうなんですね、同じことが疑問になっている
人がいると知って私も安心しました。

キューネンの本（集合論）の３節に３つの典型的な立場の人が描かれています。
実在主義者（プラトン主義者）、有限主義者、形式主義者の３つの立場です。
実在主義者は、数学は頭の中であっても、実在するものなので
「数学は発見されるものである」という立場を取ります。従って
数学を記述する公理系も原則は無矛盾となります。
無矛盾性には意義を感じないかもしれませんが、抽出した公理の
妥当性にはこだわるはずです。この命題は公理として採用するのに
十分な普遍性を持っているのかとか・・・。

有限主義者は割愛します。
形式主義は「数学は発明されるものである」という立場に立つのでしょう。
形式主義者は公理系を記号列による無意味な体系と見て、形式的に操作を行います。
その道具が１階述語論理などの形式的言語です。無意味な体系と見ますが、非公式に
意味が対応付けられていて、それが実際の数学の公理、定理（の意味）になります。
公理系は人工物なので公理系から矛盾が導かれないことつまり無矛盾性の証明が
必要であると考えます。

だから、基礎論として１階述語論理を考える人たちは形式主義者であるということ
になります（どちらかというと）。
キューネンの本では実在主義者の立場で本を記載すると書いてますから、
参考となるのはここまでかと思います。

数学の最前線研究している人たちにとっては１００年前の話題なんでしょうね。

（続き）
だんだんと哲学の方向に近づいてきてしまいました。

関連して哲学の本も少しかじってみましたが、結局はあまりよくわかってません。
哲学の本もかじってみて感じたことは次のようなことです。
数学者は、振り返らず先へと進みます。
哲学者は、同じ場所に踏みとどまります。

だから哲学的議論に終始してしまうと先へ進めなくなります。

そこで今考えているのは、実際に自分の気の済むような方法で
1階述語論理や公理的集合論を展開してみようという事です。

つまり、1階述語論理の確立において、集合論を使用したり
自然数の帰納法を使用したりしないで、うまいこと公理的集合論
にたどりつけないのかという事です。

具体的には次のようなプログラムを模索中です。

１）形式主義の立場で考察を進める。
２）１階述語論理を用いて公理的集合論（ZFC）を展開する。
３）１階述語論理での考察の対象は記号及び記号列である。
４）帰納的な定義（generalized inductive definition）
とそれにより定義された概念に対する、帰納法による証明は認める。
５）自然数については、数字の列としての存在を認める。
　　（ちょっとややこしいのですが、記号あるいは記号の組み合わせとして
　　　0,1,...,10,11,...
　　　が好きなだけの長さに書き表わせる、という前提です。
　　　でもこれは単なる記号の列なので、PA公理系を満たすもの
　　　ではありません。だから自然数に関する帰納法は使いません。）
・・・
（このあとがちょっとまだ決めきれてません。）

Godel数化を使えば自然数と自然数列と記号列は全部ほぼ同一視できる。
この同一視を行ったとして、（変数の添字なんかの話も含めて）
記号列や論理式に関する構文論的な操作を行うためには
或る程度の弱い算術は前提とする必要があるし、
またそれ以上の集合論的な概念は要らない。
完全性定理みたいな意味論的議論は集合論が既に展開されていないとできないけど、
それは集合論なしには数学を基礎付けることは全くできない、ということではないからね。

Poincareは、自然数論の無矛盾性を証明するのに数学的帰納法を使ったのでは
証明になっていないではないか、みたいなことを言ったんだけど、
それは正にその通りで、Hilbert達が考えていたのは、
明らかに信頼できそうな弱い算術を最低限度の前提にして
そこからより強い自然数論や実数論や集合論などの信頼性を確立する、ということ。
これが実際には遂行不可能な計画だというのがGodelやvon Neumannの発見。

じゃあHilbertの形式主義で最低限の前提として認めなければならない自然数論とは何かというと、
Taitが原始再帰的算術（Primitive Recursive Arithmetic）だろうということを言っていて、
これが通説でもある。ただしParsonsのように異説を唱える人も居る。

因みに「有限主義」というのは、いわゆる「有限の立場」と
ほぼ同義語として使われているのでその点に注意。

数理論理というよりは数学の哲学に属する話ですね。
この分野の専門書や論文を読めば詳しく書いてあったりもするんだけど
さすがに日本語だとほとんど無いですね。

自分の馬鹿さをもう少し晒します。

自分は第一不完全性定理の証明を勉強したときにも、表現可能性やゲーデル数を使う部分で、
>>750さんの仰る「或る程度の弱い算術」が何であるかとか、それについてどの程度のことまで
仮定されているのかが分かりませんでした。自分が読んだのは前原先生の日本語の本です。
それに関係すると思われる記述はあったのですが、自分の能力では字面以上の行間は読めませんでした。

あと、たとえば、論理学でリンデンバウム代数などを扱う際に、なんの断りもなく普通の？代数学の結果・手法
（たとえばツォルンの補題など）を使い始める教科書がありましたが、そのときも気持ちが悪かったです。

その部分を「保留」して読めば、書いてあることは一応追えるんですが…。

それに対して、例えば、ゲンツェンによる自然数論の無矛盾性のメタ証明については、
たいていの教科書に「超限帰納法」を使うことを強調されているので、ある意味では納得して読めました。


最後に、これは興味本位の質問ですが、基礎論では論文投稿の際、
>>750さんの書き込みにあるような「最低限の前提」が異なるレフェリーに当たった場合には、
それが原因となってリジェクトされたりすることはあるのでしょうか？
（経験上ですが、通常の数学分野ではそのようなことはまずないと思います。）

詰まるところ、自分がおそれているのは、上手く表現し切れませんが、
論理学が（弱い意味であれ）算術や集合論（有限集合の概念も含めて）に依って出来ていて、
一方、数学はきちんと記述しようとすると論理学を必要とする。
よって、いずれもが相手を基礎付けに必要としている、という循環になっているのではないかということです。
（多分、そうはなっていないのかもしれませんし、なっていたとしても不都合はないのかもしれませんが。）

上では敢えて、形式化されたものと、されていないものを区別せずに書きました
（自分でもはっきり分かっていないからです）。　

このような議論がこのスレで不毛/不適切であれば、以降、発言は控えます。
ただ、このスレにはプロの方もいらっしゃるでしょうから、もし教科書など書かれる際には、
このような詰まらないことで躓く基礎論入門者もいるということを思い出していただければ幸いです。

ある意味ブートストラップ問題なんだろうか？
自分もわからないことだらけです。

超数学といったって普通の数学と同じで、
何の前提も無いところからは何の証明も出来ない。
弱い算術は記号列の構文論的な操作を行うために
どうしても必要だと思う。この部分をもっと簡単な理論によって
基礎付けるということはできないだろうし、そうでなくても、
何であれ無からスタートして基礎付けを行うというようなことはできない。

そもそも現代のロジックは数学全体を基礎付けるというような
問題意識自体が薄いと思う。一部の証明論とかは分からないけれども。

>>754
誤解が生じるといけないのですが、何も無からスタートして基礎付けたいわけではありません（し、仰るとおりそれは無理でしょう）。

>>752で書いた、私が知りたいことは、
「数学と論理学、それぞれ何からスタートすればよいのか」
ということと、
「数学と論理学の関係（独立であるのか、包含関係があるのか、依存関係にあるのか、その他、など）」
です。

問題意識が１００年前のものであることは、上でも書いたように重々承知していますが、気になるので仕方ないのです。

（追記）
さらに、上で書いたことは、何か２つのメタ理論を形式化して強弱や独立性を決める、というレベルのことではありません。
教科書で言えば、まさにその教科書が書かれている「地の文」の論理についての疑問です。
（上手く説明できないので、さらに誤解を生んだらすみません。）

確かに、こういったことは初学者の妄想に類することかもしれません。
少ししゃべりすぎたようなので、無責任ですが、また当分ROMに戻ります。すみません。

７４０の書き込みを1/3にした後、しばらく誰からも反応がなかったので
がっかりしてましたが、久しぶりに書き込みがあり、読ませて頂いています。
ただ、長過ぎる書き込みをしたためか私の意見に対する直接の反応はないよう
です。（744さん747さんは触れてくれていますが）

標準的な数学の基礎付けについて、今度は簡単に私見を述べてみます。
（より詳しくは740-743も参考にして下さい。）
�@日常語によって論理と集合の公理を定義します。
「ゲーデルと２０世紀の論理学　４」１．１と１．２参考
�A集合論の古典的な結果の多くをこの前提で証明していきます。
�B１階述語論理による集合論の公理化（形式化）を行います。このときの
　「議論領域」としての集合は�@、�Aのレベルのものであって形式化されて
　いません。しかし、�Aの結果は形式化されて有限の記号列の変形に翻訳
　されます。（真理値が必要な場合は「議論領域」の世界から取ってきます。）

このようにして、日常的なことばによって構成された数学は形式化され、
数学の基礎付けをより固めることとなります。

上記の書き方はかなりぞんざいでつっこみところ満載なのですが、正確に
書こうとすると長くなりすぎるので思い切りはしょりました。

ついでに、この種の問題について、哲学ではなく、数学者がかなり
つっこんで書いている本がありますので紹介しておきます。
「数学　その形式と機能」（S.マックレーン）
著者はあのベルナイスに師事して学位をとり、圏論の創始者の一人
ですから内容には定評があります。なお、この本は基礎論だけでは
なく数学を全方位に捕らえており、どの分野の数学に興味を持たれる
方にも一読の価値があります。但し、量が多い（６２１P)

別件で一つ質問です。
私たちは１０００＋１０００＝２０００を位取りの原理から簡単に
計算することが出来ます。しかし、この位取りの原理をきちんと証明
した基礎論の本を私は知りません。（そんなものなくても高級な数論の定理は
証明出来るとの考え方もありますが、我々が使う1番簡単な定理を証明
出来ないのは寂しいではないかとの考え方もあるでしょう。）
そもそも、自然数論の標準構造
R=(N;+,・,0,1；＜）
でこれが証明出来るのでしょうか？
記号として不足している2,3・・・,8,9は予め与えておけば良いとは
思いますが10,11,・・・・をすべて与えるには余りに芸がない気がし
ます。記号としても0,1,2,・・・9を結合させる関数を適切に定義す
れば良いように思いますが、それならRに事前にその関数が入っていなければ
ならないでしょう。しかし、これは記号自身の生成法則を規定するも
ので通常の+,・とは異なりメタ理論での関数になるのかもしれません。
ご意見頂戴いたしたく。

759での本質的でない間違いの修正

R=(N;+,・,0,1；＜） 　のＲは独逸語の毛文字のエヌと呼んで下さい。

759　での本質的でない間違いの訂正をしておきます。

R=(N;+,・,0,1；＜）のＲはドイツ語の毛文字のエンの大文字の間違い

愛

２は１＋１の略記でいいんじゃないの？以下同様。

メタ圏みたいな直感的な無定義語を数学の基礎においてほしい

述語論理って認知できる構造を
自然発生型の一般的な言語(日本語・英語・ラテン語・・・)に
強制的に適応するから不自然に発展しているような気がするんだよなぁ
俺は不完全性定理も何らかの構造に対する解釈にしか思えないんだよね、
もしくは別の構造の部分かもしれないし
そういう意味でメタ圏みたいな構造を極限まで抽象化した世界が自然に思えます

「数学と論理学、それぞれ何からスタートすればよいのか」 （７５５）
→答えにはなっていないと思いますが、基礎論という視点
で言えば、歴史的な背景により「論理学→数学」の順番だと思います。
とうのはそもそも数学の基礎についての問題は、フレーゲが
数学を論理学に還元できないかと研究を始めたことがその始まりです。
その過程で発見されたパラドックスをいかに解決するか
という問いから、ラッセルやヒルベルトに引き継がれていったのです。
（飛躍のしすぎかもしれない）

だから基礎論を論じるならば論理学を利用してどこまで数学の営みを
厳密化できるのかという視点が前提になるのではないでしょうか。

ただ、論理学→数学といった一方通行ではなく、考える人さん
の７５７のように、その間を行ったり来たりすることもあるのだろうから
数学と論理学を分けて考えずに、数学を基礎づけるプログラムはどうあるべきか
と考えるのがよいと思います。

考える人さん（７５７）はその一つの回答だと思いますが、質問です。
�@〜�Bのプログラムを実際に行って、何かノートでも作った事はありますか？
「ゲーデルと２０世紀の論理学　４」が手元にないので詳しいことを
確認できませんが、通常、公理的集合論の展開においては、建前上は
述語論理を前提としつつも、実質は日常語で論理が展開されています。
このことから類推していますが、実質的には�Aと�Bは全く同じ作業の
繰り返しになりませんか？
主旨には同調しています（というか一度同様のことをやりかけました）。
�@で定義する公理や論理などは、必要最低限に限定すべきと思いますが、
どのようなものを想定されていますか？（書ききれなくて
書いてないだけかもしれませんが）

>763
>２は１＋１の略記でいいんじゃないの？以下同様。

確かに、２から９まではこの方法で良いと思います。
しかし、１０、１１、・・・・をすべてこの方法で
定義することは可能ですがその記号の作成方法自身
をどこかできちんと定義しなければいけませんよね。
また、１０００＋１０００＝２０００等の位取りの
原理は小学生時代からあまりに慣れ親しみ過ぎてい
ますが単に記号を定義しただけではだめで証明も必要
だと思います。

>>767は位取り記数法以前に、自然数のm-進展開を知らんのだろう。
的外れもいいトコ。

>768
自然数のm-進展開は勿論知っています。
それはさておき、
あなたの意見では形式化されていない世界で以下のように定数記号を
10進展開した際の係数を並べることで作成してから形式化すれば良いと
云うことですか？
2=1+1
3=1+1+1
・・・
R=(N;+,・,0,1,2,3・・・；＜）

関数や定数はあらかじめ記号として言語に入ってる必要なんてないよ
defining schemeで内部で定めればいいのでは

そういう細々した算術の性質の形式的証明は
Bounded arithmeticの本でも読めば載ってるんじゃないの？

>766
＞�@〜�Bのプログラムを実際に行って、何かノートでも作った事はありますか？
ノートもどきのものは作ったことはあります。
例えば次は集合の部分の抜粋です。

数学に於ける集合と云う概念を定義する。
集合どうしの間の関係（述語）は次の２つがあるものとする。
集合aは集合bと等しい。（a=b　と表す）
集合aは集合bの要素である。（a∈b　と表す）

集合は以下の約束事（公理）を満足するものとする。
（同等関係の公理　　詳細は略）
（外延性公理）任意のx,yに対し、すべてのzで、z∈xとz∈yが同値になる
　なら、x=yである。（同値の定義も事前にしてあるが略）
（以下　空集合公理等々）

これらの公理に基づく集合の概念と古典的な論理で理論展開したものを素朴
集合論と云います。（本によっては「公理主義による集合論」詳しくは742 )
この立場で集合論の古典的な結果の多くは理解出来る。
しかし、構成的集合の理論や強制法の理論の正確な記述や理解には、
１階述語論理による集合論の公理化が必要不可欠
つまり、言語も記号化し、使用される論理も特定して、数学の理論を単なる
記号の羅列としてみる必要がある。

述語論理の定義で必要な言語Ｌの定義の中でつぎのように議論領域が現れる。

言語Ｌにおける構造またはＬ構造μは次のものからなる
（１）空でない集合Ｍ＝｜μ｜.これをμの領域または宇宙とよぶ.
・・・
このＭは上記の素朴集合論によって構成された集合です。

まぁ，Nの場合なら
(N;+,・,0,1;<)と(N;+,・,0,1,2,3...;<)はelementarily equivalentだから
この二つに本質的な違いは何も無いな

>759の疑問は，何か算術の形式体系の本を一冊まじめに読めば解決するでしょ

>771
構造の領域を素朴集合論で考えるのは非常にまずいです．
モデル理論（の初歩ではなくある程度進んだ内容）では，公理的集合論の概念が必要だし，
モデルを扱う時は何らかの形式体系内で考えているのが普通．（ただしそれが必ずしもZFCとは限らない）

モデル理論以外でも，例えば理論Tで別の理論Sの無矛盾性を証明する際は，
理論T内部でSのモデルを作る領域を確保しなければならず，それは決して素朴集合論に依拠するものじゃない．

通常、述語論理を展開するには
有限列や有限集合くらいは扱える、有限の立場を前提としてるんでないの？
または、有限を扱える程度の算術でいいかもしれんけど

もともと、無限を扱う数学を、有限の立場に還元したかったんだから
素朴な有限の立場程度であれば基礎におくのは問題ないはず

有限列と有限集合さえ扱えれば、形式的にZF集合論などを扱うような述語論理を定義できるし
言語が無限の体系に対する述語論理はそういう理論の中で行えばいい

>770
集合論（ケスト・キューネン）第1章§８新しいことばの定義について
より
「公式見解として、形式化された言語に変更が加わることは一切なく、
新たに導入される記号は式を略記する新しい方法を示しているにすぎない
と云う立場をとりましょう。」の後半にある略記とみなしましょうと云う
ことですね。ただ、有限個の略記ならなんとも思いませんが、加算無限
の略記で、しかも略記方法にm-進展開を前提にしていることを考慮する
と少し不安な気がしますが、夜もふけたので寝ます。

考える人が挙げてる文献が集合論のものばかりなのが気になるが...
集合論は国外の一部ではmathematical logic扱いすらしてもらえない分野で，
形式論理の細かい話は，集合論の本を頼りきらない方がいい
集合論の本が間違ってるとは言わんが，形式化に関してはいい加減な記述が多いしな

776補足
間違ってるっつーか，集合論の本は悪くないが，基本，記述が大雑把だから，
形式化について詳細に書かれた他の本も少しは当たった方がいいってことな

>>775
集合論だって最初から全ての集合を記号として入れておくなんてしないでしょ？
自然数の理論だって同じこと
形式体系には単純な記号だけを導入しておいて，体系内で扱う概念は体系内で定義する

略記方法にm-進展開云々は関係ない
算術の体系内で，たとえば
xをm進展開したときのn桁である，を意味する論理式 A(x,m,n) のようなものも簡単に定義できるし，
xをm進展開したときのn桁目はiである，という論理式 B(x,m,n,i) のようなものも定義できる．
こういう風にやっていけば，目的のものも定義できるし，欲しい性質も証明できる．

こういうものをきちんと証明した基礎論の本を知らないっていうが，
まともな本なら多少は書かれていると思うんだけどな

そもそも述語論理ってのは、別に日常の数学における
主張や証明を、すべて実際に論理式のみを使って行いたいが為に
定式化されたり研究されたりするわけじゃないんだよね。
そういうことが問題になるのはproof checkerとかの実装くらいのものだと思う。
だから論理学の教科書がそういうことの為に書かれてると思うと
大きな齟齬が生じることになる。

それからKenneth Kunenだから、「ケネス」・キューネンね。

>>775
＞加算無限の略記
なんて、どういう時出てくるの？

＞�@日常語によって論理と集合の公理を定義します。
＞�A集合論の古典的な結果の多くをこの前提で証明していきます。（757）

別に�@の段階で素朴集合論を展開したわけではないですよね。
ZFCのうちのいくつかを日本語で適用したものと想定します。

私も同様のことをやってみました。理由は述語論理を使用するうえで
躊躇なく自然数を利用したかったからです。
まず、ZF（の一部）を日本語で記述し、加えて所属関係と等号について
の公理を設定しました。これにより一応は自然数が定義できるのです。
その後、述語論理の展開に入ります。これは考える人さん７５７の�B
の部分に当たるかと思います。（ちょっと違うかな）
で、実際やってみて思ったことは、わざわざ日本語レベルで公理的集合論を
展開して自然数を定義した意味はなんだったのかということです。

述語論理の展開にほとんど関係がないし、x_0,x_1,...
といった可算無限個の記号を躊躇せずに使用出来るくらいで、それくらいなら
最初から「自然数」の列
　　　　　　　0,1,2,...
があるとして、いきなり述語論理に入った方がよっぽど綺麗ではないか
と思ったのです。

集合論を展開するうえで使用する道具１階述語論理に関する数学がメタ数学
というならば、それを使用するために使用する前提はメタ「メタ数学」
となるわけで、それを行うならばもっと単純なものであった方がいいと
思うのです。

先人を疑うんならそれも大いによし
しかし自力で全部やれないなら意味はないな

>>757
＞�@日常語によって論理と集合の公理を定義します。
＞�A集合論の古典的な結果の多くをこの前提で証明していきます。
この段階で使用している論理について、それが曖昧性のある論理かもしれない
という不安はないの？無矛盾であるかどうか以前に、あるとき行った推論を
何年か経ってからも同様に理解する自信ある？

そんなこんなで、私はいきなり１階述語論理で集合論を記述してしまってます。
１階述語論理の範囲で実際にZFC書き下して展開するのに自然数なんて使いますか？
私は使いませんでしたよ。ZFCの中で順序数を定義した段階で自然数も同様に定義
してその自然数を使って記述してみました。

＞�B１階述語論理による集合論の公理化（形式化）を行います。このときの
＞　「議論領域」として．．．

議論領域なんて、ある意味考えません。とにかく上記のZFCは、一定の規則に従った
単なる有限文字列の有限列、という意味ではゆるぎのないものですから、とりあえず
それで満足しました。そして、その有限文字列の有限列をどういう意味に解釈する
かは、自由に行います。その解釈は揺らぐことがあるかもしれませんが、前述の
通り、有限文字列の有限列は揺らぎませんから。

>778
>形式体系には単純な記号だけを導入しておいて，体系内で扱う概念は体系内で定義する

主旨は大変よく理解できます。ただ、私がこの辺にこだわる理由は略記と関数の違い
に対して少し神経質なところがあるからです。（単に無知なだけですが）
御存じと思いますがペアノ算術PAから
掛け算を取り除いた公理系（プレスバーガーの体系）は完全で決定可能になります。
つまり、PAのように不完全性定理がなりたちません。
もし、単なる略記ではなく関数のようなものが簡単に定義出来るなら
ku=u+u+・・・+u（k個）を略記ではなく関数（掛け算）として定義出来て
しまえるのではないかと思えます。しかし、そんなことは出来ないはずです。
（数の体系と超準モデル）（田中一之）第５章参照

新しい話題をひとつ
（パラドックス）（林晋）の中で
「無矛盾性のパラドックス」と云う私には大変面白いテーマが語られ
ていました。基礎論の知識ないので深いところまでは判りません。
ご意見頂きたく。

形式的証明は論理式の組み合わせとしてあらわされる。
論理式の組み合わせが形式的証明と呼ばれるには、それを列状にならべた
とき、列のなかの論理式は必ず次の２条件の一方をみたしていなければ
ならない。
条件１：その論理式は公理である。
条件２：その論理式は、それより列の前の方にある何個かの論理式から
　　　　推論規則に従って導かれる。
ゲーデルの第二不完全性定理によると、形式的体系は自身の無矛盾性を証明出来ない。
ところで、形式的証明の定義につぎのような条件３を追加してみよう。
条件３：証明の結論は矛盾でない。つまり、証明の最後の論理式は
　　　　A∧¬Aという形であってはいけない。

この体系は決して矛盾しない。この体系では第二不完全性定理がなり
立たない。

面白いと思いませんか？

くだらね

第二不完全性定理の前提としての証明可能性述語に関する条件は割と微妙で、
Nでの真偽の一致だけを考えては駄目でもっと細かい条件が必要だということですよね。

>>784
β関数を使って再帰的な関数定義が
論理式の略記として書き直せるというメタ定理があるからそれで良いんじゃないでしょうか。
集合論でただの関数合成の略記と超限帰納的定義が違うというのと似たような話だと思います。

785の話題のおもしろさを伝えることは難しそうですね。
もう少し、追記してこの話題は終わりにします。（でも、上記の本はお奨めです。）

体系S：785の条件１，２をみたす。
体系S'：条件１，２，３をみたす。
体系S"：条件1，2、条件3a：証明は標準形でなければならない。（回り道のない証明）をみたす。
　　　　ゲンツェンのカット除去定理からこの条件３aがなくてもSで標準形は作れることに注意。

S’もS"もその無矛盾性が証明できる。（S'は定義から直に、S"はゲンツェンが示した）
しかし、S’もS"もモダスポネス（A→B∧B⇒B）が成り立つためにはSの無矛盾性が必要。
とは言え、Sが矛盾していたらS自身の意味がないから、このような議論に意味があるのは
Sが矛盾していない場合だけだろう。では、Sは無矛盾と仮定してもよいはずだ。
そうするとS'とS"の無矛盾性は証明され、しかもSとS'は一致し、Sの証明から回り道を除去
してS"と一致させることが出来る。
もし誰かがS'やS"で数学の無矛盾性が達成されるからゲーデルの不完全性定理は意味がないと
主張し始めたらどうすればよいのか？

>787
>β関数を使って再帰的な関数定義が
>論理式の略記として書き直せるというメタ定理があるからそれで良いんじゃないでしょうか。

この考えに従うとペアノ算術PAから掛け算を取り除いた公理系（プレスバーガーの体系）で
ku=u+u+・・・+u（k個）を略記ではなく関数（掛け算）として定義出来ないことをもう少し
詳しく教えて頂ければ助かります。

>785
A、¬Aがともに公理の場合について考察願います。

>>788
カット消去定理は公理なのか？そこそこ強い算術が必要だ。
そこらあたりに興味があったら、
竹内外史Proof TheoryやBussの制限算術関係の解説でも読んだらどうかな。
http://math.ucsd.edu/~sbuss/ResearchWeb/HandbookProofTheory/index.html

>790
>A、¬Aがともに公理の場合について考察願います。
形式的証明がこの体系では存在できないと思います。

知っていたら教えて下さい。

ゲーデルの第1不完全性定理により足し算と掛け算が定義された自然数論を
含む無矛盾な理論では肯定も否定も証明出来ない命題が存在する。

このスレの読者のみなさんには常識でしょう。しかし、このような決定不能
命題がどの程度存在するのかについてかかれたものを私は知りません。
もちろん、具体的ないくつかの例は見聞きしていますが。

全く、根拠のない予想ですがこのような決定不能命題は実は決定可能命題
よりもずっと沢山あるのではないかと思っています。
全然関係のないレベルの話ですが、実数で自然数や有理数、代数的数はすぐに
見つけられますが超越数となるとe,πの親戚を除くとかなり苦労しなければ
指定できません。リュービル数なんて云うのもありますが、それにしても
自然数の指定に比べればかなり大変です。しかし、実際はほとんどの実数は
超越数なわけですから、上記の決定不能命題も探すのは大変でも、実は殆ど
の命題はこのタイプでは・・・。と云う私の妄想です。

>791
>カット消去定理は公理なのか？そこそこ強い算術が必要だ。

カット消去定理はもちろん公理ではありません。しかし、回り道
をすべて除去した標準形の証明以外は証明とは認めませんと云う
定義はありかなと思います。

まあ、この辺の話は上記の林晋さんの本の受け売りなのでつっこまれ
ると良く判りませんとしか言えません。

あと、参考文献の紹介ありがとうございました。
ただ、初めて開いたときは下の方に少し過激な写真があってびっくり
してしまいました。あまり、慣れていないもので・・・。

少し哲学的な話題

ラッセルが記述理論を発表したとき
A　この犬は吠える。
B　犬は吠える。
この２つの文はそれぞれ正しいだろうか。

と問いかけたとか。タイプの理論からはAは正しい文だが、Bは無意味だとか。
興味のある人は（ラッセルのパラドックス）（三浦俊彦）を参照

>>795
これは三浦俊彦が間違っている

日本語でも英語でも『犬』の意味がどういうタイプ（テクニカルな意味で）なのか
postulateしなければ、正しいとも無意味ともいえない。

>>789
関数として定義できないと言っている意味が
いまいち分からんが、もし定義出来たら
Presburger算術の保守拡大が不完全になっちゃって矛盾するから
背理法で定義出来ないことが分かる、というだけ。

787は1+1+.........+1+1みたいな原理的な表記でない
10進法による表記が実際できるのかということに妙に拘っているようなので
そういう関数も後者関数と加法、乗法を使って論理式で表現できるのだから
それで良いではないかというつもりのレスだったんですが。

785の話題について
>792
>>A、¬Aがともに公理の場合について考察願います。
>形式的証明がこの体系では存在できないと思います。

そうなのかな、もしそうならば、この体系は最初から
無矛盾な公理系しか許容しないという事になります。
だとすると無矛盾であることは前提条件という事になり、
それなら条件３がなくとも無矛盾であるという事になります。
また、無矛盾なものは無矛盾であると言っているのに過ぎなくなるので
パラドックスでもなくなります。

矛盾の定義を
「A∧¬Aが証明されること」でなく
「A及び¬Aが一つの証明の中で現れること」に定義しなおせば
よいと思います。

そうすればこの体系も矛盾を導き得るので、無矛盾であるとは
言えなくなります。
ゲーデルの定理もこの矛盾の定義で書きなおせばいいのです。


この問題は詭弁の一種だと思います。
（詭弁もパラドックスと言えなくもないのかな）。
昔、小泉さんが首相だったころ、改革になっていない改革案を出して
野党やマスコミから批判されたとき、こんなことを言っていました、
改革案だと言って出したんだから改革案なんだ、と

そんなことを思い出してしまったので躍起になって考えてみました。
面白いと言えば面白かったです。

関係もないのに政治の話しないでくれるかな。

＞797
１０進法表記については、伝統的な基礎論ではなく計算機科学への応用に
ついての書物を読めば良いような気がして来たのでいったん下げます。

プレスバーガー算術においては掛け算は定義出来ないことは797さん
の云うとおり、（数の体系と超準モデル）（田中一之）p148に明記されて
います。しかし、私自身は、加法から掛け算が関数としてて素朴に定義出来そうな気がし
ていて、どこかで私自身が勘違いしているなと思っています。でも、それ
がどこなのかが明確ではありません。

ゲーデルと２０世紀の論理学　２　P7　でヒルベルトのつぎのような意見が
記載されています。

生成的方法は確かに高度の教育的及び発見的な価値あるものではあるが我々
の知識の内容を決定的に記述し且完全に論理的に保証するには公理的方法の
方が尚優れて居る。

ここでは、実数について自然数からどんどん概念を拡張して実数を定義する
デデキントのような方法が生成的方法で、杉浦さんの解析入門のような実数
の公理を最初に提示する方法が公理的方法だと思われます。ヒルベルトの意見
がどうも腑に落ちません。と云うか、実数の公理を見たときこれらををみたす
ものがあると云う保証がどこにあるのかと思いました。デデキント流で実数を
構成し、それらが確かにヒルベルトの実数公理を満たしていることを確認して
この公理にモデルがあるなと感じました。どう思われます？
（モデル論的にかなり変なことを言っていることを承知で大学1年当時の感想
を懐古してみました。）

条件1〜条件3を満たすような式の列は必ず存在するでしょ。
公理が矛盾していたら「A、¬A」の形以外の任意の式が証明できてしまう、というだけ。
「形式的証明がこの体系では存在できない」ということはない。

>>785は別に著者は矛盾の定義の仕方が良くないなんてことを
言おうとして書いたものではないし、そういう風に書き直したところで
条件３’：証明の結論をA、証明の長さ（Godel数）をhとしたとき、¬Aの証明でh未満の長さのものはない
みたいなものに置き換えれば同じ問題は起きる。
というかRosserの不完全性定理を示す時に使う証明可能性述語はこれで、
この種の議論で最初に指摘されたのもこの形のもの。

>>801
＞ここでは、実数について自然数からどんどん概念を拡張して実数を定義する
＞デデキントのような方法が生成的方法で、
え？そうなの？違う気もするけどなあ。

>803
ヒルベルト　幾何学基礎論（中村幸四郎訳）
数の概念について　参照

この中に「生成的方法」の説明があります。
デデキントの名前こそ出ていませんが、自然数からはじめて最後に実数を「切断」もしくは基本列で
定義するとまで書いていますから、「数とは何か、何であるべきか」（デデキント）
を意識していることは疑いようもありません。　と、私には思えますが。

Hilbertは公理系は無矛盾ならそれでOKだ、くらいに考えてたはずなので。
無矛盾ならモデルを持つはずだとまで考えていたかどうかは知れないけど。

＞全く、根拠のない予想ですがこのような決定不能命題は実は決定可能命題
＞よりもずっと沢山あるのではないかと思っています。

俺も同感やな。
決定可能命題は可算濃度、決定不能命題は実数濃度あるのとちやうか。

>806

もしこのようなことが示されればすごいことでしょうね。
ちなみに、昔、１変数関数論のリーマンの写像定理を多変数に拡張すること
を考えたとき、球と多重円盤でさえ正則同型でないと云う、ポアンカレの定理
をしり、更に、実は殆どの高次元での正則領域は自己同型群が単位群しかない
と知り、リーマンの写像定理と云うものの見え方が変わったことがありました。

命題は有限文字列なんだから高々可算しかないんだが

>>808

そうですね。決定不能命題も高々可算無限個しかありませんね。

>808,809

命題をどう捉えるかによってかわってくるんですが、
命題論理式の全体にブール代数の構造を入れることが出来て、
そのスペクトルはカントール集合になると云うことが云えます。
（位相と論理）（田中俊一）

は？お前全然内容理解してないだろ？

（数学の限界）（チャイティン）は私には大変刺激的な本でした。

彼が定義したチューリングマシンの停止確率
　　　　　　−｜ｐ｜
０＜Ω＝Σ２　　　　　＜１
　　　　ｐ停止
が構成可能性と構成不能性との間のちょうど境界だと主張は
カオスが偶然と必然の境界であることを知って以来の衝撃を受けました。
皆さんのご意見頂戴致したく。

８１２の補足です。

詳しい定義は書きませんが、
ｐは勝手なプログラムリストで
｜ｐ｜はそのプログラムのビット数
と思ってください。
全てのプログラムが停止しない、爆発するなら　Ω＝０
ですし、全てのプログラムがきちんと停止してくれるならΩ＝１
です。しかし、実際はその間にあることは明白なので０＜Ω＜１
ですね。

「考えるひと」さんは本当にロジック関連を読んでないような。
集合論で強制法の初歩をやってたら、
論理式のなすブール代数くらい知っているだろう。
集合論はもちろん、
チューリングマシンや帰納関数論もきちんとした日本語の本があるし、
ブール代数一般も日本語で読めるぞ。

現代のブール代数
S. コッペルベルク (著), 広瀬 健 (翻訳), 渕野 昌 (翻訳)

>>812
それはチャーチの提唱と同じでしょ。

面白そうなトピックを取り上げて
「俺ってこんなこと考えてるんだぜ」
と悦に入りたいナルシストなんだろう。

実際は理解せず鵜呑みにしてるからコテとは正反対なんだけどな。

>814
>「考えるひと」さんは本当にロジック関連を読んでないような。
それは認めます。

>>812
>それはチャーチの提唱と同じでしょ。

それは多分違うように思います。
チャイティンはランダム性の定義を圧縮不可能性ととらえ、
NビットのプログラムからはNビットを超えるランダムな数列は
作れない。従って、プログラム（この場合は公理と考えていいです）
を増やす以外にΩの判っている部分のビット数を伸ばすことが出来ないと
主張しています。それ故、Ωは構成的にアプローチ出来るにも関わらず
その判っているビット数を増やすために公理を増やすと云う非構成的な
方法をとるしかないところが構成的と非構成的の境界だと言っているので
はないかと思います。

ただ、私は素人なので間違った読み方をしているかもしれません。それで
書き込みでほかの人の意見を聞きたいわけです。

間違った読み方を危惧するならちゃんと理解してから一歩一歩すすみなさいよ。
君が参照にしてる文献もそんなんでは宝の持ち腐れだ。
自分を素人だと思うのならなおさらのことだ。

>815
>面白そうなトピックを取り上げて
>「俺ってこんなこと考えてるんだぜ」
>と悦に入りたいナルシストなんだろう。

私の書き込みが他の人を不快にさせたなら、残念なことです。
私の周りにはカオスもチューリングもゲーデルも聞いたことが
ないと云う人しかいませんし、そのような話題が話せる環境で
もありません。日々の読書で面白そうな話題について
「こんな面白い話があるけで、あなたはこれについてどう考える。
これに関連した何か面白い話はない？」
と云ったたわいもない会話のキャッチボールを楽しみたいだけです。
この動機はこのスレッドの主旨から反しますか？

微積分が面白そうと思って質問しに来る人間がいたとして
その人が九九すら言えないとわかったら、それを講釈する気には
ならないでしょう。

会話のキャッチボールをしてもどんなふうに相手にどんな風に
理解されるかわからない虚しさってわかるかな。

質問スレッドではあるけどある程度のレベルの質問に回答を願うのなら
相応の基礎知識は必要。これは質問者としての最低限の礼儀だと思うけ
どね。スレッドの主旨云々の問題ではない。

>819

と云うことは818のチャイティンの理解は間違っていると云うことですね。
でも、チャーチの提唱と同じとは思えないのですが・・・。と、聞きたいところ
ですが「講釈する気にはならない。」と言われそうなので、

「小学生相手でも親切に微分を意味を教えてくれる人」限定で、気が向いたら説明して
頂けると助かります。

間違いの修正です。
818⇒816

>>818
俺自身カオスと言う言葉は聞いたことがあっても知らないに等しい状態だ。
だから、もしあるスレでカオスについて質問したいときは、
そのスレで挙がってるような本をまず読んでみるだろう。
このスレでも同様だ。

何も、難しいことを言ってるんじゃない。
形式的体系とは何か、特に式や項についてはきちんと理解していること。
演繹定理くらいはきちんと証明を追ってみた経験、
できれば、完全性定理も理解していてほしい。
そこから始めれば親切なひとも多いいんだから、
大丈夫きっと大丈夫だよ。

>>820
正確かどうかは保証しかねるが
http://ja.wikipedia.org/ででも
コルモゴロフ複雑性、チャイティンの定数、停止性問題と辿って見ては？

>823

ウキペディアと云う、もっとも身近な調査方法を忘れていました。
チャイティンの本に書いていないことがいろいろ判って非常に面白かったです。
特に、数論の未解決問題（ゴールドバッハやリーマン予想）についてはチャイティン
が示唆していただけの内容を明確にしてくれたので大変参考になりました。
手元に本がないからあいまいな記憶で言いますが、ヒルベルトが超数学的手法に
よって理論的ではあるけれど「証明を単純な計算に帰着させる。」ことを夢見て
いたようなことを読んだことがあります。ヒル
ベルトが生きていたらなんと言ったか
聞きたいところですね。

また、コロモゴロフが晩年、確率について再考していたと云話もどこかで読んだ
ことがありましたが、こんなチャイティンみたいなことを考えていたとは知りません
でした。驚きです。

ウィキペディアは文献を探す足がかり以上の調査には使えない。
それはウィキペディア自身が言っていること。
ウィキペディアは誰でも嘘を書き放題なシステムの上に
参考文献を明示せよというルールを敷く事により
内容保証を外部文献に丸投げしている。
したがって調査候補にウィキペディアを数えるべきではない。

それより山のように出してる文献を読解する方が先だよな

>>824
ヒル
ベルト

とか工夫のあとが見えるんだが、どうしても何処を殺陣読みしたら言いか分からないよ

>>824
cca-net.deからたどってみたらこんなひともいた。
Kohtaro Tadaki - Research on Chaitin Ω Numbers and Their Extensions
http://www2.odn.ne.jp/tadaki/

基礎論以外の数学：基礎論≒量子力学：観測の理論

上は全くの個人的感想です。異論は当然あると思いますが、
基礎論以外の数学者は基礎論について、例外もいますが大抵の場合、あまり詳しくなく
かつ知らないことが平気な人が多いような気がしますし、
量子論を実際に使っている物理学者も観測の理論について、例外もいますが、
あまり詳しくなくかつ知らないことが平気なような人が多い気がします。

昔、非常に優秀な原子物理の研究者と否定的測定（対象系をまったく攪乱
せずに波束の収縮をさせる実験）について話したことがありましたが、まず
その内容を知らなかったし、興味もなさそうでした。理由はどんなに解釈を
精緻化しようとも実際の論文を書く際の計算には役に立たないと思われる
からだそうです。まあ、確かにそうかもしれませんね。
でも、私のような素人には、この辺にとても惹かれます。（ちょっと、基礎論から
外れてしまいました。御容赦）

雑談がしたいだけならよそへ行ってくれ。
流石に場違いも甚だしい。

考えるひとは荒らし。

まったく、「考えないひと」だねえ。

「うわべだけなぞるひと」が適当かな

829は流石に評判が悪かったみたいですね。（場違いとまで言われてしまいました。）

実は、久しぶりに「数学的世界観」（竹内外史）を読み返してみて、量子論理
のことを思い出したのですが昔から有名なEPRパラドックスについてはいろいろ
書いているけど割とあたらしい「否定的測定」についてはなにも書いてないから
ひょっとして、この本以降に量子論理に「否定的測定」を反映させた話しでも
あれば面白いと思ってあげてみましたが、評判が悪そうなので下げます。

ちなみに、「理性の限界」（高橋昌一郎）はゲーデル、チューリング、チャイティン
についても触れている魅力的な本ですが、p138で「否定的測定」の存在を無視した
不正確な表現があります。

考えるひとは荒らし。

ここは日記帳ではありません。
個人の雑感を述懐したいならブログにでも書くとよろしい。

昔、解析学の教授が夏休みの「頭の体操」と称して学生に出した問題です。

[0,1]⊂R　上に整列順序を定義せよ。

勿論、整列可能定理より存在します。しかし、具体的には整列順序は
定義出来ないと間接的には聞いていますが本当のところは知りません。
（丁度、休み明けに風邪をひいて解答を聞きそびれてしまったからです。）
整列可能定理は選択公理やツオルンのレンマと同値だから「あることだけは
保証する存在定理」なわけで、一般には整列順序が存在だけしても
具体的に定義出来ないことは当然あり得ます。しかし、[0,1]の場合は正に
その場合に当てはまると言うのはどうやって証明するんでしょうね？

とうとう基礎論の話題からも外れ始めた…
まさか選択公理つながりで関連性有りだとか思ってないだろうな。

ロダン考える人・・・・・

>838

この問題は基礎論の問題だとばかり思っていましたが、違うんですか？
「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」
と云う意味だと理解しているのですが。

もしこのようなタイプの命題が基礎論の範疇から外れるとすればたとえば
「可換環論において、重要な役目を果たす閉点定理がZFでは証明出来ない。
つまり、選択公理を使わなければ証明出来ない。」
なんて言うのも基礎論から外れるんですか？

〜終了〜

〜終了〜

まさかと思ったらそのまさかだった…

あえて、通常の基礎論的な問題はではないが、もし扱うとしたら基礎論学者以外
は扱えないと思われる問題を一つ。

なぜ、数学では２次形式の構造が豊かなのか？
詳しく言うと、３次形式や４次形式ではなく２次形式なのか？

たぶん、これも「基礎論とは関係ない変な書き込みをする荒らしだ！」って
言われそうですね。（先に言っときます。）
しかし、個人的には基礎論学者にこそこう言うタイプの問題について発言し
て欲しいと思っていますが。（一般の数学者でエッセイ風に述べている人は
結構います。）

>>840
ちょっと質問なんですけどね、
「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」
ではなくて、
「選択公理を使わなければ[0,1]上に整列順序を定義出来るかどうか
判定出来ないことを示せ。」
の誤りではないでしょうか？

もしピントがズレていたらスミマセン。

猫

>841−843

つまり、基礎論と言えないくらい簡単な話しだと言うことですね。

もし、御存じなら答えの書いてある書籍の名前を教えて下さい。

ちなみに、「数学的世界観」（竹内外史）に、著者が学生時代に「Rを
整列順序に並べてみてくれ。」と聞いて回った同級生の話が載っていました。
勿論、解答は載っていませんでしたが。

>845

同級生から聞いた教授の言いぶりは、
「実は、[0,1]⊂R　上に整列順序は具体的に与えられないことが証明されて
　いる。つまり、君たちのなかで出来たと思った者がいればそれは勘違いだ。」
だったとか。
つまり、角の三等分を中学生に解かせるような話だったと云うことです。
その言いぶりから
「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」
かなと推測しました。私の勘違いまたは同級生の聞き違いの可能性はあります。

はっきり言っとくが、数学の証明のどこで選択公理を使ったか
チェックするのは基礎論の役目じゃないよ。
Rが整列できない宇宙のモデルを作れというのも
厳密には集合論であってロジックかどうかは微妙。

閑古鳥鳴いてるけど、今は折角こういうスレもあるんだから
集合論固有の話題についてはこっちでやった方が良いかも。
http://science6.2ch.net/test/read.cgi/math/1228995380/

>>847
私は伝聞や他人の考えを問うているのではなくて：
★★★「貴方ご自身の考えを聞いています。」★★★
なので「貴方の考え」をご返答下さい。貴方は：
★★★「考えるひと」★★★
ですから。

猫

教授が言ってるのは
「選択公理を仮定しても構成的に順序を入れられない」
っつーことでしょ。ということで君の勘違い。

「ある命題に反例が存在する」ことが証明できても
ことと、その反例が具体的になんであるかはわからない。
反例を求めるアルゴリズムがみつからない。っつーのは両立する。

＞849

自信は有りませんが、
「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」
だと思っています。

>>851
ああ、そうですか。私もちょっとだけ考えてみます。
尤も私は選択公理を仮定しない数学には然程興味は
アリマセンけど。例えばソロベイの公理系とかですね。

猫

どうでも良いですけど「定義可能な」順序というのは
集合論・モデル論上きちんと厳密に定義された意味を持つ術語なので
ちゃんと意味分かってから使うか、自分で別の言葉を
定義してから使うかどっちかにして下さいね

>850

>「ある命題に反例が存在する」ことが証明できても
>ことと、その反例が具体的になんであるかはわからない。
>反例を求めるアルゴリズムがみつからない。っつーのは両立する。

それは判ります。ルベーグ非可測関数を具体的に具体的に構成するアルゴリズム
はないでしょう。選択公理を使って超越的に構成するしかないと理解しています。

>「選択公理を仮定しても構成的に順序を入れられない。」
意味が良く判らないのですが。多分、私の理解する構成的の意味が
基礎論的な意味ではなく一般数学的だからかもしれません。
ちなみに、ルベーグ積分の本によく出ているルベーグ非可測関数は
わたしの理解では構成的ではなく、超越的です。

>>854
わかんないかな、これは素朴集合論の初歩だぞ。
「集合Aは整列可能である」
ことは
「集合Aに ”具体的に順序をいれて” 整列集合にできる」ことを保証しない。

選択関数を具体的、構成的に提示する手段を保証することなくただ「存在する」と割り切る
のが選択公理。これと全く同じ事だ。パラレルで考えればわかりそうなもんだ。

それゆえ選択公理を公理として採用することに違和感を感じる人が一定数いるわけ。
（ツォルンの補題や整列可能定理も同様）

間違っても教授の言いたかったことは
「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」ではない.。
ちゃんと「考えない」から誤解するんだよ。

そして誰もいなくなった

「集合Aは整列可能である」
ことと
「集合Aに具体的に順序をいれて整列集合にできる」
ことが異なることだ
ということを示そうとしたら、まず「具体的に順序をいれる」という
のはどういうことかということをいわないといけない。定義可能という
ことにしたとする。それでもそれが異なるということを本当にいおう
としたら 847 のようになる。それは、強制法の対称モデルを使って
成り立たない例をつくることになる。
別の解釈は存在することと定義できるもので存在するということは別だ
という意味ともいえるが、どちらにして定義できるということはどう
いうことかをいわなければはっきりしない。
もともとの解析の先生の出した問題というのは、いわゆる問題になって
いない。

Bell の本の 74 ページ

exp(log(x)log(y))という二項演算を見掛けたのですが何という名前でしたっけ？

もしかしたら変な質問なのかもしれませんが、
「理論Tで\phiが証明できない」
というのは
「理論Tでの\phiの証明が存在すると仮定すると矛盾する」
というのが定義なんでしょうか。

>>860
そんなことはない。
そもそも理論Tが矛盾を含んでいる場合などはその定義が成立しない。

矛盾するといってもメタレベルで矛盾するのと
Tから矛盾が証明できるのと二通りに読める

すみません。
メタレベルでの矛盾というつもりで書きました。

テイラー展開教えてくれるかたいませんか？
授業でやったんですが理解できませんでした↓

まずは落ち着いてスレを読んでほしい

理論Tでのφの証明とかと関係無しに
数学における論理を形式化する際には
否定¬と矛盾⊥はどちらを取っても
それからもう片方を定義することが出来て
結果としては同じになる。だから、ただの好みの問題。

>>860
正しい。

ただ、「…でない」ということ何らかの意味で証明しようとすれば
「…」を仮定して、矛盾するという以外にない。
だから、「定義なんでしょうか？」という質問をきかれたら、「そん
なわけのわからんやつに何を答えてもむだだ」というのがまともな
答えだろう。

>>866
ものすごく細かいことを言うと、否定と矛盾のどっちをプリミティブに取るのかには違いがあるけどね。

但し最小論理がどうとか書こうかとは思ったんだが
細かすぎるなので遠慮したｗ

形式的な公理系とは別に人間がより原始的に持っている観念は
どちらかと言えば否定のほうなんじゃないだろうかと思う
実際初学者は (A∧¬A)→B が直観的に納得できないことが多い
人間の信念なんて案外細かい所では矛盾していたりするもので、
仮にそれが矛盾しても判断を保留したり信憑性を検討したりして
うまくやっていく仕組みは誰だって殆ど生得的に持っていると思われる

kk

>848
>はっきり言っとくが、数学の証明のどこで選択公理を使ったか
>チェックするのは基礎論の役目じゃないよ。
>Rが整列できない宇宙のモデルを作れというのも
>厳密には集合論であってロジックかどうかは微妙。

私の持っていた基礎論のイメージとかなり違っていて、びっくりしました。
しかし、分野の名前の定義は本質ではないので特に異論はありません。

ちなみに、下記の命題は「数学基礎論とその応用」と云う講究録からもって
きました。
「可換環論において、重要な役目を果たす閉点定理がZFでは証明出来ない。
つまり、選択公理を使わなければ証明出来ない。」

証明論ならロジックの範疇になるけど
「選択公理」のトピックが全て基礎論関連になると思ったら大間違いだ。

そして君が最初に持ち出したトピック>>837は素朴集合論の話題だっつーのに。

しかも
>「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」
こんな誤解をやらかしてるんだから尚更意味がない。

>855

そうなんですか？
私は下記にあるような「努力」が結構身近な例で無駄になるんだよ、と云うことを悟らせる
ためにわざと無駄な努力を少し学生にさせてみようとされたと思っています。


「数学的世界観」（竹内外史）p152
選択公理を用いて存在を証明される関数や集合には、存在するというだけで
定義を与えることも出来ず、構成することも出来ないものが多いから、
選択公理というものに何か不純なものを感じて、出来れば選択公理をもちいない
で証明しようという努力が数学のなかでは沢山ある。

それから、質問スレッドその４で831近辺でこれと同様の議論がされていました。

>>873
おまえどこまで考える力がないんだよ…

まさに竹内先生のいわれる
>選択公理を用いて存在を証明される関数や集合には、存在するというだけで
>定義を与えることも出来ず、構成することも出来ないものが多い
例がまさにその出題だろ。

教授に出題意図があったとすれば順序を入れようとしてそれが困難であることに
気付かせどこに原因があるのか、大元の整列可能性に違和感を抱かせたかった
んだろ。
無論その違和感を抱かせることは即選択公理を否定して欲しいということまで意味
しない。とにかくこれは基礎論の話題じゃなくて素朴集合論の範囲。
ついでにいうと竹内先生の引用されてる一節もメタレベルの話題じゃない。実数学の
範疇の話だ。
誤解に誤解を重ねそうだからいちいちこんな補足までつけなきゃいけないってのも
情けないけど。

ちゃんと読んでちゃんと考えて正しく理解しなさい。

>874

私はどこまでが基礎論の話題でどこまでが実数学（この用語は初めて知りました。）
の話題なのかは良く判りません。ヒルベルトの第10定理などは実数学の問題を基礎論
の手法で解かれたと理解しています。つまり、一応便宜上の差異はあってもその境目
は実はないと思っています。ですから、素朴集合論であろうと公理的集合論であろうと
その問題がどの分野に属するかは、少なくとも私にとっては、大した問題ではないと
考えます。
それはさておき、話しが少し噛み合っていない気がします。選択公理を使って整列順序
を実数に定義することはなにも難しいことではありません。それはただ存在すると言って
いるだけです。そうではなくて、有理数で実行出来たような具体的な構成が、存在するに
も拘わらず、実数の場合は出来ないことの不思議さと選択公理の威力とその
ある種のいかがわしさを感じることが本件の主題だと思うのです。
ちなみに、その教授も一般的な数学者と同じく、選択公理や背理法は使わずに
すませるなら使わない証明の方が優れていると云う考えをお持ちでした。
私も実のところ同じ考えの持ち主です。

>>875
>素朴集合論であろうと公理的集合論であろうと
>その問題がどの分野に属するかは、少なくとも私にとっては、大した問題ではない

あなたにとってどうでもよくてもここは「基礎論の質問スレッド」であなたの私スレでは
ない。トピックがスレ主旨外のものだとの指摘を
「私にとって大した問題ではない」と居直る神経の方が理解しがたいものだが。

話が噛み合わないのも無理はない

>「選択公理を使わなければ[0,1]上に整列順序を定義出来ないことを示せ。」

>選択公理を使って整列順序を実数に定義することはなにも難しいことではありません。
>それはただ存在すると言っているだけです。

>有理数で実行出来たような具体的な構成が、存在するにも拘わらず、実数の場合は出
>来ないことの不思議さ

とどんどん主張することが変わっていってるからな。その主張自体も矛盾してる内容だし。
精神病院であなたは頭がおかしいですよと言ってる医者に患者がそんなことないと
食ってかかってるような状況だ。話が噛み合う訳がない。

もうＮＧにしとけ
相手にするな

相手にするなら必ずアンカーをつけてくれたまえ

ここ質問スレだと思ってた

質問であるとか基礎論関連の話題であるとかどちらかなら対処のしようもあるけど
どちらでもないからなぁ

ＮＧしかないだろ

別に初心者の質問を受け付けないスレではないよ。
でも、成長しようとしない初心者は例外。

例えば、選択公理関連で質問してきたら、
http://www.iranian.com/Times/Subs/Music/April2000/Axiomofchoice/index.html
とはぐらかさずに
田中 尚夫「選択公理と数学―発生と論争、そして確立への道」とか、
Thomas J. Jech　The Axiom of Choice (Doverからでてるのか)
文献案内したうえでできる限り適切に答えるだろうね。

でも「考える人」みたいに居直るひとには答えない。

>>881
いや参考にしてる文献ならそれなりのものを出してきてるでしょ、この人。
誤解だらけで身に付いてないので他を紹介しても無駄だよね。

普通に正しいことを書いてるのに権威的に出される文献が気の毒でならない。

というより相手にしてる人も罵倒の形をとりつつもちゃんと丁寧に答えてるんだよね。
それでもそれを理解する基礎をもたず居直るからタチがわるい。

とうとう、「居直っている。」と言われてしまいました。（笑）
そのようなつもりは全くないのですが、そのように見えてしまったのは残念です。

>881　
　田中 尚夫「選択公理と数学―発生と論争、そして確立への道」
　は一応目を通しておりますがこれを見ても解答を得ることは出来ませんでした。
　具体的にどのページを見れば良いか教えて頂けると助かります。

それからスレッドその４で似たような（同じではない）次の質問があります。
　　831 実数は、選択公理があっても、｢具体的な｣整列順序を定めることは不可能。
　　　　ただ、整列順序の存在を示せるだけ。
　　832 その不可能って言うのは証明されてる？

それに対する解答のひとつ（下記）では選択公理の独立性が使われています。
　 839 選択公理は独立だから偽でもいいはずなのに具体的に構成できちゃったら偽にできないでしょ

この解答は結局正しいと思われますか？
（後を読み進めると大体正しいと云った意見が多いようですが）
この問題が解決すれば私の出した問題も、個人的には終結します。
選択公理があってさえ具体的に構成出来ないなら、いわんや選択公理がない
場合も具体的には構成出来ない。と思えるからです。

「数」（足立恒雄）P15

こうした対象世界Xの言語と、Xにおける証明や真理値の問題を論じているわれわれの
言語との区別がどうしてもつかない人は、「直ちに本を閉じて養蜂学かクロスワード学
か、何か別の科目をとりなさい」とある高名な基礎論学者が暴論を吐いている。

⇒この高名な基礎論学者とは誰の事だかお判りの方はお教え下さい。

おいおいそんなんでいいわけないだろ！
東工大狙ってるやつはみんな数学できてあたりまえなんだよ。
実は東工大の合格者の数学平均は9割だよ。うへへ

>>885
それは暴論でないことはわかるが、誰の言葉かは知らない。

>>885
逆に考えると、根気よく教えることによってその「区別」を納得させるのが困難だということかな？

>>884
私は >>857 に答えを書きました。対称モデルと書いたのは少しウソ
でブール代数の自己同型写像での不変性を使うということです。
J. L. Bell Boolean valued model and independence ,,,,
という本です。

>>858 の方が Bell の本のページを書かれているようです。私は
手元にその本がないので、それでよいのかわかりませんが、Bell
の本に書いてあることは確かですし、そこだと思います。ただ
あなたには理解できないだろうと思います。

>889　ありがとうございます。この本は残念ながら持ってませんが
図書館で探してみることにします。多分、あなたの言う通り、見ても判らない
でしょう。しかし、そこに解答があることが判れば、それで今回の質問の目的
の半分は達成しました。

>888

ご存じとは思いますがツェルメロでさえゲーデルの論文が出た後、
数学とメタ数学を混乱し、ゲーデルが丁寧な説明の手紙を出しても、
やはり理解出来なかったと言うことです。齢を取ると認識方法を
ドラスティックに変えるのが大変と言うことでしょうね。

こんな難しい（ここのスレの方々には易しい？）例ではなく、
今なら一年生でも簡単に判る
φ≠｛φ｝
でさえ述語論理の生みの親フレーゲを悩ましたそうです。

844に対する回答が全くないので手持ちの非常に不満のある回答案を出しておきます。

　　　　　ｐ
例えば、L　　空間について考えてみればｐ＝２の場合だけが豊かな
構造を持つヒルベルト空間になる。そして、その豊かさの原因は双対
空間が自分と同じ次元になり、それ故、双対空間に自分を埋め込んだ
議論が出来るところにある。（他の次元だとこうは行かない。）

私は圏論は普通の数学でおさわり程度に使ったことしかないので判りませんが
上記の特別な場合の議論を圏論を使って一般化出来なものかなどと考えたこと
がありました。（そんなこと考えていると専門の論文が書けないのですぐ辞めましたが）
一般の数学者にはびこる「2次元は豊か」信仰を裏付けるものが基礎論にあれ
ば知りたいものです。

>>891
下の例はちょっとアレですが混乱は学べば解消すると思いますよ。
馴染めない、というのが長引くのではないかと。
自分も「理論は理論、メタはメタ」という考え方がダメでした。

>>884
そこの839の回答は間違い。
ただし831は正しい。うろ覚えだがその後に証明の概略は書いてあったと思う。

839を見てなぜ間違いなのかわからないならば絶望的にセンスがない。

到達不可能基数の存在からＶ≠Ｌは従いますか？

選択公理を採用しても、採用しなくても、数学は造れる。
唯一の数学があると思うのが間違いですかね？

いちいち余計な口を利く奴にお稽古事は無理だ

>896

だいぶ前ですが、竹内外史さんが、有用な公理系を模索するために物理学
にかなり傾倒されていたことがあるました。うろ覚えで恐縮ですが、次の
ような主張だったように思います。

公理系をどう取るかで同じ数学の問題でも結果が変わってくるから
問題によって公理系を使い分けると言う発想もあるが（物理学と幾何学で良くある発想）
集合論の公理系ではそのような発想ではなく最も適切な公理系を模索
すべきである。その為の指針として物理学が有用と考えられる。

当時は、なんとなくゲーデルのプラトニズムに似た香りを感じました。
しかし、自然（物理）に聞いてみる言うところが面白かったです。

今でも、同じようなことをされている人はいるのでしょうかね。

それは単にそのとき、量子論理上の集合論を考えていたというだけの話でしょう。

> 　田中 尚夫「選択公理と数学―発生と論争、そして確立への道」
> 　は一応目を通しておりますがこれを見ても解答を得ることは出来ませんでした。
> 　具体的にどのページを見れば良いか教えて頂けると助かります。

「一応目を通した」だけではどうにもならないよ
電話帳か何かと間違えてないか？

知っている人もいるかもしれませんが
Banach-Tarskiにある意味大変“近い”結果が、選択公理なしに証明できたとか。
Banach-Tarskiの証明を読んだものとしてはにわかには信じがたい内容です。
個人的に細かく検証する気にはとてもなりません。
（砂田さんあたりがしてくれると助かるんですが）

興味のある方はどうぞ↓

http://antimeta.wordpress.com/2006/10/01/banach-tarski-the-axiom-of-choice-and-notions-of-size/

覚える
解答が書いてある場所を探す
語る

文系の数学

>>902
さすがにそれは文系に対して失礼だ。
センターテスト受験で使えればいいやの数学と限定しようよ。

>>901
書いている人がよくわかっていない。
Daughty-Foreman の結果は Banach-Tarski の定理で有限分割した集合
がベールの性質をもつものにできる、ということである。
あなたも、このような記事の端を読むことだけで内容に関するところの
話でないところに終始するので嫌がられる。

>904　まさか、Daughty-Foreman の結果を紹介しただけで批判されるとは思いませんでした。
詳しい内容が知りたいひとは紹介してある記事を見れば事足れりと判断したのですが。
とは言え、「にわかには信じがたい」と私が思った理由を全く述べなかったので不評を買った
ようですので、簡単に記しておきます。

BTの背理は3次元球が選択公理を使って非構成的に体積の定義出来ない有限集合に分解されて、
それぞれの集合が空間の運動群で移った集合を組み立てると元の3次元球とは異なる体積に
なると云うものであるが、ポイントは体積の定義出来ない（恐ろしくいかがわしい）集合
に分けられるところで本質的に選択公理を使っていることと、このようなことが1次元、
2次元では起きなくて3次元で起きる理由が空間に働く運動群の性質の違いによることにある。
ところで、Daughty-Foreman の結果の驚くべきところは
Perhaps the most surprising result is ・・・と書かれている部分にあるとおり
disjoint open(!) subsets に分けられるところである。
つまり、各パーツは有界な開集合だから、もちろんルベーグ可測で、体積を持つ、という点。
加えて選択公理を使わないと言う点。

904さんが言っている部分はおそらく下記ではないかと思いますが（違っていたらすみません）
the central result of Dougherty and Foreman is a Banach-Tarski-style decomposition where every set involved has the property of Baire.
私は下記の部分の方に興味を持ちました。
it turns out that it only looks bad when using Baire’s notion of almost equality.
つまり、この定理では通常のベールの「痩せた集合」という概念が、あまり「無視できる」
とは言い難い集合であるということを意味しているのではないかと云うところです。

いづれにせよ、この定理の証明はホローしていませんから、この程度の「感想」しか言えません。
それで「嫌がられる」とするなら、甘んじて受けるしかないでしょうね。全ての定理を
読み切るのは大変ですから。私はプロではないのでそこまでする積りはありません。

主張を弱める際にA〜Bを
（Aの或る稠密部分集合）〜（Bの或る稠密部分集合）で
置き換えちゃう訳ですから体積もへったくれも無いと思いますけども。。

件の論文に関してはBSLのStan Wagonのreviewに
「全ての実数の集合はBaire」はZFと無矛盾等価だが
「全ての実数の集合はLebesgue可測」は「ZF+innaccessible cardinal」
と無矛盾等価だからそもそも
巨大基数的な性質であるLebesuge可測とそうでないBaireでは
概念の性質が全然違うんだ、というような話が載ってますね。

たぶん「考える人」さんを含む多くの一般的な数学者は
基礎論ってのは数学の基礎に関する哲学っぽい議論のことを言うんだろう、
くらいに思っているんじゃないかと思うんですが
いわゆる基礎論の人は大抵、自分の研究分野は
数理論理学の応用分野であるという風に思っているんじゃないかと思うんですよね。

だから例えばHilbertの第10問題で言えば、Matiyasevichによる
A⊆ωがr.e.ならばAはDiophantine という結果は数理論理を応用する話なんですけど
Bakerによって同じICMの会場で発表された
有理係数の二元n次同次不定方程式の解を上から評価する結果
|x|,|y| < Ce^(log m)^(n+1+ε) は全く基礎論の話じゃありません。
どの分野の話かは些細な問題だとか言ってこのスレで積分による
不定方程式の解のサイズの評価の話をしたりするようなのは何だかなあ、ということになる訳です。