Les limites de la connaissance 3-1) le programme de Hilbert et les indécidables. Partie 1) le programme de Hilbert.

Les limites de la connaissance 3) le programme de Hilbert et les indécidables.

 Partie 1) le programme de Hilbert.

Préambule.

La science nous permettra-t-elle un jour de tout savoir? Ne rêve-t-elle pas d'une formule qui explique tout? N'y aurait-il rien qui entrave sa marche triomphale? Le monde deviendra-t-il transparent à l'intelligence humaine? Tout mystère pourra-il être à jamais dissipé?

Hervé Zwirn pense qu'il n'en n'est rien.La science, en même temps qu'elle progresse à pas de géant marque elle même ses limites. C'est ce que montre la découverte des propositions indécidables qui ont suivi le théorème de Gôdel. Ou celle des propriétés surprenantes du chaos déterministe. Ou encore les paradoxes de la théorie quantique qui ont opposé Einstein et Bohr  en mettant en cause toute notre manière de penser.

L'analyse de ces limites que la science découvre à sa propre connaissance conduit à poser une question plus profonde: qu'est ce que le réel?

La certitude en mathématiques. 

Les conclusions de l'article sur l'empirisme logique aboutissent à une vision du monde qui refuse au savoir toute certitude assurée et qui remet en cause le statut même de la réalité extérieure; la science n'est que le discours le plus simple et le plus commode en adéquation avec nos expériences; Les objets physiques ne sont que des entités intermédiaires que nous postulons pour que nos lois soient les plus simples possibles, mais rien ne nous garantit que leur existence est plus réelle que celle des dieux de l'antiquité. 

Le programme finitiste de Hilbert.

L'idée de Hilbert est d'enfermer la totalité des mathématiques dans un système formel finitiste

Ces espoirs ont été ruinés par les théorèmes de Gödel les "indécidables".

Le programme de Hilbert et les indécidables.

"Est-il possible de raisonner sur des objets qui ne peuvent être définis en un nombre fini de mots? [...]Quant à moi, je n'hésite pas à répondre que ce sont de purs néants. Poincaré (1919).

"Du paradis créé pour nos par Cantor, nul ne doit pouvoir nous chasser."                     Hilbert (1926). 

Blog images des mathématiques: la vérité et les indécidables

1) La certitude en mathématiques. 



Les conclusions de l'article sur l'empirisme logique aboutissent à une vision du monde qui refuse au savoir toute certitude assurée et qui remet en cause le statut même de la réalité extérieure; la science n'est que le discours le plus simple et le plus commode en adéquation avec nos expériences; Les objets physiques ne sont que des entités intermédiaires que nous postulons pour que nos lois soient les plus simples possibles, mais rien ne nous garantit que leur existence est plus réelle que celle des dieux de l'antiquité. 
Il est possible de considérer que cela est dû au fait que les sciences empiriques traitent du monde extérieur, que celui-ci nous résiste et que l'absence d'assurance vient de ce que notre cerveau n'est pas assez puissant pour comprendre pleinement le monde qui nous entoure. 
Les Mathématiques semblent par contre un domaine où il semble que notre exigence de certitude soit parfaitement satisfaite, car le raisonnement mathématique symbolise par excellence la rigueur et la sûreté. Les mathématiques et la logique sont considérées comme des sciences dont la sûreté et la fiabilité ne sauraient être mises en doute. 
Jamais, avant le début du 20e siècle, les mathématiciens et les logiciens n'ont rencontré de contradictions qu'ils n'aient éliminé après avoir construit un raisonnement correct. 
Cette foi est particulièrement exprimée par David Hilbertt: "Qu'en serait-il de la vérité de notre connaissance, des progrès de la science si la mathématique ne donnait pas de vérité sûre? [...] La théorie de la démonstration renforce la conviction de l'absence de toute limite à à la compréhension mathématique [...]. 
C'est ainsi qu'il propose son célèbre programme où lors d'une conférence , il s'exprime ainsi: "Je voudrais réduire tout énoncé mathématique à la présentation concrète d'une formule  obtenue rigoureusement et donner ainsi aux notions et déductions mathématiques une forme irréfutable montrant bien l'ensemble de la science. Je pense pouvoir atteindre ce but avec ma théorie de la démonstration." Ce programme est un réaction à l'orage des antinomies qui avait éclaté en théorie des ensembles construite par georg Cantor et qui se matérialisait par la découverte de contradictions internes dans ses concepts et dans la logique elle-même.Elles aboutissaient à des paradoxes graves que les mathématiciens ne purent éliminer qu'après une refonte de la théorie des ensembles et une remise en cause du rôle de l'intuition en mathématiques. La formalisation, plus poussée, permit de montrer qu'il existe des limites à la puissance de démonstration en mathématiques. Le résultat le plus connu est dû à Gödel: 
a) Quelque soit le système formel grâce auquel on axiomatise l'arithmétique, il existe toujours des propositions vraies mais indécidables (limite au formalisme et différence entre entre ce qui est vrai et ce qu'on peut démontrer).
b) La consistance (non contradiction) de tout système formel décrivant l'arithmétique est elle-même une proposition indécidable de ce système. Il est donc impossible de prouver que l'arithmétique n'est pas contradictoire en s'appuyant seulement le formalisme qui décrit l'arithmétique (sauf si l'arithmétique est incohérente).
Le problème des indécidables est tel qu'en mathématiques ou en logique, il est impossible d'être assuré qu'on ne démontrera jamais une contradiction (problème de la consistance) ou que ce qui est vrai est démontrable (problème de la complétude). 


