大学(専門)数学-参考書で証明が論理式・記号の羅列

質問

私は、大学数学科以上向けの数学のある参考書を探しておりまして、
　それは、定義・定理・証明が、殆ど、言葉でなく論理式・数学記号で書かれている物です。
　多くの数学の参考書において、著者は、数学的現象を、論理式・数式・記号で説明できる所を初学者の理解の為に(？)日本語でウダウダと説明している事がよくあります。例えば、関数が連続である事を使う証明等の時、”∃δ∈(a,b)(|x-c|<δ⇒ウンタラカンタラ)"と言えばいい物を、"xが十分cに近い時,ウンタラカンタラ と出来る"と日本語で言う といった事です。私はこういうのがイヤです。
　私は、数学理論・体系を日本語を通して理解するよりも、もっと、論理式・数式・記号等の羅列を通して理解したいのです。数理論理学のシーケントを用いた演繹みたいな感じで。。。

そういった参考書をご存知でしたら、本でもサイトでも構いませんので、是非ご教示ください。数学の分野なら何でも構いません。

　上記の私の探している参考書が、どういうものであるのかを知って頂く為に、下に、私の勉強ノートのコピーをアップロードしたサイトへのURLを示させて頂きます（2011年06月27日現在)：
　　　(1)http://www.megaupload.com/?d=73U56FA1
　　　(2)http://www.megaupload.com/?d=WSA8F5MA
それぞれのファイルに、次の証明に関する私の勉強ノートがあります。
(1);ツォルンの補題の証明。(「集合と位相」(斎藤毅 著))
(2);絶対収束級数は、任意に並び替えても同じ値に収束し、条件収束級数は、任意の実数に対し、ある並び替えによりその値に収束させれる、、という定理の証明。(「解析入門」(小平邦彦 著))
また、それぞれのファイルは、pdｆファイルとなっており、その中が私の勉強ノートの複写となっております。

長々となりましたがどうか宜しくお願い致します。

回答No.3

itukadarekato

>mizarをググりました。自動証明検証システムなんですね。

単に自動証明検証システムとは少し違います。

与えられた公理と推論規則から、一切の省略を許さず
より信頼できる形で数学を再構築しようという試みです。

証明を決まった言語で書き証明の検証に
コンピュータの圧倒的な処理能力を使います
Mizarはこのプルーフチェッカーを含むシステムと
これによって得られた数学データベースの総称でもあります

この新しい数学は通常の数学よりずっと厳密ですが手間もかかります
2005年に完成したJordanの曲線定理の証明は
日本とポーランドの数学者の共同研究で
14年20万ステップを必要としました

ツォルンの補題はZFCでは選択公理と同値だと思いますが
Mizarの公理系では定理になるそうです

補足

回答ありがとうございます。

>>与えられた公理と推論規則から、一切の省略を許さず
より信頼できる形で数学を再構築しようという試みです。

　これこそ正に”数学”たるものを感じ、私が興味を持つものです。
　しかし、私はまだそこまでのプロではありませんので、そこまでの細かさ(=ロボットが理解出来るまでの数学の論理式への還元)には、行けません。

　私は、数学の参考書によくある”～という事から、(議論を数ステップ飛ばし)明らかに…が成り立つ”や、”～と言う事は、今までの議論により、成り立つ”という表現が嫌いで、出来るだけ避けたいです(「明らか」と著者が言っているときには、著者が賢いから明らかといえるだけの場合が多いです)。
　<級数が条件収束するならば、任意の実数ｃに対し、ある数列の並び替えが存在し、その並び替えによる級数がｃに収束する>という定理の証明において、非常に多くの本(ほぼ全部？？)では、証明の概略だけ(！)であって、たとえ、元の級数から、cに収束する級数を作っても、それが並び替え(=自然数の集合間の可逆写像を合成させたもの)である事の証明は全くありません。”明らか”で済ませています。これが嫌なのです。
　数学の証明においては、’並び替え’や’選ぶ’という事に関する証明は、人間の直感では明らかであっても、そういった選択が本当に出来るか？などの点で詳しく証明しようとすると、とても複雑になりやすいですが、そこを出来るだけ”明らか”で済ましたくないです。

回答No.2

itukadarekato

http://mizar.uwb.edu.pl/version/current/html/

お礼

ご回答ありがとうございます。
私の探している参考書・サイトは、定義・定理・証明がプログラミング的に論理式・記号が羅列されてあるもの でありますので、ご提示してくださったサイトは興味深いです。
　英語表記でも頑張って理解したいのですが、私は英語が苦手で理解に苦しみます。
　このサイトは、どういうもので、何をどう扱っているのか？教えていただけますか？

補足

mizarをググりました。自動証明検証システムなんですね。
wikiでも調べましたが、まさに私が関心を抱いている分野です。
今後、mizarを少しずつ勉強したいと思います。

しかし、私が投稿した勉強ノートの(1)ツォルンの補題の証明　の様な感じで記述された参考書・サイトだった方がもっとうれしいんですが。こんな事やってる日本人は、いないのかなぁ。

回答No.1

ur2c

> 数学の分野なら何でも構いません。

一旦、意味がわかってしまった後では、私も記号の羅列の方が自然言語でくどくど書かれるより好きです。だから証明法は圏論の diagram chasing がカッコイイと思います。"Category theory" で検索すると、講義録や本がたくさん出て来ます。やさしいのから、めちゃムズいのまで、いろいろあります。