私が趣味で研究している形式化数学について書いていこうと思います。研究の進捗に伴い改稿される予定です。脱稿するのは数十年後の予定です。
履歴
2015/11/03 初版
形式化数学とは
形式化数学（formalized mathematics）とは、一言で言えば、形式化された数学のことです。そのため、形式化数学とは何かということを説明するためには、形式化（formalization）とは何かということと、数学（mathematics）とは何かということを説明しなければなりません。
数学とは
数学とは何かということを説明するのは非常に難しい問題です。なので、潔く、ここでは説明を諦めることにします。ちなみに、数学とは何かという問題は数学の哲学（philosophy of mathematics）の問題の1つです。数学とは何かということについての哲学的な議論が知りたい場合には、数学の哲学の文献を参照しましょう。
一言メモ
数学の哲学の文献としては「New Directions in the Philosophy of Mathematics」（Tymoczko, 1986）、「Thinking about Mathematics: The Philosophy of Mathematics」（Shapiro, 2000）、「Philosophy of Mathematics」（Horsten, 2008）などがあります。
しかし、これだけではあまりに投げやりなので、数学の幾つかの分野を列挙しておきましょう。数学の分野としては、代数学、幾何学、解析学、数理論理学などがあります。時としてこれらの分野の垣根は曖昧であったりしますが、数学とは何かということを哲学的な議論にまで踏み入らないで考えるに際しては、これらの分野で行われている実際の研究こそが数学の一部であるという漠然とした感覚で捉えるしかないでしょう。そして、そのような研究で取り扱われているモノ（数学的物件（mathematical object））が、そのようなモノの取り扱い（数学的理論（mathematical theory））を含めて、数学の内容（content of mathemetics）を構成しています。そして、数学の内容を理解したり、論考したり、はたまた発見したりすることが数学の実践です。
もう少し数学について書きましょう。当たり前過ぎますが、数学を実践する際には何らかの言語を使用します。数学の内容を理解しようとする際には、数学の教科書を読むかもしれません。数学の教科書は何らかの言語で書かれています。数学の内容を論考する際にも、何らかの言語を使用して思索し、場合によっては思索の結果を何らかの言語を使用して通常は明瞭な形で記述することになります。数学の内容を発見した際にも、その内容は何らかの言語で通常は明瞭な形で記述されることになるでしょう。このような言語の目的は数学の内容の表現や記録や伝達です。それは数学というものに特化しているという点を除けば、言語全般の目的とそう異なるものではありません。そして、このような数学の実践において使用される言語を特称して数学言語（language of mathematics）と言います。数学言語は唯1つという訳ではありません。それは日本語で書かれた数学の教科書もあれば英語で書かれた数学の教科書もあることから明らかでしょう。
形式化とは
形式化とは、形式的にすることです。
それでは、形式的（formal）とはどのような状態でしょうか。形式的という言葉には幾つかの意味がありますが、数学における形式的は、非形式的（informal）と対を成す言葉です（他に、法学などで使われる、実質的と対を成す言葉としての形式的などがありますが、これは数学における形式的とは意味が異なります）。そして、形式的とか、非形式的というのは、論考の対象あるいは論考そのものがどのような形で表現されているかを表現する言葉です。
核心に入る前に根本的な話をしましょう。当たり前過ぎますが、論考の対象を表現したり、実際に対象について論考したりするためには何らかの言語が必要です。一般的に、最もよく使われるのは日本語や英語などの自然言語ですが、しかしながら、このような自然言語には本質的に曖昧さが内包されているという大きな欠点があります。勿論、論考を成る丈明確にするために、曖昧さを軽減する工夫が為されることが多いですが、自然言語を使っている以上完全に曖昧さをなくすのは難しく、意図せず曖昧さが混入することを防ぐことができません。
完全に曖昧さをなくすためにはどうすれば良いでしょうか。1つの方法としては、論考に使用する言語自体を1から完全に明確な形で定義するということが考えられます。すなわち、その言語で使用される語彙（vocabulary）を完全に明確な形で余すところなく定義し、語彙から文（sentence）を作る方法、すなわち、文法（grammar）も完全に明確な形で余すところなく定義し、定義した語彙と文法から生成できる文により、完全に明確な形で論考を行うということです。
実はこれが正に形式的ということです。このような語彙と文法から成る言語を形式言語（formal language）と言い、このような論考を形式的論考（formal discourse）と言います。逆に、そうでないのが非形式的ということです。非形式言語（informal language）や非形式的論考（informal discourse）も同様です。
とは言え、形式言語さえ定義すれば言語から曖昧さがなくなるという単純なものではありません。形式言語であっても、依然として曖昧さのある言語を定義することは可能です。あくまでも定義の仕方によって曖昧さのない言語も定義できるということです。そのため、形式言語を定義する際には、敢えて曖昧さを含めるような場合を除いて、曖昧さが入り込まないように細心の注意を払わなければなりません。しかし、一度曖昧さのない形式言語を定義してしまえば、その言語をそのまま使用する限り、曖昧さが入り込む余地はありません。
また、形式言語の利点は曖昧さのない言語を定義できるということだけではありません。もう1つの大きな美点は、コンピュータの上で形式言語を定義することが可能であるということです（もっとも、非形式的なものを好む者から見れば、コンピュータなど所詮形式的なものしか処理できない融通の利かない代物でしかないという消極的な見方になるのかもしれませんが・・・）。コンピュータの上で形式言語を定義することによって、ある文が形式言語の文法に従っているかコンピュータで検証したり（証明検証（proof checking））、論考の一部をコンピュータに自動的に行わせたり（自動定理証明（automated thorem proving））、論考で得られた知識をコンピュータで管理したり（知識管理（knowledge management））と、様々な可能性が広がります。実のところ、18世紀末葉から19世紀初葉に数理論理学の創始に伴い形式言語という概念が見い出された原初の目的は偏に論考を明確にするというところにありましたが、19世紀中葉からは、計算機科学の興隆に伴い寧ろコンピュータでの利用という側面が益々大きくなってきています。
一方で、形式的な問題解決方法には概して費用が高いという欠点があります。実のところ、必ずしも人間は形式的な物事に秀でている訳ではありません。寧ろ、非形式言語を使用しても自然に、すなわち、特段費用を掛けることもなく、ある程度の厳密さを達成できるということこそが人間の秀でている点です。逆に、絶対的な厳密さが必要な場面では、形式的な問題解決方法が必要となってきます。結局のところ、形式的な方法にも非形式的な方法にもそれぞれ利点と欠点があり、適材適所が肝要だということです。
形式化数学とは
ここまでの説明で明らかかもしれませんが、形式化数学とは、数学言語として何らかの形式言語を使用して数学を実践することです。本項では数学言語として非形式言語を使用する従来の数学と形式言語を使用する形式化数学とを数学言語の観点から比較してみましょう。
まず、具体的な例として、日本語で書かれた数学の教科書を考えましょう。このような教科書は日本語で書かれています。それは日本語で書かれている教科書であるのだから当然なのですが、この日本語というものが曲者です。想像してみれば（あるいは、手許に数学の教科書があるのならば実際にその内容を観察してみれば）分かるかと思いますが、日本語で書かれた数学の教科書の日本語は、その実、通塗の日本人が日常的に使っている普通の日本語とは些か異なる様相を呈しています。
最も分かりやすいのは数学記号です。これは数学の教科書には頻出しますが、日常的な文書では極々初等的なものを除いて滅多に出てくることはありません。
つまり、数学を実践するために使われる日本語は普通の日本語とは明らかに異なるものです。そして、どのような点が異なるのかというと、次のような点が異なります。
- 数学用語（mathematical terminology）が使われる。
- 数学記号（mathematical symbol）が使われる。
- 数学記号を組み合わせて数式（mathematical formula）を構成するための文法が明示的又は黙示的に使われる（明示的又は黙示的な文法を使って数式が構成される）。
一言メモ
ちなみに、このような文法のことを特に記法（notation）と言います。記法に従っているという意味で正しい数式を正しい形式の数式（well-formed formula）と言い、逆に、従っていないという意味で正しくない数式を正しくない形式の数式（ill-formed formula）と言います。
つまり、数学を実践するために使われる日本語は普通の日本語に数学用語や数学記号や記法を添加したものだということです。普通の日本語を一般的な日本語と表現するならばこのような言語は特殊な日本語の1つです。この場合における普通の日本語を基盤言語（substrate language）と言います。数学の実践の場合には、基盤言語に数学の実践で必要となる言語的な要素を加えて拡張したものを数学言語として使用するということになります。
そのため、基盤言語には少なくとも拡張性が必要だということになります。他には、当然ながら、数学を実践するのが容易な言語である方が良いです。少なくとも数学の実践が妨げられないような言語であることが望ましいです。また、どのような基盤言語が適しているかは人や環境によることもあるかもしれません（たとえば、日本人であるならば、基盤言語もまた普通の日本語であった方が良いかもしれません）。
さて、話の方向性は少し変わりますが、先程説明したように言語は形式言語と非形式言語に両分され、結果として数学言語も形式的数学言語（formal language of mathematics）と非形式的数学言語（informal language of mathematics）に両分されます。形式的数学言語は記号数学言語（symbol language of mathematics）とも言い、非形式的数学言語は文章数学言語（textual language of mathematics）とも言います。また、記号数学言語を使用して実践される数学を記号数学（symbol mathematics）と言い、文章数学言語を使用して実践される数学を文章数学（textual mathematics）と言います。
一言メモ
記号数学及び文章数学という用語は「The Language of Mathematics（Ganesalingam, 2009）」を参考にしています。
形式的数学ではなく形式化数学である理由
形式化数学は何故形式的数学ではなく形式化数学と呼ばれるのでしょうか。
普通の数学は（少なくとも現時点では）非形式言語を使用して行われることが圧倒的に多く、形式言語を使用して行われることは非常に稀です。なかんずく、最先端の、正に研究の途上にあるような数学はほぼ全てが非形式言語を使用したものであると言って良いでしょう。
一言メモ
普通の数学が非形式言語を使用して行われることが多いという事実は、先述した、形式的な問題解決方法の費用の高さと関連しています。しかしながら、昨今、数学が益々高度化、複雑化していく中で、数学における重要な要請の1つである厳密さを確保することがいよいよ難しくなってきています。たとえば、有限単純群の分類に関する結果はその膨大さゆえ完全に正しいと言うことが難しいものとなっています。今後は数学においても形式的な方法が重要になってくるかもしれません。
そして、形式的数学言語というものは、一旦非形式的数学言語を使用して記述された数学の内容を、特にコンピュータの上で表現、記録、伝達などするに際して、使用されることの多いものです。そのような場合は、正に非形式的な数学を形式化するということであり、これが形式化数学と呼ばれる所以です。
実際のところ、形式化数学のことを形式的数学と呼ぶ人も多いのが実情です。断じて形式化数学と呼ばなければならないという謂れはありませんが、本稿では専ら形式化数学という用語を用いるものとします。
論理との関係
論理とは、論考を進める筋道のことです。ある論考の筋が通っている場合、その論考は論理的（logical）であると言い、そうでない場合、非論理的（illogical）であると言います。そして、論理体系（logical system）とは、筋の通った論考を進めるための枠組みのことです。
一言メモ
論理体系の上で論考を進めていくことを推論（inference）と言い、正しい推論を妥当な（valid）推論と言い、正しくない推論を妥当でない（invalid）推論と言います。
そのため、論考を行う際には何らかの論理体系が必要となります。
非形式言語の場合、通常は最初から言語の中に論理体系が埋め込まれており、非形式言語を使用して論考を行う場合には、言語に埋め込まれている論理体系をそのまま使用することが多いです。また、最初に非形式言語で何らかの論理体系を定義して、その論理体系を使用して論考を行うこともできます。
形式言語の場合、形式言語の一部として定義するか、形式言語の上で定義するかという違いはあれども、どこかの時点で必ず論考で使用するための論理体系を明確な形で定義しなければなりません。
一言メモ
形式的に定義されている論理体系を形式論理体系（formal logical system）と言い、そうでない論理体系を非形式論理体系（informal logical system）と言います。
数学に限った話をすると、数学を実践するには数学の基礎（foundation of mathematics）と言う、あらゆる数学的物件を表現し、それに対する論考を行うための数学的な基盤が必要となります。数学言語として形式言語を採用する場合には、数学の基礎は、その形式言語と、その形式言語に論理体系が含まれていない場合にはその形式言語で定義される何らかの論理体系と、あらゆる数学的物件を表現するための何らかの理論から構成されます。また、論考に複数の種類の論理体系が必要であるような場合には、最初に複数の論理体系を定義するための枠組みを定義し、その枠組みを使用して論考に使用する具体的な論理体系を定義することもあります。このような枠組みを論理の枠組み（logical framework）と言います。
一言メモ
論理の枠組みという用語は「Representing Logics and Logic Translations（Rabe, 2008）」を参考にしています。