2) Les difficultés des anciennes théories.


Une grande part des difficultés est issue du concept d'infini actuel, c'est à dire de l'infini considéré comme un tout achevé et non comme une simple potentialité. Le recours à l'intuition est trompeur. Il a fallu bâtir progressivement des formalismes y faisant appel le moins possible et reposant sur des mécanismes ne pouvant raisonnablement mis en doute. Cette démarche a conduit au début du 20e siècle à une révolution conceptuelle majeure et abouti à la construction de la logique moderne. Ce qui suit permet de mieux comprendre les motivations qui ont conduit les mathématiciens à élaborer des systèmes de plus en plus sophistiqués et des théories dans lesquelles ils pouvaient placer leur confiance.


          2-1) La géométrie euclidienne
Longtemps, elle a été considérée comme un modèle de rigueur mathématique. Mais elle fait largement appel à l'intuition et utilise des figures pour les démonstrations. Elle n'est que la description mathématique de l'espace dans lequel nous vivons. Un grand nombre de propriétés sont évidentes sur les figures, mais ne sont explicitées nulle part dans le système d'axiomes (les propriété y vont de soi car elles sont vraies).Au départ, il y a 5 postulats mais le cinquième a un statut particulier (par un point hors d'une droite, il ne passe qu'une parallèle à cette droite). Euclide échoue pour le démontrer à partir des quatre autres et toutes les autres tentatives échouèrent aussi, y compris les tentatives de démonstration par l'absurde (on n'a pu démontrer qu'en ajoutant sa négation aux 4 autres postulats, le système obtenu était contradictoire). Cela implique que l'axiome des parallèles doit être considéré comme indépendant des 4 autres et qu'il est possible de construire un système apparemment cohérent en ajoutant cet axiome, ou bien sa négation aux autres axiomes. L'existence de géométries non-euclidiennes a montré que la géométrie ne peut prétendre faire reposer sa validité sur son adéquation avec le réel et que sa cohérence doit reposer sur sa structure logique. Le recours à l'intuition doit alors être éliminé dans la mesure du possible. Les efforts furent donc dirigés vers l'axiomatisation formelle de la théorie.


          2-2) L'axiomatisation de la géométrie par Hilbert.
On aboutit ainsi aux géométries non-euclidiennes: K.F. Gauss, J Bolyaï et N. Lobatchevski, puis B. Riemann au 19e siècle.  Les travaux de Felix. Klein, E. Beltrami et H. Poincaré ont montré plus tard que les géométries euclidiennes et non-euclidiennes étaient solidaires, elles sont toutes consistantes (non contradictoires), ou bien aucune ne l'est. En 1822, Pasch tente la première axiomatisation rigoureuse de la géométrie, amis il est resté attaché à une conception selon laquelle les axiomes sont suggérés par l'observation du monde extérieur. 
C'est Hilbert qui résout totalement le problème en 1899. Il construit un système formel dans lequel il explicite tous les axiomes utilisés pour les démonstrations et les répartit en 5 groupes.
1) La géométrie projective axiomes qui traitent des liaisons entre le point, la droite et le plan). 
2) Ce groupe, de nature topologique, traite de la relation "être entre". 
3) Ce groupe contient les axiomes d'égalité géométrique.
4) Ce groupe est limité à un seul axiome: celui des parallèles.
5) Ce groupe concerne les axiomes de continuité dont l'axiome d'Archimède: en ajoutant sur une droite un segment plusieurs fois à lui-même à partir d'un point A, on finira par dépasser tout point B situé du même côté de cette droite. 
Liaison de axiomes? Un  axiome est indépendant des autres si le système obtenu en ajoutant sa négation aux autres n'est pas contradictoire. cela conduit à construire des géométries nouvelles (non-euclidiennes) et des géométries non-archimédiennes, qui prouvent à la fois l'indépendance de l'axiome des parallèles et de l'axiome d'Archimède. Hilbert ramène aussi le problème de la consistance de la géométrie à celui de la consistance des théories antérieures qu'il utilise. On ne peut partir de zéro et l'axiomatisation de la géométrie suppose données la logique et l'arithmétique sans lesquelles il est impossible de construire un raisonnement déductif ou d'énoncer une proposition géométrique. Sa démonstration de la consistance se situe donc à l'intérieur d'un cadre dont il suppose la consistance ("consistance relative"). On sait maintenant que c'est la théorie des ensembles de Zermelo-Fraenkel (théorie "ZF"). Mais on revient ici à la théorie de la confiance (voir l'empirisme logique) et une démonstration rigoureuse de la théorie reste à trouver.


           2-3) La nécessité de la formalisation. 
