ブルバキ　等号を持つ述語論理について

Question

ブルバキ数学原論　集合論１　をお持ちの方に質問です。

Ｐ５５、演習§５、７）Ｔにおいてシェーマ（Ｒ⇔Ｓ）⇒（τz（Ｒ）＝τz（Ｓ））(Ｒ、Ｓは関係式、ｚは文字)が非明示的公理を与えていれば、ｘ＝ｙがＴの定理となることを示せ（ヒント：Ｒとして関係式ｘ＝ｘ、Ｓとして関係式ｘ＝ｙをとり、次に得られた公理の中でｙにｘを代入する）

この問題の証明をお願いします。

なお、Ｔは以下のシェーマを持ちます。
Ｓ１　ＡがＴの関係式ならば、関係式（Ａ∨Ａ）⇒ＡはＴの公理
Ｓ２　ＡとＢがＴの関係式ならば、関係式Ａ⇒（Ａ∨Ｂ）はＴの公理
Ｓ３　ＡとＢがＴの関係式ならば、関係式（Ａ∨Ｂ）⇒（Ｂ∨Ａ）はＴの公理
Ｓ４　Ａ、ＢおよびＣがＴの関係式ならば、関係式（Ａ⇒Ｂ）⇒（（Ｃ∨Ａ）⇒（Ｃ∨Ｂ））はＴの公理
Ｓ５　ＲがＴの関係式、ＵがＴの対象式、ｘが文字ならば、関係式（Ｔ｜ｘ）Ｒ⇒（∃ｘ）ＲはＴの公理
Ｓ６　ｘを文字、ＵおよびＫをＴの対象式、ＲをＴの関係式とする。
　　　関係式（Ｕ＝Ｋ）⇒（（Ｕ｜ｘ）Ｒ⇔（Ｋ｜ｘ）Ｒ）は公理
Ｓ７　ＲおよびＳがＴの関係式であり、ｘが文字ならば、
　　　関係式（（∀ｘ）（Ｒ⇔Ｓ））⇒（τｘ（Ｒ）＝τｘ（Ｓ））は公理

これに加えて質問ですが、Ｔがシェーマ（Ｒ⇔Ｓ）⇒（τz（Ｒ）＝τz（Ｓ））を持たない時にも、Ｔが明示的公理を持たない場合、ｘが文字、Ｒが関係式ならば、ｘは定数でないので（Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）は定理となり、Ｓ７より（Ｒ⇔Ｓ）⇒（τｘ（Ｒ）＝τｘ（Ｓ））は定理。
これから上の問題のようにｘ＝ｙが定理となるように思うのですが、ｘ≠ｙが定理となるｘ、ｙも存在すると思います。これでは矛盾が生じているように思うのですが、何がいけないのでしょうか？

stomachman · Accepted Answer

ANo.5へのコメントについてです。

> 意味を教えて下さったおかげで、∀ＡとＡの違いを理解することができ、とても勉強になりました。

ここまでの回答はあくまでも「ご質問とANo.1のコメントに書かれたことを辻褄の合うように解釈するとしたら、こうなる」という話に過ぎません。で、やってみたら、フツーの数学でいう∀xＡとＡとはだいぶ違っているらしい、ということになったのです。が、これがまぎれもなく正しい解釈なのかどうか、これだけの材料では確定できないように思います。…とか言ってる端から：

> 「（文字ｘがＴの定数でない限り）Ｔにおいて定理Ｒを述べること、定理（∀ｘ）Ｒを述べること、
> あるいは超数学的な規則：ＵがＴのいかなる対象式であっても、（Ｕ｜ｘ）ＲはＴの定理である、
> ということを述べることは、すべて同じことになる。」 > 「仮定（∀ｘ）Ｒを追加する。しからばＲは真」

ひえ～、なんという事でしょう！
　やっぱり最初にお書きの通り、数学原論をお持ちの方限定の質問だった訳ですな。（「よっぽど腰を据えないと」という直感も正しかったようで。）
　ここでポイントになるのは「定数」という用語に違いなく、これは「明示的公理に現れる文字」のことなのでした。「明示的公理」とは「非明示的公理」ではない公理（つまりシェーマに対象式や関係式を入れて作ったもの以外）ということかと思われます。が、気になるのが、シェーマSと超数学的な規則Cとが区別して分類されている、という点です。どっちも似たようなもんじゃないかと思う訳ですけど、わざわざ分けてある。（Tをいろいろ取り替えて比較するための便法なのかとも思いましたが、以下Tの話しかしない、みたいなことも書いてある。）すると、規則Cnから作り出したらそれは「明示的公理」なのか。いやそうじゃないのか。そこんとこがよく分かりません。
　こうなったら、数学原論を買うしかないか？

