307
个编辑
更改
跳到导航
跳到搜索
第407行：
第407行： + 第412行：
第413行： − 一组自然数的图灵度与使用一阶公式定义该自然数的困难度(用算数阶层表示)有密切的关系。波斯特定理使这种关系变得精确。库尔特 · 哥德尔在他的完备性定理和不完备性定理的证明中证明了一个较弱的关系。哥德尔的证明表明，一个有效的一阶理论的逻辑结果集是一个递归可枚举集合，如果这个理论足够强大，这个集合将是无法计算的。类似地，塔斯基的不可定性定理可以从可定性和可计算性两方面来解释。+ 第420行：
第421行： − 可计算性理论也与二阶算术有关，二阶算术是一种关于自然数和自然数集合的正式理论。某些集合可计算或相对可计算的事实往往意味着这些集合可以在二阶算术的弱子系统中定义。逆数学的程序使用这些子系统来测量众所周知的数学定理所固有的不可计算性。辛普森(1999)讨论了二阶算术和逆数学的许多方面。+ 第428行：
第429行： − 证明理论包括二阶算术和 Peano 算术的研究，以及比 Peano 算术弱的自然数的形式化理论。对这些弱系统的强度进行分类的一种方法是通过描述系统可以证明为完整的可计算函数(见 Fairtlough 和 Wainer (1998))。例如，在基元递归算法中，任何可证明总和的可计算函数实际上是基元递归的，而 Peano 算法证明了类似于阿克曼函数递归的函数是总和的，它不是基元递归的。然而，并不是所有的可计算函数在 Peano 算术中都是可证明的总和，这样的函数的一个例子就是 Goodstein 定理。+ − −
→Relationships between definability, proof and computability
==Relationships between definability, proof and computability==
==Relationships between definability, proof and computability==
可定义性、证明性和可计算性之间的关系
There are close relationships between the Turing degree of a set of natural numbers and the difficulty (in terms of the [[arithmetical hierarchy]]) of defining that set using a [[first-order logic|first-order formula]]. One such relationship is made precise by [[Post's theorem]]. A weaker relationship was demonstrated by [[Kurt Gödel]] in the proofs of his [[Gödel's completeness theorem|completeness theorem]] and [[Gödel's incompleteness theorem|incompleteness theorems]]. Gödel's proofs show that the set of logical consequences of an effective first-order theory is a [[recursively enumerable set]], and that if the theory is strong enough this set will be uncomputable. Similarly, [[Tarski's indefinability theorem]] can be interpreted both in terms of definability and in terms of computability.
There are close relationships between the Turing degree of a set of natural numbers and the difficulty (in terms of the [[arithmetical hierarchy]]) of defining that set using a [[first-order logic|first-order formula]]. One such relationship is made precise by [[Post's theorem]]. A weaker relationship was demonstrated by [[Kurt Gödel]] in the proofs of his [[Gödel's completeness theorem|completeness theorem]] and [[Gödel's incompleteness theorem|incompleteness theorems]]. Gödel's proofs show that the set of logical consequences of an effective first-order theory is a [[recursively enumerable set]], and that if the theory is strong enough this set will be uncomputable. Similarly, [[Tarski's indefinability theorem]] can be interpreted both in terms of definability and in terms of computability.
There are close relationships between the Turing degree of a set of natural numbers and the difficulty (in terms of the arithmetical hierarchy) of defining that set using a first-order formula. One such relationship is made precise by Post's theorem. A weaker relationship was demonstrated by Kurt Gödel in the proofs of his completeness theorem and incompleteness theorems. Gödel's proofs show that the set of logical consequences of an effective first-order theory is a recursively enumerable set, and that if the theory is strong enough this set will be uncomputable. Similarly, Tarski's indefinability theorem can be interpreted both in terms of definability and in terms of computability.
There are close relationships between the Turing degree of a set of natural numbers and the difficulty (in terms of the arithmetical hierarchy) of defining that set using a first-order formula. One such relationship is made precise by Post's theorem. A weaker relationship was demonstrated by Kurt Gödel in the proofs of his completeness theorem and incompleteness theorems. Gödel's proofs show that the set of logical consequences of an effective first-order theory is a recursively enumerable set, and that if the theory is strong enough this set will be uncomputable. Similarly, Tarski's indefinability theorem can be interpreted both in terms of definability and in terms of computability.
一组自然数的图灵程度与用'''<font color="#ff8000">一阶公式 first-order formula</font>'''定义该集合的难度(就'''<font color="#ff8000">算术谱系 arithmetical hierarchy</font>'''而言)之间存在密切关系。'''<font color="#ff8000">波斯特定理 Post's theorem</font>'''使这种关系变得精确。'''<font color="#ff8000">库尔特·哥德尔 Kurt Gödel</font>'''在他的'''<font color="#ff8000">完备性定理 completeness theorem</font>'''和'''<font color="#ff8000">不完备性定理 incompleteness theorems</font>'''的证明中证明了一个较弱的关系。哥德尔的证明表明，一个有效的一阶理论的逻辑结果集是一个'''<font color="#ff8000">递归可枚举集 recursively enumerable set</font>'''，如果这个理论足够强大，这个集合将是无法计算的。类似地，'''<font color="#ff8000">塔斯基的不可定义定理 Tarski's indefinability theorem</font>'''可以从可定义性和可计算性两方面来解释。
Recursion theory is also linked to second order arithmetic, a formal theory of natural numbers and sets of natural numbers. The fact that certain sets are computable or relatively computable often implies that these sets can be defined in weak subsystems of second order arithmetic. The program of reverse mathematics uses these subsystems to measure the noncomputability inherent in well known mathematical theorems. Simpson (1999) discusses many aspects of second-order arithmetic and reverse mathematics.
Recursion theory is also linked to second order arithmetic, a formal theory of natural numbers and sets of natural numbers. The fact that certain sets are computable or relatively computable often implies that these sets can be defined in weak subsystems of second order arithmetic. The program of reverse mathematics uses these subsystems to measure the noncomputability inherent in well known mathematical theorems. Simpson (1999) discusses many aspects of second-order arithmetic and reverse mathematics.
递归理论也与'''<font color="#ff8000">二阶算术 second order arithmetic</font>'''有关，二阶算术是一种关于自然数和自然数集合的形式理论。某些集合是可计算的或相对可计算的这一事实通常意味着这些集合可以在二阶算术的弱子系统中定义。'''<font color="#ff8000">逆数学 reverse mathematics</font>'''的程序使用这些子系统来测量众所周知的数学定理所固有的不可计算性。辛普森(1999)讨论了二阶算术和逆数学的许多方面。
The field of proof theory includes the study of second-order arithmetic and Peano arithmetic, as well as formal theories of the natural numbers weaker than Peano arithmetic. One method of classifying the strength of these weak systems is by characterizing which computable functions the system can prove to be total (see Fairtlough and Wainer (1998)). For example, in primitive recursive arithmetic any computable function that is provably total is actually primitive recursive, while Peano arithmetic proves that functions like the Ackermann function, which are not primitive recursive, are total. Not every total computable function is provably total in Peano arithmetic, however; an example of such a function is provided by Goodstein's theorem.
The field of proof theory includes the study of second-order arithmetic and Peano arithmetic, as well as formal theories of the natural numbers weaker than Peano arithmetic. One method of classifying the strength of these weak systems is by characterizing which computable functions the system can prove to be total (see Fairtlough and Wainer (1998)). For example, in primitive recursive arithmetic any computable function that is provably total is actually primitive recursive, while Peano arithmetic proves that functions like the Ackermann function, which are not primitive recursive, are total. Not every total computable function is provably total in Peano arithmetic, however; an example of such a function is provided by Goodstein's theorem.
'''<font color="#ff8000">证明理论 proof theory</font>'''包括二阶算术和'''<font color="#ff8000">皮亚诺算术 Peano arithmetic</font>'''的研究，以及比皮亚诺算术弱的自然数的形式化理论。对这些弱系统的强度进行分类的一种方法是通过描述系统可以证明的'''<font color="#ff8000">全部 total</font>'''可计算功能(见 费尔托夫 和 韦纳 (1998))。例如，在'''<font color="#ff8000">原始递归算法 primitive recursive arithmetic</font>'''中，任何可计算的可证明总函数实际上是'''<font color="#ff8000">原始递归 primitive recursive</font>'''，而'''<font color="#ff8000">皮亚诺算术 Peano arithmetic</font>'''证明了像'''<font color="#ff8000">阿克曼函数 Ackermann function</font>'''这样的函数，不是原始递归的，是总函数。然而，并不是所有的可计算函数在皮亚诺算术中都是可证明的总和，此类函数的一个例子就是'''<font color="#ff8000">古德斯坦定理 Goodstein's theorem</font>'''。
==Name==
==Name==