形式と意味①
私たちは数学を形式的に扱います。自然言語を使ったり意味に訴えることはしません。記述は機械に処理できることが必要十分です。
「\(x^2=1\) の解は \(x=\pm1\)」は \(\{x \mid x^2=1\}=\{1,-1\}\) としましょう。
意味を取ろうとするのは邪魔になることすらあります。
\(\log_{10}2=0.3\Longrightarrow0=1\)
はどう読めば良いでしょうか？
根源的な問にはしばしば沈黙します。例えば「集合とは何か」には答えません。Cantorを始め多くの人が頑張って説明しようとしてきましたが、「集合が満たすべき性質」があるだけ良いのです（公理的集合論の立場）。\(\sqrt2\) の定義は「\(2\) 乗して \(2\) になる正の数」で、初めのうちはよくわからないと感じるものでしょう。
形式と意味②
意味は形式の上のレベルで処理されねばなりません。自然言語では同時に出現させることができてしまいますが…
見る対象の切り替えを迅速に行うことができますか？
空は青いし青くない(黒い)。
自己言及のパラドクスを避けるにはどうしたら良いですか？
この文には1が□個ある。
私たちのシステムは内部に何層もの階層を持ち、例えばRusselのパラドクスも自然に表現できます。
数学の形式化
数学の形式化はHilbertによって始められました。彼は1920年頃には完成していた一階言語を使おうとしました。「数学のほぼ全領域は一階言語で表現できる」とあるように、彼の目標は「原理的には」達成されています。しかし、実際に数学を一階言語で表現しようとすると、すぐにうんざりする目に遭います。
形式化により冗長・雑多になるのを避け簡潔に済ます方法を模索することは、地味かもしれませんが創造的でやりがいがあります。「美しい記述を正当化する枠組み」を作ることが最初にやるべきことで、それがより大きな世界への扉を開くはずです。
数学の機械化
「一階言語のATP」も2010年頃には完成しています。proverを始めとして無料で使用できるATP softwareもあります。だから数学のATPも「原理的には」出来ていると言えます。四色問題の解決など一定の成果もあります。
しかし2020年頃の状況では、抽象数学において機械はほとんど役に立っていません。機械は、単純な計算では人間を凌駕しても、少し高度なことをやらさせると計算量が爆発してしまいます。
機械は意味を理解しないし人間の直観に当たるものを持ちませんが、正確・忠実に命令を聞いてくれます。その良い点を数学に生かすことはできるはずです。
\( \displaystyle\frac{D}{A\class{reflect}{B}C} \)
何卒ご協力を