>数学科の人間ではありませんし、論理学などの授業があるわけでもないため、誰かに質問することができません。

stomachmanだって、教えてくれる先生なんかいませんでした。ネットで「誰かに質問することが」できるようになったんですから、文句言わないの！

>  論理学を独学で勉強するのに適した本を教えていただけないでしょうか。

「論理学」というタイトルの、ギリシャ哲学を解説した縦書きの本もあります。ですが、ここで仰る「論理学」は、普通の数学で使う一階述語論理のことでしょう。それは数学基礎論に当然含まれているし、既に使いこなしていらっしゃる。

> また、証明論、計算理論、様相論理、高階述語論理、ゲーデルの超数学、
> 将来学びたいと思ったときのために、どういう順番で学ぶべきか

順番はどうでもいいから、乱読することです。まずはいろんなのを軽く通して読んでみて、どういうような話なのかを掴む。それだけでも、他の分野との関連がいっぱい見えて来るでしょう。で、興味があれば突っ込む。
　素養はほとんど必要ありませんで、一応でも数学基礎論をやったなら文句無しです。むしろ、見慣れない概念を次々と消化していく訓練になると思います。（その点は数学原論に似ているけれども、数学原論だと消化した結果は先刻承知の数学でしかないのに対して、まるきり新しい観点が学べるのが利点です。）

計算理論は「コンピュータができること」の理論です。その中で「どんなコンピュータにも絶対できないこと」の存在が証明され、さらに「どんなコンピュータにも絶対できないこと」の中にも難しさの階層があることが示されます。また、チューリングマシンという模型からのアプローチ（神話に出てきそうなマシン）、λ計算という記号操作のアプローチ（代入ということを真髄まで極めたもの）、そして、帰納関数という算術からのアプローチ(いわば漸化式の極致。これは不完全性定理のゲーデルによる証明のための準備部分でもあります)が全部同じ結論に至る、という驚くべき結果が得られます。計算理論は実地のプログラミングと無関係ではありません。分かってなくてもプログラムは書けますけどね。（なお、「計算量の理論」は計算の効率を問題にしていて、計算理論とは別の話です。）
　ここで言う証明論は、ブルバキを読もうとなさる方には避けて通れない、形式主義のことです。記号を機械的に操作する、というわけで、計算理論と深く関わっています。しかしそれは、実際どういうものか、そもそもどういう思想・アイデアなのか、そして結局どうなったのか、ということだけ理解しておけば充分でしょうから、ヒルベルトの伝記を読むだけでも足りるかも。
　超数学は、数学の体系を対象として扱う数学であり、ゲーデルより以降では「ある公理系ならXが証明できるが、別の公理系では証明できない」というような、公理系同士の比較が主題になります。マニアックで、実践的な数学とはほぼ無関係であり、深入りはお勧めしません。が「選択公理が気に入らない」とか仰るんですから、興味がない筈はないだろうと。（バナッハ・タルスキーの定理を経済に応用したい！なんて方もいるぐらいですし。 http://oshiete.goo.ne.jp/qa/4779702.html ）
　論理というのは、元々「ヒトの物の考え方を抽象化・形式化したもの」でした。様相論理は「Xである」「Xでない」だけじゃなく、たとえば「Xは必然だ」「Xは偶然だ」だとか、「Xは義務だ」あるいは「Xだと信じる」のような命題も扱えるような体系です。当然、(ガンジガラメの数学ではない）日常の推論（奇妙なものもふくめ）と直接の関係があります。しかし、これを様相論理の内側から眺めていたのではピンと来ない。様相論理の体系を対象として扱う数学、という立場で考えると、随分分かり易くなりますし、いろんな様相論理の体系同士の比較が出来るようになります。ゲーデルが不完全性定理との関わりにおいて深く研究した分野です。レイモンド・スマリヤンは、このあたりに関わるユニークな本を沢山出しています。どれも親しみ易い簡単なパズルから始まっていて、記号はほとんど使われず、文章の見た目は最後まで易しそうである。ところが、きちんと理解しようとすると、ページを繰るごとにレベルが指数関数的に上昇しているのに気付きます。副読本と思えば、読んでみる価値はあります。
　高階述語論理は、述語を変数にする体系です。ですから、シェーマについて考えるには必要だろうと思うんです。イトモ簡単に矛盾が出てしまうやっかいな体系ですが、実地の応用もあります。どういうようなものなのかを知り、超数学との関わりをある程度感じられれば充分かと思います。

wwpqq · Answer

突然のおじゃま、失礼します。
高校数学も怪しいまま、60歳を越えてしまった者です。ブルバキの論理学のところだけでもと思い、眺めてますが・・・。
ワケも分からないのに書いてます。間違い多しです。適当に流して下さい。
τ記号は、Tと書いてます。τとロを繋ぐ線も表示できてません。


　
 


ブルバキ集合論１のP.55、§5の7)についてです。
内容的な意味は全く分かってないのに、ただ形式的に記号列を弄くってみただけのシロモノです。
竹下元首相の「言語明瞭、意味不明（瞭）」かー。言語も明瞭でないかー。