La formalisation de Hilbert n'est pas encore totalement dégagée des images intuitives liées au sens concret des termes (ex: figures pour illustrer le texte) avec le risque que s'introduise subrepticement un maillon d'une propriété évidente mais non explicitée dans les axiomes. Ainsi, les mathématiciens ont cherché à supprimer tout recours à des noms pouvant évoquer un sens concret et en utilisant exclusivement une forme symbolique. Les axiomes deviennent les règles régissant les relations entre symboles. Par exemple: les droites sont des lettres majuscules, les points des minuscules. l'intersection de 2 droites sera le symbole intersection (^); la phrase "deux droites se coupent en un point c" deviendra "A^B = c". 
Ainsi formalisé, le système obtenu peut représenter d'autres modèles, par exemple, les axiomes de la géométrie projective peuvent être interprétés en en permutant les termes de droite et de plan et les mêmes axiomes restent valables. Russel a pu dire: "la mathématique est une science où on ne sait jamais de quoi on parle ni si ce qu'on dit est vrai". 


           2-4) La théorie des ensembles de Cantor.
La théorie des ensembles a été construite durant le dernier quart du 19e siècle par Georg Cantor. Son apport décisif concerne les ensembles infinis. L'utilisation sans précaution de ce concept a conduit à de nombreux paradoxes dont l'un des plus célèbres est celui de Zénon d'Elée. Au 19e siècle, l'infini avait acquit moins de un statut moins problématique l'analyse y devenait plus efficace dans l'étude des limites de suites et la convergence des séries (travaux de Bernard Bolzano, Cauchy et surtout Weierstrass). Cependant, devait-il être considéré en tant que potentialité (possibilité de rajouter toujours de nouveaux objets), ou comme actualité (collection d'une infinité d'objets existant simultanément à un moment donné)? Dedekind, avait adopté comme définition des ensembles infinis une propriété mise en avant par Bolzano: un ensemble infini peut être mis en correspondance biunivoque avec un des sous ensembles propres (par exemple, l'ensemble des nombres entiers avec l'ensembles des nombre pairs qui y est pourtant strictement inclus). Mais cela ne règle pas le problème de l'infini actuel, car cette possibilité n'assure nullement la légitimité de considérer l'ensemble des entiers naturels comme un tout achevé, comme une donnée actuelle et la situation est pire pour l'ensemble des nombres réels sans lequel l'analyse mathématique s'effondrerait. 
La théorie de Cantor jette les nouvelle bases des ensembles infinis.  La définition est intuitive: "par ensemble, j'entends toute collection, dans un tout M, d'objets définis et distincts de notre intuition ou de notre pensée". Le mot collection comporte un aspect circulaire, mais cela n'est pas grave si les règles d'utilisation des concepts sont non ambiguës puisque la définition ne joue dans ce cas aucun rôle opérationnel. L'impossibilité de définir précisément ce qu'on entend par "ensemble" ou "élément" n'empêche pas de construire une théorie qui en retour éclairera ce que sont les ensembles et les éléments, exactement, selon Boolos comme pour des termes comme "il existe" ou "non" dans la logique quantifiée. 
Une propriété (être "rouge", être un "nombre pair"...)  est caractérisée par un prédicat. Il existe un ensemble qui est celui des objets satisfaisant cette propriété. Deux ensembles ont même puissance s'il est possible de les mettre en correspondance biunivoque. Ainsi l'ensembles des nombres entiers (N) et des nombres pairs (ou des couples, des triplets, des nombres rationnels....) ont même puissance (équipotents). Un ensemble équipotent à N est dit "dénombrable". Cette puissance set désignée par un nombre cardinal (le nombre d'éléments de l'ensemble s'il est fini). Le cardinal de N et de tous les ensembles dénombrables est appelé No. Cantor va encore plus loin: la puissance des parties d'un ensemble (ensemble de tous ses sous-ensembles)  est strictement > à celle de l'ensemble lui-même. Pour les ensembles finis, c'est évident, P(A) a 2(puissN) éléments => Card P(A) = 2 (puissCardA). Cantor généralise aux ensembles infinis avec Card P(A) = 2(puissCard(A) > Card A. Ainsi, il existe des ensembles de puissances croissantes supérieures au dénombrable (on les appelle N1, N2 ...). Pour les réels, Cantor montre qu'il est impossible de construire une correspondance biunivoque entre N et l'ensemble des réels R, donc N et R n'ont pas même puissance et, comme N est inclus dans R, on a puissance R > N. Cette puissance est appelée "puissance du continu". On peut aussi montrer que R peut être mis en correspondance avec un des ses segments ou avec R puiss2 (ou RpuissN). Il est possible de montrer que la puissance du continu est identique à celle de l'ensemble des parties de N, ce qui veut dire que Card R est 2puissN0 qu'on appelle N1. Y a-t-il une puissance entre N0 et N1, entre celle du dénombrable et celle du continu? Cantor a répondu non (c'est l'hypothèse du continu), mais il ne l'a jamais démontré. Depuis, Godël et Paul Cohen ont montré qu'elle est indécidable (on ne peut  ni la démontrer ni la réfuter).


          2-5) Les antinomies de la théorie des ensembles.
La théorie de Cantor représente un immense pas en avant dans la compréhensions de l'infini après la solution des problèmes de l'infiniment petit (Weierstrass), de l'infini et de la continuité (Dedekind), solution que Cantor accomplit définitivement. Mais cette théorie, dite "théorie naïve des ensembles" est contradictoire. Elle engendre des des incohérences inacceptables, malgré son aspect intuitif apparemment satisfaisant. Le plus connu est le paradoxe de Russel concernant les ensembles qui ne sont pas éléments d'eux-même. Soie E l'ensemble des choses pensables. Etant une chose pensable, il fait partie de lui-même. Par contre l'ensemble des lettres du mot "théorie" est l'ensemble {t, h, é, o, r, i, e}. Cet ensemble n'est pas une lettre du mot "théorie", il n'est donc pas élément de lui-même. Considérons alors l'ensemble A des ensembles qui ne sont pas éléments d'eux-mêmes. A est-il élément de lui-même? Répondre non, c'est dire que A possède la propriété qui définit des propres éléments (il n'est pas élément de lui-même) et  donc il appartient à A . Répondre oui, c'est dire qu'en temps qu'élément de A, il doit posséder la propriété qui définit ces éléments et donc il n'appartient pas à lui-même. Cela conduit dans les 2 cas à une contradiction. De multiples autres paradoxes sont ainsi apparus, tel celui du menteur qui dit "je mens" ou celui de Burali-Forti concernant l'ensemble de tous les ordinaux.


        2-6)   La logique de Frege et de Russel et Whitehead.
Sans changement notable depuis Aristote, entamé avec De Morgan, le renouveau date vraiment de 1847 avec "de l'Analyse mathématique et de la logique" puis des "lois de la pensée" de Boole  sous forme d'une algèbre permettent d'élargir et de faciliter les types possibles de déduction. Mais c'est Frege qui est considéré comme le père de la logique moderne. Son "Begriffs-Schrift" est le début de la formalisation de la logique où il introduit les prédicats et les quantificateurs et un système formel indépendant de toute interprétation. Son objectif, dans le cadre du logicisme, est de montrer que l'ensemble des mathématiques est réductible à la logique. Mais en 1902, il découvre les paradoxes de Russel, et poursuivant dans voies du logicisme, il publie les Principia Mathématica avec Whitehead. Ils fournissent l'essentiel des mathématiques de l'époque et le système formel qui contient la théorie des ensembles sous une forme appelée "la théorie des types", échappant aux paradoxes. C'est dans ce formalisme que Godël fera la démonstration de ses théorèmes d'incomplétude. De son côté, Zermelo proposa en 1908 une axiomatique de la théorie des ensembles, complétée et améliorée par Fraenkel et Skolem, appelée "théorie ZF". 


3) Les systèmes formels modernes.


