PHẠM VIỆT HƯNG
Gọi chung là Định Lý Bất Toàn nhưng thực ra có hai định lý. Cả hai đều chỉ ra rằng toán học về bản chất là bất toàn (không đầy đủ), vì nó luôn chứa đựng những mệnh đề không quyết định được (undecidable), tức những mệnh đề không thể chứng minh và cũng không thể bác bỏ.
Định lý 1: Nếu một lý thuyết dựa trên một hệ tiên đề phi mâu thuẫn thì trong lý thuyết ấy luôn luôn tồn tại những mệnh đề không thể chứng minh cũng không thể bác bỏ.
Định lý 2: Không tồn tại bất cứ một quy trình suy diễn nào cho phép chứng minh tính phi mâu thuẫn của một hệ tiên đề.
Chẳng hạn, hãy xét mệnh đề được đóng khung sau đây:
Mệnh đề này không có bất cứ một chứng minh nào
NGUYỄN BÁ TRINH
Các điều kiện cho hệ hình thức của chương trình Hilbert:
- Tính phong phú (Richness) (Hay cõ thểdịch là tính phức tạp cũng được) Hệ đó phải đủ phong phú để diễn tả được các định lý của số học, các tính chất của số học, vì đây là mục tiêu của chương trình. Chứ nếu ta chỉ làm 1 hệ để chơi cờ ca rô thì chắc dễ rồi.
- Tính hiệu quả(Effectiveness) Ở đây nó có nghĩa là hệ sẽ bao gồm một tập hữu hạn các tiên đề và qui tắc biến đổi khả dĩ máy tính có thể xử lý được. Và nhờ đó một tính chất nào đó của số học có thể qui về tiên đề sau 1 số bước hữu hạn biến đổi. Nếu số bước là vô hạn thì nó treo luôn máy thì cũng vô dụng. Ở đây ta để ý là số học nếu diễn tả trong logic bậc 1 thì cần tới vô số tiên đề
- Tính nhất quán (consistency) Tính này có nghĩa là nếu một mệnh đề trong xác định là ĐÚNG bằng cách đưa về 1 tiên đề, thì phủ định của nó phải là SAI. Tức là trong hệ, ta không thể nào viết một mệnh đề đúng văn phạm của hệ mà lại vừa ĐÚNG lại vừa SAI.
- Tính đầy đủ (Completeness) Tính này nó nghĩa là hệ phải có đủ tiên đề và qui tắc biến đổi sao cho bất kỳ một mệnh đề cũng tồn tại một phép biến đổi để có thể xác định được là ĐÚNG hay SAI. Thí dụ, dễ hiểu là hệ hình học mình học hồi nhỏ, hình học Euclid (Ơ-clit) có năm tiên đề. Tiên đề số năm là tiên đề về đường song song. Nếu ta lấy tiên đề đó ra khỏi hệ thì hệ sẽ trở thành không đầy đủ, vì nó tồn tại ít nhất một mệnh đề mà ta không thể đưa về 4 tiên đề còn lại được. Mệnh đề đó chính là tiên đề thứ 5 này. Tiên đề này không thể chứng minh bằng cách dùng 4 mệnh đề kia.
Hai định lý về sự không đầy đủ của Godel (Incompleteness Theorems) nói cái gì ?
Định lý1: Nếu một hệ mà phong phú, và hiệu quả, và nhất quán thì không thể đầy đủ được.
Định lý2: Trong một hệ S nào đó phong phú, và hiệu quả, thì tồn tại mệnh đề T cụ thể là “S là 1 hệ nhất quán”. Mệnh đề đó không thể chứng minh trong S nếu S là nhất quán thật.
Định lý này nói rằng :
“Bất kỳ một lý thuyết nào được tạo ra một cách hiệu quả đủ khả năng biểu diễn số học sơ cấp đều không thể vừa nhất quán vừa đầy đủ”
“Bất kì một lý thuyết hình thức nào nhất quán, được tạo ra một cách hiệu quả cho phép chứng minh một số chân lý số học căn bản, sẽ tồn tại một mệnh đề số học đúng nhưng không thể chứng minh trong lý thuyết ấy”
He proved for any computable axiomatic system that is powerful enough to describe the arithmetic of the natural numbers (e.g., the Peano axioms or Zermelo–Fraenkel set theory with the axiom of choice), that:
- If a (logical or axiomatic formal) system is consistent, it cannot be complete.
- The consistency of axioms cannot be proved within their own system.
First incompleteness theorem
Gödel’s first incompleteness theorem first appeared as “Theorem VI” in Gödel’s 1931 paper “On Formally Undecidable Propositions of Principia Mathematica and Related Systems I”. The hypotheses of the theorem were improved shortly thereafter by J. Barkley Rosser (1936) using Rosser’s trick. The resulting theorem (incorporating Rosser’s improvement) may be paraphrased in English as follows, where “formal system” includes the assumption that the system is effectively generated.
First Incompleteness Theorem: “Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.” (Raatikainen 2015)
The unprovable statement GF referred to by the theorem is often referred to as “the Gödel sentence” for the system F. The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence.
Each effectively generated system has its own Gödel sentence. It is possible to define a larger system F’ that contains the whole of F plus GF as an additional axiom. This will not result in a complete system, because Gödel’s theorem will also apply to F’, and thus F’ also cannot be complete. In this case, GF is indeed a theorem in F’, because it is an axiom. Because GF states only that it is not provable in F, no contradiction is presented by its provability within F’. However, because the incompleteness theorem applies to F’, there will be a new Gödel statement GF′ for F’, showing that F’ is also incomplete. GF′ will differ from GF in that GF′ will refer to F’, rather than F.
Syntactic form of the Gödel sentence
The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in F. However, the sequence of steps is such that the constructed sentence turns out to be GF itself. In this way, the Gödel sentence GF indirectly states its own unprovability within F (Smith 2007, p. 135).
To prove the first incompleteness theorem, Gödel demonstrated that the notion of provability within a system could be expressed purely in terms of arithmetical functions that operate on Gödel numbers of sentences of the system. Therefore, the system, which can prove certain facts about numbers, can also indirectly prove facts about its own statements, provided that it is effectively generated. Questions about the provability of statements within the system are represented as questions about the arithmetical properties of numbers themselves, which would be decidable by the system if it were complete.
Thus, although the Gödel sentence refers indirectly to sentences of the system F, when read as an arithmetical statement the Gödel sentence directly refers only to natural numbers. It asserts that no natural number has a particular property, where that property is given by a primitive recursive relation (Smith 2007, p. 141). As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form. In particular, it can be expressed as a formula in the language of arithmetic consisting of a number of leading universal quantifiers followed by a quantifier-free body (these formulas are at level of the arithmetical hierarchy). Via the MRDP theorem, the Gödel sentence can be re-written as a statement that a particular polynomial in many variables with integer coefficients never takes the value zero when integers are substituted for its variables (Franzén 2005, p. 71).
Truth of the Gödel sentence
The first incompleteness theorem shows that the Gödel sentence GF of an appropriate formal theory F is unprovable in F. Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). For this reason, the sentence GF is often said to be “true but unprovable.” (Raatikainen 2015). However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence GF may only be arrived at via a meta-analysis from outside the system. In general, this meta-analysis can be carried out within the weak formal system known as primitive recursive arithmetic, which proves the implication Con(F)→GF, where Con(F) is a canonical sentence asserting the consistency of F (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403).
Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel’s completeness theorem (Franzén 2005, p. 135). That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false. As described earlier, the Gödel sentence of a system F is an arithmetical statement which claims that no number exists with a particular property. The incompleteness theorem shows that this claim will be independent of the system F, and the truth of the Gödel sentence follows from the fact that no standard natural number has the property in question. Any model in which the Gödel sentence is false must contain some element which satisfies the property within that model. Such a model must be “nonstandard” – it must contain elements that do not correspond to any standard natural number (Raatikainen 2015, Franzén 2005, p. 135).
Relationship with the liar paradox
Gödel specifically cites Richard’s paradox and the liar paradox as semantical analogues to his syntactical incompleteness result in the introductory section of “On Formally Undecidable Propositions in Principia Mathematica and Related Systems I“. The liar paradox is the sentence “This sentence is false.” An analysis of the liar sentence shows that it cannot be true (for then, as it asserts, it is false), nor can it be false (for then, it is true). A Gödel sentence G for a system F makes a similar assertion to the liar sentence, but with truth replaced by provability: G says “G is not provable in the system F.” The analysis of the truth and provability of G is a formalized version of the analysis of the truth of the liar sentence.
It is not possible to replace “not provable” with “false” in a Gödel sentence because the predicate “Q is the Gödel number of a false formula” cannot be represented as a formula of arithmetic. This result, known as Tarski’s undefinability theorem, was discovered independently both by Gödel, when he was working on the proof of the incompleteness theorem, and by the theorem’s namesake, Alfred Tarski.
Extensions of Gödel’s original result
Compared to the theorems stated in Gödel’s 1931 paper, many contemporary statements of the incompleteness theorems are more general in two ways. These generalized statements are phrased to apply to a broader class of systems, and they are phrased to incorporate weaker consistency assumptions.
Gödel demonstrated the incompleteness of the system of Principia Mathematica, a particular system of arithmetic, but a parallel demonstration could be given for any effective system of a certain expressiveness. Gödel commented on this fact in the introduction to his paper, but restricted the proof to one system for concreteness. In modern statements of the theorem, it is common to state the effectiveness and expressiveness conditions as hypotheses for the incompleteness theorem, so that it is not limited to any particular formal system. The terminology used to state these conditions was not yet developed in 1931 when Gödel published his results.
Gödel’s original statement and proof of the incompleteness theorem requires the assumption that the system is not just consistent but ω-consistent. A system is ω-consistent if it is not ω-inconsistent, and is ω-inconsistent if there is a predicate P such that for every specific natural number m the system proves ~P(m), and yet the system also proves that there exists a natural number n such that P(n). That is, the system says that a number with property P exists while denying that it has any specific value. The ω-consistency of a system implies its consistency, but consistency does not imply ω-consistency. J. Barkley Rosser (1936) strengthened the incompleteness theorem by finding a variation of the proof (Rosser’s trick) that only requires the system to be consistent, rather than ω-consistent. This is mostly of technical interest, because all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel’s theorem as originally stated applies to them. The stronger version of the incompleteness theorem that only assumes consistency, rather than ω-consistency, is now commonly known as Gödel’s incompleteness theorem and as the Gödel–Rosser theorem.
Second incompleteness theorem
For each formal system F containing basic arithmetic, it is possible to canonically define a formula Cons(F) expressing the consistency of F. This formula expresses the property that “there does not exist a natural number coding a formal derivation within the system F whose conclusion is a syntactic contradiction.” The syntactic contradiction is often taken to be “0=1”, in which case Cons(F) states “there is no natural number that codes a derivation of ‘0=1’ from the axioms of F.”
Gödel’s second incompleteness theorem shows that, under general assumptions, this canonical consistency statement Cons(F) will not be provable in F. The theorem first appeared as “Theorem XI” in Gödel’s 1931 paper “On Formally Undecidable Propositions in Principia Mathematica and Related Systems I“. In the following statement, the term “formalized system” also includes an assumption that F is effectively axiomatized.
Second Incompleteness Theorem: “Assume F is a consistent formalized system which contains elementary arithmetic. Then .” (Raatikainen 2015)
This theorem is stronger than the first incompleteness theorem because the statement constructed in the first incompleteness theorem does not directly express the consistency of the system. The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the system F itself.
There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of F as a formula in the language of F. There are many ways to express the consistency of a system, and not all of them lead to the same result. The formula Cons(F) from the second incompleteness theorem is a particular expression of consistency.
Other formalizations of the claim that F is consistent may be inequivalent in F, and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that “the largest consistent subset of PA” is consistent. But, because PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA “proves that it is consistent”. What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term “largest consistent subset of PA” is meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration).
The Hilbert–Bernays conditions
The standard proof of the second incompleteness theorem assumes that the provability predicate ProvA(P) satisfies the Hilbert–Bernays provability conditions. Letting #(P) represent the Gödel number of a formula P, the derivability conditions say:
- If F proves P, then F proves ProvA(#(P)).
- F proves 1.; that is, F proves that if F proves P, then F proves ProvA(#(P)). In other words, F proves that ProvA(#(P)) implies ProvA(#(ProvA(#(P)))).
- F proves that if F proves that (P → Q) and F proves P then F proves Q. In other words, F proves that ProvA(#(P → Q)) and ProvA(#(P)) imply ProvA(#(Q)).
There are systems, such as Robinson arithmetic, which are strong enough to meet the assumptions of the first incompleteness theorem, but which do not prove the Hilbert—Bernays conditions. Peano arithmetic, however, is strong enough to verify these conditions, as are all theories stronger than Peano arithmetic.
Implications for consistency proofs
Gödel’s second incompleteness theorem also implies that a system F1 satisfying the technical conditions outlined above cannot prove the consistency of any system F2 that proves the consistency of F1. This is because such a system F1 can prove that if F2 proves the consistency of F1, then F1 is in fact consistent. For the claim that F1 is consistent has form “for all numbers n, n has the decidable property of not being a code for a proof of contradiction in F1“. If F1 were in fact inconsistent, then F2 would prove for some n that n is the code of a contradiction in F1. But if F2 also proved that F1 is consistent (that is, that there is no such n), then it would itself be inconsistent. This reasoning can be formalized in F1 to show that if F2 is consistent, then F1 is consistent. Since, by second incompleteness theorem, F1 does not prove its consistency, it cannot prove the consistency of F2 either.
This corollary of the second incompleteness theorem shows that there is no hope of proving, for example, the consistency of Peano arithmetic using any finitistic means that can be formalized in a system the consistency of which is provable in Peano arithmetic (PA). For example, the system of primitive recursive arithmetic (PRA), which is widely accepted as an accurate formalization of finitistic mathematics, is provably consistent in PA. Thus PRA cannot prove the consistency of PA. This fact is generally seen to imply that Hilbert’s program, which aimed to justify the use of “ideal” (infinitistic) mathematical principles in the proofs of “real” (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out (Franzén 2005, p. 106).
The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would actually provide no interesting information if a system F proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of F in F would give us no clue as to whether F really is consistent; no doubts about the consistency of F would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system F in some system F’ that is in some sense less doubtful than F itself, for example weaker than F. For many naturally occurring theories F and F’, such as F = Zermelo–Fraenkel set theory and F’ = primitive recursive arithmetic, the consistency of F’ is provable in F, and thus F’ cannot prove the consistency of F by the above corollary of the second incompleteness theorem.
The second incompleteness theorem does not rule out consistency proofs altogether, only consistency proofs that can be formalized in the system that is proved consistent. For example, Gerhard Gentzen proved the consistency of Peano arithmetic in a different system that includes an axiom asserting that the ordinal called ε0 is wellfounded; see Gentzen’s consistency proof. Gentzen’s theorem spurred the development of ordinal analysis in proof theory.