- ベストアンサー
ブルバキ等号を持つ述語論理について
- ブルバキ数学原論集合論１を持つ方への質問です。
- 問題の証明をお願いします。
- また、Tが(R⇔S)⇒(τz(R)=τz(S))を持たない時にも、Tが明示的公理を持たない場合、xが文字、Rが関係式ならば、xは定数でないので、(R⇔S)⇒(∀x)(R⇔S)は定理となり、S7より(R⇔S)⇒(τx(R)=τx(S))は定理です。しかし、x≠yが定理となるx、yも存在すると思います。これでは矛盾が生じているように思うのですが、何がいけないのでしょうか？
- みんなの回答 （7）
- 専門家の回答
質問者が選んだベストアンサー
その他の回答 (6)
- wwpqq
- ベストアンサー率0% (0/1)
- stomachman
- ベストアンサー率57% (1014/1775)
ANo.4へのコメント： > 規則C24*：4)(∀x)Ａ⇒Ａ はＴの定理 > という規則がおかしい理由 については、予定通りにτについて考えると、その理由が見えて来るような気がします。というわけで、（形式主義ではホントは禁法であるところの、意味解釈の）続き。 [2] ご質問のもうひとつのキモになってるのは、τ記法の意味解釈だと思います。 (∃x)Ａは(τxA|x)Ａで定義されるんですから(∃x)P ⇔ (τxP|x)Pは自明。しかし、普通に数学を学んだ大抵の人にとっては「(∃x)Pの意味なら分かってるけどτxPって何？」じゃないでしょうか。まして「￢(∃x)Pのときには、τxPはどうなる？」という所まではなかなか頭が回らない。 そこでひとつ、「＃＃である場合のτxPって何だ？」という風に逆に考えてみましょう。すると、 (∃x)Pすなわち￢(∀x)(￢P)が定理であるときのτxP, (∀x)Pすなわち￢((∃x)(￢P))が定理であるときのτxP, (∀x)(￢P)すなわち￢((∃x)P)が定理であるときのτxP, (∃x)(￢P)すなわち￢(∀x)Pが定理であるときのτxP, はそれぞれどういう意味なのか。さらに、裸のPは(∀x)Pとは違うんですから、 Pが定理であるときのτxP, ￢Pが定理であるときのτxP, がそれぞれ何を意味しているか。 ● (∃x)Pすなわち￢(∀x)(￢P)が定理であるときのτxPは何を意味するか。∃の定義から(∃x)Pとは(τxP|x)Pのことである。すなわち、τxPは「(τxP|x)Pが定理になるようなドレカの対象x」という意味。 ●(∀x)Pすなわち￢((∃x)(￢P))が定理であるときのτxPとは何か。￢((∃x)(￢P))とは￢(τx(￢P)|x)(￢P))のことだけれど、問題はτx(￢P)じゃなくてτxPです。(∀x)Pなら必ず(∃x)Pであるから、τxPは「(τxP|x)Pが定理になるようなドレカの対象x」。 ●(∀x)(￢P)すなわち￢((∃x)P)が定理であるときのτxPとは何か。∃の定義から￢((∃x)P)とは￢(τxP|x)Pですから、それは（τxPと書かれるくせに）「￢(τxP|x)Pが定理になるようなドレカの対象x」。 ● (∃x)(￢P)すなわち￢(∀x)Pが定理であるときのτxPは何を意味するか。((∃x)(￢P))とは(τx(￢P)|x)(￢P))のことだけれど、問題はτx(￢P)じゃなくてτxPです。同じ(∃x)(￢P)であっても、τxPは、 ・(∃x)Pの場合なら、τxPは「(τxP|x)Pが定理になるようなドレカの対象x」 ・(∀x)(￢P)の場合なら、τxPは「￢(τxP|x)Pが定理になるようなドレカの対象x」 ● Pが定理であるときのτxPとは、つまりxを縛る条件が何も無いってことですから、「対象ならナンデモ」という意味ですよね。 ● Pが定理であるときのτx(￢P)、同じ事ですが￢PであるときのτxPとは何か。それは（τx(￢P)と書かれるくせに）￢(τxP|x)Pが定理である。つまりxを縛る条件が何も無いってことですから、結局「対象ならナンデモ」という意味。 こうして見ると、(∀x)PであるときのτxPと、PであるときのτxPにはさして違いがないような気もしますけれども、両者は交換できない（Tで同値性が証明できない）んだから、どうしても区別しなくちゃいけません。さしたる違いがないように見えるのは、この意味解釈がへたくそだからです、スイマセン。 ポイントは、(Aを含む条件1) ⇒ ((τx(Aを含む関係式2))を含む関係式） という格好の定理において、「⇒の左側がどうなってるかということが、⇒の右側にある(τx(Aを含む関係式2))の意味に影響する」ということでしょう。言い換えれば、三段論法に慣れちゃってると、⇒の左辺と右辺がまるで別の物であるかのように思ってしまうし、対象式(τx(Aを含む関係式2))は局所的に、つまり単独で、その意味が決まると思ってしまうけれど、実はそういうことではないようだ。 さて、ご質問のシェーマ S8 (Ｒ⇔Ｓ)⇒(τx(Ｒ)＝τx(Ｓ)) に適当に関係式と文字を割り振ってやって、 (S⇔S)⇒(τxS=τxS) という格好の定理を得たとしましょう。ただしSは何らかの定理だとします。すると(S⇔S)も定理だから、(τxS=τxS)も定理である。また、Sが定理なので、τxSとは上記の「● Pが定理であるときのτxP」つまり「ナンデモ」である。 (τxS＝τxS)とは【「ナンデモ」は「ナンデモ」と等しい】ということですが、ただし左辺のτxSが指す「ナンデモ」と右辺のτxSが指す「ナンデモ」には、どちらも何の縛りもないから、両者は独立であり、互いに別物でもかまわない。 一方、 1文字xだけからなる対象式の意味するところは、(何の制約も付いていないのだから）「ナンデモ」である。1文字yだけからなる対象式も「ナンデモ」を意味していて、それはxの指す「ナンデモ」とは独立である。 なので、 (τxS＝τxS)とは、x=y ということを丁度意味している。（なお、規則C23によって、(∀x)(∀y)(x=y)も定理になる。かくて、S8があると、"="がせいぜい「両辺は対象式だ」というぐらいのことしか意味しないという、なんだか空虚な理論になる。） （シツコイですけど：これはTにおける証明【Tで許される形式的な操作だけによる構成列の構成】ではなくて、意味解釈に基づく論証であることに注意。つまりご質問の直接の回答ではありません。そこはご自分で辛抱強くやらないと。） 一方、 S7 ((∀x)(Ｒ⇔Ｓ))⇒(τx(Ｒ)＝τx(Ｓ)) においては、((∀x)(Ｒ⇔Ｓ))である場合、Rも(∀x)Rも￢Rも(∃R)Rも、どれも必ずしも定理ではない。なので、このときのτx(R)が何を意味するかというと、上記(●)のすべての場合があり得ます。もちろん興味があるのは、Rや￢RやSや￢Sは定理ではなく、そして((∀x)(Ｒ⇔Ｓ))が定理である場合。 ○(∃x)Rが定理であるとき。(∀x)(Ｒ⇔Ｓ)なので(∃x)(R∧S)である。だからτxRが意味する「(τxR|x)Rが定理になるようなドレカの対象x」とは「(τxR|x)(R∧S)が定理になるようなドレカの対象x」に他ならず、ゆえに、「(τxR|x)Rと(τxR|x)Sが共に定理になるようなドレカの対象x」であり、つまり(τxR|x)R,(τxR|x)Sは共に定理であるはず。そして、τxSが意味するのも、「(τxS|x)Rと(τxS|x)Sが共に定理になるようなドレカの対象x」であるから(τxS|x)R, (τxS|x)Sは共に定理であるはず。ここでS7によれば、τxRとτxSは同じ対象を指しているのであり、だからτx(Ｒ)＝τx(Ｓ)とはx=yを意味しない。 ○(∀x)Rが定理であるとき。(∀x)(Ｒ⇔Ｓ)なので、(∀x)(R∧S)であるから(∃x)(R∧S)である。つまり、S7によれば、τxRとτxSは同じ対象を指しているのであり、τx(Ｒ)＝τx(Ｓ)とはx=yを意味しない。 ○(∀x)(￢R)が定理であるとき。(∀x)(Ｒ⇔Ｓ)なので、(∀x)￢(R∨S)であり、τxRが意味する「￢(τxR|x)Rが定理になるようなドレカの対象x」とは「￢(τxR|x)Rと￢(τxR|x)Sが共に定理になるようなドレカの対象x」である。同様に、τxSとは「￢(τxS|x)Rと￢(τxS|x)Sが共に定理になるようなドレカの対象x」である。つまり、S7によれば、τxRとτxSは同じ対象を指しているのであり、τx(Ｒ)＝τx(Ｓ)とはx=yを意味しない。 ○ (∃x)(￢R)が定理であるとき。(∀x)(Ｒ⇔Ｓ)なので、(∃x)(￢R∧￢S)である。(∃x)Rの場合なら、(∃x)(R∧S)であるから、τxRとτxSは同じ対象を指しているのであり、x=yということではない。また、(∀x)(￢R)の場合なら、(∀x)(￢R∧￢S)である。τxRは「(τxR|x)Rと(τxS|x)￢Sが共に定理になるようなドレカの対象x」で、τxSは「(τxS|x)Rと(τxS|x)￢Sが共に定理になるようなドレカの対象x」。つまり、S7によれば、τxRとτxSは同じ対象を指しているのであり、τx(Ｒ)＝τx(Ｓ)とはx=yを意味しない。 S7は要するに、「∀x(R∧S)ならば、RとSを満たすある同じ対象のことをτxR、τxSと二通りに表せる。また、∀x(￢R∧￢S)であっても、やはりある同じ対象のことをτxR、τxSと二通りに表せる」ということを意味するシェーマ。 一方、S8に出て来るτxRとτxSは、それぞれ独立に「対象ならナンデモ」を指している。 ご質問の「演習§５、７）」ってのは、要するに「だから∀xPとPとは全然違うんだぞ」という話だったわけで、規則C24と規則C24*との違いもここから生じていると言えるんじゃないでしょうか。 でも、えー！？でも、えー！？ これってすごくトリッキーですよね。分かりにくいですよね。 そのヤラシさを避けようとしてでしょう、大抵の基礎論では、少々長ったらしくなるのを厭わずに、このあたりに関しては別の定義の仕方・説明の仕方が工夫されています。たとえば、対象とは別の概念として、自由変数、束縛変数、定数という概念をあからさまに使うとか。
お礼
意味を教えて下さったおかげで、∀ＡとＡの違いを理解することができ、とても勉強になりました。 ですが、数学原論のなかでこんな文章をみつけました。 「（文字ｘがＴの定数でない限り）Ｔにおいて定理Ｒを述べること、定理（∀ｘ）Ｒを述べること、あるいは超数学的な規則：ＵがＴのいかなる対象式であっても、（Ｕ｜ｘ）ＲはＴの定理である、ということを述べることは、すべて同じことになる。」 「仮定（∀ｘ）Ｒを追加する。しからばＲは真」 いったいなにがおきているのかさっぱりわかりません。正直、数学原論は自分の手には負えないような気がしてきました。もう数学原論はあきらめて、島内剛一の数学の基礎、を読んでみようと思います。 今回の質問で、論理学について興味を持つことができました。私は大学生ではありますが、数学科の人間ではありませんし、論理学などの授業があるわけでもないため、誰かに質問することができません。どのような勉強をすればいいのかまったくわからないのです。そこで、最後の質問として、論理学を独学で勉強するのに適した本を教えていただけないでしょうか。また、証明論、計算理論、様相論理、高階述語論理、ゲーデルの超数学、これらがどのような分野なのか今の私にはよくわかりませんが、将来学びたいと思ったときのために、どういう順番で学ぶべきか教えていただければ幸いです。
- stomachman
- ベストアンサー率57% (1014/1775)
ご質問の > これに加えて質問ですが、 の部分に関してです。 確かにフツーの数学では、変数xを含む命題P(x)において、xを自由変数として（つまり束縛するという断りを入れないまんま）P(x)を証明する。すると、xを束縛変数にした∀xP(x)が帰結できますね。しかし、数学原論ではどうでしょうか。 ======== 規則C23:ＡがＴの定理、文字ｘがＴの定数でなければ、(∀x)ＡはＴの定理 において、Aを（Ｒ⇔Ｓ）とすれば、 > （Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）は定理 というシェーマが得られる。残念ながら、その逆の規則 C-23: (∀x)ＡがＴの定理なら、ＡはＴの定理 ってのはありません。だけど、 規則C24：4)(∀x)Ａ⇒(Ｕ|x)Ａ はＴの定理 を使うと、Aを（Ｒ⇔Ｓ）とすれば、 （∀ｘ）（Ｒ⇔Ｓ）⇒ (U|x)（Ｒ⇔Ｓ） が出て、Uをxにすれば、 （∀ｘ）（Ｒ⇔Ｓ）⇒ (x|x)(R⇔S) である。 (U|x)ってのは代入なのだから(x|x)は「何もしない」ということであり、従って新しいシェーマ （∀ｘ）（Ｒ⇔Ｓ）⇒（Ｒ⇔Ｓ） が得られた！ ======== …ように思われますよね。（質問者氏もおそらくこのようにお考えになったのではないかと推測しています。）で、 > 何がいけないのでしょうか？ それはですね： ★ あるシェーマ・規則を別のシェーマ・規則に適用する、なんてことできましたっけ？まして、それによって「新しくシェーマ・規則を作る」なんて手段が体系Tにはありましたっけ？ つまり、上記の議論は、Tに関する超数学と、Tそのものとを混同しているんです。まず、ここがおかしいんですね。 では、混同にならぬよう、始めに「R,S,x,Uに具体的に関係式や文字を割り当てたものを考えているんだ」という断り書きを入れて修正しておきましょう。（「ほら修正終わり。なんだ、ただの揚げ足取りじゃないか」と思われるでしょうが、ま、ま。）すると、規則C24を使って （∀ｘ）（Ｒ⇔Ｓ）⇒ (U|x)（Ｒ⇔Ｓ） という形をした公理が得られる。（「だから、ほらやっぱり結論は同じ」と言いたくなるでしょうけれども、ま、しばらくご覧じ。） このとき、(U|x)という代入は、xは何らかのTの文字でしかも定数ではないもの、すなわち本来ただの□であるのに対し、Uは何かTの対象式であり、つまり何か対象を指している。確かに、□を対象で埋めるのが代入ですから、これは問題ない。 ところが、(x|x)はというと、□を□で置き換える操作であり、実際「何もしないのと同じだ」というんですから、代入になっていない。それによって、 規則C24：4)(∀x)Ａ⇒(Ｕ|x)Ａ はＴの定理 を 規則C24*：4)(∀x)Ａ⇒Ａ はＴの定理 に差し替えちゃったわけです。 で、そもそも： ★ シェーマ・規則に対して( | )で何かを代入するなんてこと、できましたっけ？ また同じ間違いをしてました。 別の言い方をすると： 代入( | )に限らず、 ★ 規則やシェーマに書いてある"x"それ自体はTの文字ではなくて、「Tの、何か或る決まった文字」を表す記号。もっと言うなら、規則やシェーマはテンプレートであって、"x"は「テンプレート中で対象式が置かれる場所を示すただのマーク」であった筈ですね。一方、Tの関係式や対象式に"x"があれば、これはホントにTの文字xである。両者は全然別物。 （両者の"x"を混同しないためにこそ、□と鎖の記法から話が始まってるんじゃないでしょうか。） 実はこのあたり、似たような混乱がちょいちょい生じます。 簡単なところでは、推論規則と、A⇒Bの形の論理式との混同： http://okwave.jp/qa/q96470.html 。さらに、カリーのパラドックス: http://okwave.jp/qa/q4893333.html 。 集合論のラッセルのパラドックス: http://okwave.jp/qa/q3290945.html もよく似ています。様相論理の抜き打ちテストの話: http://okwave.jp/qa/q2346446.html だって、深いところで繋がっているように思います。 ------------ かくて、Tに関する超数学とTそのもののとの区別を厳格に付けた上で、数学原論を再読しなくちゃなりません。 でも、差し当たり「(∀x)Pが定理であることと、裸のPが定理であることとは、違う意味を持っている」らしいと分かりましたよね。 （裸のPが定理であるというのは、何も「文字をひとつも含まない関係式Pが定理である」ということを意味しているのではありません。たとえば、Pが(∃y)(ナンタラカンタラ)で、(∀x)Pは(∀x)(∃y)(ナンタラカンタラ)であるとか。丁度「(∀x)Pの(∀x)を脱がせたんだけど、その下にまだパンツ穿いてたんだヨ…」 というような。) 次に、τについて考察してみようと思います。(予定)
お礼
＞ 規則C24：4)(∀x)Ａ⇒(Ｕ|x)Ａ はＴの定理 を 規則C24*：4)(∀x)Ａ⇒Ａ はＴの定理 に差し替えちゃったわけです。 すばらしいです。まさにそこが自分が勘違いしていたところです。 しかし、大変申し分けないのですが、これほど丁寧に回答してくださってもまだ納得できない部分があります。 ＞★ 規則やシェーマに書いてある"x"それ自体はTの文字ではなくて、「Tの、何か或る決まった文字」を表す記号。もっと言うなら、規則やシェーマはテンプレートであって、"x"は「テンプレート中で対象式が置かれる場所を示すただのマーク」であった筈ですね。一方、Tの関係式や対象式に"x"があれば、これはホントにTの文字xである。両者は全然別物。 自分では理解しているつもりなんですが、 「R,S,x,Uに具体的に関係式や文字を割り当てたものを考えているんだ」 としたときに、ｘはすでにＴの文字であり、「Tの、何か或る決まった文字」を表す記号、ではないように思えてしまうのです。これは間違いでしょうか？ 後もう少しで理解できそうなので、何度もお手間をかけさせて申し訳ありませんが、 規則C24*：4)(∀x)Ａ⇒Ａ はＴの定理 という規則がおかしい理由を、今回の説明とは少し違った感じで説明していただけないでしょうか。
- stomachman
- ベストアンサー率57% (1014/1775)
まずANo.2へのコメントについてです。余計なお世話に応答して下さってありがとうございます。 > 選択公理を用いる証明に納得できなかったため、 > どういったものが集合といえるのかが知りたい ということでしたか。それならなるほど、公理的集合論の基本を（研究じゃなくて）勉強なさるのは適切ですね。でも数学原論は形式主義に忠実であろうとするために意味解釈を徹底的に排除していて、もうヘンタイの域に入ってます。たしかに、数学やってますってだけでも多少ヘンタイの気があると言われたら抗弁は難しいわけですが、しかしこれは極端でしょう。たとえば「構成列」だの「第一種の記号列」だのと言っちゃうし、背理法はいちいち理論を丸ごと差し替えるシカケとみなすんですから、分かりにくいんじゃないでしょうか。いやむしろ、分かってる人にしか読めんものじゃないか、つまり無味乾燥な記述を「あー、あのことね」と先回りして解釈し（つまり読み替え）ながらなら読める、そういうものだという気がします。あんまり極端に走ることなしに、しかしイーカゲンには陥らず、また抽象性だけを追い求めるのでもなく論理から始めてZF公理系をきちんと押さえた上で、となると、例えば島内剛一の数学の基礎とかどうでしょう。位相空間論のような具体的な理論を組み立てるために必須のごく基礎的な概念を構成する形式的方法とその意味をバランスを取って学ぶのが狙いでしょうし。 次に、ANo.1へのコメントについてです。 どうも、大変な作業をして戴いて申し訳なかったですね。鎖の記法はハッキリ見覚えがあります。「うわーめんどくせえ」というのが印象でしたが、これはτの後ろに文字を添えることで不要になるのでした。 形式主義で意味を論じるのはモチロン反則。ですが、意味を考えるとスジが分かり易くなるんで、こっそりやる分には良い手です。ってか、ホンネを言えば「あー、あのことね」抜きじゃやってられません。ただし、ヘタな意味づけ・読み替えをしてしまったためにウッカリ間違えるということが非常にしばしば生じますから、相当慎重にやらねばなりません。いや、ウッカリをしでかしてみて初めて、徹底して形式に拘わりどんなステップも絶対にすっ飛ばさない、というクソめんどくさい態度がいかに強力であるかを実感できるってもんです。（そういや、始祖のヒルベルト自身もウッカリ間違いをやらかしています。）そういう注意を念頭に置いた上で考えてみましょうよ。とは言っても長ーくなりそうなんで、これからボチボチ上げて行こうと思っています。当座のシュクダイとして、（「普通の数学」からの類推ではなしに、あくまでも形式主義に則って）S7からS8を本当に導き出せるものなのかどうか、もう一度検討なさってみてはと思います。
お礼
ありがとうございます。 ＞島内剛一の数学の基礎 こちらの本のほうが今の自分にはふさわしいようですね。近くの本屋さんで見かけたことがありますので一度中身をみて、よければ購入してみようと思います。
- stomachman
- ベストアンサー率57% (1014/1775)
回答ではない余計なお世話なんですけど、一体どうしてブルバキの数学原論をお読みになってるんでしょうか。 「ヒルベルト的形式主義によって数学を基礎付けることができる、というアイデアを、例を構成する事で実証して見せた」というのが、この膨大な著作の意義であり、つまり（中身がどうであれ）存在するという事自体にこそ意義がある。そして、数学基礎論を学ぶための教科書にはあんまり適していません。なぜなら、数学の体系をもっと的確・明快に整理した数学基礎論が沢山書かれていますから。 もし、数学ではなしに、証明論そのものを学ぶのが目的であれば、まず記号論理学のいくつかの流儀をマスターすることが先決。次に、計算理論（シューのプロダクションシステムや、チャーチのλ計算、形式言語とオートマトンの理論のような、）すなわち（意味を度外視して）形式を機械的に扱うことの理論、様相論理などの非古典論理学、高階述語論理、ゲーデルの超数学などを学ぶのが適切でしょう。 また、もし数学史の研究のため、あるいは数学原論に紛れ込んでいるミスを探すため、というのであれば、そういう作業は相当な素養を蓄えた上で取りかかるべきであって、ご質問のように、読解に難渋するというレベルでは歯が立たないでしょう。 いずれにせよ、数学原論は余り良いチョイスとは言えません。
補足
自分が数学原論を読んでいるのは数理論理学を学ぶためでは決してありません。 素朴集合論や位相空間論を学んでいる時に、帰納的に定義した集合が本当に集合と言えるのかがわからなかったことや選択公理を用いる証明に納得できなかったため、どういったものが集合といえるのかが知りたいと思ったからです。しかし数学基礎論や公理的集合論を研究したいとはまったく思いません（少なくとも今のところは）。 この本を選んだのは、基礎論に深入りせず、効率よく自分の知りたいことが学べると思ったからです。数学原論のようにロジックの部分から厳密に数学を展開しており、なおかつ基礎論のに深入りしていない本は調べたところほかに見つけれませんでした。ほかにそのような本があればいいのですが…。
- stomachman
- ベストアンサー率57% (1014/1775)
> ブルバキ数学原論 集合論１ をお持ちの方に質問 あたしゃ持ってませんから回答の資格がない。持ってる人がどれだけ居るんだろ。 ところで、系Tには、シェーマS1～S7以外にもいくつか規則（=の反射律、(P⇔Q)⇒(P⇒Q)、τの除去規則などなど）があるのではないかと思うんですが。いや、そう考えないと、Tはパワー弱過ぎじゃないかと。 シェーマとしてではなく、述語論理の一部として、あるいは記法の定義として組み込まれているのかもしれません。それらも一緒に列挙なされば、本を持ってない人でも回答できるんじゃないでしょうか。ま、使える手駒を全部並べてみる、というのは、エキゾチックな（普通の数学の公理系とは違う）系における証明を考える際に、まずやるべきことでしょうし。（あと、S5はミスプリ？） ところで「数学原論」の証明においては、もちろん、記号の列を機械的に操作する以外の推論は一切ダメですよね。（なにしろ、それこそが「数学原論」の主張するところのキモなんですから。）なのでたとえば、 > これに加えて質問ですが、 の部分でお書きの「定数だから」「変数だから」というような意味解釈(モデル)に基づく議論だとか、フツーの数学からの類推は反則です。 すると、三段論法とS1～S7だけでは"∀"をくっつける手段がありませんから、「（∀ｘ）（Ｒ⇔Ｓ）」が作れない。もし系Tにたとえば、【ＲおよびＳがＴの関係式であり、ｘが文字ならば、（Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）】というシェーマがあるとか、あるいはこれと同等の「∀の付加規則」がTを記述する述語論理の推論規則として存在しているとかすれば、「（Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）」は自明になるわけですが。 ＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊ 以下では、「質問において、Tに関する諸条件の記載はカンペキであって、何も抜けがない」と仮定したらどうなるか、簡単な超数学をやってみます。 Tにおける証明は、 http://okwave.jp/qa/q8256668.html のANo.3への補足にお書きになった、 > a1)RはＦの明示的公理である > a2)Ｒは補助的な構成手続き中に現れる対象式または関係式に対しＦのあるシェーマを適用して得られる： > b)その列の中でＲより前に二つの関係式Ｓ、Ｔがあり、ＴがＳ→Ｒである。 という規則だけを使って行われる。（"Ｓ→Ｒ"というのは、"Ｓ⇒Ｒ"の間違いじゃないでしょうか。）ただし、このご質問での記号の使い方に合わせて、 (a1)RはTの明示的公理である (a2)Ｒは補助的な構成手続き中に現れる対象式または関係式に対しtのあるシェーマを適用して得られる (b)その列の中でＲより前に二つの関係式Ｓ、Qがあり、QがＳ⇒Ｒである と直しておきます。この3通りのどれかに該当するように関係式Rを並べて行って、証明、すなわち関係式の列を作るわけです。しかしTに明示的公理はないから、(a1)には出番がない。また、(a2)で使うシェーマは下記のS1～S7と、問題で追加されたもの(S8としましょう)だけである。すなわち A, B, C, R, SがＴの関係式、U, KがＴの対象式、x, zが文字のとき、以下は公理である： Ｓ１ （Ａ∨Ａ）⇒Ａ Ｓ２ Ａ⇒（Ａ∨Ｂ） Ｓ３ （Ａ∨Ｂ）⇒（Ｂ∨Ａ） Ｓ４ （Ａ⇒Ｂ）⇒（（Ｃ∨Ａ）⇒（Ｃ∨Ｂ）） Ｓ５ （Ｔ｜ｘ）Ｒ⇒（∃ｘ）Ｒ Ｓ６ （Ｕ＝Ｋ）⇒（（Ｕ｜ｘ）Ｒ⇔（Ｋ｜ｘ）Ｒ） Ｓ７ （（∀ｘ）（Ｒ⇔Ｓ））⇒（τｘ（Ｒ）＝τｘ（Ｓ）） Ｓ８ （Ｒ⇔Ｓ）⇒（τz（Ｒ）＝τz（Ｓ）） （Ｓ５は（Ｕ｜ｘ）Ｒ⇒（∃ｘ）Ｒとかの間違いでは？） 以上から、証明である関係式の列（以下「列」とします）の末尾に追加できるのは、 (a2) S1～S8のA, B, C, R, S、U, K、x, zに具体的な関係式、対象式、文字を割り当ててできる関係式 (b) S⇒RとSが既に列中に存在しているときに、R （つまり三段論法） のどっちかである。 一方、証明の基本的な性質として （★）「(x = y)を証明する」ということは、「列の最後が(x = y)であり、しかも列の最後よりも前には(x = y)がないような有限長の列」を作る、ということ。 であるのを確認しておきます。 さて、関係式(x = y)には"⇒"が含まれていない。けれども、S1～S8はどれも"⇒"を含む。だから、列の最後にある(x = y)は(a2)によって作られたのではない、と直ちに分かります。となると、列の最後に並べた(x = y)は、(b)の三段論法で作ったのである。 S1～S8はどれも⇒で結ばれた二つの関係式で出来ている（【S⇒R】の形である）ので、それらのうちどれかのシェーマにおいて、⇒の右側にある関係式が(x = y)の形になったのが、三段論法の【S⇒R】のRの部分である。 ところが明らかに、S2, S3, S4, S5, S6の⇒の右側は、A,B,C,R,S,T,U,x,zにどんな風に関係式、対象式、文字を割り当てても "(x=y)"にならない。だから、(x = y)を作るのに使われた(b)の[S⇒R]の関係式とは、 (1) Ｓ１ （Ａ∨Ａ）⇒Ａ において Aを(x=y)にしたもの (2) Ｓ７ （（∀ｘ）（Ｒ⇔Ｓ））⇒（τｘ（Ｒ）＝τｘ（Ｓ））において τｘ（Ｒ）をx, τｘ（Ｓ）をyにしたもの (3) Ｓ８ （Ｒ⇔Ｓ）⇒（τz（Ｒ）＝τz（Ｓ））において τｘ（Ｒ）をx, τｘ（Ｓ）をyにしたもの のどれかでなくてはならない。 もし(1)によって(x=y)が作られたのだとすると、すなわち ((x=y)∨(x=y)) と ((x=y)∨(x=y))⇒(x=y) が列中に存在するはずです。 ここで、((x=y)∨(x=y))は"⇒"を含まないからやはり(b)によって作るしかなく、その手段となった(b)の[S⇒R]の関係式とは (1-1) Ｓ２ Ａ⇒（Ａ∨Ｂ）において、AとBを共に(x=y)にしたもの (1-2) Ｓ３ （Ａ∨Ｂ）⇒（Ｂ∨Ａ）において、AとBを共に(x=y)にしたもの のどちらか以外にはありえない。しかし、(1-2)は⇒の左右が同一だから、((x=y)∨(x=y))が既に列中にあるときにしか((x=y)∨(x=y))を作り出せない。なので、((x=y)∨(x=y))は(1-1)によって作られたのである。 ところが、(1-1)から(b)によって((x=y)∨(x=y))を作るには、Aすなわち(x=y)が列の最後よりも前に存在していなくてはならない。これは（★）と矛盾。なので、列の最後の(x=y)は(1)によって導かれたのではない。 一方、(2)か(3)の場合、 τｘ（Ｒ）をxで置き換えるためには記号"τ"を除去する必要がある。それには Ｓ６ （Ｕ＝Ｋ）⇒（（Ｕ｜ｘ）Ｒ⇔（Ｋ｜ｘ）Ｒ） による以外にはない。しかも、Rがxを含まない関係式であるとき、その時に限って、⇒の左側である（Ｕ＝Ｋ）の部分に"τ"があっても、右側には"τ"がないようにできる。ところが、こうして得られる"τ"を含まない関係式は Ｒ⇔Ｒ の形に限られる。つまり、S6では(x=y)は得られない。だから、列の最後の(x=y)は(2)や(3)を使って作られたのではない。 以上から、お書きの条件では、最後が(x=y)で終わる列（証明）を作るのは不可能であると分かります。 ＊＊＊＊＊＊＊＊＊＊＊＊＊＊ そういうわけで、なんか抜けてるんじゃないかなと。
お礼
補足欄では足りませんでしたのでお礼のところに続きを書かせていただきます。 C18:Ａ⇔Ｂ、Ｂ⇔ＣがＴの定理ならばＡ⇔ＣはＴの定理 C19:Ａ⇔ＢがＴの定理とする。しからば以下の関係式はすべてＴの定理 1)(￢Ａ)⇔(￢Ｂ) 2)(Ａ⇒Ｘ)⇔(Ｂ⇒Ｃ) 3)(Ｃ⇒Ａ)⇔(Ｃ⇒Ｂ) 4)(Ａ∧Ｃ)⇔(Ｂ∧Ｃ) 5)(Ａ∨Ｃ)⇔(Ｂ∨Ｃ) C20:以下の関係式はすべてＴの定理 1)(￢￢Ａ)⇔Ａ 2)(Ａ⇒Ｂ)⇔((￢Ｂ)⇒(￢Ａ)) 3)(Ａ∧Ａ)⇔Ａ 4)(Ａ∧Ｂ)⇔(Ｂ∧Ａ) 5)(Ａ∧(Ｂ∧Ｃ))⇔((Ａ∧Ｂ)∧Ｃ) 6)(Ａ∨Ｂ)⇔￢((￢Ａ)∧(￢Ｂ)) 7)(Ａ∨(Ｂ∨Ｃ))⇔((Ａ∨Ｂ)∨Ｃ) 8)(Ａ∧(Ｂ∨Ｃ))⇔((Ａ∧Ｂ)∨(Ａ∧Ｃ)) 9)(Ａ∨(Ｂ∧Ｃ))⇔((Ａ∨Ｂ)∧(Ａ∨Ｃ)) 10)(Ａ∧(￢Ｂ))⇔￢(Ａ⇒Ｂ) 11)(Ａ∨Ｂ)⇔((￢Ａ)⇒Ｂ) C21:AがＴの定理であれば、Ｔの任意の関係式Ｂに対して(Ａ∧Ｂ)⇔ＢはＴの定理 C22:￢AがＴの定理であれば、Ｔの任意の関係式Ｂに対して(Ａ∨Ｂ)⇔ＢはＴの定理 C23:ＡがＴの定理、文字ｘがＴの定数でなければ、(∀x)ＡはＴの定理 C24:ｘをＴの文字、ＵをＴの対象式とする。以下の関係式はすべてＴの定理 1)(∀x)Ａ⇔(τx(￢Ａ)|x)Ａ 2)￢(∀x)Ａ⇔(∃x)(￢Ａ) 3)￢(∃x)Ａ⇔(∀x)(￢Ａ) 4)(∀x)Ａ⇒(Ｕ|x)Ａ C25:Ａ⇒ＢがＴの定理ならば、(∀x)Ａ⇒(∀x)Ｂおよび(∃x)Ａ⇒(∃x)ＢはＴの定理。 C26:Ａ⇔ＢがＴの定理ならば、(∀x)Ａ⇔(∀x)Ｂおよび(∃x)Ａ⇔(∃x)ＢはＴの定理。 C27:ｘを文字とする。(∀x)(Ａ∧Ｂ)⇔((∀x)Ａ∧(∀x)Ｂ)はＴの定理 C28:ｘを文字とする。(∃x)(Ａ∨Ｂ)⇔((∃x)Ａ∨(∃x)Ｂ)はＴの定理 C29:ｘをＡの中に現れない文字とする。関係式(∀x)(Ａ∨Ｂ)⇔(Ａ∨(∀x)B)は定理 C30:ｘをＡの中に現れない文字とする。関係式(∃x)(Ａ∧Ｂ)⇔(Ａ∧(∃x)B)は定理 C31:ｘとｙを文字とする。以下の関係式は定理 1)(∀x(∀y)Ａ⇔(∀y)(∀x)Ａ 2)(∃x)(∃y)Ａ⇔(∃y)(∃x)Ａ 3)(∃x(∀y)Ａ⇒(∀y)(∃x)Ａ C32:xとｙとｚを文字、Ｕ、Ｋ、Ｖを対象式とする。Ｔは定数を持たないとすると以下の関係式は定理 1)ｘ＝ｘ 2)(ｘ＝ｙ)⇔(ｙ＝ｘ） 3)((ｘ＝ｙ)∧(ｙ＝ｚ))⇒(ｘ＝ｚ) 4)(Ｕ＝Ｋ)⇒((U|x)Ｖ＝(K|x)Ｖ)
補足
非常に丁寧な回答ありがとうございます。自分は独学で勉強しているもので、また論理学を勉強するのが初めてだったので。ブルバキのやり方が普通のやり方だと思い込んでいたため、説明を省いてしまいました。すみません。修正しておきます。 ＞Ｓ５は（Ｕ｜ｘ）Ｒ⇒（∃ｘ）Ｒとかの間違いでは？ そのとおりです。間違って入力してしまいました。 理論Tにおける記号 １ 論理記号：□、τ、∨、￢ ２ 文字（アルファベットやそれらにダッシュをつけたもので表す） ３ 特殊記号（集合論では＝と∈） 記号列とはＴの記号を一列に並べて書いたものであり、文字以外のある種の記号を２つずつ、その列の上を走る鎖と呼ばれる線で結ぶこともある。 ＿＿＿＿＿＿＿ | | | 例：τ∨￢∈□a'∈□a'' ｘを文字、Ａを記号列とする。τｘ(Ａ)という表現は次の方法で得られる記号列を意味する： 記号列τＡをつくり、次にＡの中に現れるｘの一つ一つをＡの左に書かれたτに鎖で結び付け、最後に、そのおのおのの場所においてｘをすべて□に置き換える。 ＿＿＿ | | 例：τx(∈xy)はτ(∈□y)を表している。 ＡとＢを記号列、ｘを文字とする。Ａの中にｘが現れるたびにそれを記号列Ｂに置き換えて得られる記号列を(B|x)Aとあらわす。 あらゆる特殊記号には、その重みと呼ばれるひとつの整数が対応している。 ある記号列がτで始まるか、または、一つの文字のみからなるとき、それを第一種、そうでなければ第二種と呼ぶ。 理論Ｔにおける構成手続きとは、次の性質を持つ記号列の列のことである：その列に属す各記号列Ａに対し、下記の条件の一つが成立する。 a)Ａは一つの文字である。 b)その列の中に、Ａより前に或る第二種の記号列Ｂがあり、Ａは￢Ｂである。 c)Ａより前に（必ずしも相異ならない）第二種の記号列ＢおよびＣがあり、Ａは∨ＢＣである。 d)Ａより前に或る第二種の記号列Ｂがあり、或る文字ｘにたいして、Ａはτｘ（Ｂ）である。 e)Ｔにおける重みｎの特殊記号ｓ、ならびにＡより前に或るｎ個の第一種の記号列Ａ1,Ａ2,…,Ａnがあって、ＡはｓＡ1Ａ2…Ａnである。 Ｔにおける構成手続き中に現れる第一種の記号列をＴの対象式、第二種の記号列をＴの関係式と呼ぶ。 簡単のため∨ＡＢの代わりに(Ａ)∨(Ｂ)とかいてもよいことにする。時には括弧は省略する。 Ａ、Ｂを記号列とする。 記号列(￢Ａ)∨ＢをＡ⇒Ｂと表す。 記号列￢((￢Ａ)∨(￢Ｂ))をＡ∧Ｂと表す。 記号列(Ａ⇒Ｂ)∧（Ｂ⇒Ａ）をＡ⇔Ｂと表す。 記号列(τx(A)|x)Ａを(∃x)Ａと表す。 記号列￢(∃x)(￢Ａ)を(∀x)Ａと表す。 理論Ｔの公理 １ Ｔにおけるいくつかの関係式を書く；これらをＴの明示的公理と呼ぶ；明示的公理の中に現れる文字 を定数という。 ２ Ｔのシェーマと呼ばれる規則は以下の性質を持つ：a)かかる規則の任意の一つを適用して得られる結 果はＴの関係式である。；ｂ）ＵがＴの対象式、ｘが文字、Ｒがあるシェーマの適用によって得られ るＴの関係式であれば、(U|x)Rはそのシェーマを直接適用することでも得られる シェーマの適用によって得られるすべての関係式をＴの非明示的公理と呼ぶ。 Tにおける証明とは (a1)ＲはＴの明示的公理である (a2)Ｒは補助的な構成手続き中に現れる対象式または関係式に対しＴのあるシェーマを適用して得られる (b)その列の中でＲより前に二つの関係式Ｓ、Ｑがあり、ＱがＳ⇒Ｒである Ｔにおける定理とはＴの証明の中に現れる関係式のことである。 これ以降は以下のシェーマを持つ理論のみを考える A, B, C, R, SがＴの関係式、U, KがＴの対象式、xが文字のとき、以下は公理である： S1 (Ａ∨Ａ)⇒Ａ S2 Ａ⇒(Ａ∨Ｂ) S3 (Ａ∨Ｂ)⇒(Ｂ∨Ａ) S4 (Ａ⇒Ｂ)⇒((Ｃ∨Ａ)⇒(Ｃ∨Ｂ)) S5 (U|x)Ｒ⇒(∃x)Ｒ S6 (U＝K)⇒((U|x)Ｒ⇔(K|x)Ｒ) S7 ((∀x)(Ｒ⇔Ｓ))⇒(τx(Ｒ)＝τx(Ｓ)) S8 (Ｒ⇔Ｓ)⇒(τx(Ｒ)＝τx(Ｓ)) 代入に関する超数学的な法則(証明は省く) CS1:Ａ,Ｂを記号列、ｘ,ｘ'を文字とする。ｘ'がＡの中に現れなければ、(B|x)Aは（B|x')(x'|x)Aと同じである。 CS2:Ａ,Ｂ,Ｃを記号列、ｘ,ｙを異なる文字とする。ｙがＢの中に現れなければ、（B|x)(C|y)Aは (C'|y)(B|x)Aと同じである；ただし、Ｃ'は記号列(B|x)C CS3:Ａを記号列、x,x'を文字とする。x'がAの中に現れなければ、τx(A)はτx'(A')と同じである；ただしA'は記号列(x'|x)A CS4:Ａ,Ｂを記号列、ｘ,ｙを異なる文字とする。ｘがＢの中に現れなければ、(B|y)τx(A)はτx(A')と同じである；ただし、A'は記号列(B|y)A CS5:Ａ,Ｂ,Ｃを記号列、ｘを文字、ｓを文字とする。記号列(C|x)(￢A),(C|x)(A∨B),(C|x)(A⇒B),(C|x)(sAB),(C|x)(A∧B),(C|x)(A⇔B)は それぞれ￢A',A'∨B',A'⇒B',sA'B',A'∧B',A'⇔B'と一致する；ただしA',B'はそれぞれ(C|x)A,(C|x)Bである。 CS6:Ｒを記号列、ｘ,ｘ'を文字とする。もしｘ'がＲの中に現れなければ、(∃x)Ｒおよび(∀x)Ｒはそれぞれ(∃x')Ｒ'および(∀x')Ｒ'と一致する ;ただしＲ'は(x'|x)Ｒであるとする。 CS7:ＲとＵを記号列、xとｙを相異なる文字とする。ｘがＵの中に現れなければ、(U|y)(∃x)Ｒおよび(U|y)(∀x)Ｒはそれぞれ(∃x)Ｒ'および (∀x)Ｒ'と一致する；ただしＲ'は(U|y)Ｒである。 構成に関する超数学的な法則(証明は省く) CF1:Ａ,ＢがＴの関係式、R1,R2,…RnがＴの対象式、xが文字、ｓが重みｎの特殊記号ならばＡ∨Ｂ、￢Ａ、ｓR1R2…Rn、Ａ∧Ｂ、Ａ⇔Ｂ、(∃x)Ｒ、 (∀x)ＲはＴにおける関係式、τx(A)はＴにおける対象式 CF2:A1,A2,…AnをＴにおける一つの構成手続きとし、xおよびyを文字とする。さらに、ｙはどのＡiの中にも現れないと仮定する。しからば、 (y|x)A1,(y|x)A2,…(y|x)AnはＴにおける一つの構成手続きである。 CF3:AがＴの関係式、ＵがＴの対象式、ｘとｙが文字ならば(y|x)AはＴの関係式、(y|x)UはＴの対象式 CF4:AがＴの関係式、ＢとＵがＴの対象式、ｘが文字ならば(U|x)AはＴの関係式、(U|x)BはＴの対象式 理論における代入 Ｔを一つの理論とし、A1,A2,…Anをその明示的公理全体、xを文字、ＵをＴの対象式とする。記号およびシェーマはＴと同じで、明示的公理が (U|x)A1,(U|x)A2,…(U|x)Anである理論を(U|x)Tと表す。 理論の比較 理論Ｔのすべての記号が理論Ｔ'の記号で、Ｔのすべての明示的公理がＴ'の定理であり、ＴのすべてのシェーマがＴ'のシェーマであるとき Ｔ'はＴより強いと言われる。ＴおよびＴ'のおのおのが他方より強いとき、ＴとＴ'は同値であるという。 推論に関する超数学的な法則(証明は省く) R1:ＡをＴの定理、ＵをＴの対象式、ｘを文字とする。しからば(U|x)Ａは(U|x)Ｔの定理。とくにｘが定数でないとき(U|x)AはＴの定理。 R2:Ｔ'がＴより強ければＴのすべての定理はＴ'の定理である。 R3:A1,A2…AnをＴの明示的公理全体、a1,a2,…,ahをその定数の全体、T1,T2…TｈをＴの対象式とする。(i=1,2…nに対し) (T1|a1)(T2|a2)…(Th|ah)Aiが或る理論Ｔ'の定理であり、Ｔの記号はすべてＴ'の記号、ＴのシェーマはすべてＴ'のシェーマであるとする。 しからば、ＡがＴの定理ならば、(T1|a1)(T2|a2)…(Th|ah)AはＴの定理である。 A,B,CをＴの関係式とする。しからば以下の法則が成り立つ C0:(三段論法)ＡとＡ⇒ＢがＴの定理のならば、ＢはＴの定理 C1:Ａ⇒ＢおよびＢ⇒ＣがＴの定理ならばＡ⇒ＣはＴの定理 C2:Ｂ⇒(Ａ∨Ｂ)はＴの定理 C3:Ａ⇒ＡはＴの定理 C4:ＢがＴの定理ならばＡ⇒ＢはＴの定理 C5:Ａ∨(￢Ａ)はＴの定理 C6:Ａ⇒(￢￢Ａ)はＴの定理 C7:(Ａ⇒Ｂ)⇒((￢Ｂ)⇒(￢Ａ))はＴの定理 C8:Ａ⇒ＢがＴの定理ならば(Ｂ⇒Ｃ)⇒(Ａ⇒Ｃ)はＴの定理 C9:(演繹定理)Ｔの公理にＡを追加して得られる理論をＴ'とする。ＢがＴ'の定理ならばＡ⇒ＢはＴの定理である。 C10:(帰謬法)Ｔの公理に￢Ａを追加して得られる理論をＴ'とする。Ｔ'が矛盾すればＡはＴの定理である。 C11:((￢Ｂ)⇒(￢Ａ))⇒(Ａ⇒Ｂ)はＴの定理 C12:(￢￢Ａ)⇒ＡはＴの定理 C13:(場合分け)Ａ∨Ｂ、Ａ⇒Ｃ、Ｂ⇒ＣがＴの定理ならばＣはＴの定理である。 C14:(補助定数)xが文字で定数でなく、Ｂの中に現れないで、(U|x)ＡがＴの定理となるＴの対象式が知られているとする。 Ａ⇒ＢがＴの定理ならばBはＴの定理。 C15:Ａ，ＢがＴの定理ならばＡ∧ＢはＴの定理 C16:(Ａ∧Ｂ)⇒Ａならびに(Ａ∧Ｂ)⇒ＢはＴの定理 C17:Ａ⇔ＢがＴの定理ならばＢ⇔ＡはＴの定理
お礼
今回非常に長い間お相手していただきありがとうございました。 今後もまた質問させていただくかもしれませんが、そのときはよろしくお願いします。