Wilfried Sieg引读[1]:

两位年轻的逻辑学家在1931年初交换了两封信，他们的工作对严峻的逻辑产生了巨大的影响。雅克-埃尔布朗于4月7日发起了这一交流，而库尔特-哥德尔则于7月25日作出了回应，此时埃尔布朗在拉贝拉尔德(Isere)发生登山事故仅两天。埃尔布朗的信在可计算性理论的发展中发挥了重要作用。哥德尔在他1934年的普林斯顿演讲中以及在后来的场合都肯定，这封信向他建议了一般递归函数定义的一个关键部分。详细了解这一作用是非常有意义的，因为这一概念是绝对的核心。这封信的全文直到最近才有，而且其内容（如哥德尔所报告的）与埃尔布朗同时代发表的作品不一致，这封信反映了当时更广泛的知识潮流：它们与不完备性定理的讨论及其对希尔伯特计划的潜在影响密切相关。

一，埃尔布朗给哥德尔的信

I. Herbrand to Godel 

Dear Mr Godel,

I am sending you, at this same time, reprint of some my papers in mathematical logic. Mr. von Neumann had spoken to me of your work and recently Mr Bernays showed me a set of proofs of your next paper. It was of great interest to me, and here I would like to make a few remarks that your results bring to my mind.

我同时给你寄去我在数理逻辑方面的一些论文的重印本。 von Neumann 先生曾向我谈起过您的工作，最近 Bernays 先生给我看了您下一篇论文的一组证明。我对这篇论文很感兴趣，因此，在这里，我想说说我对您的结果的一些看法。

Let us consider arithmetic; I would first of all like to write down its axioms precisely. In them we have only one type of variables, a constant 0, a function x+1, and a primitive expression x=y. We have the usual axioms :

让我们考虑算术；我首先想精确地写下它的公理。在其中，我们只有一种类型的变量，一个常数0，一个函数x+1，以及一个原始表达式x=y。我们有通常的公理：

all the logical axioms

x=x x=y ⊃ y=x   x=y x y=z  ⊃ x=z      （I）

x+1 /= 0

x+1 = y+1 = x=y

and the axiom of complete induction（完全归纳法）:

Φ0 x (x)Φx ⊃ Φx+1 ⊃ (x)Φx                （2）

Let us call this axiom (2’) when we require that no bound variables (no existential or universal quantifiers) occur in Φx.

当我们要求Φx中不出现任何约束变量（无存在或全称量词）时，让我们把这个公理称为（2’）。

In arithmetic we have other functions as well, for example functions defined by recursive, which I will define by means of the following axioms. Let us assume that we want to define all the functions fn(x1,x2,…,xpn) of a certain finite or infinite set F. Each fn(x1…) will have certain defining axioms; I will call all these axioms (3F). These axioms will satisfy the following conditions :

在算术中，我们也有其他的函数，例如由递归定义的函数，我将通过以下公理来定义。让我们假设我们要定义某个有限或无限集合F的所有函数fn(x1,x2,…,xpn)。每个fn(x1...)都将有某些定义公理；我将把所有这些公理称为(3F)。这些公理将满足以下条件：

1）The defining axioms of fn contain, besides fn, only functions of smaller index.

2）These axioms contain only free variables and constants.

3）We must be able to show, by means of intuitionistic proofs, that it is possible to compute with these axioms the value of the functions univocally for each particular system of values of their arguments.

1）fn的定义公理除了fn之外，只包含较小索引的函数。

2）这些公理只包含自由变量和常数。

3）我们必须能够通过直觉证明（intuitionistic proofs）指出，用这些公理有可能确定计算每个特定数系的函数的值。

We have e.g. the following examples :

例如，我们有以下的例子。

a) The functions x+y and x.y, which constitute the set E1, that are defined by means of the following axioms :构成集合E1的函数x+y和x.y，是通过以下公理来定义的：

x+0 = x   x+(y+1)=(x+y)+13’ oder 3E1

x.0=0   x.(y+1)=xy + x

b) Your recursive functions, Φ(x1, x2, …xn), (I shall denote their set by E2), defined by means of the following axioms :