L'exigence des mathématiciens de ne as tomber dans la contradiction a engendré des découvertes surprenantes et contre-intuitives dont certaines se manifestent sous la forme de théorèmes limitation dans les systèmes formels. 


          a) Les méthodes finitistes.
 Si on veut utiliser un systèmes d'axiomes pour en tirer des conséquences, il est essentiel de savoir s'il est cohérent (ou consistant, non-contradictoire). S'il est possible de trouver un modèle (un ensemble d'objets tels que les axiomes sont vrais pour eux) alors il semble que qu'on sera assuré que les axiomes seront cohérents. Si une propriété est la conséquences de propriétés vérifiées, alors il n'est pas possible de croire que la propriété conséquence n'est pas vérifiée elle aussi ("le réel doit être logique"). Le modèle est non contradictoire et toute propriété le concernant satisfait le principe du tiers-exclu, est soit vraie, soit fausse. Voir le modèle du triangle page 62 de "les limites de la connaissance)
Ces raisons semblent indubitables, mais elles reposent sur le fait que le modèle est simple et évident pour qu'on puisse décider par simple observation de sa valeur de vérité (on dit qu'il est utilisable). Il est constitué d'objets bien définis en nombre fini qui permet les vérifications en nombre fini. Cela revient à faire confiance à notre intuition du fini. En progressant vers la généralisation, on trouve des systèmes ayant un nombre fini d'axiomes et un modèle infini, puis un nombre infini d'axiomes et des modèles infinis. Or, les mathématiques concernent en général des collections infinies d'objets et nous ne pouvons pas les inspecter un par un, et on a bien vu que pour des ensembles intuitifs, au sens initial de Cantor, l'existence même d'un de ces objets pouvait conduire à une contradiction. Comment alors aller au-delà de notre intuition finie sans tomber dans le piège de l'infini?
On appelle "décidable" un propriété dont on peut s'assurer directement (par observation au sens précédent), qu'elle est vraie ou fausse, par exemple la propriété: être pair. Une généralisation pour généraliser, on peut étendre l'examen des propriétés sur des ensembles infinis dénombrables. Pour chacun des éléments de l'ensemble, il est possible de savoir par observation s'il vérifie P ou non, puisque P est décidable. Par contre, on ne peut vérifier que tout élément de l'ensemble vérifie P, il en faudrait un nombre infini. Par contre, on peut accepter le principe "d'induction": si la propriété P est vérifiée par 0 et si, lorsqu'elle est vérifiée par un nombre entier, elle est vérifiée par le nombre entier suivant, alors elle est vérifiée par tout nombre entier. Ce principe ne peut être établi par observation, mais sa validité semble suffisamment raisonnable. Il devient alors possible de s'assurer que qu'une propriété est décidable est vérifiée sur un ensemble infini (dénombrable). Mais en fait, c'est loin d'être suffisant pour s'assurer de la vérité ou de la fausseté de toute propriété de N où de nombreuses propriétés ne s'expriment pas sous cette forme. 


          b) Un système formel rudimentaire: le système "a,b,c,d"
