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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 167 名前：１３２人目の素数さん [05/01/12 21:44:31] >>166 そういう体系（公理がreでnon-recursive）の例はどんなものがあるんですか？ 168 名前：１３２人目の素数さん mailto:sage [05/01/13 02:39:24] >>167 多くの体系では、定理全体が r.e. で recursive でないのだから、 いくらでも作ることができる。 こういう話での基本的なトリックに、r.e. な公理系を持つ体系は、 recursive な公理系が存在するという結果がある。 169 名前：１３２人目の素数さん [05/01/13 18:17:04] >>168 ありがとうございます。定理全体を公理にすればよいんですね。 170 名前：１３２人目の素数さん mailto:sage [05/01/14 02:14:04] もっとくだらない例。 トートロジー A をひとつ固定し、An = A∧A∧...∧A (n個) と定める。 r.e. だが recursive でない自然数の集合 S に対し、 { An | n∈S } は r.e. だが recursive でない公理系。 171 名前：１３２人目の素数さん mailto:sage [05/01/14 19:20:56] >>170 は、明らかに recursive 172 名前：１３２人目の素数さん [05/01/17 03:32:37 ] なぁなぁみんな cot(x) ってなんだ？ 173 名前：１３２人目の素数さん [05/01/17 03:44:59 ] >>172 市ね 174 名前：１３２人目の素数さん [05/01/17 03:45:29 ] >>172 いやマジで聞いてるんだが 175 名前：１３２人目の素数さん mailto:sage [05/01/17 23:55:52 ] 高校生スレにGO！ 176 名前：伊丹公理 ◆EniJeTU7ko mailto:sage [05/01/21 17:54:51 ] 以前 ＞ロビンソン算術ってなぁに？ と言う質問をしたことがあるが、 本日、田中一之、数の体系と超準モデル、裳華房 を購入して大体読んだので理解した。 177 名前：１３２人目の素数さん mailto:sage [05/01/21 23:34:22 ] 一日で全部読んだの！？ まあそれは兎も角、その本は悪い本じゃないけど かなり特殊な章立ての本ですね。 どうも筆者が学んだ順になっているらしいけど。 178 名前：伊丹公理 ◆EniJeTU7ko mailto:sage [05/01/23 11:22:37 ] どこかに誤爆したようなのでもう一度。 >>176-177 大して深いことは書いてなかったな。 以前読んだ G. E. Sacks, Degrees of Unsolvability, 同じく G. E. Sacks, Saturated Model Theory 等々のほうが余程面白かった。 勿論、A. Robinson, Non-standard Analysis も。 179 名前：伊丹公理 ◆EniJeTU7ko [05/01/25 14:01:08 ] G を具体的な有限個の生成元と有限個の関係式で定義された群：有限表示群とする。 （有限表示可能群を単に有限表示群と云うこともあるが、ここでは上記の意味に取る。） H も有限表示群とする。 G において語の問題が解け、 H が抽象群として G に同型なら、 H も語の問題が解けることを示せ。 180 名前：１３２人目の素数さん mailto:sage [05/01/25 15:44:40 ] ﾜﾗ 181 名前：１３２人目の素数さん [05/01/25 19:08:31 ] 基礎論初心者です。どちらの本がお勧めですか。 Shoenfield/Mathematical Logic Ebbinghaus, Flum, & Thomas/Mathematical Logic 182 名前：１３２人目の素数さん [05/01/25 20:11:17 ] >>181 だんぜんうえ　したはうんこちゃん 183 名前：１３２人目の素数さん [05/01/25 21:30:28 ] >>182 良く知ってるな。 logic の本なんで読んだこと無い。 一度お勧め本でKleeneの本少し読んだが、すぐやめた。 >>181 logic は止めとけ。 Cohn, Universal Algebra は logic も含んでいて面白い。 184 名前：１３２人目の素数さん mailto:sage [05/01/26 02:01:31 ] >>181 上は何十年か前にLogicの素養の無い院生のために 書かれた基礎論の概論、下はLogicに興味を持った 学部生のためのUTMの本。下の本はpartAは大分簡単だと 思いますが、paｒtBでは、無限論理、Fraisse の定理、 Lindostromの定理なんかも扱っています。 と言うわけで、本格的に勉強するつもりなら上がお勧めです。 一寸齧ってみよう、ということなら下でもよいでしょう。 185 名前：１３２人目の素数さん mailto:sage [05/01/30 23:19:04 ] いまさらShoenfield、ツー気もしないでもないな。 186 名前：181 mailto:sage [05/01/31 10:53:40 ] >>185 Shoenfieldの他にお勧めがあれば教えて下さい。 187 名前：１３２人目の素数さん mailto:sage [05/01/31 17:12:24 ] Shoenfield といえば、中途半端で汚ない formal system, Goedel interpretation の変な改良、近藤--Addison の定理の泥臭い証明など文句をたらたら言った後で、 「でも良い本だよね」でしめるのが標準的な評価だったけど、今はどうなんでしょ。 章末の演習問題はたくさんあるけれど、初学者が少しづつ手探りで進むための問題が ないので、>>185 の言うようにある程度数学の本の読み方を知っていないとつらいかも。 188 名前：１３２人目の素数さん mailto:sage [05/02/05 13:04:20 ] 『「知」の欺瞞』関連情報 ●ｂｋ１の『「知」の欺瞞』のページ * 佐々木力、ポストモダン思想の軽薄さを完膚なきまでに暴露した、知的刺激溢れる書物、2000/07/10 www.math.tohoku.ac.jp/~kuroki/FN/#links このページは黒木玄個人の責任で維持しております。 クレームその他は黒木個人におよせください。 ★2002年新学習指導要領の中止を［上野、戸瀬、黒木］→NAEE2002で署名を！★ www.math.tohoku.ac.jp/~kuroki/index-j.html 189 名前：１３２人目の素数さん [05/02/05 15:25:58 ] afo 190 名前：１３２人目の素数さん mailto:sage [05/02/05 15:40:09 ] >>187 「近藤--Addison の定理の泥臭い証明」なんて、誰がいったんだ。 近藤基吉のもとの証明、見てみい。 191 名前：１３２人目の素数さん [05/02/05 16:10:47 ] こんど見てみる。 192 名前：１３２人目の素数さん [05/02/05 16:28:27 ] 面白いと思ってるの？ 193 名前：１３２人目の素数さん [05/02/08 12:31:46 ] しゃれが分からん香具師 194 名前：１３２人目の素数さん mailto:sage [05/02/08 12:53:05 ] ぬるぽ？ 195 名前：１３２人目の素数さん mailto:sage [05/02/08 14:38:00 ] (ﾟдﾟ)ﾎﾟｶｰﾝ 196 名前：１３２人目の素数さん [05/02/08 17:54:21 ] LKの基本定理とか無矛盾性証明を学びたいのですが、分かりやすめの本を紹介してもらえませんか。 竹内さんのはきつそうなので勘弁。すると自分ではあとは共立の赤い本（数理論理学）しか知りません。 洋書でも構わないので、お願いします。 書き方は無味乾燥でも大丈夫ですが、証明のギャップが大きいと逝きますので、 その辺を考慮していただければ、たいへんありがたいのですが。 197 名前：１３２人目の素数さん mailto:sage [05/02/08 18:27:18 ] 竹内さんのってGTMのProof Theoryのこと？ それとも証明論入門の事？ あまり知らないのだけど、一応レスしとくと 前者の事を言っているのなら、後者がより易しい。 で、後者でも難しすぎるなら、最近書かれた 松本先生ので勉強するのが一番賢いと思うけど、 他には『数学基礎論入門』とかか。あと、 "Basic proof theory" by A.S. Troelstra & H. Schwichtenberg なんてのもあるようです。Smullyanの"First-Order Logic"にも カット除去定理の証明はあったような感じです。 まあ自分で現物を見て判断してください。 198 名前：１３２人目の素数さん mailto:sage [05/02/08 18:28:30 ] PrawitzとかでOPACってみてもいいかもね。 199 名前：１３２人目の素数さん mailto:sage [05/02/08 18:42:20 ] >>197 GTMじゃないYO! Studies in Logic and the Foundations of Mathematics だYO! 200 名前：１３２人目の素数さん mailto:sage [05/02/08 21:05:04 ] >>196 今はもう絶版になったり品切再版未定のものですが、 図書館などで長期の貸し出しをしてもらえる環境にあるならば、 次の二冊を薦めます。 ・前原昭二「数理論理学 数学的理論の論理的構造」培風館 無矛盾性証明の前に、カット除去定理とその簡単な応用までを まず身につけたいのならば、この本のε定理の前のところまで 読んでください。 ・竹内外史、八杉満利子「証明論入門」共立出版 Peano Arithmetic の無矛盾性証明まで一気に読む力があれば、 これを通読するのが一番です。(「数学基礎論(増補版)」でもよい) >>197 でちょっと触れている、松本和夫「数理論理学」共立出版 は 該当部分は、竹内-八杉に完全に含まれているので、上記の本が手に 入らない場合の次善の策と思います。 201 名前：１３２人目の素数さん mailto:sage [05/02/08 22:19:40 ] 『証明論入門』って易しめですかね 数学基礎論（増補版）だと、最後の章の 二階論理が無くなっちゃう気がする 書いてるのは竹内さんじゃなくて八杉さんだけど 202 名前：197 mailto:sage [05/02/08 22:22:19 ] 今更だが一寸書き間違いが 【誤】最近書かれた⇒【正】最近復刊された 203 名前：１３２人目の素数さん mailto:sage [05/02/08 23:16:15 ] >>197-202 たくさんのレスに激しく感謝します。 ＯＰＡＣると、プラヴィッツさんのは一冊だけ無関係ぽいのがあるのみでした。 数学基礎論入門はグッドステインというひとの著書ですか？ 以前少し見たときはコンパクトでつらそうでしたが、 証明論入門が最良ということですので、もう一度じっくりと見極めてこよう・・。 204 名前：１３２人目の素数さん mailto:age [05/02/10 00:35:38 ] パラメータをもつ関数同士の合成について質問します。 例えばa, b, c（全て正）をパラメータとし、3つの関数 　y=a/x，　y=b/x，　y=c/x を合成して、これらに共通したグラフ形状（ある意味、平均約な形状）を示す 新たな関数y=A/x を作り出す理論・手法というのは存在するのでしょうか？ 関数の合成といえば三角関数の合成と、フーリエ展開における指数関数の 合成くらいしか知りませんので、よろしくお願い致します。 205 名前：204 mailto:age [05/02/10 00:42:09 ] すみません ×　平均約な 〇　平均的な 206 名前：１３２人目の素数さん mailto:age [05/02/10 13:23:12 ] ageました 207 名前：１３２人目の素数さん mailto:sage [05/02/12 06:06:06 ] スレ違い 208 名前：１３２人目の素数さん mailto:sage [05/02/13 06:35:15 ] 別に数学が好きでもないし、ちょっとした疑問が出来たけどスレ立てるまでも無いのでここで聞いてみる 360角形と円は同じ物だと考えれますかね 209 名前：１３２人目の素数さん mailto:sage [05/02/13 10:11:07 ] 円と多角形は違う図形です 210 名前：１３２人目の素数さん mailto:sage [05/02/13 11:00:12 ] 全然違うじゃん というか普通の質問スレで質問してください 基礎論というのは、一つの数学の分野 （証明可能性とかを扱う）なので。 211 名前：１３２人目の素数さん mailto:sage [05/02/13 13:02:00 ] 数学板を｢質問｣で検索して一番まともそうなスレタイがここだったんですが もしかして高校生のための〜が数学板での標準質問スレですか 212 名前：１３２人目の素数さん mailto:sage [05/02/13 13:48:44 ] >>211 質問スレは目的に応じていくつかあるので、どれが「標準」かは決まって ないけど、その質問がここではスレ違いになることだけは確か。 とりあえず雑談スレで聞いてみるのがいいと思います。 雑談はここに書け！【２１】 science3.2ch.net/test/read.cgi/math/1107597473/ ただ、質問する際は「同じ」ということの意味をもっと精確に規定 したほうがいいと思うよ。それによって答えがかわってくるから。 213 名前：１３２人目の素数さん mailto:sage [05/02/13 15:16:51 ] どうも、とりあえずそっちのスレで聞いてみますね。ありがとうございました 214 名前：１３２人目の素数さん [05/02/14 02:17:14 ] っていうか数学ってなんなん？ 215 名前：１３２人目の素数さん mailto:sage [05/02/14 13:46:55 ] >>214 スレ違い。 216 名前：１３２人目の素数さん [05/02/15 17:05:15 ] 等号を含む一階述語論理の等号って、あれは、述語記号ですか？ 217 名前：１３２人目の素数さん mailto:sage [05/02/15 18:34:50 ] 二変数の述語記号ですよ。 ただ、等号に関する公理はやたら沢山ありますけど 218 名前：１３２人目の素数さん [05/02/15 19:45:02 ] モデルにおける付置の処理は、どんなことになってんでしょうか？ 219 名前：１３２人目の素数さん mailto:sage [05/02/16 16:56:43 ] ああいうことになってます。 としか答えようないんですけどね。 どんなことになってんでしょうか、とか意味不明なこと言われても。 220 名前：１３２人目の素数さん [05/02/17 10:30:43 ] 昔、ブラウアーとか言う人が「直観主義」とかいうことを言い出して ヒルベルト（だったかな）と論争したと思うんですけど、結局あれは決着 ついたのでしょうか。それともまだ解析学のような普通の数学をするのに 2重否定の除去はいつもできるとは限らないなどと言いながら数学してる 数学者も今現在いるのでしょうか。 221 名前：１３２人目の素数さん mailto:sage [05/02/17 11:02:31 ] >>220 1927年　ヒルベルトのハンブルクでの講演「数学の基礎について」で自分の視点から論争を総括 同年　ブロウウェルの論文「形式主義についての直感主義的反省」で４つの妥協案を提案→実質的和解 1931年　ゲーデルが不完全性定理を発表 222 名前：１３２人目の素数さん [05/02/17 11:44:14 ] 直観主義 -> 位相や層 223 名前：１３２人目の素数さん [05/02/17 12:19:47 ] > 等号に関する公理はやたら沢山ありますけど 沢山って？？？ 224 名前：１３２人目の素数さん [05/02/17 13:13:37 ] >>221 ＞同年　ブロウウェルの論文「形式主義についての直感主義的反省」で４つの妥協案を提案→実質的和解 へーーーすごいや。そんなことがあったんですね。その「４つの妥協案」と 言うのはどのようなものなんでしょう。もし嫌でなかったら教えていただけ ないでしょうか。あるいはどこか参照先をお教えいただけるとうれしいです。 当方、一般ピープルなので、論文の調べ方なんて知らないもので。(;_;) それともその論文はネットで調べられるのかな。英語なら根性で読むけど 他の外国語だとちょっと．．． 225 名前：220 [05/02/17 14:22:40 ] よく調べもしないで質問するなと怒られそうですが。もしやと思って 「直観主義 和解」でググって見たら www.shayashi.jp/history/Books/books.html を見つけることができました。このページの 「ゲーデル、不完全性定理」と題した文章の「たとえば、１９２７年ころに」 から始まるあたりを読んで見ますと 「和解ではなく、ヒルベルトがブラウワーを政治的にねじ伏せた」 と書いてあります。さてさて．．．今現在の数学者の皆さんはどうなのでしょう？ 例えば普通の解析学はどのように教えられているのでしょう？ あるいは 「フェルマーの最終定理」の証明は排中律や2重否定の除去はまったく用いられて いないのでしょうか？普通に用いられているとするならそれに文句をつける数学者は いないのでしょうか？ なんか教えて訓になっちゃいましたが、同じように疑問に思っている人 他にもいるんでないかなあ。 226 名前：１３２人目の素数さん mailto:sage [05/02/17 14:48:12 ] 現在、二重否定除去を無条件に認めない数学は確かにあって、 構成主義解析とかはそれを認めません。 ただ、二重否定は兎に角認めちゃいけないんだ、 とただ宗教のように二重否定除去を拒絶するんじゃなくて、 本人の人たちは、それなりの理由があってそうしています。 ただ、今の数学においては明らかに異端で、 数学者が1000人いたら、999人は普通の論理を普通に使う数学者です。 多分直観主義で数学やるのなんて、直観主義自体の研究を 除いたら構成主義解析くらいしか無いんじゃないかと思います 「数学の基礎をめぐる論争―21世紀の数学と数学基礎論のあるべき姿を考える」 「リーディングス 数学の哲学―ゲーデル以後」 なんかが参考になるかと。 227 名前：１３２人目の素数さん mailto:sage [05/02/17 14:49:30 ] >>223 任意の論理式〜に関して、〜が公理、 という形で沢山ある、というだけですね 228 名前：１３２人目の素数さん mailto:sage [05/02/17 14:55:49 ] どちらが正しいか？などという不毛な争いをする時代はとっくに過ぎ去った。 今は、通常の数学は従来通り進められ、同時に、数理論理学や 基礎論の一部では、使える論理を制限した場合にどのような 体系ができるかという研究が行われている。 229 名前：１３２人目の素数さん [05/02/17 16:08:29 ] www.mec.gr.jp/aij/wiki.cgi?AIJ%A1%E1%C3%DD%C6%E2%B3%B0%BB%CB ところが直観主義は、ある程度昔からわかっていたことなのですが、位相的な 数学と非常に密接な関係になるのです。(中略) 位相、トポロジーなどと妙な 具合に結びつき、具体的なものとして急速に用いられるようになってきたので す。それは、ここ10年かあるいは15年ぐらいでの大きな発展の一つではないで しょうか。また、例えばカテゴリーの方でのトポスのような話も、トポロジー、 位相と直感論理の関係とは同様なものなのです。 kurt.scitec.kobe-u.ac.jp/~sato/kyoto.html 層の概念で、これは集合が時間に沿って連続的に変化して行くものをモデル化 したものであると考えることも出来ます。そして層の世界を支配する論理は古 典論理ではなく直観主義論理であり、「すべての実数上の函数は連続である」 など、古典論理に従う数学では到底成り立ち得ない直観主義の様々な考え方が、 層の世界では非常に自然になります。 230 名前：１３２人目の素数さん mailto:sage [05/02/17 16:18:06 ] >>229のリンク先の話は 「直観主義数学のよいモデルが存在する」 ということ。 非ユークリッド幾何学のモデルが存在するからといって ユークリッド幾何学が否定されたわけではないように 直観主義数学のモデルが存在するからといって、 古典論理による数学が否定されたわけではない。 231 名前：１３２人目の素数さん mailto:sage [05/02/17 16:29:18 ] >>220 ところで君は、二重否定が矛盾をもたらすと思っているのかな？ ブラウアーの発言を「二重否定が矛盾をもたらす」ととらえるなら それは何の根拠もない言いがかりである。 普通なら「矛盾するというなら証拠を出せ」で終わりなのだが、 ヒルベルトは、数学における二重否定使用の矛盾性を証明しようとした。 しかし、このもくろみはゲーデルによって「無理」であることが示された。 232 名前：１３２人目の素数さん mailto:sage [05/02/17 16:39:46 ] >>231のつづき もっとも、ゲーデルの結果は、二重否定の矛盾を示すものではない。 ゲーデル自身、そんなことは信じていなかった。 彼は、単にヒルベルトのもくろみに無理があるといったまでである。 少なくとも「古典論理は矛盾する」と主張するのは 確たる根拠を示しえない点で、�dデモである。 直観主義数学の研究は、古典論理による数学を 否定するものではなく、その意味では上記のような �dデモ的態度とはまったく異なるものである。 233 名前：１３２人目の素数さん mailto:sage [05/02/17 16:46:38 ] >>226 ＞今の数学においては明らかに異端で、 ＞数学者が1000人いたら、999人は ＞普通の論理を普通に使う数学者です。 通常の数学では、見た目上非構成的な対象や論法を 使っていても、議論の本質とは無関係な場合が多い。 しかしながら、通常の数学者は、精密な検討を なしえない為、漠然と自分の数学が直観主義に 反するものだと思い込んでいるに過ぎない。 234 名前：１３２人目の素数さん mailto:sage [05/02/17 17:14:11 ] ＞直観主義で数学やるのなんて、 ＞構成主義解析くらいしか無いんじゃないか 林晋氏は、ヒルベルトの形式主義の源として 不変式論の有限基底定理をあげていたが･･･ 不変式論に着目すれば、その後、ワイルが 古典群の不変式を具体的に構成している。 このことと、ワイルがヒルベルトの形式主義に 異を唱えたこととは関係があるのかどうか･･･ 235 名前：220 [05/02/17 17:30:26 ] いやあ、たくさんの情報ありがとうございます。おもしろいですねえ。 >>231 ＞ところで君は、二重否定が矛盾をもたらすと思っているのかな？ いえいえ。それどころか、二重否定の除去や、排中律が使えないなんて いわれたら不自由で嫌だなあ、と思っています。 ＞ヒルベルトは、数学における二重否定使用の矛盾性を証明しようとした。 ＞しかし、このもくろみはゲーデルによって「無理」であることが示された。 へーーー。具体的にはゲーデルは何を示したんでしょう？もしかして 第2不完全性のことですか？（この言葉って一般的なんでしょうか？私は 前原昭二の「数学基礎論入門」で読んだだけです。その本の第2不完全性 のあたりは、はしょってある証明があまりにも多くて〔帰納的関係が算術 的論理式で表現可能とかいうところだったかな〕あきらめました。 だから、第2不完全性についてはよくわかってないかも。） >>229 ありがとうございます。これからそのリンク先を読んで見ます。 236 名前：１３２人目の素数さん mailto:sage [05/02/17 18:12:45 ] ＞具体的にはゲーデルは何を示したんでしょう？ ＞もしかして第2不完全性のことですか？ Yes． 237 名前：１３２人目の素数さん [05/02/17 23:09:02 ] ＞ 現在、二重否定除去を無条件に認めない数学は確かにあって、 ＞ 構成主義解析とかはそれを認めません。 　すでに古典になっちゃったとは思いますが、構成主義数学といえば、Bishopが 有名ですね。 plato.stanford.edu/entries/mathematics-constructive/ 　この数学を一言で言えば、排中律と外延性公理を仮定せず、しかし選択公理は 仮定するというものです。選択公理を仮定していると非構成的になると思うかも 知れませんが、排中律を仮定していないため、そのような非構成的な現象は生じ ないのです（ただし外延性公理を仮定すると排中律が導かれてしまいます）。 　Bishopのすごいところは、今まで非構成的にしか議論できないだろうと思われ ていたいくつかの理論を排中律なしで構築できることを示したことで、既にBishop 以前にも代数学の基本定理が排中律なしで証明できることは知られていたのです が、Bishopは、抽象空間におけるルベーグ積分論や、一般の局所コンパクトアー ベル距離群におけるハール測度の構成とか、一変数複素解析におけるリーマンの 開写像定理とか、少し弱い形ではあるが、局所凸空間のハーン・バナッハの定理 とかを証明して見せたのです。 　現在でも例えばシュワルツの超関数の空間の完備性とかを調べている人が日本 にもいます。 238 名前：１３２人目の素数さん mailto:sage [05/02/18 13:15:33 ] >>237 ＞外延性公理 集合論ではそういう建前はあるけど、実際には 群の元の異なる表示が、同じ元を表すかどうか 判定するアルゴリズムが存在しないなんていう 結果もあるわけだから。 もっともこの話は排中律には関係ないか。 239 名前：１３２人目の素数さん [05/02/20 17:43:41 ] 超ひも理論なんか研究してる奴は馬鹿 science3.2ch.net/test/read.cgi/rikei/1108248830/l50 240 名前：１３２人目の素数さん [05/03/01 14:07:11 ] 321 241 名前：１３２人目の素数さん [05/03/01 21:19:09 ] >>239 オマエモナー 242 名前：１３２人目の素数さん [05/03/11 15:05:45 ] モデル論の入門書として適当な本ってありますか？ 243 名前：１３２人目の素数さん mailto:sage [05/03/11 22:56:07 ] >>242 最近の本だとこのあたり。 David Marker, Model Theory: An Introduction, GTM, Springer, 2002. www.amazon.co.jp/exec/obidos/ASIN/0387987606/ Bruno Poizat, A Course in Model Theory: An Introduction to Contemporary 　Mathematical Logic, Universitext, Springer, 2000. www.amazon.co.jp/exec/obidos/ASIN/0387986553/ 244 名前：１３２人目の素数さん [05/03/13 22:30:30 ] 一階述語の証明の集合が原始帰納的であることは完全性定理と実質的に等しい。 というような文章を読んだのですが、なぜだか分かりません。 前者にはモデルの概念も何もないと思うのですが・・。 正確には下のように書かれていました。なぜか教えてください。 Putative proofs of universal validity of first-order formulas can be checked for validity, algorithmically. In technical language, the set of proofs is primitive recursive. Essentially, this is Godel's completeness theorem, although that theorem is usually stated in a way that does not make it obvious that it has anything to do with algorithms. 245 名前：１３２人目の素数さん [05/03/14 19:59:47 ] ランダム性の概念を数学的に追求した書物はありますか？ 246 名前：１３２人目の素数さん [05/03/14 21:42:30 ] クレタ人はみんな頭がいいとクレタ人が言った 247 名前：１３２人目の素数さん mailto:sage [05/03/15 01:31:50 ] 坪井明人　モデルの理論 河合出版 248 名前：１３２人目の素数さん mailto:sage [05/03/15 02:12:08 ] へー、坪井先生　本書いてたんだー。（by元ゼミ生） 249 名前：１３２人目の素数さん [05/03/15 02:37:37 ] 高１です。すれ違いかもしれませんが質問がスレタイだったので質問させて下さい 因数分解なのですが、これって公式全部覚えないとダメなんでしょうか？ 確か中学校の時、因数分解は −2a / −b±√−b^2−4ac　で解くと言ってたのですが。 複雑になってくると応用が利きません。 250 名前：１３２人目の素数さん mailto:sage [05/03/15 02:55:14 ] >>249 オマイさんは激しく勘違いしていると思われ。 数学基礎論ってのは大学くらいから専攻の対象になる数学の一分野のことで基礎の数学のことでは ない。 ttp://messages.yahoo.co.jp/bbs?.mm=GN&action=topics&board=1835554&type=r&sid=1835554 Yahoo数学板の「高校生の為の数学質問コーナー」あたりで聞いてきなさいな。 251 名前：１３２人目の素数さん mailto:sage [05/03/15 19:47:27 ] ちょっとなごんだw 252 名前：１３２人目の素数さん mailto:sage [05/03/16 00:24:52 ] >>243 >>247 レスｻﾝｸｽｺ >>247 のが手に入りそうなんで、とりあえず、それから読んでみます。 253 名前：１３２人目の素数さん [05/03/16 11:21:22 ] あのーみなさんは自由変数と束縛変数で文字の使い分けしてますか？ 例えば自由変数にはa,b,cなどのアルファベットの最初の方を使い、 束縛変数にはx,y,zなどのアルファベットの後ろの方を使う、というような。 私はどうせ本質は変わらないのだからいちいち区別すんのやめよーー、 と思っていました。 　最近GentzenのCut除去定理の証明をなぜかもう一度フォローしたくなって 読んでるんですが、この証明見ると自由変数と束縛変数を区別しなかったら ちょっとやりにくいなあ、としきりに思えてくるわけです。そこでいろいろ 疑問がわいてきたのですが、私はもう社会人？？年生。いまさら近くにこんな 話題にのってくれる人もなし、文献もなし。どなたかご教示ください。 ・そもそもGentzenのLKの形式って自由変数と束縛変数の区別をするのが普通な 　のでしょうか？ ・もし、GentzenのLKで自由変数と束縛変数を区別しない場合、例えば（∀右） 　の推論規則は 　Γ⇒Θ、A −−−−−−−　 　Γ⇒Θ、∀xA 　のように∀xを付け加えるだけなのでしょうか。それとも 　Γ⇒Θ、A(x) −−−−−−−−−　 　Γ⇒Θ、∀yA(y) 　のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の 　なかに含めてしまうのでしょうか。 ＊そもそも自由変数と束縛変数を区別しないGentzenの流儀なんてなかったりして。 ＊こんな細かいことってどこ探しても説明なんてないんだよなあ。 ＊ほんと、誰かたすけてちょ。 254 名前：１３２人目の素数さん mailto:sage [05/03/16 14:11:26 ] >>253 自由変数と束縛変数を区別しない Hilbert 流の体系の本はたくさんあるので、 それを参考にすれば自然に作れるはずですが。 255 名前：253 [05/03/16 16:31:22 ] >>254 どうも舌足らずですみません。自由変数と束縛変数を区別しないだけなら もちろん何の問題もないのですが、Cut除去定理の証明をどのように工夫する のかなあ、と思いまして。 もしかして、その区別をしない場合は 「終式（証明図の最後のSequent）を変えず」にCut除去するの ではなくて、「束縛変数の違いを無視して、終式を変えずに」Cut除去 するのかなあ、と思ったわけです。 256 名前：１３２人目の素数さん mailto:sage [05/03/16 17:08:49 ] （∀右）と（∃左）の推論規則には、それの適用により 束縛されることになる変数に関する条件が付いているはず。 いつでもどこでも無制限に適用できるわけではないので、 本を読み返してみよう。 257 名前：253 [05/03/16 17:59:48 ] >>256 私が今読んでる証明は、数学的帰納法を2重に使用する方法でCutを除去する のですが、その場合、今着目している証明図の固有変数(eigen variable) が各々の（∀右）と（∃左）で”固有”なものとなるように書き換えを行う んです。とすれば、 　Γ⇒Θ、A(x) −−−−−−−−−　 　Γ⇒Θ、∀yA(y) のように変数を換えてしまうのも推論規則の中に含めていないと考えづらい ですよね。そこで上記のような話になるんです。 「下式に固有変数がないこと」という条件を無視して推論すると言うこと を言っているのではありません。 258 名前：１３２人目の素数さん [05/03/16 22:21:38 ] Bourbakiみたいに束縛変数のところを□に置き換えて、頭の quantifier と□を鎖 で結んじゃう流儀を使えば何にも問題なくなる。 259 名前：253 [05/03/16 22:42:01 ] >>258 それはそうですけど、私がひっかかってるのは、どちらかと言うと 　Γ⇒Θ、A −−−−−−−　 　Γ⇒Θ、∀xA のように∀xを付け加えるだけの流儀も捨てがたいなあと言う気持ち があるからなんです。 話は違いますが、鎖で結ぶってところが抵抗あるんですよねえ。 ワープロ（というよりTeXですが）で書きづらいし。 260 名前：１３２人目の素数さん mailto:sage [05/03/17 00:08:47 ] ＞ 話は違いますが、鎖で結ぶってところが抵抗あるんですよねえ。 □ が出てくるときは、いつも □ とそれより左にある quantifier とただ一本の 鎖で結ばれているから、□ とその quantifier の間にある記号の個数だけ □ に ダッシュを付けた記号 □''…' を □ と鎖のかわりに使えばいい。 261 名前：253 [05/03/17 10:54:43 ] >>260 ＞□ とその quantifier の間にある記号の個数だけ □ に ＞ダッシュを付けた記号 □''…' を □ と鎖のかわりに使えばいい。 なるほどねえ。簡単に工夫できるんですねえ。 >>255に誰か偉い人のコメントあるといいなあ。 262 名前：偉い人 mailto:sage [05/03/17 14:06:41 ] >>261 自分で考えろ 263 名前：253 [05/03/17 15:00:25 ] 残念(;_;) 264 名前：１３２人目の素数さん mailto:sage [05/03/17 15:49:18 ] >>244 にレスしてあげたいが気力がでない。 >>263 カット消去の証明を書き換えるのはまんどくさいので、区別無しの システムを作って、区別ありのシステムとの間で証明図の相互書き換えが 可能であること示せば？ 265 名前：253 [05/03/17 18:02:42 ] >>264 レスありがとうございます。 ＞区別無しの ＞システムを作って、区別ありのシステムとの間で証明図の相互書き換えが ＞可能であること示せば？ とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が 自由変数としても束縛変数としても使用されている場合を考えると、あまり うまくいかない気がします。やはり「終式（証明図の最後のSequent）を変えず」 にCut除去するのではなくて、「束縛変数の違いを無視して、終式を変えずに」 Cut除去すると言う風になるような気がしてきました。 266 名前：253 [05/03/17 18:12:22 ] あ、私も勘違いしてた。Cut除去の証明においては、自由変数と束縛変数を区別する というよりも、もし区別しない流儀を選んだ場合、 >>253の ＞例えば（∀右） ＞　の推論規則は ＞　Γ⇒Θ、A ＞−−−−−−−　 ＞　Γ⇒Θ、∀xA ＞　のように∀xを付け加えるだけなのでしょうか。それとも ＞　Γ⇒Θ、A(x) ＞−−−−−−−−−　 ＞　Γ⇒Θ、∀yA(y) ＞　のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の ＞　なかに含めてしまうのでしょうか。 のところが良く分からないのです。 267 名前：１３２人目の素数さん [05/03/17 22:18:54 ] 集合論の基礎から高度な内容までを含んだ優れた書籍はありませんか？ 洋書でも結構です。

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef