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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 411 名前：１３２人目の素数さん mailto:sage [2005/05/12(木) 01:43:58 ] マルチさん乙！ 412 名前：１３２人目の素数さん [2005/05/13(金) 20:07:30 ] 数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い 413 名前：１３２人目の素数さん [2005/05/15(日) 17:04:14 ] >>399 ＞ロッサーの可証述語というものについて、誰か教えてください。 教えてやってもよいが、いくら払う？ ＞「ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものは ＞どれも¬φの証明ではない」ということらしいですが ＞なんで、〜より小さなもの、ということを ＞言わなければいけないのか、がわかりません。 わからん、とすればそこだろうな ＞「ある論理式φの証明があって、ある¬φの証明は無い」 ＞ではだめなのでしょうが、その理由がよくわかりません。 その文章ではダメだな。せめて 「ある論理式φの証明があって、どれも¬φの証明では無い」 くらいにいわんと。 414 名前：１３２人目の素数さん [2005/05/15(日) 17:17:44 ] >>413 しかし 「ある論理式φの証明があって、どれも¬φの証明では無い」 を論理式でかくと、∃ｙProv(y,x)∧¬∃ｚDispr(z,x) となってしまって、zはyと何のかかわりもなくなる。 ∃ｙ(Prov(y,x)∧¬∃ｚ((ｚ＜ｙ)∧Dispr(z,x))　 だとｚはｙに依存する。 415 名前：１３２人目の素数さん [2005/05/15(日) 17:42:32 ] >>414 ｙを具体的に与えたとき Prov(y,x)∧¬∃ｚ((ｚ＜ｙ)∧Dispr(z,x)) を判定する述語はつくれるが、zがyと独立だった場合 ¬∃ｚDispr(z,x) （つまり∀ｚ¬Dispr(z,x)）を 判定するのは無理。 416 名前：１３２人目の素数さん [2005/05/15(日) 18:56:06 ] 解析接続てなんですか？ 417 名前：GreatFixer ◆ASWqyCy.nQ [2005/05/15(日) 18:59:41 ] Re:>>416 正則関数の定義域を広げること。 418 名前：１３２人目の素数さん [2005/05/16(月) 13:05:23 ] 可証性述語を表現するとされる論理式を、ちょっと強くしたんだろうな、 くらいで通り過ぎようと思っていましたが、なんか教えてもらえそうなので、もう少しくらいついてみます。 >>413 >>414 >>415 ∃ｙProv(y,x)∧¬∃ｚDispr(z,x) 「ある論理式φの証明があって、どれも¬φの証明では無い」では、ｚがｙと関係付けられていないので、まずい、 〜より小さい、というのは、ｚをｙと関係付ける一つの方法だ、 というように読めるのですが、 それが、 ・〜より小さい、という表現を用いている ・「ある論理式φの証明があって、どれも¬φの証明では無い」 ではだめ ということの理由ですか 419 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 14:46:36 ] >>418 つーか、>>414ぬきに、>>415で"ｙより小さい"という 限定を行って計算可能になったからＯＫなのでは？ 420 名前：１３２人目の素数さん mailto:age [2005/05/16(月) 21:22:37 ] >>409 詳細キボンヌ　ハァハァ 421 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 23:51:08 ] >>418 T を PA を含む帰納的な理論、Prov(y,x) を T の標準的な可証性述語、 P が T の証明図、A が T の論理式のとき、g(P), g(A) をそれぞれ P, A のゲーデル数を表す数字とする。 このとき、ゲーデルの第一不完全性定理は次の表現可能性と対角化補題 から導くことができる。 P が論理式 A の T での証明図 ⇔ Prov(g(P),g(A)) が T で証明可能. 一方、Prov'(y,x) ≡ Prov(y,x)∧¬∃z＜y Dispr(z,x) とおくと、 T が無矛盾という仮定の下で、次が成立する。 ロッサーの不完全性定理は、これよりゲーデルの第一不完全性定理と 同様の方法で証明できる。 P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能 ところが、Prov*(y,x) ≡ Prov(y,x)∧¬∃z Dispr(z,x) とおくと、 T が無矛盾という仮定があったとしても、 「P が論理式 A の T での証明図」と「Prov*(g(P),g(A)) が T で証明可能」 との同等性が証明できない。 422 名前：１３２人目の素数さん [2005/05/17(火) 12:07:17 ] ありがとうございます。 ＞Prov(y,x)∧¬∃z＜y Dispr(z,x) とおくと、・・ ＞Prov(y,x)∧¬∃z Dispr(z,x) とおくと、・・ というくだりで、ずいぶんと、わかんない部分が補完されてきたような気がします。 ところで、 標準的な可証性述語もロッサーの可証性述語も 扱ってる関係は ＞P が論理式 A の T での証明図 であるのに、 それを表現するとされる論理式は、 標準的な可証性述語　　∃ｙProv(y,x） ロッサーの可証性述語　　∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ））　 で異なってるわけで、 これは、ただ単に、必要な条件を無矛盾である、にするための工夫ということですか はじめ、標準的な可証性述語の∃ｙProv(y,x）だけ、見てたときには、扱う関係のメタ的な情報を表したものなのかな、くらいに思ってましたが、 ロッサーの可証性述語の∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ））の場合は、扱ってる関係（P が論理式 A の T での証明図）とは、あんまり（全部は）関係ありませんよね 423 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 13:17:32 ] >>420 直感的には x≦yの→a_x∪a_y＝a_y なので ∪Ａ＝(...((((a0∪a1)∪a2∪)a3∪)a4∪)...a∞)＝a∞ 論理式は有限である必要があるので複雑さも有限 複雑さが∞のa∞という論理式は存在しない。 厳密な解はｼﾗﾈ。 424 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:35:47 ] 恐らく分かる人にはレベルが低すぎなのかもしれませんがご教授ください。 計算式も書いてもらえると嬉しいです。m(_ _)m 例題 チョコレートAには30％のホワイトチョコが含まれている。 チョコレートBには１０％のホワイトチョコが含まれている。 両方のチョコを使わなくてはならない。 以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは いくつ用意しなければいけないが？ 425 名前：>424 [2005/05/17(火) 22:37:23 ] 少し訂正です。 以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは 何キロずつ用意しなければいけないが？ 式 426 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:39:19 ] >>424の問題のどこらへんが、数学の基礎をゆるがすんだろう。 427 名前：１３２人目の素数さん mailto:age [2005/05/17(火) 23:07:54 ] R^2はR^3の部分空間ではないことを説明して、＊と比較せよ。 ＊…平面ベクトル全体からなる集合は自然に空間ベクトルの全体からなる線形空間の部分空間と見ることができる。 （;TωT） ナゼR^2がR^3の部分空間でないのか？？昨日からずっとモヤっとしています。誰か処方箋をキボンヌ。 428 名前：１３２人目の素数さん mailto:sage [2005/05/18(水) 00:09:00 ] マルチすんなよ 429 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:13:35 ] >>422 ＞扱ってる関係 なんかこの言い方がキモチ悪いのだが、それはさておき･･･ ＞標準的な可証性述語だけ、見てたときには、 ＞扱う関係のメタ的な情報を表したものなのかな、 ＞くらいに思ってましたが、 メタ的な情報って何だい？ ぶっちゃけていえば、 「命題も証明も数字であらわして、 　後者が前者の証明であることを 　算術だけで言い表したもの」 だな。数字＝ビット列、算術＝プログラムと思えばいい。 430 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:19:12 ] >>422 ＞ロッサーの可証性述語の場合は、扱ってる関係とは、 ＞あんまり（全部は）関係ありませんよね なにいってんのかわかんねぇぞ！ これもぶっちゃけていえば、 「単にシンタクスチェックをするだけではなく 　与えられた証明よりも小さな証明の中に 　与えられた命題の否定の証明がないことを 　チェックするもの」 ということだな。 ここで、「与えられた証明よりも小さな証明」と 上限を設けてるのがミソ。これがないと、 チェックする証明が無限になってしまう。 それではプログラムが終了するとは限らない。 （実際、終了しない） 431 名前：１３２人目の素数さん mailto:age [2005/05/19(木) 23:12:57 ] >>405 >>409 詳しくヨロ♪ 432 名前：１３２人目の素数さん [2005/05/19(木) 23:23:47 ] p,qが命題変数のとき p∧q この選言標準形と連言標準形を求めよ。 すごいレベル低いと思いますが選言標準のほうがわかりません。どうやって求めるのでしょうか？ 433 名前：１３２人目の素数さん [2005/05/19(木) 23:38:55 ] あ。解決しました　お恥ずかしい 434 名前：１３２人目の素数さん [2005/05/20(金) 14:03:53 ] >>421 でそのロッサーの不完全性定理ってどんなものなんでしょう？結論はどうなっているの？それから 　　P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能 はどう証明すればいいんでしょう。 きっと⇒が本質的なんですよね。それで¬Dispr(1,g(A)), ... ¬Dispr(g(P) -1, g(A)), Prov(g(P), g(A))の証明を作ればいいんでしょうか。 このDispr(p,g(A)) は Dispr(MP(p,q),g(A)) ≡ Prov(p,g(A⇒B))∧Dispr(q,g(B)) のように具体的なpについて原始帰納的に定義されているの？でもそれだと∃z<y(Dispr(z,x))は定義できない。。。 435 名前：１３２人目の素数さん [2005/05/20(金) 17:50:26 ] ちっともわかってませんでした。証明木の全ての箇所が正しいように。。。 Dispr(p,x) ≡ ∃d(DTH_SENTENCE(p,d,x) ∧∀d'<d,y,z(DTH_SENTENCE(p,d'+1,y) ∧DTH_SENTENCE(p,d',z) ∧DTH_SUBPROOF(p,d',q) ⊃ Prov(q,IMP(y,z))) ∧∀y(DTH_SENTENCE(p,0,y)⊃ IS_AXIOM(INVERSE(y)) 436 名前：１３２人目の素数さん [2005/05/20(金) 21:52:36 ] 証明: pの大きさに関する帰納法 PROOF(p)がPROP(a)の証明である(PROP(a)が公理) → 示すことはない。 PROOF(p)がPROP(a)の証明である(PROP(a)は公理でない) → あるbがあってpの部分木であるfst(p)とsnd(p)がそれぞれPROP(b)⊃PROP(a)とPROP(b)の証明である。 → ∀q<fst(p)(¬Dispr(q,impl(b,a)))と∀q<snd(p)(¬Dispr(q,b))の証明がある。(帰納法の仮定) → ¬Dispr(0,impl(b,a)),..¬Dispr(fst(p)-1,IMPLIES(b,a))と¬Dispr(0,b),..¬Dispr(snd(p)-1,b)のそれぞれの証明がある。 → ... → ¬Dispr(1,a),..¬Dispr(p-1,a)の証明がある。 → ∀q<p(¬Dispr(q,impl(b,a)))の証明。 という感じになると思います。 で何でq<pがついてるかですがひとつには帰納法のベースケースが作れることと思う。つまりpが葉ならばなにひとつ¬Disprを示せていなくてよいわけです。 PROP(a)が公理だとしても∀q¬Dispr(q,a)の証明を作ることはT内での無矛盾性の証明だと思う。 437 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 22:23:05 ] 集合Xから集合Yへの写像fが全射となる条件って量化記号でどう表現できますか？ 438 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:24 ] ∀y(y∈Y → ∃x∈X(f(x)=y)) 439 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:58 ] ∀y∃x (x∈X∧y∈Y∧f(x)=y) 440 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:36:10 ] 下が成り立ってたらすごいことになるな 441 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 23:06:11 ] >>438-440 えーーーと…、で結局答えはあるのでしょうか？ 442 名前：１３２人目の素数さん [2005/05/24(火) 00:02:29 ] >>439 すごいかはともかく。こっちはどんなyも必ずYに入っている。かつfは全射といってる。 443 名前：１３２人目の素数さん [2005/05/24(火) 00:07:30 ] ∀y∈Y∃x∈X(f(x)=y) は ∀y(y∈Y → ∃x(x∈X ∧ f(x)=y)) の省略。 444 名前：１３２人目の素数さん [2005/05/24(火) 14:24:40 ] 完全性証明 T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である よって Tで証明可能である　なら　Tで真である は何故言えるんですか？ T∪{¬φ}で証明可能である　なら　T∪{¬φ}で真である は、分かるんですが 445 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 18:07:55 ] 基礎論ムズイ 446 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 23:24:52 ] 基礎論ズームイン 447 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:13:14 ] 命題論理の範囲だと、古典論理でAが証明可能なとき、 直観主義でも¬¬Aが証明可能になることは比較的簡単に言えるのは 皆さんご存知かと思いますが、述語論理の範囲では似たようなことは 言えないのでしょうか？ご存知の方おられましたら何とぞご教示ください。 448 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:32:02 ] >>447 Glivenko の定理の拡張の話ですね。 "Glivenko theorem" "predicate logic" で検索するといろいろ出てくるようです。 449 名前：１３２人目の素数さん [2005/05/25(水) 00:52:17 ] >>444 「Tで証明可能である　なら　Tで真である」のことは健全性といいますよ。 450 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 01:25:53 ] > T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である > よって > Tで証明可能である　なら　Tで真である こんなことが書いてあるはずがない。 「(φが) T で真であるなら T で証明可能である」 でしょ。 451 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 02:10:15 ] 基礎論の学部授業がある大学ってありますか？ 452 名前：１３２人目の素数さん [2005/05/25(水) 02:13:40 ] >>449 健全性は公理を真とするベースステップからはじめて証明の大きさの帰納法で簡単にでてくる。 453 名前：447 mailto:sage [2005/05/25(水) 09:04:59 ] >>448 早速情報ありがとうございます。ぐぐってみます。 454 名前：１３２人目の素数さん [2005/05/25(水) 12:59:32 ] >>450 そう、それ、ミスった、 健全性の逆の方向 完全性証明 T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である よって >「(φが) T で真であるなら T で証明可能である」 は何故言えるんですか？ でした、 455 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 16:12:50 ] >>454 対偶考えろ。 456 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 00:14:00 ] 解決しますた。お騒がせしました。 457 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 04:36:47 ] >>451 京大では「計算機科学」っていう3回生向けの講義でそれっぽいことやってた。 458 名前：１３２人目の素数さん [2005/05/27(金) 05:28:24 ] ε記号、ε定理ってなんですか？ ∀や∃より便利なものみたいなんですが、ニュアンスとしては どう捉えればいいんでしょう？ また、様相論理ってのは数学基礎論の対象になるものなんでしょうか？ 459 名前：１３２人目の素数さん mailto:sage [2005/05/27(金) 10:48:07 ] >>458 plato.stanford.edu/entries/epsilon-calculus/ これでもよめ。 εx F(x) は、「F(x)をみたすようななにか（の一つ）」を意味する。 英語で言うなら関係代名詞のようなもの。 460 名前：１３２人目の素数さん mailto:sage [2005/05/27(金) 17:12:11 ] ε-δ論法は数学基礎論で扱えるの？ 461 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 00:18:50 ] ∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x) っていうのはすごく引っかかるんだが、 「which asserts that the epsilon operator assigns the same witness to equivalent formulae A and B.」 って言われてもまだなんかなあ。 どなたかこれについてご教示くださる方いませんか。 （確かこの公理って、ブルバキでも使われてましたよね？ ブルバキでは説明はなかったような。） 462 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 07:08:13 ] なんでひっかかるの？ 卑劣っぽいから？ 463 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 09:15:23 ] A(x)をみたすxがただ一つとは限らないから？ 464 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 12:26:24 ] >>460 無理です 465 名前：１３２人目の素数さん [2005/05/28(土) 13:16:39 ] なんで？ 466 名前：１３２人目の素数さん [2005/05/28(土) 13:36:31 ] 素数の歌ってなんですか？ 467 名前：１３２人目の素数さん [2005/05/28(土) 13:48:37 ] 質問： 山口人生博士の、博士論文のころの業績の評価を教えていただけますか？ （集合論、論理学の全業績） 468 名前：１３２人目の素数さん [2005/05/28(土) 14:13:09 ] εｘA(x)は、選択順位の情報も暗に含んでいると思ったら？ Hilbertの有限数学では、ｘは最小の自然数にとればいいし。実際そのよう。 ∀x(A(x)⇔B(x))をみたすｘが存在しない場合でも、εxA(x)=εxB(x)=0で成り立つ。 εｘA(x)は、A(x)をみたすｘであることに加えて ・存在、非存在の情報 ・デフォルト選択順位の情報 を含んだ実体で、 論理学のnandや、ライプニッツモナドのような複合的存在なのだと思う。 469 名前：１３２人目の素数さん [2005/05/28(土) 14:13:52 ] 選択公理が包含されるのは当り前。ところで選択公理は構成的数学に落とせるの？ 470 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 14:58:03 ] >>469 　落とせる、というか、選択公理それ自体は構成的なので、これを仮定する ことに何も問題は無い。 　通常の数学において選択公理が非構成的だと言われるのは、排中律を併用 すると、背理法によって存在しないと仮定すると矛盾するからということで しか存在が証明されていないのに、存在するもののうちの任意の一つを指定 できてしまうということが生じるからで、排中律を仮定しない構成数学では、 存在が証明できるときは必ずその命題を満たす具体的な項が構成できるから、 その「最初に構成して見せたもの」をεで表すのだということにしておけば、 ε記号や、そこから必然的に導出される選択公理を拒否すべき理由は無い。 471 名前：470 mailto:sage [2005/05/28(土) 15:22:22 ] >>461 貴方の「すごく引っかかる」とういうセンスは正しい。 この公理は、一見何も問題無いように見えるが、実はこの公理から排中律が 導びかれてしまうので、実は非構成的な公理である（というよりも、この公 理を前提にするなら、等号の公理 Ｐ(s), s=t → Ｐ(t) をもっと弱い形に 修正しなければいけない）。 472 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 20:33:23 ] >>470 ずっと前からそう思ってたんだけど最近になって必ずしも構成的ではないんじゃないかと思い始めた。 集合族 {A_i} について ∀i∃x(x∈A_i) が証明できたとしても、 それは i が一つ与えられれば A_i の要素を取り出せるということでしかない。 その要素の構成は i の表し方に依存しないとは限らない。 だとすれば ∀i∃x(x∈A_i) の証明から構成される選択関数は、 普通にいう関数(つまり外延的関数)には必ずしもならなくて、 i=j であっても f(i)=f(j) だとは限らないような関数になるのでは？ というのがその理由なんですが。 ところでこれ、等号の公理のことと関連してますね。書いてから気付いたんですが。 473 名前：461 mailto:sage [2005/05/28(土) 23:28:59 ] うひゃー、亀レススマソ。油断してたらすげーレスついてる。 >>463 ＞A(x)をみたすxがただ一つとは限らないから？ そうです。それが素朴にひっかかるとこです。 >>468 ＞εｘA(x)は、選択順位の情報も暗に含んでいると思ったら？ なるほどなあ。わしゃぁ、普通の数学のときは選択公理ばんばん使う派 なんだけど、なぜか基礎論のあたりになると二の足踏んじゃう変な性格 なんだなあ。結局、すべてのモデルにおいて、その対象領域には整列 順序がついてると思え．．．．そこまでは言ってないんでしょうか？ >>471 ＞実はこの公理から排中律が導びかれてしまう ガビョ〜〜〜〜〜ン(oOo)。排中律まで導かれちまうの？それ、どの文献 にのってるか教えていただけるとうれしいです。但し、一般ピープルにも 手に入るやつだとうれしいなあ。しかも、日本語か、英語で．．． （ワガママスマソ．もしやブルバキヨメバワカル？） しかし、普通の数学のときは排中律もばんばん使う派だけど、これすごい ショーゲキだなあ。 やっぱ、基礎論のときだけこんなこだわっちゃうのは矛盾してんのかなあ。 474 名前：470 [2005/05/29(日) 19:51:14 ] ＞実はこの公理から排中律が導びかれてしまう 　文献を参照する必要も無いくらい簡単な話で、任意に取った命題 Ｒ に対して ( Ｒ ∧ x=0 ) ∨ x=1 という命題を Ｐ x=0 ∨ ( Ｒ ∧ x=1 ) という命題を Ｑ と書くことにすると、∃xＰ も ∃xＱ も共に成り立つから、εxＰ は Ｐ を満たし、 εxＱ は Ｑ を満たす。これは ( Ｒ ∧ (εxＰ)=0 ) ∨ (εxＰ)=1 (εxＱ)=0 ∨ ( Ｒ ∧ (εxＱ)=1 ) が共に成り立つということを意味する。 　そこで、(εxＰ)=0 の場合と (εxＰ)=1 の場合で場合分けをし、更に 、(εxＱ)=0 の場合と (εxＱ)=1 の場合で場合分けをすれば、 CASE1：(εxＰ)=0 又は (εxＱ)=1 のとき。いずれの場合でも Ｒ が証明される。 CASE2：(εxＰ)=1 かつ (εxＱ)=0 のとき。Ｒ を仮定すると ∀x(Ｐ⇔Ｑ) が成り立 　　　　つので、ε公理により (εxＰ)=(εxＱ) が成り立つので矛盾する。言いかえ 　　　　ると Ｒ⇒⊥ すなわち ¬Ｒ が成り立つ。 　すなわち Ｒ∨¬Ｒ が成り立つ。命題 Ｒ は任意だったので、これは排中律が成り 立つことを意味する。証明終わり。 475 名前：461 mailto:sage [2005/05/29(日) 23:38:38 ] >>474 ほんとだすげーーー。ひさしぶりにドキドキするなぁーーー。 でもそうすると、 （＊）「∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x)」がどれだけの内容 　　　　を含んでしまっているか とか、その辺のことが気になってくるなあ。実は >>471 ＞等号の公理 Ｐ(s), s=t → Ｐ(t) をもっと弱い形に ＞修正しなければいけない がいまいちよくわかんなかったんですが、（＊）を気にすると 理解できるようになるのかな。あまり聞きすぎるのは教えてクン で良くないですが、気が向くなら情報ください。 メモ　Ｒを仮定すると ∀x(Ｐ⇔Ｑ)のところ。 　　　(P∧R)⇒Q、(Q∧R)⇒P 476 名前：470 mailto:sage [2005/05/30(月) 06:40:28 ] >>475 （＊）「∀x(A(x)⇔B(x))⇒εxA(x)=εxB(x)」というのは、ある項の間に等号が 成り立つことを結論する推論規則とみなせる。 　これは(ZF)の公理の一つである「外延性公理」： （**）「∀x(x∈A ⇔ ｘx∈B) ⇒ A=B」 でも同じことで、実際、ε記号を導入して(＊) を仮定するかわりに、外延性公 理(**)と選択公理を仮定してもやはり排中律が導かれてしまう（その証明は上 の証明とほとんど同じだから省略。ただし竹内先生の直観主義的集合論の本に は証明が載っている）。 　竹内先生は、この事実から、「直観主義的(ZF)集合論では選択公理は仮定で きない」としてその後の議論を展開しているのだが、私見では、ワルサをして いるのは選択公理ではなく、(＊)あるいは(**)のような「等号を導入する公理 （推論規則）」を追加したにもかかわらず、等号を消去する推論規則を修正し なかったからだと思っている。そのことの説明は少し長くなるんで、要望があ れば何回かに分けて解説してもいい。 　この問題は、>>472 の問題提起とも実は関係がある。 477 名前：461 mailto:sage [2005/05/30(月) 08:58:00 ] >>476 ＞要望があれば何回かに分けて解説してもいい。 要望するする！絶対する！ いやぁ。２ちゃんねるでこんなに興奮すんのはじめてだぁ。 ついでに ＞外延性公理(**)と選択公理を仮定してもやはり排中律が導かれてしまう のときの>>474のPに当たるものだけでも教えてもらうのは、調子に乗りすぎ ですか？そうでないと思ってくださるなら、お願いしたいのですが。 478 名前：１３２人目の素数さん mailto:sage [2005/05/30(月) 10:00:11 ] >>477 P={ x | ( R ∧ x=0 ) ∨ x=1 } Q={ x | x=0 ∨ ( R ∧ x=1) } とするとできそう。 479 名前：１３２人目の素数さん mailto:sage [2005/05/30(月) 16:36:37 ] >>476 あいかわらず同じネタだなStromdorf（ｗ ＞私見では、ワルサをしているのは選択公理ではなく、 ＞(＊)あるいは(**)のような「等号を導入する公理（推論規則）」 ＞を追加したにもかかわらず、等号を消去する推論規則を ＞修正しなかったからだと思っている。 そもそも構成的に考えるなら、外延性公理のような 非構成的公理を導入するのは自殺行為。 下手な小細工で逃れようとするのは間違ってる。 480 名前：470 mailto:sage [2005/05/30(月) 22:14:29 ] 　通常の数学で、等号の公理といえば、 （= 導入） ｔ が項なら ├ ｔ=ｔ あるいは同じことだが、 （= 導入)' ｓ と ｔ が同一の項なら ├ ｓ=ｔ という推論規則と （= 消去） ｓ=ｔ, Ｐ(ｓ) ├ Ｐ(ｔ) という２つの推論規則を仮定する（もちろん他の流儀もあるが）。 　このとき、上のつの推論規則はある意味で“対”になっている。 　それは、（= 消去）で“消去”される等式 ｓ=ｔ を（= 導入） の前提「ｓ と ｔ が同一の項」で置き換えると、 ｓ と ｔ が同一の項, Ｐ(ｓ) ├ Ｐ(ｔ) あるいは同じことだが Ｐ(ｔ) ├ Ｐ(ｔ) となって「当たり前の結論」が得られる。このように、消去規則の消去 すべき式を導入規則の前提で置き換えたとき、当たり前の結論しか得られ ないという性質は、等号に関する推論規則だけでなく、自然推論における 論理記号 ∧ ∨ ⇒ ⊥ ∀ ∃ の推論規則についても成り立ち、このことが 直観主義論理をある意味で「特徴づけて」いる。（これに対し、¬ に関す る古典論理の推論規則はこのような性質を持たない。） 481 名前：470 mailto:sage [2005/05/30(月) 22:15:33 ] 　ところが、ε公理 (＊) を仮定するということは、 自由変数 x に対し、Ｐ(x) ├ Ｑ(x) と Ｑ(x) ├ Ｐ(x) が成り立てば ├ (εxＰ) = (εxＱ) という推論規則を仮定することに他ならず、これは等号の導入規則の形をしていて、言い換え ると等号の導入規則が２種類に増えたことを意味する。 　ところが、上に挙げた (= 消去) というのは、これら２個の導入規則の組とは、 上に説明した意味では“対”になっていない。ここがポイントである。 482 名前：１３２人目の素数さん [2005/05/31(火) 22:11:20 ] >>480 ＞これに対し、¬ に関する古典論理の推論規則はこのような性質を持たない。 ¬A∨A と ¬A∨B, A∨C ⇒ B∨C のこと？ 483 名前：470 mailto:sage [2005/06/01(水) 00:00:25 ] >>482 (¬ 導入) Ｐ ├ Ｑ Ｐ ├ ¬Ｑ ------------ 　¬Ｐ (¬ 消去) ¬¬Ｐ -------- 　Ｐ のペアのこと。他の論理記号については、（導入）規則は、当該論理記号が 陽に出てくるのが横線の下に一箇所だけだし、（消去）規則は当該論理記号 が陽に出てくるのが横線の上に一箇所だけであるのに、古典論理の ¬ に関 する推論規則は、（導入）規則には ¬ が横線の上段にも出てくるし、（消 去）規則には ¬ が横線の下段に２個出てくる。これでは「導入して直ちに 消去」した場合でも、そもそも当該論理記号を消し去ることができない。 　なお、直観主義論理では、¬ を基本的な論理記号とみなすと古典論理と 同じことになるが、直観主義論理では ¬ のかわりに ⊥ を基本的な論理記 号とみなせば、他の論理記号と同じ性質を持つ（古典論理ではそうはいかな い）。 484 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 00:16:38 ] >>481 >>483 古典論理に対する自然推論の体系のうちどれを指しているのか？ 少なくとも本質的に異なるものが三つはあるのだが。 485 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 10:43:31 ] >>480 ＞（= 消去）で“消去”される等式 ｓ=ｔ を ＞（= 導入） の前提「ｓ と ｔ が同一の項」で置き換えると なんか一気に馬鹿げた結論を主張したな。Stromdorf 本当のポイントは＝を2つの項を引数する関数として考えた場合 真偽が完全に判定できると考えるのは「非構成的」だという点 にある。 486 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 23:42:23 ] ＞　＝を2つの項を引数する関数として考えた場合 ってのがどう効いてくるのか。 余計じゃない？ 487 名前：１３２人目の素数さん mailto:sage [2005/06/01(水) 23:47:19 ] 　ここで、ε記号とε公理の組合せよりも、外延性公理と選択公理の組合せの 方がその後の議論、というか、問題点がわかりやすいので、後者において排 中律を証明する方法を念のため書いておく： 　任意に与えられた命題 Ｒ に対して、集合 Ａ と Ｂ を Ａ = { x | ( Ｒ ∧ x=0 ) ∨ x=1 } Ｂ = { x | x=0 ∨ ( Ｒ ∧ x=1 ) } で定義する。1∈Ａ かつ 0∈Ｂ だから、Ａ も Ｂ も元を持つ。従って、選 択公理により、Ａ とＢ から成る集合 {Ａ, Ｂ} 上に選択関数、すなわち f(Ａ)∈Ａ かつ f(Ｂ)∈Ｂ となる関数 f : ｛Ａ, Ｂ} → Ａ∪Ｂ が存在す る。このとき ( Ｒ ∧ f(Ａ)=0 ) ∨ f(Ａ)=1 f(Ｂ)=0 ∨ ( Ｒ ∧ f(Ｂ)=1 ) が共に成り立つ。 　そこで、f(Ａ)=0 の場合と f(Ａ)=1 の場合で場合分けをし、更に f(Ｂ)=0 の場合と f(Ｂ)=1 の場合で場合分けをすれば、 CASE1：f(Ａ)=0 又は f(Ｂ)=1 のとき。いずれの場合でも Ｒ が証明される。 CASE2：f(Ａ)=1 かつ f(Ｂ)=0 のとき。Ｒ を仮定すると、∀x((x∈Ａ)⇔(x∈Ｂ)) が成り立つので、外延性公理により Ａ = Ｂ となるので等号の公理 (= 消去) により f(Ａ) = f(Ｂ) が成り立つので矛盾する。言いかえると Ｒ⇒⊥ すな わち ¬Ｒ が成り立つ。 　すなわち Ｒ∨¬Ｒ が成り立つ。命題 Ｒ は任意だったので、これは排中律 が成り 立つことを意味する。証明終わり。 488 名前：１３２人目の素数さん mailto:sage [2005/06/02(木) 00:05:43 ] どっかで重要な前提を忘れているような希ガス 489 名前：１３２人目の素数さん [2005/06/02(木) 22:19:49 ] どっか、とは？ 特段の前提などどこにもないような気がするが。 490 名前：１３２人目の素数さん [2005/06/03(金) 07:38:14 ] このスレッド向きかどうかわからないのですが、質問です。 Ｐ＝∀Ｑ．（Ｐ→Ｑ）→Ｑ という論理式は成り立っていますか？ これは、三段論法Ｐ∧(Ｐ→Ｑ)⊃Ｑを正当化する論理式で、 成立しそうに思えます。 真理値表で考えます。 Ｐが偽、Ｑが真のとき、 Ｐ→Ｑは真、(Ｐ→Ｑ)→Ｑは真 一方、Ｐは偽。成り立たないように思えます。 なぜでしょう？どこがおかしいのでしょうか？ 491 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 08:51:29 ] >>490 ∀Ｑ． の部分はどこへいった？ 492 名前：１３２人目の素数さん [2005/06/03(金) 11:00:21 ] >>490 Ｑって0変数の述語変数記号なの？これって2階述語論理？ Ｐって論理式？Ｐの後にイコールの記号が来るのはなぜ？ 493 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 13:47:46 ] >>491のいうとおり、>>490は ∀Ｑ．が読めてない Ｐが真のときは、 Ｑが真でも偽でも(Ｐ→Ｑ)→Ｑは真 だから∀Ｑ．（Ｐ→Ｑ）→Ｑが真 一方 Ｐが偽のときは、 Ｑが真なら(Ｐ→Ｑ)→Ｑが真 Ｑが偽なら(Ｐ→Ｑ)→Ｑが偽 だから∀Ｑ．（Ｐ→Ｑ）→Ｑが偽 494 名前：１３２人目の素数さん mailto:sage [2005/06/03(金) 18:44:22 ] εxP(x)を具体的な対象と見なす事自体に 無理があると思うけどなあ 495 名前：１３２人目の素数さん mailto:sage [2005/06/04(土) 23:28:16 ] 言語のスペックとしてどこまで求めるか、ってことだろ。 無理があると思う ＝ 言語に多くの機能を求めないという立場 496 名前：１３２人目の素数さん [2005/06/09(木) 20:04:41 ] モデル 論議領域={1,2} V（P）={1,2} のもとで、Pxは真、ですか？ 497 名前：497 mailto:sage [2005/06/09(木) 20:56:12 ] √49 = 7 498 名前：１３２人目の素数さん [2005/06/11(土) 14:52:39 ] ラムダ論理ってのはここでいいですか？質問なんですが、 (λy.g(y))(λx.f(x))をβ変換すると、g(λx.f(x))になりますね？ これって何ですか？ 一般に、λ引数に関数を代入すると、こういう形が出るような気がするけど。 499 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 14:56:27 ] >>498 λって、数学屋さんの言葉で言うと├→ ですよね。 (λy.g(y))(λx.f(x)) も数学屋さんの言葉で言えば合成関数 g 。f のこと。 500 名前：１３２人目の素数さん [2005/06/11(土) 15:50:15 ] しかしそれならλx.g(f(x))の形になりますよね。 この場合、関数を引数にとって何かを実行する高階の作用が定義されているようなに見えるのです。 501 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 18:24:24 ] ヒント η簡約 502 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:20:56 ] おいおいめちゃくちゃ言ってんな。>>500で正しいんだよ。 503 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:35:54 ] 原始帰納的関数でない関数でもλ計算で証明可能なの？ 504 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 20:48:20 ] >>503 λ計算は全ての計算可能関数をシミュレート出来るよ。 505 名前：１３２人目の素数さん mailto:[sage] [2005/06/11(土) 20:57:46 ] 一次式の計算（中一レベル）をできるだけ詳しく教えてください。 506 名前：１３２人目の素数さん mailto:sage [2005/06/11(土) 21:41:25 ] >>505 よくある勘違いだがスレ違い。 507 名前：１３２人目の素数さん mailto:[sage] [2005/06/12(日) 21:30:27 ] >>506 っつざけんな厨房！！！ 508 名前：１３２人目の素数さん [2005/06/14(火) 15:48:58 ] ∀：全肯定 ∃：部分肯定 Α＝¬∀：全否定 Ε＝¬∃：部分否定 ∀∧∃：全肯定かつ部分肯定 Α∨∃：全否定または部分肯定 Ε∧∀：部分否定かつ全肯定 Ε∨Α：部分否定または全否定 ¬（∀∧∃）＝Ε∨Α Α∨（¬∃）＝Ε∨Α ¬（（¬Ε）∧∀）＝Ε∨Α まさかこんなところにEVAが潜んでいたとは 509 名前：１３２人目の素数さん [2005/06/14(火) 23:01:50 ] gは関数をうけとり何かを返す関数ととろう。型は (α→β)→γ だ。 510 名前：１３２人目の素数さん mailto:sage [2005/06/21(火) 22:25:41 ] で？ 511 名前：１３２人目の素数さん [2005/06/22(水) 01:44:57 ] age

---

---

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

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