Pour composer un système formel, on se donne un vocabulaire ou alphabet A qui regroupe les symboles utilisés dans le système. Toute "suite finie de symboles" est une expression. On se donne ensuite des règles qui permettent de construire des "expressions bien formées" (e,b,f) appelées des 'formules" (des suites de symboles). Cette partie du système formel est appelée "morphologie" car elle spécifie la forme que prendront les objets formels du système. On se donne ensuite des règles pour pour construire des preuves (des suites de formules conformes à ces règles). Les axiomes du système sont choisis parmi les formules (ce sont en eux-même des preuves, donc ils sont prouvés dans le système). Il est à noter que les règles de formulation des formules ou des preuves peuvent être exprimées, elles,  dans le langage ordinaire ou un langage qui préexiste à celui du système formel. Ce dernier est appelé un "métalangage".On a alors construit l'aspect syntaxique du système, aspect entièrement formel, qui ne concerne que la forme des objets qu'il est licite construire. 
Par exemple, Le système "a,b,c,d" est formé à partir de l'alphabet A = {a;b;c;d}. "acba" et "acbdb"sont des expressions. Soit la règle suivante: On appelle "composante" toute expression qui est soit réduite à un unique symbole a ou b, soit de forme fc@ où f est une composante et @ peut être a ou b.  Une formule est alors toute expression e la forme fdg où f et g sont des composantes. 
Cette règle définit donc des formules comme étant des expressions avec un nombre arbitraire mais fini de a et b liés ou non par des c et d'autre part de l'unique signe d (acab n'est par une formule alors que acbda l'est). 
On se donne aussi la règle suivante de construction des preuves: une preuve est une suite de formules  vérifiant les propriétés: 1) ou bien elle est réduite à un axiome. 2) ou bien elle commence par un axiome, et la formule n°i s'obtient à partir de la formule n°( i-1)en remplaçant dans cette dernière une occurrence de a par aca, ou bca, ou en remplaçant dans cette dernière une occurrence de b par bcb.  
On peut ainsi prouver des formules ou voir que d'autres formules n'ont pas de preuve. Jusqu'ici il n' a été attribué de signification aucun des symboles et les règles du jeu concernent exclusivement la forme des suites de symboles ("formules", "axiomes", "preuves"). Cette syntaxe peut être comparée aux règles de déplacement du jeu d'échecs qui n'ont en elles-même aucune signification, il faut la compléter par une sémantique: on appelle "modèle" du système formel une structure d'interprétation dans laquelle les axiomes sont vrais: cette interprétation permet de saisir intuitivement " parle le système".
Dans le système présenté, le domaine d'interprétation sera l'ensemble {0,1,x,=}. La formule "acbda" sera interprétée comme signifiant " 0x1=0. Une formule sera une égalité entre deux produits d'un nombre arbitraire de 0 et de 1. Les axiomes interprétés deviennent: 0=0, 1=1... {0,1,x,=] est un modèle du système formel.  Les preuves permettent de prouver toutes les égalités vraies (comme 1x0x1x0=0x1), car aucune égalité fausse (comme 0x0x1x=1x1) ne peut être prouvée. Il y a donc équivalence pour une formule entre "être prouvée" et "être vraie dans le modèle". Remarques: On voit ainsi pourquoi "acab" (0x01) n'est pas une formule, alors que "acbda" (0x1=0) en est une. Un système formel qui possède la propriété d'être prouvable est dit "correct" (ou fiable) et "complet". Comme il n'est pas possible de prouver une formule fausse, il est dit "consistant". Les démonstrations de la complétude et de la consistance du système ne font ici appel qu'à des raisonnements de type finitiste (avec le principe d'induction) portant sur la structure des preuves.


          b La logique des propositions (initiation).
