Navigation – Plan du site

« Je le vois, mais je ne le crois pas... ». Preuves et vérités dans les sciences formelles

Henri Volken
p. 145-160

Texte intégral

1Dans le cours d’une argumentation, la preuve devrait fournir un moyen indiscutable d’établir la vérité. Cela implique, que dès l’apparition de la preuve d’une affirmation, celle-ci devrait être acceptée par tous les interlocuteurs. Détenir une preuve reviendrait à posséder une stratégie gagnante dans une discussion contradictoire. Convaincre consisterait donc simplement à construire et présenter des preuves.

2Pourquoi les choses ne sont-elles pas si simples, notamment dans les sciences sociales et les sciences humaines ? Tout d’abord cette situation idéale exige de la part des interlocuteurs de partager un langage univoque, dont la sémantique soit acceptée par tous. Ensuite il faut une logique commune, c’est-à-dire un ensemble de règles partagées, qui permettent de déduire un énoncé à partir d’un ensemble d’autres énoncés. Ces deux conditions ne sont probablement remplies que dans des sciences formelles comme les mathématiques, dont l’univers se compose d’objets abstraits, donc simples, même si la nature de ces objets et les liens qu’ils entretiennent avec la réalité reste le sujet de savantes controverses. Cela n’est possible que parce que les objets mathématiques sont créés en quelque sorte par les définitions que les mathématiciens en donnent, et n’ont pas de substrat matériel. La physique par exemple, pourtant proche des mathématiques par son formalisme et son langage, utilise en plus des preuves, la vérification expérimentale pour étayer son argumentation.

3Les sciences sociales semblent avoir d’autres priorités que de favoriser un langage commun. La notion de preuve y joue donc nécessairement des rôles différents, beaucoup plus dépendants des contextes, comme l’illustre clairement ce colloque. Nous allons néanmoins présenter la nature et le statut de la preuve dans les sciences formelles, non pas pour en faire un idéal pour les sciences sociales, mais pour approfondir le concept et en montrer la force et aussi les limitations dans un cadre strict. Certains aspects de la recherche d’une preuve ou, au contraire, de la difficulté ou l’impossibilité d’établir une preuve, peuvent par analogie, influencer la démarche et la méthode d’autres sciences, plus éloignées par leur nature des mathématiques et de la logique.

4Le but de ce travail serait atteint, s’il permettait de voir que la quête d’une preuve en mathématiques, est une activité créatrice, essentiellement humaine – parfois ludique – et basée sur l’intuition, mais que la preuve elle-même une fois trouvée, est rigoureuse et indiscutable. Une petite restriction à ce tableau subsiste cependant et indique que malgré tout, ce sont les conventions intellectuelles partagées des protagonistes qui permettent l’insolente solidité de la preuve mathématique. Nous pensons que le portrait qui suit, montrant les diverses facettes et la complexité de la notion de preuve dans les sciences formelles, peut présenter un intérêt certain pour l’analyse de la démarche argumentative dans les sciences sociales – ne serait-ce que par la confrontation d’approches radicalement différentes. Et c’est peut-être l’évocation des limites de la preuve, lorsque celle-ci tente de capter l’idée du vrai dans notre monde réel, qui peut intéresser les chercheurs des disciplines non formelles. Car c’est précisément cette limitation qui rend plus précise et complète l’image d’un concept guetté par la polysémie. Alors, qu’est-ce qu’une preuve dans le monde formel des mathématiques ?

La preuve comme construction

5Parmi les questions que Piaget posait à des enfants lors de ses expé-riences sur le développement de l’intelligence, il en est une qui semble un peu saugrenue au premier abord. Dans cette expérience, Piaget montrait à l’enfant un bouquet de fleurs, contenant enre autres des roses et demandait alors : « Ce bouquet contient-il plus de roses ou plus de fleurs ? ». Il s’agissait dans cette expérience de tester la compréhension de l’enfant de la notion de « sous-ensemble », de « cardinal d’un sous-ensemble » et surtout de la relation entre le cardinal du sous-ensemble par rapport au cardinal de l’ensemble. Or si la réponse est simple en ce qui concerne les fleurs, la question n’est pas innocente, notamment lorsqu’on la pose à propos d’ensembles infinis. Cette dernière remarque nous ramène à Georg Cantor.

6Au milieu du XIXe siècle, le mathématicien allemand Cantor, créateur de la théorie des ensembles, entreprit de clarifier la notion d’infini qui jusque-là n’apparaissait en mathématiques que sous une forme négative, dans le sens de « non-fini », ou alors sous la dichotomie « infini actuel – infini potentiel » qui exprimait plutôt un embarras devant la possibilité de l’existence réelle d’une forme d’infini. Dans le cours de ses recherches Cantor en est venu à se poser la question suivante : Y a-t-il plus de points sur un segment de longueur 1 ou dans un carré de côté 1 ? La question est analogue à celle posée par Piaget, puisque le segment se retrouve dans le carré, mais elle concerne cette fois des ensembles infinis (voir fig. 1).

  • 1 En français dans le texte.

7La réponse qui s’est imposée à Cantor – il y a exactement autant de points sur la droite que dans le carré ! – est dérangeante à plus d’un titre. En premier lieu elle contredit notre intuition sur les notions de « autant » et de « contenu dans ». Car après tout, il y a au moins autant de points dans le carré que sur le segment, celui-ci étant contenu dans le carré. Elle met d’autre part en doute notre concept géométrique de « point » et le rapport de celui-ci avec « droite » et « carré ». La notion de « dimension » elle-même semble paradoxale à la vue de ce résultat. Cantor fut effrayé par cette réponse que sa croyance rejetait mais que sa raison dut admettre, parce qu’il avait découvert une preuve irréfutable qui ne lui permettait pas de douter de sa véracité. Dans une lettre du 29 juin 1877 à son collègue Dedekind, il rend compte de son désarroi par les simples mots1 : « Je le vois, mais je ne le crois pas... ».

