“形式主义的内在局限- 研究哥德尔定理和相关定理在数学基础理论中的意义”一书的作者让-拉德里埃（Jean Ladrière，1921-2007），比利时哲学家、逻辑学家和卢万天主教大学的教授，他曾是高等哲学研究所的主席。

一，前言

1，译文

在过去的半个世纪里，数学基础研究经历了相当大的发展，给哲学批评带来了新的任务。如果不考虑新的基础科学所取得的所有成果，就不可能再质疑数学对象的性质或数学思维的过程，这要归功于逻辑学家和关注其科学合理性的数学家的共同努力。这些努力不仅有助于澄清旧问题，而且也使哲学不可忽视的新问题得以曝光。正是通过基础科学的成果，哲学批评必须恢复对数学本质的思考。

在基础科学所依据的并成功赋予其精确内容的基本思想中，形式系统（或形式主义）的思想起着特别重要的作用。

为了克服数学思想在19世纪末遇到的困难，不再可能满足于那时充分的定义和证明的过程，它们需要太多的直觉；必须对概念和方法进行严格的分析。

人们很快意识到，这样的分析不能直接进行，必须绕道而行：在能够研究某一特定数学理论（如算术、几何或分析）的属性之前，必须将其具体化为一种有形的形式，让人一眼就能看到。因此，有了使用形式化方法的想法。形式化实际上是一个遵循精确操作规则的符号系统：它作为一个具体的对象出现，其结构可以以详尽的方式进行研究。如果人们成功地用一个形式化系统来表示自己希望研究的数学理论，就会把对这一理论的性质的研究简化为对这一形式化系统的性质的研究，从而可以获得完全令人满意的严格的结果。

从这一想法出发，基础科学被引导提出两种问题：数学理论在多大程度上可以用形式化系统来表示—用什么方法可以研究这些形式化系统的特性？起初，一个形式系统似乎被认为是一个相对简单的对象，人们倾向于相信对其属性的研究不会带来太大的困难。基础科学的历史很快就就推翻了这种观点，人们意识到，形式化的方法有其局限性：人们对形式主义的属性所能获得的知识是有局限性的，这些局限性是由形式主义的性质决定的。

当时，有一些属于基础科学的定理确立了此局限的事实，最重要的是哥德尔定理，并由他在1931年证明。这些结果澄清了形式化方法的意义，并限定了可以从它那里得到的预期，对哲学批评具有很大的意义。然而，我们必须小心，不要从它们中得出太多的东西，例如，不要声称从哥德尔定理中推导出关于一般数学思想的本质不完全性的过于草率的结论。本工作的目的是研究这些局限的定理的意义，它的主要部分是对这些定理的阐释。由于哥德尔定理在这些定理中起着主要作用，所以介绍的内容以该定理和相关定理为中心，此书并不以严谨的数理逻辑技术研究的形式出现，然而它试图尽可能地接近事实。它的目的是提出某些哲学问题，如果不考虑所研究的事实的准确表述，就有可能误解其真实范围。它们的表述服从双重要求：不预设读者方面的任何事先的数学逻辑知识，但又要足够深入到证明的机制中去，以便对它们有一个确切的概念。因此，以下几页指出了对于完整理解限制性的主要定理来说，什么是必要和充分的。

在本书的编写过程中，只考虑到了截至1956年3月发表的作品。

2，目录：

一、导言： 形式系统

二、形式系统与元理论 

三、哥德尔定理

四、哥德尔定理的直接一般化

五、哥德尔推论与证明理论 

六、丘奇定理与判定问题

七、Kleene的谓词理论

八、语义方法，Tarski定理和 MOSTOWSKI定理

九、局限性的其他事实

十、哲学建议

3，前言的原文

Les limitations internes des formalismes - Etude sur la signification du théorème de Godel et des théorèmes apparentés dans la théorie des fondements des mathématiques

Avant-Propos

Le développement considérable que connaissent, depuis un demi-siècle, les recherches sur les fondements des mathématiques impose à la critique philosophique des taches nouvelles. Il n’est plus possible, désormais, de s’interroger sur la nature des objets mathématiques ou sur les procédés de la pensée mathématiques sans tenir compte de tous les résultats qui ont été obtenus par la nouvelle sciences fondements, grace aux efforts conjugués des logiciens et de mathématiciens soucieux de la solidité de leur science. Ces efforts n’ont d’ailleurs pas seulement contribué à préciser et à clarifier d’anciens problèmes ; ils ont fait apparaître des problèmes nouveaux qu’il n’est pas permis à la philosophie d’ignorer. C’est désormais à travers les acquisitions de la science des fondements que la critique philosophique doit reprendre sa réflexion sur la nature des mathématiques.