La logique est la discipline qui codifie les règles que nous utilisons pour nous exprimer. Le système le plus simple est celui qui codifie le calcul propositionnel, raisonnements les plus simples qui portent sur des propositions non analysées en constituants (ex: "Si je chante alors il pleuvra, or je chante, donc il pleuvra"...). Un système formel correspondant est le suivant:
On se donne un ensemble infini de variables propositionnelles P = [p,q...t]. Le vocabulaire V se compose de P et de deux symboles connecteurs {--, -->}, la "négation" et "l'implication". Les règles de formation des formules, suites finies de symboles de V sont les suivantes:
- Toute suite de variables ayant pour seul terme une variable propositionnelle est une formule.
- Si F est une formule, le terme --, suivi des termes de la formule, est une formule (notée --, F).
- Si F et G sont deux formules, la suite obtenue en faisant suivre les termes de F par --> puis par les termes de g est une formule notée (F --> G) .
- Toute formule est obtenue par itération des procédés ci-dessus. 
 Les axiomes sont les formules suivantes: 1). A --> (B--> A).  
2). {A--> (B--> C)} --> {(A --> B) --> (A--> C)}  3). (--, A --> B) --> {(--, A --> --, B) --> A}
Il y a une infinité d'axiomes puisque A, B, C peuvent être n'importe quelle formule. 
Les règles de formation des preuves sont les suivantes:
- Toute suite de formules ayant un axiome pour seul terme est une preuve.
- Si D est une preuve et A un axiome, le suite obtenue en faisant suivre D par A est une preuve. 
- Si D est une preuve comprenant deux termes de la forme A et  (A --> B), le suite obtenue en faisant suivre D par B est une preuve. Cette règle s'appelle le "modus ponens".
Une formule est prouvable et s'appelle un "théorème" s'il existe une preuve dont elle est le dernier terme.
Ces règles constituent la syntaxe du calcul des propositions (on constate l'analogie avec du système " abcd ").  
Pour la sémantique, on pourrait rechercher une structure d'interprétation en donnant une signification aux deux symboles (--, et -->), comme  on l'a fait pour le système {a,b,c,d} ou pour l'arithmétique, mais ici, il s'agit de modéliser le raisonnement logique lui-même. Ce n'est pas le sens des propositions qui nous intéresse, mais la vérité des propositions. Les raisonnements doivent partir de prémisses vraies et aboutir à des conclusions vraies, indépendamment de leur sens. On définit une assignation de valeurs de vérité comme l'assignation à chaque variable propositionnelle de la valeur V (vrai) ou F (faux). Le domaine d'interprétation des variables propositionnelles sera donc l'ensemble {V,F} et les connecteurs seront associés à ce qu'on appelle leur table de vérité:
           p          q          --,p          --,q           p-->q
           V          V           V             F             V
           V          F           F             V              F
            F         V           V              F             V
            F          F          V              V             V


Un modèle particulier sera donc donné par une assignation particulière de valeur de vérité à chaque valeur de vérité dan {V,F} qui rende vrais les axiomes. Nous aurions modélisé un domaine particulier, correspondant à une assignation particulière, mais pas encore le raisonnement lui-même. Nous cherchons l'assurance que quelque soit la valeur de vérité des variables propositionnelles, le raisonnement permettant de déduire une formule d'une autre, le raisonnement sera licite et la conclusion aussi. Faisons un pas de plus, on s'intéresse aux propositions qui sont vraies pour toute assignation.de valeurs de vérité: on les appelle des "tautologies". Il est possible de montrer que si les règles de preuve sont telles que toute formule prouvée est une tautologie le système est correct),et que toute tautologie est démontrable (complétude), alors, pour chaque assignation particulière de valeurs de vérité, toute formule prouvée à partir de formules non tautologiques  sera vraie chaque fois que les formules seront vraies, et si une formule est vraie chaque fois que qu'un ensemble d'autres formules est vrai, alors la première sera prouvable à partir des secondes. On a ainsi formalisé ce que nous entendons par règles de raisonnement. 
Le système que nous cherchons se donne donc pour objet de formaliser les règles qui permettent de prouver les tautologies qui en seront les axiomes. Le calcul propositionnel est donc correct et complet. Ce calcul des propositions est aussi consistant car il est impossible de prouver une proposition et sa négation (on aurait une formule tautologique dont la négation est tautologique, ce qui est impossible). 
A côté des axiomes tautologiques, on peut maintenant se donner des axiomes complémentaires, qui sont des formules contingentes, vraies pour certaines assignations des valeurs de vérité et fausses pour d'autres ainsi qu'un modèle du système obtenu. On obtient ce qu'on appelle "une théorie" (d'ordre 0). On a ainsi bien réalisé une modélisation générale du raisonnement qui incorpore toute modélisation particulière. La consistance et la complétude du calcul des propositions ont pu être montrées d'une manière qui semble à l'abri de tout soupçon. Mais seules des méthodes finitistes qui ne suscitent aucun doute ont été employées.


          c) Le calcul des prédicats.
