| | 不完全性定理
incompleteness theorem
证明论中的一条重要定理。由k.哥德尔于1931年证明，是数理逻辑发展史上的一个极为重要的定理。
设有一个以皮亚诺自然数论为其子系统的、自身协调的（即不自相矛盾的）形式系统，暂记为 u；在形式系统中凡不含自由变元的公式叫做语句；如果语句 a和塡a在某形式系统内均不可证，则a就叫做该形式系统的不可判定语句。不完全性定理说，任何一个上述的系统u都必有一个不可判定语句a。依照排中律，a和塡a之间必有一个是真语句，故不完全性定理可改为：任何一个上述的系统 u都必有一个真语句是不能推出的。如果一个系统对任何语句 a能够推出a或推出塡a，则这个系统叫做完全系统，这样不完全性定理又可改述为：任何一个上述的系统 u必是不完全的。
在证明不完全性定理时,主要是使用算术化方法,即先把形式系统中所使用的各符号都逐一给以一个自然数编号，然后依次对各公式也给以一个编号，再后又对各公式序列，例如证明中所使用的公式序列给以一个编号。凡属编号必须满足下列条件，即给出符号或公式或公式序列后，可以唯一地决定其编号。反之，当给出一个自然数后，则可以决定其是否用作编号，如果是，就可以唯一地决定其是符号的或者是公式的，还是公式序列的编号。满足这种条件的编号，叫做哥德尔编号。利用编号可以把有关形式系统的各性质用算术函数算术公式来表示。例如，可以作出一个算术公式 prov(a,b)，使得prov(a,b)成立当且仅当编号为a的公式序列是对编号为b的公式的证明,这也表明证明关系是可以算术化的。有了这些（以及别的）算术函数算术公式后，就容易作出不可判定语句。
根据不完全性定理的证明过程，还可以推得下列结论：如果包含皮亚诺自然数论为子系统的形式系统 u是协调的，则表示" u是协调的"这个事实的算术公式不可能在系统 u内证明，这个结果叫做第二不完全性定理。它也是证明论中很重要的结果。
虽然证明关系、可证性、协调性等等是可以算术化的，但由不完全性定理却可推得：真假性是不能算术化的，亦即不可能找到一个算术公式tr(a)使得tr(a)成立，当且仅当以a为编号的公式a为真，也就是说,在系统u内下列公式tr(a)刼a（这里a为a的编号）是不可证的。这是不完全性定理的另一内容，它是由a.塔尔斯基首先给出的。 | | buwanquanxing dingli
不完全性定理
incompleteness theorem
证明论中的一条重要定理。由K.哥德尔于1931年证明，是数理逻辑发展史上的一个极为重要的定理。
设有一个以皮亚诺自然数论为其子系统的、自身协调的（即不自相矛盾的）形式系统，暂记为 U；在形式系统中凡不含自由变元的公式叫做语句；如果语句 A和□A在某形式系统内均不可证，则A就叫做该形式系统的不可判定语句。不完全性定理说，任何一个上述的系统U都必有一个不可判定语句A。依照排中律，A和□A之间必有一个是真语句，故不完全性定理可改为：任何一个上述的系统 U都必有一个真语句是不能推出的。如果一个系统对任何语句 A能够推出A或推出□A，则这个系统叫做完全系统，这样不完全性定理又可改述为：任何一个上述的系统 U必是不完全的。
在证明不完全性定理时,主要是使用算术化方法,即先把形式系统中所使用的各符号都逐一给以一个自然数编号，然后依次对各公式也给以一个编号，再后又对各公式序列，例如证明中所使用的公式序列给以一个编号。凡属编号必须满足下列条件，即给出符号或公式或公式序列后，可以唯一地决定其编号。反之，当给出一个自然数后，则可以决定其是否用作编号，如果是，就可以唯一地决定其是符号的或者是公式的，还是公式序列的编号。满足这种条件的编号，叫做哥德尔编号。利用编号可以把有关形式系统的各性质用算术函数算术公式来表示。例如，可以作出一个算术公式 prov(a,b)，使得prov(a,b)成立当且仅当编号为a的公式序列是对编号为b的公式的证明,这也表明证明关系是可以算术化的。有了这些（以及别的）算术函数算术公式后，就容易作出不可判定语句。
根据不完全性定理的证明过程，还可以推得下列结论：如果包含皮亚诺自然数论为子系统的形式系统 U是协调的，则表示“ U是协调的”这个事实的算术公式不可能在系统 U内证明，这个结果叫做第二不完全性定理。它也是证明论中很重要的结果。
虽然证明关系、可证性、协调性等等是可以算术化的，但由不完全性定理却可推得：真假性是不能算术化的，亦即不可能找到一个算术公式tr(□)使得tr(□)成立，当且仅当以a为编号的公式A为真，也就是说,在系统U内下列公式tr(□)□A（这里a为A的编号）是不可证的。这是不完全性定理的另一内容，它是由A.塔尔斯基首先给出的（见不可定义性理论）。
（莫绍揆）
| | | Johann wolfgang von goethe, 1749-1832, german poet you Faultiness nature axiom | |
|
|
|