Rとしてx=x、Sとしてx=yを採用すると、((x=x)⇔(x=y))⇒(Tx(x=x)=Tx(x=y))となりますか。
この関係式は、シェーマ適用により得られた関係式なので定理。

この関係式の中のｙの箇所を全部ｘに代えて得られる関係式
(x|y)(((x=x)⇔(x=y))⇒(Tx(x=x)=Tx(x=y)))もC3.により定理。


CS5.により((x=x)⇔(x=x))⇒(Tx(x=x)=(x|y)Tx(x=y))と書き直した関係式も定理。
A⇔Aという形の関係式は、今問題にしてるS7.が登場して来る前に定理となることが示されてるから、この記号列の⇒以降、
Tx(x=x)=(x|y)Tx(x=y)が定理。

(x|y)Tx(x=y)を書き直そう。(x|y)Tx(=xy)、(x|y)(T=ロy)、(T=ロx)と書き直せる。
のでTx(x=x)=(T=ロx)が定理。


S5.により(x|y)(y=x)⇒(∃y)(y=x)は定理。
(x|y)(y=x)は書き直して(x=x)。x=xは、今問題にしてるS7.を使って、御本尊様、P.41で律儀に証明されて定理となってますが、
S7.をこの問題７）のように替えてしまっても、x=xは、御本尊様なぞって定理になることはsyoumei証明されます。


ので (∃y)(y=x)は定理。(∃y)(y=x)を書き直そう。
(Ty(y=x)|y)(y=x)、 Ty(y=x)=x、(T=ロx)=x、と書き直せる。
ので(T=ロx)=xは定理。でTx(x=x)=(T=ロx)が定理だったから、
Tx(x=x)=xが定理。


この証明では、今迄、全く「仮定」（ブルバキでは、追加された明示的公理と呼ばれてるか）はナシで進んでるので、
ｙは定数でない。
以前のC3.も使いましたが、ここでも同じく、C3.が使えて、(y|x)(Tx(x=x)=x)は定理。


(y|x)(Tx(x=x)=x)を書き直そう。(y|x)((T=ロロ)=x))、(T=ロロ)=yと書き直せる。
ので、(T=ロロ)=yが定理。
Tx(x=x)=xは定理は言えてる。Tx(x=x)=xは書き直して、(T=ロロ)=xなので、x=yが定理となってしまう。

　以上です。
　
又、「補助的な構成手続き」ですが、ブルバキでは、
C30.“Rを関係式、Tを対象式、xを文字とすると、(∀x)R⇒(T|x)Rは定理”というカンジになってます。

このC30.を証明の中で使う際には、R（例えば　=xx　）が関係式、T(　例えば{x|x∈Ａ} ）が対象式となってる、
を確認しておかないとC30.は使えないようになってる気がします。

その確認作業を「見せる」、「やってる」のが｢補助的な構成手続き」のような気がします。
証明は関係式記号列の列です。
ので、対象式そのまま、例えば文字xのみをポツンと証明(記号列の列）の中にそのまま書くことは、許されませんが、
「補助的な構成」手続きの中には書けると思います。のも、証明と「補助的な構成手続き」の違うところかと。

又、C27.は“Rが定理、xが定数でない「ならば」、(∀x)Rは定理”
と読めますが、この文中の「ならば」は超数学の「ならば」であって、数学の　「⇒」とは違うと思いますが。
ので、C27.のみでは、R⇒（∀x)Rは言えない気が・・・。

間違いが多いので、テキトーに読み流して下さい。
長々おじゃま、失礼致しました。

stomachman · Answer

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)であるから(∃x)(R∧S)である。つまり、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 · Answer

