1. 引言
Tarski在1948年的一篇经典著作 [1] 中,解决了闭实数域的判定问题,其主要目的之一,是给出初等几何的机械化证明。以后Seidenberg [2] ,Robinson [3] 与Cohen [4] 等人又给出了Tarski定理的不同证法。同时这些作者也给出了初等几何定理机械化证明的一些建议,但这些建议离真正的机械化证明甚远,最终由中国科学家吴文俊院士在1977年文献 [5] 中给出了一种初等几何定理机械化证明的一种设计方法——吴方法。吴方法主要是引进笛卡尔直角坐标系,即引进坐标,然后代数化,这里条件和结论都进行代数化,即用条件代数方程组去推出结论代数方程式,从而对命题判断真伪。这里条件代数方程组运用的是吴文俊消元法进行得出结论代数方程式,从而实现定理的机械化证明。2014年初周亚南在文献 [6] 中发明了一种新的消元法,从而试想用这种新的消元法对定理的机械化证明一个大的改进,使机械化证明不在单一化,而是多元化,不仅仅世上仅存吴方法。而周亚南在文献 [7] 的论述与一些猜想和问题更使我们认为定理的机械化证明可以用新的消元法来实现。当然,这里同样离不开笛卡尔直角坐标系,同样需要对线段的长度,以及垂直关系,平行关系,相等关系等进行代数化,这里由于在文献 [5] 中吴文俊院士已经给出,我们这里省略,需要者可以查阅文献 [5] 。还有是否能够用吴方法或者本文的消元技术对文献 [8] 进行数学的机械化证明,当然如果能够对文献 [8] 进行定理的机械化证明这将是科学的一大进步。最后,能否将本文的方法推广到数学的其他科目上面,比如微分几何定理的机械化证明,对于文献 [6] 中的消元技术能否应用到代数几何以及曲面造型等上面等,由于篇幅原因,本文作者仅给出一个例子,即勾股定理的机械化证明,希望读者群体敬请谅解。
2. 命题与一些必要的条件和结论
2.1. 命题
设△ABC,∠C为直角,AC、BC为直角边,AB为斜边,则下面的结论成立:
(1)结论
2.2. 条件
首先将直角三角形ABC放入笛卡尔直角直角坐标系中,这里有一个特殊要求三角形三个顶点不在笛卡尔直角直角坐标系的两坐标轴上面,那么引入坐标
,由坐标及文献 [5] 可以知道下面的代数式子成立:
(2)条件
(3)条件
(4)条件
(5)条件
对条件(2) (3) (4) (5)进行整理可以得到下面的条件式子
(2a)变形条件
(3a)变形条件
(4a)变形条件
(5a)变形条件
在这里为了得到变形条件,同时运用文献 [6] 中的消元法,我们保持其AB、AC、BC不变,对未知量
进行消元技术,这里我们给出下面的消元关系:
(6)
将(6)式代入(2a) (3a) (4a) (5a)并进行新的消元法得到下面的关系式
(7)
(8)
(9)
可知变形条件经过新消元法第一次消元后变成了(7) (8) (9)这样的方程式,同样联立(7) (8) (9)这样的方程式得到一个新的方程组,这个方程组再次进行新消元,其消元关系如下:
(10)
将(10)代入方程式(7) (8) (9)并经过新消元后将得到下面的方程式
(11)
(12)
在这里联立(11) (12)可以得到结论方程式(1),即所要证明的勾股定理,至此定理证明完毕。
3. 另一种证明方法
在这里仅是讲述一下如何证明,但不做式子上的证明,对于变形式子(2a) (3a) (4a) (5a),将(3a) (4a)两边同时相加,再由式子(5a)可以得到式子(2a),进而得到结论方程式。
4. 一个悖论性问题
在本文中,我们主要证明勾股定理,这里有一个问题,线段AB,AC,BC的长度是怎么算出来的或者满足某种关系,这里的关系是否为勾股定理,若用的是勾股定理。那么,在本文的证明中将是一个悖论性问题,同样对于吴方法也是一个悖论性问题。用勾股定理证明勾股定理,这对于初等几何将是一个很有名的悖论难题。
5. 勾股定理的一个延伸
在这里我们将给出一个新型的勾股定理,当然证明是初等的,我们的目的是希望能有人给出这个新型的勾股定理的机械化证明,如下:
已知:如图1,半径为R的圆,内接三角形为ABC,∠A、∠B所对的边分别为边a,b。现使a边固
定不动,边a,b上的高AD,BE交于点O。
求证:
证明:我们使
,
,
,在直角三角形AEB中,我们可以得到下面的关系式:
(5.1)
(5.2)
又因为三角形AOD相似于三角形ACD,所以我们可以得到下面的式子
(5.3)
所以:
(5.4)
由四式我们可以得到下面的式子
(5.5)
又因为
(5.6)
所以:
(5.7)
又因为:
(5.8)
由(5.5) (5.7) (5.8)我们可以得到我们所要的
证毕。