Le calcul des propositions est trop rudimentaire pour suffire à exprimer des raisonnements mathématiques. On introduit le concept de prédicat pour formaliser le fait qu'une propriété est attribuée à un objet. Le fait d'être pair pour un entier revient à dire qu'il satisfait au prédicat "être pair". On note P(n) le fait que l'entier n vérifie le prédicat P. De plus, on introduit les deux quantificateurs "pour tout" (noté "V" et "il existe"  (noté "E"). Ainsi, l'énoncé "pour tout nombre pair n, il existe un nombre n tel que n est la somme de m avec lui-même" s'écrit: Vn, P(n) -->(Em, n=n+m). De même être le double s'écrit: D (m,n) est vérifié pour tout couple tel que m=2n. Le calcul des prédicats se formalise de la même manière (plus complexe) que le calcul des propositions. Il est correct et complet (toute formule dérivable à partie d'un ensemble de formules en est la conséquence logique, et si une formule est la conséquence logique d'un ensemble de formules, elle est dérivable à partir de cet ensemble et ce dernier est consistant. Le calcul des prédicats semble suffisant pour formaliser l'ensemble des mathématiques et les systèmes formels qui sont envisagés incorporent; outre les axiomes propres qui décrivent le domaine particulier envisagé (las nombres entiers, les ensembles...), le calcul des prédicats comme outil de raisonnement logique. Ces systèmes sont appelés "théories du premier ordre", le calcul des prédicats étant "le calcul du premier ordre". C'était la position de Hilbert. Depuis, Quine (1970) s'est opposé à cette logique, hintikka 1998) en propose une nouvelle avec Shapiro (1991) (logique du second ordre).


         d) Les propriétés des systèmes formels.