Fig. 1 – Le problème de Cantor

Fig. 1 – Le problème de Cantor
  • 2 Nous allons adopter la convention suivante : « démonstration » désignera la procédure argumentative (...)

8Cet exemple illustre l’importance et le pouvoir que le concept de « preuve » ou de « démonstration » possède – en tout cas – dans le domaine des sciences formelles. Une simple preuve peut surmonter toutes les croyances contraires. Mais qu’est-ce exactement qu’une preuve ? Quelle est sa nature ? Quels sont les critères sur lesquelles elle repose ? Nous allons poursuivre l’exemple de Cantor en montrant les grandes lignes de sa démonstration2.

  • 3 Nous passons sous silence un petit point technique qui n’a aucune influence sur la démonstration.

9La démonstration est constituée par la construction d’une simple corres-pondance, univoque dans les deux sens, entre les points du segment et les points du carré3. A chaque point P du segment on attribue un point P’ du carré et réciproquement. Voici les détails, dans les deux directions :

Coordonnée de P : x = 0.x1x2x3x4x5x6 ...

Coordonnées de P’ : x9 = 0.x1x3x5x7x9x11... et y9 = 0.x2x4x6x8x10x12 ...

Coordonnées de P’ : x9 = 0.x1x2x3x4x5x6 ... et y9 = 0.y1y2y3y4y5y6 ...

Coordonnée de P : x = 0.x1y1x2y2x3y3 ...

10Cantor a utilisé les mêmes idées dans un exemple encore plus simple et tout aussi troublant et paradoxal pour notre intuition. Il montre en effet qu’il y a autant de nombres qu’il y a de nombres pairs ! La correspondance explicite suivante en donne la démonstration :

Fig. 2 – Le « paradoxe » de Cantor

Fig. 2 – Le « paradoxe » de Cantor

11Ainsi à chaque nombre correspond son double et à chaque nombre pair sa moitié. La correspondance est parfaite ! Piaget pourrait donc proposer un bouquet de fleurs numérotées en suivant à partir de 1, dans lequel les roses se trouveraient uniquement aux emplacements pairs. Il y aurait, d’après le résultat de Cantor, dans ce bouquet, qui contient une infinité de fleurs qui ne sont pas des roses, autant de roses que de fleurs...

12Construire un objet dont on affirme l’existence – ici une correspondance bi-univoque – constitue l’une des formes les plus élémentaires et indiscutables d’une démonstration. Elle est aussi l’une des formes privilégiées de la démon-stration mathématique, et se trouve à l’origine d’une branche des mathématiques dites « constructives ». Mais il existe d’autres principes encore sur lesquels s’appuie le concept de démonstration. La réduction à l’absurde est l’un de ces principes.

Reductio ad absurdum

4

13Ce principe consiste donc à se projeter dans un monde imaginaire – celui dans lequel l’énoncé à démontrer est faux – puis à argumenter jusqu’à l’apparition d’une contradiction. Cela permet alors d’affirmer que l’énoncé est vrai. Cette forme de démonstration est très répandue dans le monde des sciences, mais particulièrement dans les textes mathématiques. Le principe de la réduction à l’absurde est parfois associé dans une démonstration, au principe du tiers exclu, qui a une portée plus générale et qu’on retrouve dans l’argumentation courante. Il dit qu’un énoncé doit être vrai ou faux. Sa grande simplicité et apparente évidence font qu’il passe souvent inaperçu. Voici un exemple non trivial de son application et qui se pose dans la théorie des nombres : Peut-on trouver un nombre irrationnel qui, élevé à une puissance irrationnelle, donne un nombre rationnel ?

14Bien entendu, une telle démonstration n’est pas admise par les construc-tivistes, qui exigent la construction explicite d’une solution. Nous voyons donc que même dans un domaine aussi formalisé que les mathématiques, la notion de démonstration n’est pas absolue, mais reste tributaire des conventions adoptées.

transformerk

15L’idée de la transformation – si utile dans le processus de généralisation – exige une définition plus rigoureuse de la nature et des propriétés d’une démonstration. Ce travail sera réalisé par la logique formelle, qui donnera de la démonstration un équivalent formalisé : la preuve formelle. Avant de parler de la modélisation de la démonstration par la preuve formelle, nous allons évoquer un autre principe souvent utilisé par les mathématiciens, l’induction complète.

Induction complète

16A vrai dire l’induction complète des mathématiciens n’est pas un prin-cipe d’induction mais plutôt de déduction récursive. Il renvoie à l’image d’un alignement de dominos, dans lequel la chute de l’une des pièces provoque-rait la chute de la suivante. Il repose sur la propriété mathématique suivante :

Si un sous-ensemble de nombres naturels contient le 0 et pour chaque nombrequ’il contient, il contient également le successeur de celui-ci, alors ce sous-ensemble contient tous les nombres.

17Dans le cas où nous avons une infinité de propositions, numérotées par des nombres naturels, P(0), P(1), P(2),..., dont nous voulons montrer la vérité, le principe peut s’énoncer ainsi :

Si la proposition P(0) est vraie, et que la vérité de la proposition P(n) en-traîne nécessairement la vérité de la proposition P(n+1) pour n’importe quel n, alors toutes les propositions sont vraies.

