# 用一个音节的字解释哥德尔第二不完全性定理 - George Boolos

1. if p, then p,

2. (ii) ((p q) (p q), and

3. (iii) (p 口口p)

" Proof(x,y) "是一个（我们语言中的）名词短语，表示一个（理论语言中的）公式，其构造与"......是理论中的证明____"的任何标准定义相似。因此，对于语言中的任何句子p，口p是语言中的另一个句子，可以被视为说p在理论中是可证明的。

(iv) if (p q), (p q)

1. p ¬p

2. p ¬p                         truth-functionally from 1

3. p ¬p                   by (iv) from 2

4. p 口口p                     by (iii)

5. ¬p （口p ).          A tautology

6. ¬p (p ).     By (iv) from 5

7. (p ) (口口p口⊥) by (ii)

8. p 口⊥.                      truth-Truth-functionally from 3,6,7, and 4

9. ¬口⊥ p.                       truth-Truth-functionally from 8 and 1

10. 10.¬口⊥ p                 by (iv) from 9

11. 11.¬口⊥ ¬¬口⊥.            truth-Truth-functionally from 8 and 10

(我们省略了(1)(11)中最外层的括号)

Gödel’s Second Incompleteness Theorem Explained in Words of One Syllable - George Boolos

First of all, when I say "proved", what I will mean is "proved with the aid of the whole of math". Now then: two plus two is four, as you well know. And, of course, it can be proved that two plus two is four (proved, that is, with the aid of the whole of math, as I said, though in the case of two plus two, of course we do not need the whole of math to prove that it is four).

And, as may not be quite so clear, it can be proved that it can be proved that two plus two is four, as well. And it can be proved that it can be proved that it can be proved that two plus two is four. And so on. In fact, if a claim can be proved, then it can be proved that the claim can be proved. And that too can be proved. Now, two plus two is not five. And it can be proved that two plus two is not five. And it can be proved that it can be proved that two plus two is not five, and so on.

Thus: it can be proved that two plus two is not five. Can it be proved as well that two plus two is five? It would be a real blow to math, to say the least, if it could. If it could be proved that two plus two is five, then it could be proved that five is not five, and then there would be no claim that could not be proved, and math would be a lot of bunk.

So, we now want to ask, can it be proved that it can't be proved that two plus two is five? Here's the shock: no, it can't. Or, to hedge a bit: if it can be proved that it can't be proved that two plus two is five, then it can be proved as well that two plus two is five, and math is a lot of bunk. In fact, if math is not a lot of bunk, then no claim of the form "claim X can't be proved" can be proved. So, if math is not a lot of bunk, then, though it can't be proved that two plus two is five, it can't be proved that it can't be proved that two plus two is five. By the way, in case you'd like to know: yes, it can be proved that if it can be proved that it can't be proved that two plus two is five, then it can be proved that two plus two is five.

« I wish he would explain his explanation »

If, as we shall assume, the whole of mathematics can be formalized as a formal theory of the usual sort (no small assumption), then there is a formula Proof(x,y) of the langage (of that theory) obtainable from a suitable description of the theory (« as » a formal theory) that meets the following conditions :

1. if p, then p,

2. (ii) ((p q) (p q), and

3. (iii) (p 口口p)

For all sentences p, q of the language. We have written : p to abbreviate : xProof(x, ‘p'), where ‘p’ is a standard representation in the language for the sentence p. (‘p’ might be the numeral for the Godel number of p.) «  » is a preposed verb phrase (of our language) meaning « is provable in the theory ».

« Proof(x,y) » is a noun phrase (of our language) denoting a formula (of the theory’s language) whose construction parallels any standard definition of « … is a proof of ____ in the theory ». Thus, for any sentence p of the language, p is another sentence of the language that may be regarded as saying that p is provable in the theory.

Conditions (i), (ii), and (iii) are called the Hilbert-Bernays-Löb derivability conditions; they are satisfied by all reasonable formal theories in which a certain small amount of arithmetic can be proved.

Since the theory is standard, all tautologies in its language are provable in the theory, and all logical consequences in its language of provable statements are provable.

It follows that for all sentences p, q ,

(iv) if (p q), (p q)

For : if (p q), then by (i) (p q); but by (ii), ((p q) (p q), and then (p q) by modus ponens.

is the zero-place truth-functional connective that is always evaluated as false. Of course is a contradiction. We shall need to observe later that (¬q(q )) is a tautology. If is not one of the primitive symbols of the langage, it may be defined as any refutable sentence, e.g., one expressing that two plus two is five.

With the aid of , there is an easy way to say that theory is consistent : /⊢⊥, i.e., is not provable in the theory. The sentence of the language stating that the theory is consistent can thus be taken to be ¬口⊥, which is identical with  ¬xProof(x, ‘’).

We may prove Godel’s second incompleteness theorem, as well as the theorem that the second incompleteness theorem is provable in the theory (« the formalized second incompleteness theorem »), as follow.

Via the technique of diagonalization, introduced by Godel (1931) in « On formally undecidable proposition … », a sentence p can be found that is equivalent in the theory to the statement that p is unprovable in the theory, i.e., a sentence such that

1. p ¬p

2. p ¬p                         truth-functionally from 1

3. p ¬p                   by (iv) from 2

4. p 口口p                     by (iii)

5. ¬p （口p ).          A tautology

6. ¬p (p ).     By (iv) from 5

7. (p ) (口口p口⊥) by (ii)

8. p 口⊥.                      truth-Truth-functionally from 3,6,7, and 4

9. ¬口⊥ p.                       truth-Truth-functionally from 8 and 1

10. 10.¬口⊥ p                 by (iv) from 9

11. 11.¬口⊥ ¬¬口⊥.            truth-Truth-functionally from 8 and 10

(We have omitted outermost parentheses in (1) through (11).)

Thus if ¬口⊥, then both ¬¬口⊥, by (11), and ¬口⊥, by (i), whence , by the propositional calculus. So if / , then / ¬口⊥ .

https://blog.sciencenet.cn/blog-2322490-1372836.html

## 全部精选博文导读

GMT+8, 2023-3-26 03:53