【软件中医】几何的逻辑证明并不严密

【软件中医】几何的逻辑证明并不严密
    古代西方数学，由于在负数、分数、无理数等方面遇到严重的认识困难，只能进行加法和乘法的运算，这就给其代数的发展造成了无法克服的障碍，而用代数来解决几何问题就更谈不上了；于是，就迫使古代西方数学走上了一条独特的发展道路：用逻辑推理论证几何问题。因为在逻辑证明过程中只会用到加法和乘法，最多再用到比例，这就避开了出现负数、分数、无理数的可能。
    长期以来，大家认为欧几力德几何中的论证推理过程是严密的，即使有问题，也只出在公理体系上，而且经过希尔伯特重整了欧氏公理体系之后，总不会再有问题了吧。
    但吴文俊教授（机械化数学的发明人）指出：传统的初等几何证明方法——>所谓综合法，不但不严密，而且也不可能严密，问题就出在“退化”情形上。
    欧氏几何中的概念，通常是排除了“退化”情形的，比如说：“三角形”吧，就要求三顶点不共直线，三顶点共直线，三角形就形成了线段，就是退化了，有些几何定理，对退化情形也成立，但也有些几何定理，图形一退化，定理就不成立了。
    如：‘ΔABC中，若角B=角C，则AB=AC’这条定理，当角B=角C=0度时就不成立，而当角B=角C=90度时，又成立了。可见，对退化情形要单独进行讨论。
    那么，在几何命题的假设中，排除了退化情形，是不是就万事大吉、完全严密了呢？问题没那么简单：因为用综合法证几何题，往往要作辅助线，辅助圆，对辅助图形运用一些已知定理，在辅助图形中有可能遇到退化的情形，怎样作辅助线，事先是不知道的，因而无法预先说明会出现哪些退化情形而使证明失效。证明中的推理环节越多，使用的已知定理也越多，出现退化情形而破坏证明的严密性的可能性越大；
    而证明过程中使用的这些已知定理，其本身的证明过程也大都使用了其他一些已知定理；而这些“其他定理”本身的证明又…… ……，所以，谁也无法保证我们的证明过程是严密的。
    在几何定理的机器（电脑）证明的“吴方法”中，这个问题得到了圆满的解决。在机器证明过程中，能够自然地一一列出退化情形的代数表示，并指出保证命题成立的非退化条件。至于退化情形时命题是否成立 ，这种讨论通常是容易的。
-------------------------------------------------------
注：所谓“吴方法”类似我们上初中时解方程过程中使用的“消元法”，它是吴文俊直接从中国古代——宋元时期的算术思想和方法中引入的，是一种通过解代数方程来证明几何题的方法。“吴方法”这个名是国外数学同行给起的。

===================
反对西化，人人有责

法佬说：今天是端午节，我请你们吃粽子，人肉馅儿的，来人呐，上木乃伊…