浅谈公理系统的形式化（i）

    大家知道，世界上关于欧几里德几何学的第一套公理系统是1999年由德国大数学家希尔伯特用自然语言作出来的，很容易阅读与理解，受到广泛的赞誉与推荐。

希尔伯特公理系统如下：

第一组  接合公理

共八条，说明三组几何对象点、直线和平面之间的一种接合的关系。

第二组 顺序公理

共四条，说明直线上的点的相互关系。

第三组 合同公理

共五条，主要为处理图形的移动而引进的。

第四组 连续公理

共两条，说明直线的连续关系。

第五组 平行公理

只有一条，说明两直线间的平行关系。

到了二世纪六十年代，计算机应用普遍，而用计算机处理自然语言不方便，因此，形式语言兴起。用形式语言写公理系统行不行？具体到几何学，计算机懂不懂空间的位置与形状关系？机器人对周围环境能不能快速反应？对于机器人而言，分辨三角形与正方形不是一件简单的事情、

上世纪六十年代，美国数学家塔尔斯基用形式语言写了一套欧几里德促初等几何学的完全形式化公理系统，有点儿“匪夷所思”！

现在是二十一世纪了。时间快车的车轮不能倒转，我们也不能死死抱住三百年前的“老皇历”吃饭。

老实说，写一个完全形式化的公理系统并不困难，困难在于，如何使得这一套公理系统所推出的“数学理论”恰好就是欧几里德的初等几何学。

                     今天先下点儿“毛毛雨”，有点思想准备。

袁萌  3月6日

附：

Tarski's axioms, due to Alfred Tarski, are an axiom set for the substantial fragment of Euclidean geometry, called "elementary," that is formulable in first-order logic with identity, and requiring no set theory (Tarski 1959). Other modern axiomizations of Euclidean geometry are those by Hilbert and George Birkhof.