18Nous allons illustrer l’application de ce principe par l’exemple suivant, très simple et tiré de la vie quotidienne. Est-il possible de payer n’importe quelle somme à l’aide de pièces de 2 frs et de 5 frs ? On voit immédiatement que les sommes 1 ou 3 sont des contre-exemples, mais au-delà de trois ? En réalité, à partir de 4, chaque somme (entière) peut être payée avec les pièces proposées. Mais comment s’en convaincre ? Voici une démonstration basée sur le principe de l’induction complète. Tout d’abord, il est possible de payer la somme de 4 frs à l’aide de deux pièces de 2 frs. Cela correspond à l’énoncé P(0). Supposons ensuite que ce soit vrai pour une somme de n frs. Nous allons montrer que c’est vrai dans ce cas, également pour la somme de n+1 frs. En utilisant le principe du tiers exclu, nous savons que les pièces utilisées pour former la somme n, ou bien ne comportent que des 2 frs ou alors il y a au moins une pièce de 5 frs parmi elles. Dans le premier cas on retire deux pièces de 2 frs et on les remplace par une pièce de 5 frs. Dans le deuxième cas, on retire une pièce de 5 frs et on la remplace par trois de 2 frs. Dans les deux cas le résultat est une somme de n+1. Donc dans tous les circonstances, on peut augmenter la somme de 1. L’induction complète permet alors de donner une réponse positive à la question du début.

Conceptions de la vérité

19Puisque la preuve doit convaincre de la vérité d’un énoncé, nous allons parler de l’utilisation de ce concept en mathématiques. On peut constater aisément que ce mot de « vérité » n’apparaît que rarement dans les textes des mathématiciens. En tout cas dans le sens absolu de « cette affirmation est vraie ». Il est bien plus souvent présent pour désigner une relation du type « cette affirmation est vraie dans le contexte... ». Et c’est bien dans cette acception relationnelle plutôt que monadique que le concept de vérité joue un rôle important en mathématiques. De la notion de « vérité » le mathématicien passe de préférence à celle de « vérité logique » comme nous allons le voir. Mais tout d’abord il est nécessaire de rappeler trois conceptions épistémologiques parmi les plus courantes de la notion de vérité. Selon le critère choisi pour traduire la notion intuitive de vérité, on peut distinguer les trois classes de théories de la vérité suivantes :

  • vérité-correspondance

  • vérité-cohérence

  • vérité-consensus

20Dans la première classe, on procède par l’établissement d’une correspondance entre une proposition et la réalité dont traite cette proposition. Il s’agit d’une approche sémantique et l’accent est mis sur l’interprétation des objets du langage dans un monde extérieur. On peut rattacher les noms de Russell, Wittgenstein et Tarski à cette approche.

21L’approche vérité-cohérence étudie la cohérence d’une proposition dans un système logiquement consistant et pour cela ne se base que sur des critères de forme. Il s’agit ici d’un point de vue syntaxique, dont Hilbert, Neurath et Rescher sont quelques-uns des tenants.

22Enfin, dans le troisième cas, la notion de « vrai » est attribuée à un énoncé s’il y a un consensus à ce sujet dans un cercle d’experts agréés. L’approche est cette fois clairement pragmatique. Des travaux dans cette direction se trouvent – entre autres – chez Peirce, Strawson et Prior.

23Cette distinction importante transparaît dans la formalisation de la notion de démonstration dans le contexte de la logique formelle. Elle permet de rendre compte des différentes formes que prend alors ce concept, et de la nature des liens qui les relient. Nous allons essentiellement parler de la vérité-correspondance et de la vérité-cohérence. Le point de vue pragmatique, qui n’est pas absent dans ces deux approches, fera l’objet de remarques ultérieures. La première de ces formalisations est basée sur la notion de vérité logique et de conséquence logique. Elle est d’ordre sémantique.

  • 5 Il s’agit en fait de la traduction d’un article en langue polonaise de 1933, très peu remarqué dans (...)

24La conception sémantique de la vérité est à l’origine de la théorie des modèles, cette branche de la logique mathématique qui modélise l’idée intuitive de « preuve » en utilisant les méthodes et les objets de la théorie des ensembles. C’est dans un article5 de Tarski de 1935 [6] qu’on trouve sa définition de la vérité, qui est à l’origine de la théorie des modèles :

6

25Le schéma de Tarski définit la vérité comme correspondance entre la signification d’un énoncé (et de ses éléments constitutifs) avec l’état du monde réel qu’il décrit. Cette définition se rapproche de la conception courante de ce qui est vrai et de ce qui est faux, tout en rendant cette conception formellement précise. Mais la vérité ainsi définie semble rester monadique alors que c’est la version relationnelle qui joue le rôle important dans les sciences formelles. Voici très schématiquement deux approches de la notion de vérité logique, celle de Bolzano et celle de Tarski, distantes l’une de l’autre de près d’un siècle.

  • 7 Cité dans [2].

