El-Found

Résumons

L’incomplétude des systèmes formels

Indiquons le schéma d’intervention autour duquel Gödel a bâti son fameux théorème

1) Comment construire une formule arithmétique G représentant l'énoncé suivant :

" La formule G n'est pas démontrable " ?

G est vraie ssi elle n'est pas démontrable, G dit quelque chose d'elle même , elle est autoréférentielle donc source de paradoxes.

2) Gödel montre que G est démontrable ssi sa négation non G est démontrable.

Si G et non G sont démontrables, l'arithmétique est inconsistante. Si l'arithmétique est consistante , alors ni G , ni non G ne sont démontrables. G est une formule indécidable.

3) Bien que G ne soit pas démontrable, elle est arithmétiquement vraie.

4) Puisque G est vraie et qu'elle est indécidable, alors les axiomes sont sémantiquement incomplets . Donc il y a des formules vraies qui ne sont pas décidables au sein du système.

5) Gödel construit une formule A qui représente la proposition " l' arithmétique est consistante".

Si A alors G

A implique G est démontrable, or A n'est pas démontrable dans le système. Si A était démontrable, alors G le serait aussi ; donc la formule est indécidable.

Ainsi, si l'arithmétique est consistante, alors on ne peut prouver dans l'arithmétique la formule qui exprime cette consistance

Un exemple de formalisation

On dispose un nombre n d'allumettes sur une table. Les joueurs A et B jouent

chacun leur tour et peuvent retirer de 1 à 3 allumettes du tas. Le joueur qui retire

la dernière allumette a gagné.

Exemple de partie

On dispose 10 allumettes. C'est au joueur A de commencer.

1. Le joueur A retire 2 allumettes, il en reste 8

2. Le joueur B retire 1 allumette, il en reste 7

3. Le joueur A retire 3 allumettes, il en reste 4

4. Le joueur B retire 2 allumettes, il en reste 2

5. Le joueur A retire 2 allumettes, il n'en reste plus, le joueur A a gagné.

Le système formel

Afin de bien mieux comprendre le système formel en question, nous ferons souvent

référence au parallèle avec le jeu des allumettes.

Néanmoins, il doit être bien compris que le système formel en lui même n'a aucun sens.

C'est nous qui choisissons de lui en attribuer un, qui signifie quelque chose pour nous.

Les formules

Le vocabulaire de notre système sera les lettres A,B et les nombres entiers.

Une formule correcte de notre système sera de la forme : "lettre lettre entier". Par exemple, AB14 et

BB3 sont des formules bien formées, alors que 4B12 n'est pas une formule.

On peut trouver une signification à ces formules. Convenons que la formule AB12

signifie le joueur A peut gagner de façon sûre si c'est au joueur B de jouer et qu'il reste 12

allumettes. De la même façon, la formule BB6 signifiera : le joueur B peut gagner de

façon sûre si c'est au joueur B de jouer et qu'il reste 6 allumettes.

Chacune de ces formules peut être vraie ou fausse. Nous verrons plus loin que la formule

AA10 est vraie. En effet, le joueur A peut gagner de façon sûre si c'est à lui de jouer et

qu'il reste 10 allumettes. Par contre, la formule AA8 est fausse, car le joueur 1 ne peut pas

gagner de façon sûre si c'est à lui de jouer et qu'il reste 8 allumettes.

La négation des formules

Dans ce jeu, les formules ont une négation. Cela signifie qu'à toute formule on peut en

associer une autre de façon à ce que si l'une est fausse, l'autre soit vraie et inversement.

En effet, pour une position donnée (un nombre d'allumettes x et le nom du joueur (A ou

B) qui va jouer), un des deux joueurs a forcément la possibilité de gagner. Ainsi, si ABx

est vraie c'est que BBx est fausse, et si AAx est fausse c'est que BAx est vraie.

Les règles d'inférence

Comment déduire d'une formule vraie une autre formule vraie ? On voit bien que si AB16

est vraie, alors AA17 l'est aussi, car : Si A gagne alors que c'est à B de jouer et qu'il reste

16 allumettes, alors A gagne aussi si c'est à lui de jouer et qu'il en reste 17 (car il lui suffit

d'en enlever une).

Voici la liste des règles d'inférence de notre système (n remplace n'importe quel entier):

1. ABn => AAn+1

2. ABn => AAn+2

3. ABn => AAn+3

4. ABn => ABn+4

5. BAn => BBn+1

6. BAn => BBn+2

7. BAn => BBn+3

8. BAn => BAn+4

Les Axiomes

Nous devons trouver les vérités de base de notre système. On peut les choisir

arbitrairement, mais si on veut obtenir des formules qui signifient toujours quelque chose

par rapport au jeu, il faut que nos axiomes soient vrais dans le jeu : AB4 et BA4 sont de

