« Fondements des mathématiques/Des preuves de cohérence » : différence entre les versions
Contenu supprimé Contenu ajouté
→A quoi servent les méthodes formelles ? : Orth., Format siècle |
m Bot : Remplacement de texte automatisé (-, *(…|\.\.\.) +…) |
||
Ligne 39 :
Avant de définir la moindre théorie axiomatique des ensembles, nous savons qu’il y a des systèmes d’axiomes cohérents pour les ensembles parce que nous savons que les ensembles existent d’une façon idéale. Il y a parfois des doutes sur la justesse d’une théorie particulière. Russell a prouvé que la théorie fregeienne des ensembles est contradictoire. On peut aussi avoir des doutes sur le choix de règles formelles particulières. Des logiciens se sont déjà trompés dans l’énoncé des règles pour les variables, par exemple, en omettant de mentionner des contraintes sur les occurrences libres et liées dans les règles de déduction. Mais il n’y a pas de raison d’être plus sceptique sur l’existence idéale de nombreux ensembles élémentaires que sur l’existence des nombres entiers.
Avant de définir des méthodes formelles, nous savons que certaines de nos raisonnements naturels sont fiables, parce que leurs principes sont nécessaires pour tout être rationnel, au sens où toute personne qui prend le temps d’y penser tombe d’accord sur leur nécessité. Si nous n’étions pas convaincus par la vérité de ces principes élémentaires (règles de déduction, vérités sur les mots, les formules et leurs
Que les principes fondamentaux de la raison soient faux ne pourra jamais être prouvé parce que cette preuve affirmerait qu’il n’y a aucune preuve valide et se contredirait elle-même. Est-ce que cet argument prouve que les principes fondamentaux de la raison contiennent une part de vérité ? Il peut être considéré comme une sorte de confirmation, mais le point important est que la preuve de la fiabilité des principes de preuve n’est pas une étape préliminaire obligatoire pour établir la validité d’une preuve. Cette interprétation du principe de Leibniz conduirait à une régression à l’infini et serait donc absurde. À chaque fois que nous donnons une preuve, nous pouvons supposer une sorte d’accord tacite et préalable sur la validité d’au moins quelques principes de preuve, même s’ils ne sont pas clairement formulés.
Ligne 67 :
Le paradoxe de Russell, comme de nombreux autres paradoxes ensemblistes, se pose à propos de grands ensembles, tels que l’ensemble de tous les ensembles, l’ensemble de tous les ensembles qui ne sont pas dans eux-mêmes, l’ensemble de tous les ordinaux, et quelques autres. Cette situation avait jeté un soupçon sur les découvertes de Cantor. Certains mathématiciens restaient sceptiques quant à la signification et à la portée de ses théorèmes. Mais d’autres plus audacieux ont compris que Cantor avait livré les clés d’un paradis parce qu’il a donné les moyens de raisonner avec justesse sur tous les ensembles concevables et que cela permettait de développer des théories beaucoup plus puissantes que tout ce qui avait été conçu jusque là.
Les paradoxes de la théorie des ensembles ne remettaient pas en question la vérité des principes élémentaires, tels que ceux des théories des nombres entiers. Tant qu’on se limite aux nombres entiers, l’évidence des principes n’est pas contestable. Les théories sont des ensembles de formules et peuvent être définies avec des principes semblables à ceux qui sont utilisés en arithmétique. Dans les deux cas, on peut raisonner comme si l’on parlait de suites finies de signes graphiques. Hilbert faisait remarquer que les nombres peuvent être identifiés à des suites de barres par exemple : 1=/, 2=//, 3=///, 4=////
On peut formaliser la théorie de Cantor, c’est-à-dire définir avec précision un ensemble de formules prouvables à partir d’axiomes. On obtient ainsi un ensemble finitaire de formules destinées à dire des vérités sur tous les ensembles, et pas seulement ceux qui peuvent être identifiés à des ensembles finitaires déjà construits. Pour développer la théorie générale des ensembles sans tomber dans des contradictions, on est conduit à étudier un ensemble finitaire. On peut alors espérer prouver avec des méthodes finitaires que la théorie est cohérente. Cela place les mathématiques finitaires au cœur de toutes les mathématiques, parce que si on a prouvé qu’une théorie est cohérente on a établi du même coup l’existence mathématique des êtres qu’elle définit. La fiabilité des méthodes générales peut ainsi être prouvée avec des méthodes finitaires.
| |||