26C’est en 1837 que Bolzano exprime sa vision de la vérité logique dans son livre Wissenschaftslehre. Ce qui paraît important dans la notion de vérité logique, ce n’est pas la dichotomie vrai/faux, mais les conditions dans lesquelles un énoncé reste vrai après substitution d’une partie de ses éléments. On peut citer l’exemple suivant de Bolzano7 : « Si Caius est un homme, alors Caius est mortel. » Cette phrase est vraie, quel que soit le nom qu’on substitue à « Caius ». Par contre, elle devient fausse, si l’on remplace « mortel » par « omniscient ». Dans l’exemple suivant, « la neige est blanche ou la neige n’est pas blanche » on peut substituer « neige » et on peut remplacer « blanche » sans altérer la vérité de la phrase. Pour tout changement de ce type, la phrase reste vraie. Par contre, si l’on substitue « et » à la place de « ou », l’énoncé devient faux. Selon Bolzano un énoncé est logiquement vrai s’il reste vrai après substitution d’une de ses parties qui n’est pas considérée comme fixe. La vérité logique dépend dans ce cas des parties de la proposition que l’on déclare fixe, ou immuable. Il s’agit donc bien d’un concept relationnel. La difficulté chez Bolzano est que, si le concept dépend des parties syntaxiques qu’on déclare comme fixes, il dépend également de la richesse du langage utilisé, c’est-à-dire du réservoir des termes qui peuvent intervenir dans une substitution. La solution de Tarski évite cet inconvénient en introduisant les notions de variable, de fonction prédicative et de satisfaction dans un modèle. Elle permet de définir le concept d’un énoncé « vrai dans le modèle... » ou « vrai dans le monde possible... », qui est la notion de « vérité logique » utilisée dans la théorie des modèles. Cette dernière est fortement ancrée dans un contexte mathématique ensembliste. C’est le prix à payer pour permettre une quantification sur les mondes possibles. Cette quantification est nécessaire pour définir la notion de conséquence logique, qui est le véritable concept-clé de la formalisation de la notion de preuve en logique mathématique.

Relation de conséquence logique

8modèletautologieconséquence logiquethèse

27Toutes les propriétés ci-dessus montrent que la relation de conséquence logique se comporte de manière attendue en ce qui concerne l’identité. Elle est monotone dans le sens où l’on peut ajouter des hypothèses sans affaiblir le pouvoir déductif, et elle possède la propriété de coupure, c’est-à-dire qu’elle permet l’élimination d’hypothèses intermédiaires. De plus, l’argument capital du modus ponens reste acquis : Si l’on affirme une conditionnelle et l’antécédent de cette conditionnelle, on peut aussi affirmer le conséquent de celle-ci.

28La propriété du modus ponens peut être établie, entre autres, par une table de vérité, qui permet de ramener la vérification à un calcul. Voici cette table de vérité :

Fig. 3 – Table de vérité du modus ponens.

Fig. 3 – Table de vérité du modus ponens.

vrai

vrai

vrai

vrai

faux

faux

faux

vrai

vrai

faux

faux

vrai

règle de détachement

29Si la relation de conséquence logique imite de manière précise, à l’intérieur de la logique mathématique, l’idée de démonstration et d’autres formes d’argumentation, elle permet aussi de définir de manière précise la notion de théorie. A partir d’un ensemble de formules Γ on considère toutes les formules qu’il est possible de déduire de cet ensemble. On regroupe ensuite ces dernières dans un ensemble qui constitue la fermeture déductive de Γ. Une théorie est finalement définie comme un ensemble de formules identique à sa fermeture déductive, c’est-à-dire qui contient toutes ses conséquences. Formellement :

Preuve formelle

  • 9 En anglais proof theory, mais le plus souvent appelée en français théorie de la démonstration.

30La relation de conséquence logique dépend de manière essentielle de la notion de vérité, et surtout de sa variante, la notion de vérité logique. Il s’agit d’une approche sémantique, basée sur l’idée de vérité-correspondance. Si elle précise de manière formelle la notion de démonstration, elle dépend cependant fortement de l’univers ensembliste sous-jacent en ce qui concerne ses objets et ses méthodes. Afin de s’affranchir de cette contrainte sémantique et d’atteindre une plus grande « mécanisation » de traitement de la démonstration, un concept purement syntaxique peut être introduit qui est l’objet de la théorie de la preuve 9. Cela nous amène aux diverses formes de la notion de preuve formelle, définies dans la perspective de Hilbert. Nous utiliserons la notation générale suivante :

31La notion sémantique de contradictoire devient la notion syntaxique d’inconsistant, concept défini sans allusion à la vérité :

32Une preuve formelle est un objet syntaxique, défini plus ou moins directement à partir de propriétés de la relation de conséquence logique. L’idée étant d’imiter, au niveau de la syntaxe, les propriétés de la vérité logique tout en donnant un statut d’objet mathématique à la notion de preuve formelle, de manière à la manipuler symboliquement, c’est-à-dire de la soumettre à un calcul. Il existe de nombreuses définitions de la preuve formelle, parmi lesquelles nous trouvons les preuves axiomatiques (Hilbert), les arbres de preuve (Beth, Smullyan), la déduction naturelle (Gentzen, Fitch), les séquents (Gentzen) et bien d’autres comme les systèmes de Post. Les détails techniques se trouvent dans les livres de référence comme [3] ou [1]. Nous allons nous limiter à la modélisation sous forme de séquents de Gentzen pour illustrer la démarche.

établiscalcul des propositionsobjets
)

Règle des antécédents

appartient à Γ)

Règle des hypothèses

Règle de preuve par distinction de cas

Règle de preuve par l’absurde

Règle de l’antécédent disjonctif

Règles du conséquent disjonctif

intègrentimitentobjetmodus ponens

1.

Γ

  

)

hypothèse

2.

 Γ

  

hypothèse

3.

 Γ

règle des antécédents

4.

Γ

règle des hypothèses

5.

Γ

règle des antécédents, preuve par l’absurde

6.

Γ

règle des antécédents

7.

Γ

)

règle de l’antécédent disjonctif

8.

Γ

  

enchaînement (règle dérivée)

33Cette suite de séquents est un exemple explicite de preuve formelle. Dans ce cas, la preuve établit la validité d’une règle déductive argumentative couramment utilisée. Cet exemple montre la double nature de la preuve formelle, d’une part son existence en tant qu’objet, mais aussi son aspect de processus.

Théorème de la complétude

  • 10 En tous cas dans le cadre de la logique du premier ordre, c’est-à-dire avec une quantification ne p (...)

