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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 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 ] 集合論の基礎から高度な内容までを含んだ優れた書籍はありませんか？ 洋書でも結構です。 268 名前：１３２人目の素数さん mailto:sage [05/03/18 00:36:10 ] >>267 Jech or Kunnen 269 名前：１３２人目の素数さん mailto:sage [05/03/18 03:25:01 ] >>257 束縛変数と自由変数の区別をするかどうかの問題ではなく、 eigen-variable が固有であるという条件が保証されていない 場合に Gentzen の証明をどのように修正すればいいかという 問題を考えるべきでしょう。 270 名前：253 [05/03/18 08:18:46 ] >>269 その通りです。（>>266） 271 名前：１３２人目の素数さん [05/03/19 03:43:43 ] >>265 ＞とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が ＞自由変数としても束縛変数としても使用されている場合を考えると、あまり そんな終式での照明図ではそもそもcutは除去できないと思われ。 例えば「情報科学における論理」p.78でも読んでみれ。 272 名前：253 [05/03/19 11:01:16 ] >>271 情報提供ありがとうございます。早速取り寄せてみます。（品切れ？） ところで、自由変数と束縛変数を区別しない場合、 （∀右）の推論規則として 　Γ⇒Θ、A −−−−−−−　 　Γ⇒Θ、∀xA のように∀xを付け加えるだけのものしか許さない場合、もしかしてCutなしでは 証明できない簡単なSequentがあるのではないかと思って考えてみたら、 　　∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1) はもしかしてCutなしでは証明できないのではないでしょうか。もちろん 　　∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2) は簡単に証明できますから、 　　∀x(x∈z)⇒∀y(y∈z)・・・・・(3) とのCutを使えば(1)は証明できますが、推論規則として上記の（∀右）しか 許さない場合は(1)はCutなしでは証明できないのではないでしょうか。 273 名前：偉い人 mailto:sage [05/03/19 11:32:10 ] ＞∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1) ＞はもしかしてCutなしでは証明できないのではないでしょうか。 そもそも∀の後ろに何の変数もない式は証明できないだろう。 ＞もちろん ＞　　∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2) ＞は簡単に証明できますから、 それは、君が論理法則を誤解してるということ。 274 名前：253 [05/03/19 16:40:57 ] >>273 その通りですね。xが抜けていました。正しくは 　　∀x(x=y∧x∈z)⇒∀y(y∈z)・・・(1) 　　∀x(x=y∧x∈z)⇒∀x(x∈z)・・・(2) です。失敬、失敬、(^^;) 275 名前：１３２人目の素数さん mailto:sage [05/03/19 18:15:54 ] >>274 ∀x(x=y∧x∈z)⇒∀y(y∈z) cut があろうとなかろうと、正しくない式が証明されてはいかん。 276 名前：253 [05/03/19 23:54:32 ] >>275 >>274の(2)は示せますか？ なんか、ガックシorz 277 名前：１３２人目の素数さん mailto:sage [05/03/20 02:07:38 ] >>275 >>274 の(1)や(2)は普通に正しい様だが。 278 名前：１３２人目の素数さん [05/03/20 02:19:19 ] 私は>>275じゃないですけど、(1)は何か yのboundが少々おかしくないですか？ 279 名前：１３２人目の素数さん mailto:sage [05/03/20 11:51:38 ] >>278 気持ちが悪いけど別に問題はないと思われ。free の y と、bound されてる y は無関係なわけで。 だけど、こんな変数がある時は cut を消去できなかったような気が。 280 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 13:50:46 ] あのーー。GentzenのLKやNKの形式的論理計算を支援してくれるようなソフト 探しているんですが、どなたかご存じないですか。まあ、日本語でHelpが読めるに 越したことはないですが、英語でもがんばってみたいと思うのですが。 （Hilbert式のでもいいかな。） 281 名前：280 [2005/03/30(水) 21:03:32 ] あ、すいません。当方MS-Windowsなので、MS-Windowsで使用できるものを おながいします。 282 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 21:18:11 ] >>280 Lisp かなんかで自分で作ったほうがいいんでは。 勉強になるし、拡張性も思いのままだし。 283 名前：280 [2005/03/30(水) 21:51:15 ] >>282 Lispってそういう文字列処理得意なんですか？ 284 名前：１３２人目の素数さん mailto:sage [2005/03/30(水) 23:20:42 ] >>283 MLとかOCaml使うべし。 再帰的データ型使えるしパーサとかも普通にライブラリに入ってるはず。 285 名前：280 mailto:sage [2005/03/30(水) 23:41:20 ] >>284 ちょっと検索してみましたが、MS-Winで使用するにはMeadowとかやんないと いけないんでしょうか？ やっぱ、xyzzyじゃ無理？ （つっても、xyzzyもKaTeX使ってる程度だけど） 286 名前：１３２人目の素数さん mailto:sage [2005/03/31(木) 01:11:15 ] >>280 別にMeadow入れる必要はないよ。 ↓ここから辿って適当なコンパイラ落としてくればよろし。 ttp://www.jaist.ac.jp/~ohori/texts/mllinks.html 287 名前：280 mailto:sage [2005/03/31(木) 11:55:46 ] >>286 をを！おありがとうござりあんす！ 288 名前：１３２人目の素数さん mailto:sage [2005/03/31(木) 20:12:27 ] >>283 > Lispってそういう文字列処理得意なんですか？ もちろん。 文字列処理じゃなくて記号処理っていうべきだけど。 Windows では PLT-Scheme がお勧め。 289 名前：280 mailto:sage [2005/03/31(木) 21:00:26 ] >>288 をを！ありがとうございます。 するってえと、MLとLispとどっちにするか迷いますなあ。 290 名前：１３２人目の素数さん [2005/04/08(金) 21:43:50 ] モデル理論の超フィルタを使用した超積構造の作り方って、 ルベーグ積分の almost everywhere と似ていないか？ 何か関係あるのかな。 291 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 00:30:02 ] 基礎論の入門書の良書ってどんなのがありますか？ 基礎論は全くわからないので、なんとなく流派とか色々ありそうで、 どんな本から読めばよいか分かりません。 （できれば、和書がよいのですが）どなたか教えてください。 292 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 01:39:45 ] >>291 数学基礎論シリーズ www.kawai-juku.ac.jp/bunkyo/7-2-c.html 293 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 01:46:52 ] >>292 どうもです。参考にしてみます。 294 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 02:38:36 ] クロスリーとかも入門書としてはよいような。 295 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 11:12:17 ] 291ですが、因みに、基礎論に流派とかってありますか？ （なんかG.B.流（ゲーテル・ベルヌーイだったかな）とか聞いたことがあるんだけど。） あったら、どんなのがあるのか教えてもらえませんか？ 296 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 14:02:43 ] 学派だったら無いこともないけど、 あまり数学で学派なんか気にしないですよ。 GBというのは多分ゲーデル、ベルナイスの事だと思うんですが、 単に公理的集合論の定式化に、BG式のものがあるだけで、 これも本質的にはZF式のものと同じものです。 297 名前：１３２人目の素数さん mailto:sage [2005/04/09(土) 17:49:04 ] >>296 返答ありがとうございます。 じつは位相の本で、このＢＧ流を使われていたので できれば、この体系から勉強したいと考えていて。 上に挙げていただいた本はどうなんでしょうか？ 298 名前：１３２人目の素数さん [2005/04/09(土) 22:11:41 ] 数学基礎論の研究って盛んなの? 外国でも? 299 名前：１３２人目の素数さん [2005/04/11(月) 00:02:51 ] age 300 名前：１３２人目の素数さん mailto:sage [2005/04/11(月) 15:31:04 ] >>298 日本は盛んではない国だったと思うが？ 301 名前：１３２人目の素数さん [2005/04/12(火) 21:29:33 ] アメリカじゃナウい学問 302 名前：１３２人目の素数さん [2005/04/12(火) 23:43:20 ] >300 何故だろうか？ 303 名前：１３２人目の素数さん [2005/04/12(火) 23:45:48 ] 隈部正博って知ってる？ 304 名前：１３２人目の素数さん [2005/04/13(水) 00:24:53 ] 竹内外史ゆかりの人か？ 305 名前：１３２人目の素数さん mailto:sage [2005/04/13(水) 17:26:33 ] 誤差を含めた割り算ってどうやるんですか？ 誤差のある重さと誤差のある体積を使って密度を求める問題がわからない…orz 306 名前：１３２人目の素数さん mailto:sage [2005/04/13(水) 20:04:48 ] >>303 出身が早稲田、専門が帰納的関数論だから廣瀬健先生の門下かな？ 307 名前：１３２人目の素数さん mailto:age [2005/04/13(水) 21:41:49 ] 写像ｆ：Ｘ→Ｙが単射であるとは一体何を示せばいいのですか？ 308 名前：１３２人目の素数さん [2005/04/13(水) 22:38:06 ] 微分係数と導関数って何を求めてるの？ 309 名前：１３２人目の素数さん [2005/04/13(水) 23:43:51 ] >303 放送大学助教授。

---

---

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

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