Résumé: un système formel pour la logique des propositions ou le calcul des prédicats est dit "correct" ou "fiable" si toute formule prouvable est tautologique. Il est "complet" si si toute formule tautologique est prouvable. Une théorie est obtenue en en ajoutant aux axiomes de base un ensemble d'axiomes supplémentaires (formules contingentes qui peuvent être vraies ou fausses selon l'assignation). Une théorie est complète si toute formule est soit prouvable, soit réfutable. Par ailleurs, on distingue deux sens pour le mot "complétude". La complétude sémantique, signifie que toute formule, conséquence logique d'un ensemble de formules, est dérivable de cet ensemble. la complétude syntaxique signifie que toute formule est prouvable ou réfutable. Dans un système correct sémantiquement consistant, la complétude syntaxique entraîne la complétude sémantique. mais la réciproque est fausse: le calcul des prédicats est sémantiquement complet, mais pas syntaxiquement (la formule Ex P(x) --> Vx P(x) n'est ni démontrable ni réfutable). Quand on parle de complétude sans précision, il s'agit de la complétudes sémantique (l'arithmétique du premier ordre est dans ce cas, comme l'a montré Gödel).


          e) L'axiomatique de Peano (axiomatisation formalisée de l'arithmétique _1899).
Le langage contient 4 symboles non logiques: le nom "0", la fonction à une variable "s" (successeur), les 2 fonctions à deux variables "+" et "-". L'arithmétique du premier ordre est la théorie obtenue en ajoutant au calcul des prédicats (avec identité; cad on s'est donné les axiomes régissant l'utilisation du prédicat binaire "=") les axiomes suivants:
- Vx --, {0 = S(x)} (0 n'est le successeur d'aucun nombre).
- Vx Vy {S(x) = S(y) --> (x= y)}. (si 2 nombres ont le même successeur, ils sont égaux).
- V x (x=0 = x). (0 ajouté à un nombre ne change pas le nombre).
- Vx Vy {x + S(y) = S(x+y)}. (x + le successeur de y est identique au successeur de x+y).
- Vx (x . 0 =0). (0 multiplié par un nombre = 0).
- Vx Vy (x . S(y) = x . y + x)). (x multiplié par le successeur de y = x multiplié par y plus x.
- (phi (0) ^ {Vx phi(x) --> phi(S(x))} --> x(phi(x) où phi(x) est une formule. (le principe d'induction).
L'ensemble N des entiers naturels muni de l'addition et de la multiplication est un modèle de ce système formel. Il en résulte que le système est consistant. Mais l'arithmétique possède un nombre infini d'éléments et il apparaît que des difficultés imprévues surgissent (voir le théorème de Gödel.


          f) le programme finitiste de Hilbert.
L'idée de Hilbert est d'enfermer la totalité des mathématiques dans un système formel finitiste. On considère (bien qu'il n'ait pas été totalement explicite) qu'il se limitait, outre les constructions finies, aux propriétés décidables universellement quantifiées (les formules Vx P(x)) où P est un prédicat décidable) et qu'il est possible de démontrer à l'aide du principe d'induction. Un système peut comporter un nombre infini d'axiomes, pourvu qu'il soit possible de déterminer par simple observation si une formule est un axiome ou non. Le système doit être complet et consistant. Il doit être possible de prouver la consistance par des moyens finitistes. S'il est possible de projeter la preuve de sa consistance à l'intérieur du système, elle rejaillira de manière réflexive pour acquérir un statut de sûreté indubitable. Toute déduction mathématique se ramènerait à à une preuve formelle où on pourrait décider si elle est conforme ou pas sans ambiguïté. Mais il ne serait plus possible de débattre sur la légitimité des démonstrations pour une raison profonde. Tout énoncé vrai posséderait une démonstration et l'ignorabimus serait éliminé selon le voeu de Hilbert. Il ne rejette pas les résultats qui ne sont pas conformes à la méthode finitiste, mais il veut prouver que toute démonstration qui utilise ces méthodes ("abstraites" selon lui), peut être ramenée à un méthode finitiste. Ce programme est l'analogue du désir fondationnaliste des positivistes logiques et assez conforme à l'image que l'homme de la rue se fait des mathématiques.


Ces espoirs ont été ruinés par les théorèmes de Gödel les "indécidables" que nous verrons dans le prochain message.