https://d1021.hatenadiary.com
http://d1021.hatenablog.com


 一般の科学では,「· · · になる」と「· · · である」は地続きでつながっています.例えば,ばねの伸びと荷重が正比例するというフックの法則は経験則です.しばしば「フックの法則に従う」と表現されるように「そのようになっている」に過ぎません.百回,千回,一万回と実験を重ねても常に「そのようになっている」のであれば,「そうである」と看做して,科学は前に進みます.しかし,数学ではこの二つを峻別します.証明という特殊な手続きを経た命題だけを定理と呼び,そのとき初めて「· · · である」という助動詞を与えるのです.
 証明という表現様式は今から 2500 年ほど前の古代ギリシャで誕生しました.ただ,証明は古代ギリシャから連綿と受け継がれてきたわけではなく,中世で一度実質的には失われた後,近代科学革命の中で再発見されたのです.さらに 20 世紀初頭にヒルベルト形式主義者は,与えられた公理系からいくつかの推論ルールだけを使って命題を導出するゲームとして数学を再定義しました.このことは当然ながら,「与えられた命題を機械的に証明する」という自動証明の種を胚胎することになるわけです.

→ は「ならば」を表わす論理記号です. x, y や ϵ, δ は「対象領域」である実数の上を自由に動き回る変数で, ∀xP(x) は「任意の(実数) x について,命題 P(x) が成り立つ」,∃xQ(x) は「Q(x) を満たすような(実数) x が存在する」と読みます.

17 世紀の数学者ライプニッツは「式が代わりに考えてくれる」という名言を残しました.未解決問題をいかに解くか以上に,数学の言語(記号・記法・文法)をいかに整えるかが数学の発展を左右する,ということをライプニッツは強く意識していたのです.

http://d.hatena.ne.jp/d1021/20170608#1496917939
http://d.hatena.ne.jp/d1021/20170607#1496831610
http://d.hatena.ne.jp/d1021/20170606#1496745343
http://d.hatena.ne.jp/d1021/20170604#1496573509
http://d.hatena.ne.jp/d1021/20170602#1496400397
http://d.hatena.ne.jp/d1021/20160222#1456137348