您的递归函数，Φ(x1, x2, ... xn)，(我将用E2表示它们的集合)，通过以下公理来定义：

Φ(0, x2, …xn) = Ψ(x2, …xn)3’’ oder 3E2

Φ(k + 1, x2, …xn) = μ(k, Φ(k, x2, …xn), x2, …xn).

c) In my general scheme, however, many other functions can be defined; let’s take, for example, the Hilbert function Φ(a, a,a) (in his paper « On the infinite »), which is defined by means of the following axioms :

然而，在我的一般方案中，可以定义许多其他函数；让我们以希尔伯特函数Φ(a,a,a)为例（在他的论文《论无限》中），它是通过以下公理来定义的：

The Hilbert function is Φ(a, a,a), where we have:

希尔伯特函数为Φ(a,a,a)，其中我们有：

Φ(n+1, a,b) = Φ(n, a, Φ(n+1, a,b-1))

Φ(n, a,0) = a

Φ(0, a,b) = a+b

1) We note first of all that every intuitionistic proof can be carried out in an arithmetic that has only the axioms I, 2’, and 3 F for a certain set F of functions (which depends on the proof). And each proof in this arithmetic, which has no bound variables, is intuitionistic - this fact rests on the definition of our functions and can be seen immediately.

我们首先注意到，每个直觉证明都可以在一个算术中进行，这个算术只有公理I，2'和3 F，用于某个函数集F（这取决于证明）。而在这个没有约束变量的算术中，每个证明都是直觉的—这个事实建立在我们的函数定义上，可以立即看到。

I will denote a theory with the axioms I, 2’, and 3 F by I+2’+3F.

我将用I+2’+3F表示一个具有公理I、2’和3F的理论。

2) It follows immediately from my methods that all these theories I+2’+3F are consistent (if we use bound variables).

从我的方法中立即可以看出，所有这些理论I+2'+3F是一致的（如果我们使用约束变量）。

3) You have proved that, if your method can be applied to an arithmetic that has the functions E1, the functions E2 are needed (in order to construct your functions). In general, if we want to apply your methods to an arithmetic that has the functions of a set F, we need a large set of functions. (This can be proved precisely: it is very easy.)

您已经证明，如果您的方法可以应用于一个有函数E1的算术，那么就需要函数E2（为了构造您的函数）。一般来说，如果我们想把您的方法应用于一个具有集合F的函数的算式，我们需要一个大的函数集。(这可以精确地证明：这非常容易）。

4) You prove that I+2+3’’ is equivalent to I+2+3’ (but one cannot prove that I+2’+3’’ is equivalent to I+2’+3’’). Mr. Bernays told me that he has proved the consistency of I+2+3’’. By your methods it follows that his proof is not formalizable in I+2+3’, and also not in I+2+3’’; in other words, in his proof there must be certain functions that are not deductible to addition and multiplication (as your recursive functions are). In my proof, on the contrary, that need not be the case.

您证明了I+2+3''等价于I+2+3''（但不能证明I+2'+3''等价于I+2'+3'' ）。 Bernays 先生告诉我，他已经证明了I+2+3’'的一致性。按照您的方法，他的证明在I+2+3'中不可形式化，在I+2+3''中也不可形式化；换句话说，在他的证明中，一定有某些函数不能演绎为加法和乘法（正如您的递归函数那样）。相反，在我的证明中，情况不需要如此。

We easily see, however, that many functions other than the recursive functions are reducible to addition and multiplication. I haven’t at all succeeded in devising a function that does not have this property. An example of such a function (which must be extracted from Bernays’ proof) would be very interesting.

然而，我们很容易看到，除了递归函数之外，许多函数都可以还原为加法和乘法。我完全没有成功地设计出一个不具有这种性质的函数。这样一个函数的例子（必须从伯纳斯的证明中提取）将是非常有趣的。

5) I am thus led to the following remark: I do not at all understand how it is possible that there are intuitionistic proofs that are not formalisable in Russell’s system; in other words, how there can be an arithmetic with the axioms I+2+3F that is not translatable into that system. Only an example could convince me of that; I do not believe, however, that it can be proved that every intuitionistic proof is formalisable in Russell’s system, and that for the following reasons :