Parmi des idées de base sur lesquelles s’est appuyée la science des fondements et auxquelles elle a réussi à donner un contenu précis, l’idée de système formel (ou formalisme) joue un rôle particulièrement important. 

Pour surmonter les difficultés auxquelles s’était heurtée la pensée mathématique à la fin du 19e siècle on ne pouvait plus se contenter des procédés de définition et de démonstration qui avaient suffi jusque là et qui demandaient trop à l’intuition ; il fallait soumettre les concepts et les méthodes à une analyse rigoureuse.

On s’aperçut rapidement qu’une telle analyse ne pouvait se faire directement, qu’un détour était nécessaire : avant de pouvoir étudier les propriétés d’une théorie mathématique déterminée (comme l’arithmétique, la géométrie ou l’analyse), il faut la matérialiser sous une forme tangible, immédiatement accessible au regard. D’où l’idée du recours à la méthode de formalisation. Un formalisation se présente en effet comme un système de symboles soumis à des règles précises de manipulation : il apparaît comme un objet concret dont on peut étudier la structure de façon exhaustive. Si l’on réussit à représenter la théorie mathématique que l’on désire étudier au moyen d’un système formel, on ramène l’étude des propriétés de cette théorie à l’étude des propriétés de ce système formel, et on peut ainsi obtenir des résultats d’une rigueur tout à fait satisfaisante.

Partant de cette idée, la science des fondements a été amenée à se poser deux catégories de questions :

dans quelle mesure peut-on représenter les théories mathématiques au moyen de systèmes formels - et par quelles méthodes peut-on étudier les propriétés de ces systèmes formels ? On semblait considérer, au début un système formel comme un objet relativement simple et on était enclin à croire que l’étude de ses propriétés ne pouvait offrir de bien grandes difficultés. L’histoire de la science des fondements devait rapidement démentir cette opinion. On s’aperçut que la méthode de formalisation à ses limites : il y a des limites à la connaissance que l’on peut acquérir des propriétés d’un formalisme, et ces limites tiennent à la nature des formalismes.

Il existe à l’heure actuelle un certain nombre de théorèmes appartenant à la science des fondements qui établissent des faits de limitation. Le plus important est un théorème dû à Godel, et démontré par lui en 1931. Ces résultats, qui précisent le sens de la méthode formelle et circonscrivent ce qu’on peut en attendre, sont d’un très grand intérêt pour la critique philosophique. Il faut se garder cependant de vouloir trop en tirer et de prétendre par exemple déduire du théorème de Godel des conclusions trop hatives sur le caractère d’essentiel inachèvement de la pensée mathématique en général. L’objet du présent travail est d‘étudier la signification de ces théorèmes de limitation. La plus grande partie en est consacrée à un exposé de ces théorèmes. Comme le théorème de Godel joue parmi ceux-ci un rôle capital, c’est avant tout sur ce théorème et sur les théorèmes apparentés qu’est centré l’exposé. Celui-ci ne se présente nullement comme une étude technique rigoureuse d logique mathématique. IL s’efforce cependant de serrer les faits d’aussi près que possible. Il est destiné en effet à suggérer certains problèmes philosophiques. Et on risquerait de se méprendre sur la portée réelle des faits étudiés si on ne les considérait dans leur formulation précises. Leur présentation obéit à une double exigence : ne présupposer, de la part du lecteur, aucune connaissance préalable de logique mathématique, et pénétrer cependant assez loin dans le mécanisme des démonstrations pour en donner une idée exacte. Les pages qui suivent indiquent donc ce qui est nécessaire et suffisant à une complete intelligence des principaux théorèmes de limitation.

Il n’a été tenu compte, dans la préparation de cet exposé, que des travaux parus jusqu’en mars 1956.

参考文献：

【1】https://books.google.fr/books/about/Les_limitations_internes_des_formalismes.html?id=bbShuNEmF3UC&redir_esc=y

【2】https://fr.wikipedia.org/wiki/Jean_Ladrière