ご質問の

> これに加えて質問ですが、

の部分に関してです。

確かにフツーの数学では、変数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://oshiete.goo.ne.jp/qa/96470.html 。さらに、カリーのパラドックス: http://oshiete.goo.ne.jp/qa/4893333.html 。 集合論のラッセルのパラドックス: http://oshiete.goo.ne.jp/qa/3290945.html もよく似ています。様相論理の抜き打ちテストの話: http://oshiete.goo.ne.jp/qa/2346446.html だって、深いところで繋がっているように思います。

------------

かくて、Tに関する超数学とTそのもののとの区別を厳格に付けた上で、数学原論を再読しなくちゃなりません。

でも、差し当たり「(∀x)Pが定理であることと、裸のPが定理であることとは、違う意味を持っている」らしいと分かりましたよね。

（裸のPが定理であるというのは、何も「文字をひとつも含まない関係式Pが定理である」ということを意味しているのではありません。たとえば、Pが(∃y)(ナンタラカンタラ)で、(∀x)Pは(∀x)(∃y)(ナンタラカンタラ)であるとか。丁度「(∀x)Pの(∀x)を脱がせたんだけど、その下にまだパンツ穿いてたんだヨ…」 というような。)

次に、τについて考察してみようと思います。(予定)

stomachman · Answer

まずANo.2へのコメントについてです。余計なお世話に応答して下さってありがとうございます。

> 選択公理を用いる証明に納得できなかったため、
> どういったものが集合といえるのかが知りたい

ということでしたか。それならなるほど、公理的集合論の基本を（研究じゃなくて）勉強なさるのは適切ですね。でも数学原論は形式主義に忠実であろうとするために意味解釈を徹底的に排除していて、もうヘンタイの域に入ってます。たしかに、数学やってますってだけでも多少ヘンタイの気があると言われたら抗弁は難しいわけですが、しかしこれは極端でしょう。たとえば「構成列」だの「第一種の記号列」だのと言っちゃうし、背理法はいちいち理論を丸ごと差し替えるシカケとみなすんですから、分かりにくいんじゃないでしょうか。いやむしろ、分かってる人にしか読めんものじゃないか、つまり無味乾燥な記述を「あー、あのことね」と先回りして解釈し（つまり読み替え）ながらなら読める、そういうものだという気がします。あんまり極端に走ることなしに、しかしイーカゲンには陥らず、また抽象性だけを追い求めるのでもなく論理から始めてZF公理系をきちんと押さえた上で、となると、例えば島内剛一の数学の基礎とかどうでしょう。位相空間論のような具体的な理論を組み立てるために必須のごく基礎的な概念を構成する形式的方法とその意味をバランスを取って学ぶのが狙いでしょうし。

次に、ANo.1へのコメントについてです。
　どうも、大変な作業をして戴いて申し訳なかったですね。鎖の記法はハッキリ見覚えがあります。「うわーめんどくせえ」というのが印象でしたが、これはτの後ろに文字を添えることで不要になるのでした。
　形式主義で意味を論じるのはモチロン反則。ですが、意味を考えるとスジが分かり易くなるんで、こっそりやる分には良い手です。ってか、ホンネを言えば「あー、あのことね」抜きじゃやってられません。ただし、ヘタな意味づけ・読み替えをしてしまったためにウッカリ間違えるということが非常にしばしば生じますから、相当慎重にやらねばなりません。いや、ウッカリをしでかしてみて初めて、徹底して形式に拘わりどんなステップも絶対にすっ飛ばさない、というクソめんどくさい態度がいかに強力であるかを実感できるってもんです。（そういや、始祖のヒルベルト自身もウッカリ間違いをやらかしています。）そういう注意を念頭に置いた上で考えてみましょうよ。とは言っても長ーくなりそうなんで、これからボチボチ上げて行こうと思っています。当座のシュクダイとして、（「普通の数学」からの類推ではなしに、あくまでも形式主義に則って）S7からS8を本当に導き出せるものなのかどうか、もう一度検討なさってみてはと思います。

stomachman · Answer

回答ではない余計なお世話なんですけど、一体どうしてブルバキの数学原論をお読みになってるんでしょうか。

