一，译文

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

首先，当我说“证明”时，我的意思是“在整个数学的帮助下证明”。那么现在，大家都知道：二加二等于四。当然，二加二等于四是可以证明的（正如我所说的，借助于整个数学来证明，虽然对于二加二，我们并不需要整个数学来证明它是四）。

然后，也许不是那么明显，二加二等于四是可以证明的这命题也是可以证明的。而且二加二等于四是可以证明的这命题是可以证明的命题，也是可以证明的，以此类推。实际上，如果一个说法是可以证明的，那么它是可以证明的这命题就是可以证明的。而这命题也是可以证出的。现在，二加二不等于五，而且可以证明，二加二不等于五是可以证明是可以证明的，以此类推。

因此：可以证明二加二不等于五。是否也能证明二加二等于五呢？如果可以的话，至少可以说是对数学的一个真正打击。如果可以证明二加二等于五，那么就可以证明五不等于五，那么就没有什么不能证明的了，数学也就会是一堆垃圾。

那么，我们现在想问，能不能证明不能证明二加二等于五？令人吃惊的是：不，不能证明。或者悠着点的说法是：如果二加二等于五是不可以证明的命题是可证明的，那么也可以证明二加二是五，于是数学就会是一堆垃圾。事实上，如果数学不是一堆垃圾，那么任何“主张X不能被证明”这样的命题不能被证明。因此，如果数学不是很多垃圾，那么就不会有哪个“某某说法没法证出”的说法是可以证出的。那么，虽然不能证明二加二等于五，但也不能证明不能证明二加二等于五。顺便说一下，如果你想知道：是的，可以证明，如果可以证明不能证明二加二是五，那么就可以证明二加二是五。

“我希望他能解释他的解释”（I wish he would explain his explanation）

如果，正如我们将假设的那样，整个数学可以被形式化为通常的那种形式理论（这不是一个小的假设），那么就有从对该理论的适当描述（“作为”形式理论）中获得的语言的一个公式Proof(x,y)，它满足以下条件：

1. if ⊢ p, then ⊢ 口p,

2. (ii) ⊢(口(p →q) →(口p →口q), and

3. (iii) ⊢(口p →口口p)

对于语言中的所有句子p，q。我们把 : 口p 简称为 : ∃xProof(x, ‘p’)，其中’p'是句子p在语言中的标准表示。（'p'可能是p的哥德尔数）。⊢是一个介词短语（我们的语言），意思是“在理论中可以证明”。

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

条件(i)、(ii)和(iii)被称为Hilbert-Bernays-Löb可推导性条件；它们被所有合理的形式理论所满足，其中有一定数量的算术可以被证明。

由于该理论是标准的，其语言中的所有重言式在该理论中都是可证明的，其语言中的所有可证明的逻辑后果都是可证明的。

由此可见，对于所有的句子p，q ,

(iv) if ⊢(p →q), ⊢(口p →口q)

因为：如果⊢(p →q)，那么根据(i)，⊢口(p →q)；但根据(ii)，⊢(口(p →q)→(口p →口q)，然后⊢(口p →口q)通过modus ponens。

⊥是零元的真-函数连接词，总是为假。当然，⊥是一个矛盾。我们稍后将需要观察（¬q→（q→ ⊥））是一个重言式。如果⊥不是语言的基本符号之一，它可以被定义为任何可反驳的句子，例如，表达二加二等于五的句子。

借助于⊥，有一种简单的方法表达“理论是一致的”：/⊢⊥，也就是说，⊥在理论中是不可证明的。因此，说理论是一致的语言的句子可以被看作是¬口⊥，它与¬∃xProof(x, '⊥')相同。

我们可以证明哥德尔的第二不完全性定理，以及第二不完全性定理在理论中可以证明的定理（“形式化的第二不完备性定理”），如下。

通过Godel (1931)在《论形式上不可判定的命题......》中提出的对角线化技术，可以找到一个在理论中与p在理论中不可证明的声明等价的句子p，即一个句子，如 ：

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)中最外层的括号)。

因此，如果⊢¬口⊥，那么根据(11)的⊢¬口¬口⊥与根据(i)的⊢口¬口⊥同时成立，所以根据命题计算，⊢⊥。所以如果/⊢ ⊥，那么/⊢¬口⊥。

二，原文（Jan., 1994）

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 /⊢ ¬口⊥ .

参考文献：

【1】https://zh.wikipedia.org/zh-cn/%E5%8F%B2%E4%B8%8A%E6%9C%80%E9%9B%A3%E9%82%8F%E8%BC%AF%E8%AC%8E%E9%A1%8C

【2】https://www.jstor.org/stable/2253954?seq=1#metadata_info_tab_contents