クロメル感想置き場 †
メッセージ †
誰もが一度は心に思い描く、しかし９割の人は実行しない（私もその中の一人です）数学の基礎からの組み立てですね。本物をみるのは初めてですよ。一度で読むには多すぎるので、少しずつ感想を書いていこうと思います。
まず自然数を考えて、足し算や引き算等の演算によって広がっていく世界の事かなと思ってみたら、なんと言語、文法からの構築なのですね。公理が最小限ですっきりとした印象をもちました。これから、これがどのように意味を持たせていくか楽しみです。
公理系の節に「数学の公理系も どの世界でも明らかに成り立つわけではないことに注意して下さい．」とありますが、「しかし、その世界においてはその公理は証明はできないが「正しいもの」 [*]_ なのです。」みたいな文章を追加できませんか？
以下に書く、註も付けてくださるとうれしいです。（間違っていないか不安ですが（＾＾；）現実世界で正しい推論には何か根拠ってありましたっけ？）
..[*] :ここで「正しい」という言葉を使いましたが、これはこれから体系M_0内で正しい論理と正しくない論理を判断したい時に正しい論理を表現するものです。我々はのちに体系M_0に現実の論理と対応させて意味を持たせたいのですが、現実では明らかに正しい論理がありますね。体系M_0が現実世界で正しい推論を正しいと判断することができるように、我々は慎重に公理を選ばねばなりません。もちろん、選ぶ公理や推論規則（これについては後述します）によっては現実世界では明らかに間違っている（と思われる）論理を正しいと判断してしまいます。
次に推論規則の節ですが、すこし話が分かりにくいなと思ったので、説明の文章をこうしたらいいのではないかという案を考えてみました。[]部分が私が変えたところです。
体系M_0において，理論を出発させる[証明できないが正しいものという]前提として前述の公理系 (命題論理の公理系) を導入しました．[しかしまだ体系M_0には、これら公理という前提(premise)から正しく推論(inference)して正しい論理式を作り出す方法（推論規則）がありません。][そして、その推論による結論となる論理式は]常に正しい事が担保されていなければ正しい推論[体系]とは言えませんね．そこで，体系M_0における命題論理の推論規則を導入します．
いままで書いたことはすべてあくまで私の認識に基づいた案ですので、間違っているかもしれません。変えるか、変えないか
、または別の変え方をするかはK.I.さんにお任せします。
Th0401 の証明のところで、（Ａ→Ａ）→（Ａ→Ｃ）のＣは、Ｂの間違いではないですか？
おもしろくなってきました。ところで、原子論理式とありますが、「原始」論理式の間違いではないですか？
どうでもいいことですが中盤に「その場合，証明の木の一番上にある論理式は全て公理に成増から，公理が恒真であり、」とありますが、「成増」ではなく「なります」ですね。
返答 †
- 早速お読み頂きまして有り難うございます。「まず自然数を考えて云々」は，数学のレシピ補遺で簡単な数論として組み立てる予定です。元々は，レシピに入れていたのですが，「形式的世界」と「現実世界」との区別が曖昧になってしまう事を恐れて，わざと外しました。そうですね，「補遺」も来週中にアップします。述語論理はもうちょっと待って下さい。 -- K.I.
- クロメルさん＞ 私には「現実では明らかに正しい論理がありますね」の意味が、よく分かりません。 -- Joh
- たとえば、三段論法ってありますよね。これは現実世界で明らかに正しいと言っていいと思っています。体系M_0が正しいと規定する論理式の集合は、公理や推論規則の選び方によってかわってくるものなので、三段論法が正しくないという体系もあるのだろうという認識の下書いたものです。 -- クロメル
- 気を悪くなさらないで下さいと先にお願いしておきますが，クロメルさんは恐らく誤解されていると思います (その原因は私の書き方がまずかったと真摯に受け止めています)。数学体系には「形式的世界」と「現実世界」があります。本レシピでは，最初に形式的世界の話をしています。形式的世界では，「正しい」「正しくない」という意味内容に拘わる判断はしません。そして，形式的世界では公理とは「何の仮定もなく証明可能な論理式」であると定義されます。「形式的世界」で「証明可能である」という性質と，「現実世界」で「真である (正しい)」という性質とは本来直接の関係はありません。ですから，公理を「証明出来ないが正しい」ものとは (少なくとも私は) 呼びたくありません。次に，「現実では明らかに正しい論理」についてですが，確かに，現実で，三段論法は正しいでしょう。でも，「現実で正しい論理は本当に正しいのか？」ということを問題にするのも数学基礎論の一つの目標であります。ですから，ここで，「現実では明らかに正しい論理」という表現の使用にはちょっと抵抗があります。なお，この「形式的世界」と「現実世界」との橋渡しになるのが解釈写像 (レシピ 06 の意味論で搭乗します) で，「形式的世界」の「証明可能性」と「現実世界」での「正しい」との関係を示すキーワードとして，健全性，無矛盾性，内容的完全性があります (レシピ 07 及び 08)。実は，数学の「形式的世界」と「現実世界」をきちんと区別している人はあまりいません。その二つの世界を区別せずに，「完全性定理」と「不完全性定理」とを理解 (?) している人が多いのですが，「完全性定理」は，「形式的世界での証明可能性と現実世界での正しいという意味」に関する定理で，「不完全性定理」は「形式的世界」の中での定理ですので，この二つの世界を区別せずにこの二つの定理を理解出来ないのではないかと私は信じています。長くなりましたが，今日の夕方頃には改訂すべき所は改訂するようにします。コメント有り難うございました。 -- K.I.
- KIさん、ありがとうございます。私の言いたかったことを、より適切な表現で書いていただけました。形式的数学の歴史は、「正しい」とか「正しくない」という直観的判断を排除し、論理の形式だけで体系を構築する努力であったと思います。（どんなにそれが無味乾燥であろうと！） エマニュエル・カントは、時間と空間の認識は先験的であると仮定しましたが、非ユークリッド幾何の登場によってその土台を崩され、本人も非常なショックを受けたことは有名な話です。数学基礎論をやる楽しみは、私たちの持つ「明らかな論理」を解体し、検証していくことであり（その過程で視野が広がる）、最初のうちは結果として得られるのも「明らかな論理」だけかも知れません。しかし、その過程が楽しいし、嬉しいのです。いきなり「現実世界」と対応させるのは、全く数学基礎論の趣旨に合わないと私は考えます。クロメルさんは、「明らかに正しい」とはどういうことか、「現実世界」というのが数学的に何を言っているのか（ユークリッド空間と実数のことでしょうか？）考えてみて下さい。 -- Joh
- 一つ質問したいのですが、公理は（仮定なしに？）証明可能なのですか？ -- クロメル
- 証明可能とはどういう意味ですか？ -- Joh
- K.I.さんの返事に、「形式的世界では公理とは「何の仮定もなく証明可能な論理式」であると定義されます。」とあったからです。 -- クロメル
- なるほど、形式的世界でも、無矛盾姓などでその体系を（現実世界と対応可能かどうかを）検証することができるのですか。でも形式的世界だけ考えるなら、矛盾していても、その体系は存在するということでしょうか？（ちょっと質問しすぎですね。以降、少し控えます。） -- クロメル
- なるほど。KIさんのその書き方だと、『証明可能』の部分が引っかかりますね。KIさんの返答を待ちましょう。無矛盾性というのは、（ヒルベルト以降の）公理的数学の体系で重要なキーワードです。そして、数学自体は無矛盾な体系であることが証明されていると思います。（ただし、数学的命題であっても数学で扱えないものが存在することも証明されています。）出発的として考える公理の無矛盾性、範疇性、独立性を考えれば、矛盾した体系になることはないように思いますが、私もきっちりとは分かっていません。 -- Joh
- まだ改訂していません。ごめんなさい。 返事だけ書いておきます。 ＜１＞ 証明可能の定義： レシピ (02) の下の方に書いてありますが， (論理式 P が) 証明可能であるとは，公理系及び推論規則だけを用いて論理式 P を結論する事ができる証明構造が存在することと定義されます。 ＜２＞ 形式的世界で矛盾した体系が存在するか： はい，存在します。矛盾した仮定の下では任意の論理式が証明できるという定理があります (レシピ (05) 参照)。この矛盾した仮定をすべて公理としてもつ体系を考えた時，それは形式的世界で矛盾した体系です。あと，クロメルさん，質問を控えずに，どんどん質問してください。そのための査読だと私は思っています。 ＜３＞ 公理はなんの仮定も無く証明可能であるか： はい。レシピ (02) で公理は全て証明可能である。と定義してあります。 定義だからというのが答えです。 -- K.I.
- K.I.さん、返答ありがとうございます。形式的世界では、真であるというかわりに、証明可能であると言うのですね。だんだん分かってきました(^_^)お言葉に甘えて、疑問は整理してから、質問させていただきます。改訂のペースなんかは、K.I.さんご自身のペースでいいと思いますよ。誰もせかしている人はいませんから。 -- クロメル
- Joh さん，「範疇性」とは何ですか？ ／ 「公理の独立性」，これはこれで大切な概念ですが，残念ながら本レシピでは考慮しておりません。 ／ クロメルさん，私も些細な事に拘泥しているようですが，「真であるというかわりに証明可能である」と言うわけではありません。形式的世界に，「真」という概念はありません。意味論で言う「真」のかわりに「証明可能」というかというとそうでもありません。が，殆どの場合は，「真」と「証明可能」とがイコールで結ばれているような状況を想像しがちですから，そのような誤解もあるのじゃないかなと私は思います。あと，レシピ (02) の改訂版をアップしておきました。 -- K.I.
- 一つの公理系を満たす二つ以上の体系があっても、これらが同型であるとき、この公理系を範疇的であると呼ぶと理解しています。独立性を重視していないというのは、独立でないことが分かった場合にはad hocに定理と呼べばいいということですか？ まぁ、それでもいいですが。 -- Joh
- Joh さん，範疇性のお答え，有り難うございます。ヒルベルトが公理系に要請したものの一つでしたか。 ／ 公理の独立性もヒルベルトは要請しましたが，これを考慮していないのは，公理が独立である事を証明せねばならないからです。そのような証明に私は取り組んだ事はありませんし，もし，独立でなかったとしても， Joh さんのおっしゃるように「定理」と呼べば良いと言う考えです。 -- K.I.
- 一日一個ずつ読んでいこうと思っていたのですが、予想以上に忙しく、読めていません。7/4以降また読み始めようと思います。 -- クロメル
- だいぶ時間が経ってしまいましたが、また査読を始めようと思います。 -- クロメル
|
執筆中/数学のレシピ (1) (K.I.著)/3