「ヒルベルト的形式主義によって数学を基礎付けることができる、というアイデアを、例を構成する事で実証して見せた」というのが、この膨大な著作の意義であり、つまり（中身がどうであれ）存在するという事自体にこそ意義がある。そして、数学基礎論を学ぶための教科書にはあんまり適していません。なぜなら、数学の体系をもっと的確・明快に整理した数学基礎論が沢山書かれていますから。
　もし、数学ではなしに、証明論そのものを学ぶのが目的であれば、まず記号論理学のいくつかの流儀をマスターすることが先決。次に、計算理論（シューのプロダクションシステムや、チャーチのλ計算、形式言語とオートマトンの理論のような、）すなわち（意味を度外視して）形式を機械的に扱うことの理論、様相論理などの非古典論理学、高階述語論理、ゲーデルの超数学などを学ぶのが適切でしょう。
　また、もし数学史の研究のため、あるいは数学原論に紛れ込んでいるミスを探すため、というのであれば、そういう作業は相当な素養を蓄えた上で取りかかるべきであって、ご質問のように、読解に難渋するというレベルでは歯が立たないでしょう。
　いずれにせよ、数学原論は余り良いチョイスとは言えません。

stomachman · Answer

> ブルバキ数学原論　集合論１　をお持ちの方に質問

あたしゃ持ってませんから回答の資格がない。持ってる人がどれだけ居るんだろ。
　ところで、系Tには、シェーマS1～S7以外にもいくつか規則（=の反射律、(P⇔Q)⇒(P⇒Q)、τの除去規則などなど）があるのではないかと思うんですが。いや、そう考えないと、Tはパワー弱過ぎじゃないかと。
　シェーマとしてではなく、述語論理の一部として、あるいは記法の定義として組み込まれているのかもしれません。それらも一緒に列挙なされば、本を持ってない人でも回答できるんじゃないでしょうか。ま、使える手駒を全部並べてみる、というのは、エキゾチックな（普通の数学の公理系とは違う）系における証明を考える際に、まずやるべきことでしょうし。（あと、S5はミスプリ？）
　
　ところで「数学原論」の証明においては、もちろん、記号の列を機械的に操作する以外の推論は一切ダメですよね。（なにしろ、それこそが「数学原論」の主張するところのキモなんですから。）なのでたとえば、

> これに加えて質問ですが、

の部分でお書きの「定数だから」「変数だから」というような意味解釈(モデル)に基づく議論だとか、フツーの数学からの類推は反則です。
　すると、三段論法とS1～S7だけでは"∀"をくっつける手段がありませんから、「（∀ｘ）（Ｒ⇔Ｓ）」が作れない。もし系Tにたとえば、【ＲおよびＳがＴの関係式であり、ｘが文字ならば、（Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）】というシェーマがあるとか、あるいはこれと同等の「∀の付加規則」がTを記述する述語論理の推論規則として存在しているとかすれば、「（Ｒ⇔Ｓ）⇒（∀ｘ）（Ｒ⇔Ｓ）」は自明になるわけですが。

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊

以下では、「質問において、Tに関する諸条件の記載はカンペキであって、何も抜けがない」と仮定したらどうなるか、簡単な超数学をやってみます。

Tにおける証明は、 http://oshiete.goo.ne.jp/qa/8256668.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)で終わる列（証明）を作るのは不可能であると分かります。

＊＊＊＊＊＊＊＊＊＊＊＊＊＊
そういうわけで、なんか抜けてるんじゃないかなと。

ブルバキ 等号を持つ述語論理について

ANo.5へのコメントについてです。

突然のおじゃま、失礼します。

ANo.4へのコメント：

ご質問の

まずANo.2へのコメントについてです。

回答ではない余計なお世話なんですけど、一体どうしてブルバキの数学原論をお読みになってるんでしょうか。

この回答への補足

> ブルバキ数学原論 集合論１ をお持ちの方に質問

この回答への補足

似たような質問が見つかりました

関連するカテゴリからQ&Aを探す

デイリーランキングこのカテゴリの人気デイリーQ&Aランキング

マンスリーランキングこのカテゴリの人気マンスリーQ&Aランキング

ブルバキ　等号を持つ述語論理について

　ご質問の

　回答ではない余計なお世話なんですけど、一体どうしてブルバキの数学原論をお読みになってるんでしょうか。

> ブルバキ数学原論　集合論１　をお持ちの方に質問