34Nous avons donc jusqu’ici deux approches logiques de la notion de démon-stration telle que l’utilise le mathématicien. D’une part à travers le concept sémantique de relation de conséquence, et de l’autre par le concept syntaxique de preuve formelle. Cette deuxième notion, apparemment indépendante de l’idée de vrai et de faux, est liée cependant, comme nous l’avons vu, à notre traitement sémantique de la vérité. Et le lien entre ces deux concepts est encore plus fort : Ils recouvrent exactement10 la même réalité, comme l’a démontré Gödel [4] dans sa thèse de doctorat. Formellement :

35C’est-à-dire que les diverses définitions – syntaxiques – de la notion de preuve formelle, sont suffisantes pour capter la notion de vérité logique. Cela est d’autant plus remarquable que ces différentes approches se basent sur des idées qui n’ont a priori rien en commun. Les séquents, que nous avons présentés, ainsi que les systèmes de Post, la déduction naturelle et les arbres de preuve imitent quelques-unes des propriétés de la relation de conséquence. L’approche axiomatique de Hilbert est moins intuitive. Elle retient quelques conséquences logiques comme axiomes et à l’aide de règles d’inférence permet d’en dériver d’autres. Or il a été établi que toutes ces approches permettent la dérivation des mêmes théorèmes, et le résultat de Gödel montre que cet ensemble de théorèmes est exactement celui qu’on obtient grâce à la notion de conséquence logique. Donc d’une certaine façon, il est possible dans le cadre de la logique du premier ordre, de capter par des moyens syntaxiques – en restant à l’intérieur du langage, la notion de vérité logique.

36La logique mathématique fournit ainsi un modèle formel de ce que peut être une démonstration dans le contexte des mathématiques. Mais s’il est relativement aisé de voir qu’une preuve formelle constitue bien une démonstration mathématique, il est moins évident que toute démonstration acceptée par la communauté mathématique soit représentable sous la forme d’une preuve formelle. En effet, puisque la démonstration mathématique n’a pas de définition univoque, on ne peut pas quantifier sur ce concept. Et nous sommes réduits à en faire l’objet de la thèse suivante, que l’on peut accepter ou rejeter : toute démonstration mathématique peut être exprimée sous forme de preuve formelle, et toute preuve formelle constitue une démonstration mathématique. L’idée de cette thèse remonte à Aristote pour qui toute démonstration pouvait être exprimée sous forme d’une suite de syllogismes. On sait depuis, que la forme limitée du syllogisme ne permet pas d’exprimer toute démonstration sous la forme prévue par Aristote. Par contre la thèse, telle que nous venons de la formuler, a été proposée au début du XXe siècle. On pourrait lui donner le nom de thèse de Hilbert pour rappeler le mathématicien allemand qui a été l’un des principaux défenseurs de ce point de vue. Cette thèse peut être exprimée dans notre notation de la manière suivante :

ou de manière équivalente, en tenant compte du théorème de complétude,

Limites de l’approche formelle

37L’espoir de Hilbert était non seulement de trouver un système logique qui permettrait de transcrire les démonstrations mathématiques en preuves formelles, mais de démontrer avec les mêmes moyens que le système était lui-même consistant dans le sens défini plus haut. Il voulait ainsi éviter qu’on puisse démontrer un théorème et sa négation simultanément. Un tel système logique aurait constitué une base fondamentale sûre pour toutes les mathématiques. Mais cela aurait aussi rendu mécanique, jusqu’à un certain point, le savoir mathématique, et toute innovation de ce savoir. La question de l’existence d’un tel système était le contenu de la deuxième question, dans sa célèbre série de vingt-trois questions, que Hilbert posa en 1900 lors du congrès international des mathématiciens.

38Ce n’est qu’en 1931 qu’une réponse négative fut donnée à ce problème. Gödel [5] montra en effet que tout système logique suffisamment développé, c’est-à-dire capable de prouver au moins tous les théorèmes de l’arithmétique élémentaire, ne pouvait pas prouver sa propre consistance. Pour cela il com-mença par démontrer un autre théorème, montrant qu’un tel système était incomplet, c’est-à-dire qu’il existait une formule qui n’était pas dérivable et dont la négation n’était pas dérivable non plus. Il s’agissait d’une formule qui d’une certaine façon n’était pas décidée par la théorie. Formellement :

arithmétisation

39Mais si la proposition ! n’est pas prouvable, elle est vraie. Donc la théorie contient un énoncé vrai qui n’est pas prouvable formellement.

40Décrits plus précisément, les deux résultats de Gödel, qui constituent une limitation sévère des ambitions formalistes de Hilbert, se présentent ainsi :

11

Théorème 2 (Gödel 1931) Si une théorie Γ est consistante, décidable et suffisamment développée, alors elle ne peut pas démontrer sa propre consistance.

Que signifient ces limitations ?

  • 12 Paru en 1899.

41Les démonstrations ont souvent joué un rôle capital en mathématiques, mais la nécessité de préciser, et si possible de formaliser ce concept n’est apparu qu’au début du XXe siècle. Hilbert avait alors publié son livre « Die Grundlagen der Geometrie »12 dans lequel il reprenait la présentation axiomatique d’Euclide. Dans son livre, Hilbert corrige et rend plus rigoureuse l’approche d’Euclide en clarifiant notamment la distinction entre « axiome » et « définition » ainsi que le rôle exact des nombres réels. Il donne surtout un premier exemple de traduction systématique de la notion de démonstration en un concept de preuve formelle. Le calcul, c’est-à-dire la manipulation des symboles sans référence au sens, permet une dérivation des résultats par l’application d’un nombre limité de règles d’inférence strictes à partir de quelques axiomes.