因此，我被引向以下评论：我完全不明白，怎么可能有直觉证明在罗素的体系中是不可形式化的；换句话说，怎么可能有一个具有公理I+2+3F的算术是不可翻译到该体系的。只有例子可以让我相信这一点；然而，我不相信可以证明每个直觉证明在罗素的系统中是可形式化的，而且，由于以下原因：

Let us assume that we have a certain set E of functions, with certain axioms, such that we can always ascertain whether certain defining axioms are among those axioms or not. Under these conditions, we can always define other functions that differ from all the preceding ones. We see that by means of the diagonal procedure : we can always describe, intuitionistically, a procedure for writing all the functions that have only one variable and are built up by means of the function Ee (through substitution) in the form fn(x) (n=1,2,3,…); the function fn(n)+1 then differ from all the others and from all their combinations. (In order to apply your methods to an arithmetic that contains all the functions of the set E, we must always construct such functions - from that follows what I said in 2.)

让我们假设，我们有一定的函数集E，有一定的公理，这样我们总能确定某些定义公理是否在这些公理之中。在这些条件下，我们总是可以定义与前面所有的函数不同的其他函数。我们看到，通过对角线程序：我们总是可以直观地描述一个程序，来写出所有只有一个变量并通过函数Ee（通过替换）建立起来的函数的形式fn(x) (n=1,2,3,...)；然后函数fn(n)+1与所有其他函数以及它们的所有组合不同。(为了将你的方法应用于包含集合E的所有函数的算术，我们必须始终构建这样的函数--由此得出我在2中所说的。)

In other words, it is impossible to describe exactly all the procedures for constructing function intuitionistically: When we describe such procedures, there are always functions that cannot be constructed by means of those procedures; the intuitionistic methods cannot be described in a finite number of words. This fact seems very remarkable to me.

换句话说，我们不可能准确地描述所有直觉构建函数的程序。当我们描述这样程序时，总有一些函数不能通过这些程序来构建；直觉方法不能用有限的文字来描述。这个事实在我看来是非常了不起的。

It reinforces my conviction that it is impossible to prove that very intuitionistic proof is formalisable in Russell’s system, but that a counterexample will never be found. There we shall perhaps be compelled to adopt a kind of logical postulate.

它加强了我的信念，即不可能证明直觉证明在罗素的系统中是可形式化的，但一个反例将永远不会被发现。在那里，我们也许将被迫采用一种逻辑公设。

Please excuse these long considerations, which, because of my poor knowledge of the German language, are perhaps to completely clear. But in these questions there are still many mysterious facts, and this question of the formalisation of intuitionistic proof seems to me to be very important for the philosophical signification of metamathematics.

请原谅这些冗长的考虑，由于我的德语知识贫乏，这些考虑也许并不完全清楚。但在这些问题中仍有许多神秘的事实，而且在我看来，直觉证明的形式化问题对元数学的哲学意义非常重要。

Respectfully yours,

J. Herbrand

二，哥德尔给埃尔布朗的信

II. Godel to Herbrand

Dear Mr. Herbrand,

Thank you very much for your interesting letter, as well as for kindly sending [me] the reprints of your papers. I was already familiar with your « Thèses » earlier, and the methods developed therein for consistency proofs seem to me to be very important and up to now the only ones which have led to positive results for more extended systems.

非常感谢你有趣的来信，也感谢你友好地将你的论文重印本寄给我。我早先就熟悉你的 "论文"，其中开发的一致性证明方法在我看来是非常重要的，而且是到目前为止唯一能够为更多的扩展系统带来积极结果的方法。

I would like now to enter into the question of the formalizability of intuitionistic proofs in certain formal systems (say that of Principia mathematica), since here there appears to be a difference of opinion. I think, insofar as this question admits a precise meaning at all (due to the undefinability of the notion « finitary proof », that could justly be doubted), the only correct standpoint can be that we admit not knowing anything about it. Indeed, you are of the opinion (just as I am) that an exhaustive definition of the notion « finitary proof » is impossible. That is, to say, it goes beyond the bounds of mathematics (or also just that of the arithmetic I+2+3’ in your letter); but from that nothing at all follows about the further course of the process, whose overall extent we just do not survey. 

