一百年沧桑巨变，数学大树依然长青

在十九世纪初期，希尔伯特提出一个“大纲”，想给整个数学奠定一个牢不可破的基础。大纲内容如下（有三点）：

1、A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules.

2、Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects.

3、Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.

希尔伯特的上述“大纲”，虽然想法很好，可是，被哥德尔的“不完全性定理”打乱了，世界数学界似乎乱了套。

一百年来，世界数学界沧桑巨变，似乎看不到光明的前景。直到本世纪初，2005年，R.Zach发现，只要略微改变上述三点（目标），即可恢复希尔伯特当年的“大纲”，使数学大树依旧长青。

R,Zach的更改建议如下：

1、Although it is not possible to prove completeness for systems at least as powerful as Peano arithmetic (at least if they have a computable set of axioms), it is possible to prove forms of completeness for many other interesting systems. The first big success was by Gödel himself (before he proved the incompleteness theorems) who proved the completeness theorem for first-order logic, showing that any logical consequence of a series of axioms is provable. An example of a non-trivial theory for which completeness has been proved is the theory of algebraically closed fields of given characteristic.

2、The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand, Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, Gentzen gave a consistency proof for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite induction up to the ordinal ε₀. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of second order arithmetic have been given consistency proofs by Gaisi Takeuti and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.)

3、Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non-trivial theories for which such algorithms have been found. For example, Tarski found an algorithm that can decide the truth of any statement in analytic geometry (more precisely, he proved that the theory of real closed fields is decidable). Given the Cantor–Dedekind axiom, this algorithm can be regarded as an algorithm to decide the truth of any statement in Euclidean geometry. This is substantial as few people would consider Euclidean geometry a trivial theory.

注：由此可见，无穷小微积分理论基础，坚如磐石，不受任何影响。

袁萌  10月30日