42L’ambition de Hilbert était cependant plus grande encore. Il pensait pouvoir construire sur le même schéma un système déductif pour toutes les mathématiques. Et surtout, le système devait être capable de permettre la démonstration de sa propre consistance, en excluant, par exemple, la possibilité de dériver la proposition 0 = 1. Mais Hilbert ne réussit que partiellement dans cette entreprise. Il put montrer que le système de géométrie qu’il avait défini, était consistant si la théorie des nombres (réels) était elle-même consis-tante. La limitation que constituait cette consistance uniquement relative, le poussa à poser la question de l’existence et de la consistance absolue de la théorie des nombres. Mais comme nous le montre le résultat de Gödel, toute théorie consistante qui contient au moins l’arithmétique élémentaire ne peut pas prouver sa propre consistance.

  • 13 Contrairement à une mauvaise interprétation du résultat de Gödel.

43Cela ne signifie pas qu’on ne puisse pas démontrer la consistance de l’arithmétique13, mais seulement que cette démonstration ne peut pas se faire à l’intérieur de l’arithmétique, c’est-à-dire ne peut se faire qu’avec des moyens qui dépassent le système de l’arithmétique. Gentzen a donné une telle démonstration faisant intervenir l’induction transfinie, qui dépasse largement le cadre du système dont elle montre la non-contradiction. Cela veut dire que certaines démonstrations ne pourront pas se faire de manière mécanique, mais exigeront une forme de créativité qui consiste à trouver des éléments extérieurs au système déductif pour les établir.

44Mais cela pose à nouveau la question des critères d’acceptation de démonstrations qui dépassent le cadre du système, dans lequel sont formulés les théorèmes à démontrer. Et d’un certaine façon nous sommes revenus au départ de notre interrogation lorsque nous nous sommes demandé comment un argument mathématique pouvait accéder au statut de « preuve » et quelles étaient les conditions exactes dans lesquelles cette preuve était acceptée par la communauté des mathématiciens.

45Mais nous avons pu admirer les efforts de ces derniers pour clarifier le langage dans lequel ils expriment leurs résultats, et aussi pour énumérer de manière exhaustive les principes sur lesquels ils fondent leur argumentation. Et les résultats obtenus sont remarquables : la logique du premier ordre fournit non seulement un langage univoque mais des moyens sémantiques et syntaxiques de vérification et de falsification qui rendent possible une analyse précise de la notion de démonstration. L’existence de limites, impliquées par les résultats de Gödel – mais d’autres résultats aussi, dont nous n’avons pas parlé, comme ceux de Tarski, Church, et Turing par exemple – est loin de constituer un obstacle à la production de preuves. Au contraire, elle montre que l’activité mathématique de la preuve ne peut pas être réduite à un simple mécanisme, mais qu’elle est une activité créatrice, libre, faisant fortement appel à l’imagination.

46L’image de la preuve formelle, telle qu’elle apparaît dans les sciences mathématiques, ne peut pas constituer un modèle pour les sciences humaines. La démarche et le contexte de ces deux modes de connaissance sont trop différents. Néanmoins les conditions dans lesquelles la notion de preuve a pu être précisée, ainsi que l’évocation des obstacles inhérents à son application, sont autant de points de réflexion utiles à tout chercheur qui se penche sur ce concept ubiquiste dans l’argumentation scientifique. L’utilisation d’un langage commun et l’unicité des concepts de celui-ci, constitue probablement une condition nécessaire à un concept de preuve. Mais pour que cette preuve soit admise comme renforcement ultime de l’argumentation, elle doit s’inscrire dans un contexte logique explicite et accepté.

47Y a-t-il dans les sciences sociales un besoin et une volonté d’une telle concertation ? Pour quels avantages ? Quels seraient leurs enjeux ? De toute façon, nous avons vu que même dans des circonstances idéales, des limitations apparaissent, ce qui montre que la notion de preuve ne peut pas jouer le rôle d’arbitre absolu.

48Néanmoins, lorsqu’on mesure l’impact et la force que dégagent les limitations et les paradoxes en mathématiques, on peut se demander si une étude plus précise des obstacles à la preuve dans les sciences sociales, ne pourrait pas avoir le même effet stimulant et novateur. Si tel était le cas, comme nous le pensons, cela conférerait une justification supplémentaire à ce bref portrait de la preuve dans les sciences formelles.

Haut de page

Bibliographie

[1] G. S. Boolos & R. C. Jeffrey, Computability and Logic, Cambridge University Press, 1980.

[2] J. Etchemendy, The concept of logical consequence, Harvard University Press, Cambridge MA, 1990.

[3] J. R. Shoenfield, Mathematical Logic, Addison Wesley, 1967.

[4] K. Gödel, « Die Vollständigkeit der Axiome des logischen Funktionenkalküls », Monatshefte für Mathematik und Physik, vol. 37, 1930.

[5] K. Gödel, « Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I », Monatshefte für Mathematik und Physik, vol. 38, 1931.

[6] A. Tarski, « Der Wahrheitsbegriff in den formalisierten Sprachen », Studia Philosophica I (1935): 261-405.

Haut de page

Notes

1 En français dans le texte.

2 Nous allons adopter la convention suivante : « démonstration » désignera la procédure argumentative concrète et « preuve » désignera la formalisation logique de cette notion.

3 Nous passons sous silence un petit point technique qui n’a aucune influence sur la démonstration.

4 On suppose la fraction simplifiée, donc p et q ne peuvent pas être pairs simultanément.

5 Il s’agit en fait de la traduction d’un article en langue polonaise de 1933, très peu remarqué dans sa version originale.

6 Dans ce schéma, Image19 est un nom qui désigne la forme syntaxique de la proposition Image20.

7 Cité dans [2].

8 Nous nous dispensons d’en donner ici les détails techniques. Voir par exemple [3].