我现在想谈谈直觉证明在某些形式系统（例如《数学原理》）中的可形式化问题，因为这里似乎存在着意见分歧。我认为，只要这个问题有确切的含义（由于“有限证明”这一概念的不可控性，这一点是值得怀疑的），唯一正确的立场就是我们承认对它一无所知。事实上，你认为（就像我一样），对“有限证明”这一概念的详尽定义是不可能的。也就是说，它超出了数学的范围（或者在你的信中只是算术I+2+3’的范围）；但从这一点来看，关于这个过程的进一步发展，我们根本就没有调查其总体范围。

Even your presentation of finitary arithmetic in no way convinces me otherwise. For even if we admit that every intuitionistic proof can be carried out in one of the systems I+2’+3F (which seems not at all obvious to me), the question still always remains open whether the intuitionistic proof that are required in each case to justify the unicity of the recursion axioms are all formalisable in Principia mathematica. Clearly I do not claim either that it is certain that some finitary proofs are not formalisable in Principia mathematica, even though intuitively I tend toward this assumption. In any case, a finitary proof not formalizable in Principia mathematica would have to be quite extraordinarily complicated, and on this purely practical ground there is very little prospect of finding one, but that, in my opinion, doesn’t alter anything about the possibility in principe.

即使你对有限性算术的介绍也不能使我信服。因为即使我们承认每一个直觉证明都可以在I+2'+3F系统之一中进行（这对我来说似乎一点也不明显），问题仍然始终是开放的，即在每种情况下为证明递归公理的统一性而需要的直觉证明是否都可以在数学原理中形式化。显然，我也没有声称某些有限性证明在《数学原理》中肯定是不可形式化的，尽管直觉上我倾向于这种假设。无论如何，在《数学原理》中不可形式化的有限证明必须是非常复杂的，在这个纯粹的实践基础上，找到一个有限证明的前景非常渺茫，但在我看来，这并不改变原则上的可能性。

Concerning your note in the Comptes rendus of 14 October 1929, I would like to add the following remark : I assume that in the proof of proposition b) under 2, you have presupposed that the consistency proof and the decision problem are settled by the logical means of Principia mathematica. But now, through my work it is shown that this presupposition can never apply. A proof of proposition b) without the aforementioned presupposition, that is, solely under the assumption that the consistency problem and the decision problem are settled by intuitionistic means, hardly seems possible to me.

关于你在1929年10月14日《汇辑》中的说明，我想补充以下几点：我假定在2下的命题b)的证明中，你预设了一致性证明和决定问题是通过《数学原理》的逻辑手段解决的。但现在，通过我的工作表明，这个预设永远不可能适用。在没有上述预设的情况下对命题b)的证明，也就是说，仅仅在一致性问题和判定性问题是由直觉主义手段解决的假设下，在我看来是不可能的。

I did not completely understand the remark in your letter that for the application of my methods to an arithmetic system, functions going beyond that system are always required. Rather, this going beyond is only required for the consistency proof. By contrast, the proposition « If the system is consistent, then the proposition stated by me is unprovable » can be proved within that same system.

我并不完全理解你信中所说的，为了将我的方法应用于一个算术系统，总是需要超越该系统的函数。相反，这种超越只对一致性证明有要求。相比之下，“如果系统是一致的，那么我所说的命题是无法证明的”这一命题可以在同一系统内证明。

With regard to our correspondence, I would like to suggest that each of us write in his mother tongue, in oder to spare unnecessary trouble.

关于我们的通信，我想建议我们每个人都用母语来写，以避免不必要的麻烦。

I thank you again for your kind letter, the belated response to which I ask you to excuse.

我再次感谢您的信，请您原谅我迟来的答复。

参考文献：

【1】Kurt Gödel: Collected Works: Volume V, Volume 5 (p.3-14)

https://books.google.fr/books?id=4rTYxQEACAAJ&printsec=copyright&redir_esc=y#v=onepage&q&f=false