bons axiomes, effectivement vrais dans le jeu, car le joueur A gagne forcément si c'est au

joueur B de jouer et qu'il reste 4 allumettes et de même le joueur B gagne forcément si

c'est au joueur A de jouer et qu'il reste 4 allumettes.

Testons notre théorie

Partant des axiomes et du système formel, on peut déduire un certain nombre de formules.

Par exemple, AB4 et vrai (c'est un axiome) donc AA5 est vraie aussi (en utilisant la règle

1), AB8 est vraie aussi (en utilisant la règle 4). On peut aussi enchaîner les règles : BA4

=> BA8 => BB10

Avec nos 2 axiomes de base, et nos 8 règles d'inférence, nous pouvons ainsi déduire

plusieurs formules (théorèmes), qui nous donnent pour l'ensemble des configurations de

plus de 4 allumettes le nom du joueur gagnant.

L'ordinateur démontre tout

À l'aide d'un ordinateur, on peut s'affranchir du côté mécanique du système formel pour

qu'il applique systématiquement les 8 règles à l'ensemble des théorèmes lorsque c'est

possible.

Partant des 2 axiomes de base, et en appliquant les règles applicables à chacun d'eux, il

démontre les 8 formules suivantes : AA5, AA6,AA7, AB8, BB5, BB6, BB7, BA8

Puis en réappliquant les règles (quand c'est possible) à nos 8 nouveaux théorèmes, la

machine peut démontrer 8 nouveaux théorèmes, et ainsi de suite, car le processus ne

s'arrête jamais.

Consistance, complétude...

Nous avons vu que les formules possédaient des négations. la négation de AA5 (notée

non(AA5)) est BA5. En effet, soit l'un soit l'autre des joueurs a la possibilité de gagner de

façon sûre dans n'importe quelle configuration. Choisissons une formule (par exemple

AB7654) de notre système, et attendons infiniment longtemps (en théorie) pour voir si

l'ordinateur la démontre. Quatre cas peuvent se présenter :

1. Il démontrera AB7654 et pas BB7654 (la négation de AB7654)

2. Il démontrera BB7654 , et pas la formule AB7654

3. Il démontrera la formule AB7654 et la formule BB7654

4. Il ne démontrera ni AB7654 , ni BB7654

Les 2 premiers cas ne posent pas de problème. En revanche, si le troisième se présentait

nous pourrions dire que le système est inconsistant. En effet, il permet de démontrer une

chose et son contraire. Il est bien évident que dans toute configuration (ici B7654) il est

impossible que les 2 joueurs aient une stratégie gagnante à la fois...

Le quatrième cas pose aussi un problème. Si vous étudiez mieux le jeu, vous verrez

facilement que dans toutes configuration, un des joueurs a une stratégie gagnante. Par

conséquent, nous savons que soit AB7654, soit BB7654 est vraie (en l'occurrence, c'est

AB7654). Si le quatrième cas se présentait, nous pourrions dire que le système formel est

incomplet, car il existerait certaines vérités qu'il ne permet pas de démontrer.

Bien entendu, dans notre exemple simple, le système est en fait consistant et complet,

c'est à dire qu'il ne permet pas de démontrer une chose et son contraire, et qu'il permet de

démontrer toutes les formules qui sont vraies.

Mais il n'en est pas de même pour tous les systèmes. Le travail de Gödel a consisté à

démontrer que dans les systèmes formels suffisamment complexes pour contenir

l'arithmétique :

· on ne peut pas simplement démontrer la consistance ;

.· si le système formel est consistant, alors il est incomplet

 

Maintenant on peut très bien se douter que Hilbert ne voulait pas réellement une formalisation de toute la mathématique. Il n’a pas dit qu’il fallait que tous les mathématiciens devaient obligatoirement travailler dans un langage artificiel en produisant des preuves formelles.

Les preuves formelles tendent à devenir très longues, inhumaines et très difficiles ne serait-ce qu’à lire .

On doit peut-être penser que l’objectif réel de Hilbert était plus philosophique.

Si on croit que la mathématique doit délivrer la vérité absolue, alors on peut croire que Hilbert avait raison et que l’on devait trouver une façon de formaliser une fois pour toute toute la mathématique. C’est ceci qu’essaye de faire la logique mathématique, c’est ceci qu’essaye de faire la méthode axiomatique qui une idée consistant à éclater les preuves en des preuves de plus en plus petites.

Leibnitz croyait à cela.

Boole le pensait.

Frege et Peano et Russell et Whitehead en étaient convaincus.

C’est l’idée de rendre très clair comment la mathématique opère pas après pas.

Et cette idée sonnait plutôt juste.

Malheureusement arrivé en ce point tout est tombé à l’eau.


Suite de l'article