9 En anglais proof theory, mais le plus souvent appelée en français théorie de la démonstration.

10 En tous cas dans le cadre de la logique du premier ordre, c’est-à-dire avec une quantification ne portant que sur les objets.

11 C’est-à-dire qui permet l’arithmétisation. Les détails techniques se trouvent par exemple dans [3].

12 Paru en 1899.

13 Contrairement à une mauvaise interprétation du résultat de Gödel.

Haut de page

Table des illustrations

Titre Fig. 1 – Le problème de Cantor
URL http://ress.revues.org/docannexe/image/407/img-1.png
Fichier image/png, 4,0k
Titre Fig. 2 – Le « paradoxe » de Cantor
URL http://ress.revues.org/docannexe/image/407/img-2.png
Fichier image/png, 3,9k
URL http://ress.revues.org/docannexe/image/407/img-3.png
Fichier image/png, 570 octets
URL http://ress.revues.org/docannexe/image/407/img-4.png
Fichier image/png, 570 octets
URL http://ress.revues.org/docannexe/image/407/img-5.png
Fichier image/png, 570 octets
URL http://ress.revues.org/docannexe/image/407/img-6.png
Fichier image/png, 1,1k
URL http://ress.revues.org/docannexe/image/407/img-7.png
Fichier image/png, 1003 octets
URL http://ress.revues.org/docannexe/image/407/img-8.png
Fichier image/png, 762 octets
URL http://ress.revues.org/docannexe/image/407/img-9.png
Fichier image/png, 1,0k
URL http://ress.revues.org/docannexe/image/407/img-10.png
Fichier image/png, 570 octets
URL http://ress.revues.org/docannexe/image/407/img-11.png
Fichier image/png, 621 octets
URL http://ress.revues.org/docannexe/image/407/img-12.png
Fichier image/png, 1,1k
URL http://ress.revues.org/docannexe/image/407/img-13.png
Fichier image/png, 927 octets
URL http://ress.revues.org/docannexe/image/407/img-14.png
Fichier image/png, 739 octets
URL http://ress.revues.org/docannexe/image/407/img-15.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-16.png
Fichier image/png, 725 octets
URL http://ress.revues.org/docannexe/image/407/img-17.png
Fichier image/png, 562 octets
URL http://ress.revues.org/docannexe/image/407/img-18.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-19.png
Fichier image/png, 456 octets
URL http://ress.revues.org/docannexe/image/407/img-20.png
Fichier image/png, 522 octets
URL http://ress.revues.org/docannexe/image/407/img-21.png
Fichier image/png, 958 octets
URL http://ress.revues.org/docannexe/image/407/img-22.png
Fichier image/png, 571 octets
URL http://ress.revues.org/docannexe/image/407/img-23.png
Fichier image/png, 450 octets
URL http://ress.revues.org/docannexe/image/407/img-24.png
Fichier image/png, 472 octets
URL http://ress.revues.org/docannexe/image/407/img-25.png
Fichier image/png, 467 octets
URL http://ress.revues.org/docannexe/image/407/img-26.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-27.png
Fichier image/png, 472 octets
URL http://ress.revues.org/docannexe/image/407/img-28.png
Fichier image/png, 834 octets
URL http://ress.revues.org/docannexe/image/407/img-29.png
Fichier image/png, 716 octets
URL http://ress.revues.org/docannexe/image/407/img-30.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-31.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-32.png
Fichier image/png, 730 octets
URL http://ress.revues.org/docannexe/image/407/img-33.png
Fichier image/png, 457 octets
URL http://ress.revues.org/docannexe/image/407/img-34.png
Fichier image/png, 693 octets
URL http://ress.revues.org/docannexe/image/407/img-35.png
Fichier image/png, 460 octets
URL http://ress.revues.org/docannexe/image/407/img-36.png
Fichier image/png, 460 octets
URL http://ress.revues.org/docannexe/image/407/img-37.png
Fichier image/png, 460 octets
URL http://ress.revues.org/docannexe/image/407/img-38.png
Fichier image/png, 460 octets
URL http://ress.revues.org/docannexe/image/407/img-39.png
Fichier image/png, 633 octets
URL http://ress.revues.org/docannexe/image/407/img-40.png
Fichier image/png, 746 octets
URL http://ress.revues.org/docannexe/image/407/img-41.png
Fichier image/png, 974 octets
URL http://ress.revues.org/docannexe/image/407/img-42.png
Fichier image/png, 722 octets
URL http://ress.revues.org/docannexe/image/407/img-43.png
Fichier image/png, 1,0k
URL http://ress.revues.org/docannexe/image/407/img-44.png
Fichier image/png, 1003 octets
URL http://ress.revues.org/docannexe/image/407/img-45.png
Fichier image/png, 1,1k
Titre Fig. 3 – Table de vérité du modus ponens.
URL http://ress.revues.org/docannexe/image/407/img-46.png
Fichier image/png, 402 octets
URL http://ress.revues.org/docannexe/image/407/img-47.png
Fichier image/png, 409 octets
URL http://ress.revues.org/docannexe/image/407/img-48.png
Fichier image/png, 733 octets
URL http://ress.revues.org/docannexe/image/407/img-49.png
Fichier image/png, 406 octets
URL http://ress.revues.org/docannexe/image/407/img-50.png
Fichier image/png, 728 octets
URL http://ress.revues.org/docannexe/image/407/img-51.png
Fichier image/png, 407 octets
URL http://ress.revues.org/docannexe/image/407/img-52.png
Fichier image/png, 1,1k
URL http://ress.revues.org/docannexe/image/407/img-53.png
Fichier image/png, 432 octets
URL http://ress.revues.org/docannexe/image/407/img-54.png
Fichier image/png, 1,8k
URL http://ress.revues.org/docannexe/image/407/img-55.png
Fichier image/png, 650 octets
URL http://ress.revues.org/docannexe/image/407/img-56.png
Fichier image/png, 584 octets
URL http://ress.revues.org/docannexe/image/407/img-57.png
Fichier image/png, 399 octets
URL http://ress.revues.org/docannexe/image/407/img-58.png
Fichier image/png, 401 octets
URL http://ress.revues.org/docannexe/image/407/img-59.png
Fichier image/png, 575 octets
URL http://ress.revues.org/docannexe/image/407/img-60.png
Fichier image/png, 648 octets
URL http://ress.revues.org/docannexe/image/407/img-61.png
Fichier image/png, 532 octets
URL http://ress.revues.org/docannexe/image/407/img-62.png
Fichier image/png, 405 octets
URL http://ress.revues.org/docannexe/image/407/img-63.png
Fichier image/png, 405 octets
URL http://ress.revues.org/docannexe/image/407/img-64.png
Fichier image/png, 538 octets
URL http://ress.revues.org/docannexe/image/407/img-65.png
Fichier image/png, 1,1k
URL http://ress.revues.org/docannexe/image/407/img-66.png
Fichier image/png, 546 octets
URL http://ress.revues.org/docannexe/image/407/img-67.png
Fichier image/png, 831 octets
URL http://ress.revues.org/docannexe/image/407/img-68.png
Fichier image/png, 399 octets
URL http://ress.revues.org/docannexe/image/407/img-69.png
Fichier image/png, 1,7k
URL http://ress.revues.org/docannexe/image/407/img-70.png
Fichier image/png, 2,0k
URL http://ress.revues.org/docannexe/image/407/img-71.png
Fichier image/png, 2,6k
URL http://ress.revues.org/docannexe/image/407/img-72.png
Fichier image/png, 2,8k
URL http://ress.revues.org/docannexe/image/407/img-73.png
Fichier image/png, 997 octets
URL http://ress.revues.org/docannexe/image/407/img-74.png
Fichier image/png, 734 octets
URL http://ress.revues.org/docannexe/image/407/img-75.png
Fichier image/png, 833 octets
URL http://ress.revues.org/docannexe/image/407/img-76.png
Fichier image/png, 833 octets
URL http://ress.revues.org/docannexe/image/407/img-77.png
Fichier image/png, 414 octets
URL http://ress.revues.org/docannexe/image/407/img-78.png
Fichier image/png, 479 octets
URL http://ress.revues.org/docannexe/image/407/img-79.png
Fichier image/png, 414 octets
URL http://ress.revues.org/docannexe/image/407/img-80.png
Fichier image/png, 479 octets
URL http://ress.revues.org/docannexe/image/407/img-81.png
Fichier image/png, 479 octets
URL http://ress.revues.org/docannexe/image/407/img-82.png
Fichier image/png, 479 octets
URL http://ress.revues.org/docannexe/image/407/img-83.png
Fichier image/png, 408 octets
URL http://ress.revues.org/docannexe/image/407/img-84.png
Fichier image/png, 408 octets
URL http://ress.revues.org/docannexe/image/407/img-85.png
Fichier image/png, 408 octets
URL http://ress.revues.org/docannexe/image/407/img-86.png
Fichier image/png, 833 octets
URL http://ress.revues.org/docannexe/image/407/img-87.png
Fichier image/png, 408 octets
URL http://ress.revues.org/docannexe/image/407/img-88.png
Fichier image/png, 408 octets
URL http://ress.revues.org/docannexe/image/407/img-89.png
Fichier image/png, 652 octets
URL http://ress.revues.org/docannexe/image/407/img-90.png
Fichier image/png, 600 octets
URL http://ress.revues.org/docannexe/image/407/img-91.png
Fichier image/png, 700 octets
URL http://ress.revues.org/docannexe/image/407/img-92.png
Fichier image/png, 586 octets
URL http://ress.revues.org/docannexe/image/407/img-93.png
Fichier image/png, 703 octets
URL http://ress.revues.org/docannexe/image/407/img-94.png
Fichier image/png, 635 octets
URL http://ress.revues.org/docannexe/image/407/img-95.png
Fichier image/png, 404 octets
URL http://ress.revues.org/docannexe/image/407/img-96.png
Fichier image/png, 583 octets
URL http://ress.revues.org/docannexe/image/407/img-97.png
Fichier image/png, 639 octets
URL http://ress.revues.org/docannexe/image/407/img-98.png
Fichier image/png, 391 octets
URL http://ress.revues.org/docannexe/image/407/img-99.png
Fichier image/png, 567 octets
URL http://ress.revues.org/docannexe/image/407/img-100.png
Fichier image/png, 391 octets
URL http://ress.revues.org/docannexe/image/407/img-101.png
Fichier image/png, 717 octets
URL http://ress.revues.org/docannexe/image/407/img-102.png
Fichier image/png, 406 octets
URL http://ress.revues.org/docannexe/image/407/img-103.png
Fichier image/png, 585 octets
URL http://ress.revues.org/docannexe/image/407/img-104.png
Fichier image/png, 631 octets
Haut de page

Pour citer cet article

Référence électronique

Henri Volken, « « Je le vois, mais je ne le crois pas... ». Preuves et vérités dans les sciences formelles », Revue européenne des sciences sociales [En ligne], XLI-128 | 2003, mis en ligne le 11 novembre 2009, consulté le 24 mars 2017. URL : http://ress.revues.org/407 ; DOI : 10.4000/ress.407

Haut de page

Auteur

Henri Volken

Université de Lausanne

Articles du même auteur

Haut de page

Droits d’auteur

© Librairie Droz

Haut de page