Logique Mathématique

Mathematical Logic, Computability · course

Voir tous les documents en mathématiques

Logique mathématique

Partie I - Le calcul des prédicats (cid:1)(cid:1)(cid:1)(cid:1) Formalisation

Chp.1- Le calcul des propositions (CP0)

Chp.2- Le calcul des prédicats (CP1)

Partie II - Les méthodes de calcul

Partie II - Les méthodes de calcul

(cid:1)(cid:1)(cid:1)(cid:1) Déduction

(cid:1)(cid:1)(cid:1)(cid:1) Déduction

Chp.3- Notions fondamentales

Chp.4- La méthode de résolution

Chp.5- Le calcul des séquents

ENSI

Logique Mathématique

1

Logique mathématique

Chapitre 3

Notions fondamentales

I- Notion de décidabilité

I- Notion de décidabilité

II- Introduction aux systèmes formels

III- Application au calcul des prédicats

IV- Théorème d’incomplétude de Gödel

ENSI

Logique Mathématique

2

Notions fondamentales

I- Notion de décidabilité

1- Fonction récursive

2- Ensemble récursif

3- Ensemble récursivement énumérable

4- Prédicat décidable

5- Prédicat semi-décidable

6- Cas de la logique des prédicats

ENSI

Logique Mathématique

3

Notion de décidabilité

Notation

Soient

• P un programme (ou une procédure)

• n un entier naturel (˛

à une entrée et à une sortie

˛ ℕℕℕℕ )

ℕℕℕℕ

On note par :

  • P(n) = k

si

le programme P imprime k (au bout d’un

temps fini) pour la donnée n et s’arrête

  • P(n) = ^

si

le programme P ne s’arrête pas pour

la donnée n (tourne indéfiniment)

ENSI

Logique Mathématique

4

˛

˛

^

^

^

Notion de décidabilité

1- Fonction récursive

Soit f une fonction partielle de ℕℕℕℕ dans ℕℕℕℕ

(cid:2) On dit que f est récursive ou calculable, s’il existe un

programme P tel que :

  • P(n) = f (n)
  • P(n) = ^
  • P(n) = ^

si n ˛ Dom( f )

sinon

sinon

Remarques

• Une fonction récursive est une fonction qu’on peut

« programmer » (calculer)

• Il y a des fonctions qui ne sont pas récursives

c-à-d « non calculable » (thèse de Church)

ENSI

Logique Mathématique

5

^

^

^

^

^

^

Notion de décidabilité

2- Ensemble récursif

Soit A un ensemble d’entiers naturels ( A (cid:204) ℕℕℕℕ )

(cid:2) On dit que l’ensemble A est récursif ssi

la fonction totale f : ℕℕℕℕ fi ℕℕℕℕ définie par

ℕℕℕℕ

ℕℕℕℕ

  • f (n) = 1 si n ˛ A
  • f (n) = 0 sinon

est récursive

Autrement dit

(cid:2) Il existe un programme qui pour toute donnée n ˛

  • imprime (au bout d’un temps fini) «OUI»

˛ ℕℕℕℕ

si n ˛ A

  • imprime (au bout d’un temps fini) «NON» sinon

ENSI

Logique Mathématique

6

˛

˛

Notion de décidabilité

3- Ensemble récursivement énumérable

Soit A un ensemble d’entiers naturels ( A (cid:204) ℕℕℕℕ )

(cid:2) On dit que A est récursivement énumérable ssi

il existe une fonction récursive f

telle que A = Dom( f )

Autrement dit

(cid:2) Il existe un programme qui pour toute donnée n ˛

(cid:2) Il existe un programme qui pour toute donnée n ˛

˛ ℕℕℕℕ

˛ ℕℕℕℕ

  • imprime (au bout d’un temps fini)

«OUI» si n ˛ A

  • ne s’arrête jamais (tourne indéfiniment)

sinon (n ˇ A)

Autre définition

(cid:2) Il existe un programme à 0 entrée qui

ENSI

Logique Mathématique

7

imprime tous les éléments de A

˛

˛

˛

˛

Notion de décidabilité

Exemple

Soit U = { u0, u1, u2 ...} les éléments d’une suite sur les entiers

naturels

(cid:2) si U est une suite monotone alors l’ensemble U est récursif

(cid:1) pour toute donnée n ˛

savoir si oui ou non n ˛

˛ ℕℕℕℕ,

˛ U

(cid:2) si U est une suite non monotone (ex. suite de Goodstein)

(cid:2) si U est une suite non monotone (ex. suite de Goodstein)

il est toujours possible de

alors l’ensemble U est récursivement énumérable

(cid:1) pour toute donnée n ˛

savoir si oui ou non n ˛

un ui tel que ui = n, on ne peut rien dire)

˛ ℕℕℕℕ, il n’est pas possible de

˛ U (tant qu’on ne trouve pas

(cid:1) mais on peut énumérer tous les éléments de U

ENSI

Logique Mathématique

suite

8

˛

˛

˛

˛

˛

˛

˛

˛

Notion de décidabilité

Suite de Goodstein (1980) un(m) n, m ˛

u0 = m

˛ ℕℕℕℕ

u1 : on écrit u0 complètement en base 2 (mantisse et exposant)

on remplace tous les 2 par 3 et on enlève 1 au résultat

ex. pour m = 9 : 9 = [2 2 exp1 + 1 + 1]2 , u1 = (3 3 exp1 + 1 + 1) -1 = 81

u2 : on procède de la même manière mais en base 3

u : on procède de la même manière mais en base 3

on remplace tous les 3 par des 4 et on enlève 2

ex. pour m = 9 : u2 = 1023

Proposition : pour tout m ˛

˛ ℕℕℕℕ, il existe n tel que un(m) = 0

Donc la suite un(m) n’est pas monotone

(elle croît rapidement et elle décroît subitement )

ENSI

Logique Mathématique

9

˛

˛

˛

˛

Notion de décidabilité

4- Prédicat décidable

Soit Q un prédicat à k arguments

(cid:2) On dit que Q est décidable ou récursif

ssi

l’ensemble { (a1, …,ak) : Q(a1, …,ak) = V } est récursif

Autrement dit

(cid:2) Il existe un programme qui pour tout k-uplet (a1, …,ak)

  • imprime «OUI»
  • imprime «NON»

si Q(a1, …,ak) = V

sinon

ENSI

Logique Mathématique

10

Notion de décidabilité

5- Prédicat semi-décidable

Si un prédicats n’est pas décidable alors on dit qu’il est non

Publicité

décidable (ou indécidable)

Certains

prédicats

non

décidables

ont

une

propriété

théoriquement

théoriquement

intéressante (mais pas pratique)

intéressante (mais pas pratique)

qui est

qui est

la

la

propriété de semi-décidabilité

ENSI

Logique Mathématique

11

Notion de décidabilité

Soit Q un prédicat à k arguments

(cid:2) On dit que Q est

semi-décidable (ou récursivement

énumérable)

ssi

l’ensemble

{ (a1, …,ak) : Q(a1, …,ak) = V } est récursivement énumérable

Autrement dit

(cid:2) Il existe un programme qui pour tout k-uplet (a1, …, ak)

(cid:2) Il existe un programme qui pour tout k-uplet (a , …, a )

  • imprime «OUI» si Q(a1, …, ak) = V
  • ne s’arrête jamais (tourne indéfiniment) sinon

Autre définition

(cid:2) Il existe un programme à 0 entrée qui imprime tous les

k-uplets (a1, …, ak) tels que Q(a1, …, ak) = V

ENSI

Logique Mathématique

12

Notion de décidabilité

Remarque

Il n’est pas possible de détecter la non terminaison

c-à-d le fait de savoir si un programme termine ou non est un

problème lui même indécidable (semi-décidable)

La semi-décidabilité peut être vue ainsi :

(cid:2) Ie prédicat Q est semi-décidable s’il existe un programme qui

pour tout k-uplet (a1, …, ak)

  • s’il imprime «OUI» au bout d’un temps fini
  • sinon «on ne sait pas»

alors Q(a1, …, ak) = V

ENSI

Logique Mathématique

13

Notion de décidabilité

Exemple

(cid:2) Soit U = { u0, u1, u2 ...} une suite sur les entiers naturels

Soit le prédicat Q(x) = « x ˛

˛ U »

-

-

si U est une suite monotone alors Q est décidable

si U est une suite non monotone

alors Q est semi-décidable

(cid:2) Le problème d’Epiménide le crétois (ou le paradoxe du

menteur) n’est ni décidable ni semi-décidable

« Epiménide le crétois prétendais que tous les crétois étaient

menteurs » OU Sous sa forme la plus concise :

« un homme déclare « Je mens ». Si c'est vrai, c'est faux. Si c'est faux,

c'est vrai. »

ENSI

Logique Mathématique

14

˛

˛

Notion de décidabilité

Remarques

• Tout ensemble fini est récursif

• L’ensemble des ensembles récursifs est inclus dans celui des

ensembles récursivement énumérables. L’inverse est faux.

De même pour les prédicats décidables

Remarque. Les définitions présentées dans ce chapitre sont

informelles mais suffisantes pour notre cours. Pour des

définitions plus formelles, il faut faire appel à d’autres notions :

Machine de Turing, Fonctions primitives récursives, thèse de

Turing-Church...

ENSI

Logique Mathématique

15

Notion de décidabilité

6- Cas de la logique des prédicats

(cid:2) Dans le CP0, la satisfiabilité et la validité sont décidables

(on dit que le calcul propositionnel est décidable)

(cid:1) Il suffit de dresser la table de vérité

(cid:2) Dans le CP1, la validité et la satisfiabilité sont indécidables

(cid:2) Dans le CP1, la validité et la satisfiabilité sont indécidables

(théorème de Church)

(cid:1) nous verrons dans la suite du cours qu’il existe des

procédures qui

oui chaque fois qu’une

formule A est valide. Mais ces procédures pourrons ne

pas terminer si A n’est pas valide

répondent

(cid:1) le calcul des prédicats est semi-décidable

ENSI

Logique Mathématique

16

Notion de décidabilité

Alenzo CHURCH (14 juin 1903 – 11 août 1995)

Mathématicien (logicien) américain à qui l'on doit certains

des fondements de l’informatique théorique. Ses travaux

ont eu un impact très important dans les domaines de la

logique et de la théorie de la récursivité

Il est connu principalement pour le développement du lambda-calcul (en

1930) et pour son article de 1936 (Princeton) dans lequel il démontre

l'existence d'un problème indécidable et que toute fonction calculable

peut l'être avec un ensemble réduit d'instructions. C'est une affirmation

philosophique indémontrable qui est la base de toute l’algorithmique. Ce

résultat précède le fameux travail d'Alan Turing sur le problème de l'arrêt

qui démontra aussi l'existence d'un problème insoluble par des moyens

mécaniques

suite

ENSI

Logique Mathématique

17

Notion de décidabilité

Supervisant la thèse doctorale de Turing, ils

démontrèrent alors que le lambda-calcul de Church et

la machine de Turing utilisée dans son étude du

problème de l'arrêt avaient des capacités équivalentes,

puis qu'un certain nombre de formalisations

mathématiques de la notion de traitement par des processus mécaniques

ont des aptitudes de traitement équivalentes. Cette constatation aboutit à

ont des aptitudes de traitement équivalentes. Cette constatation aboutit à

la thèse de Turing-Church.

Ses travaux influencèrent notamment le langage de

programmation LISP

Parmi ses autres étudiants à Princeton il y avait Stephen

Kleene qui a beaucoup contribué dans l’étude de la

théorie des langages.

ENSI

Logique Mathématique

18

Notions fondamentales

II- Introduction aux Systèmes formels

1- Définitions : système formel, déduction, théorème

2- Propriétés des système formels

2- Propriétés des système formels

3- Algorithme général d’application

ENSI

Logique Mathématique

19

Système formel

1- Définitions

Les systèmes formels sont des outils permettant de mettre en

œuvre des algorithmes de déduction.

ENSI

Logique Mathématique

20

Système formel

Définition Système formel

Un système formel (ou système d’inférence) S, est la donnée de :

(cid:2) Un alphabet ∑S (fini ou infini dénombrable)

(cid:2) Un sous-ensemble récursif FSSSS de l’ensemble de toutes les

suites finies d’éléments de ∑S

FS est appelé l’ensemble des formules bien formées de S

FS est appelé l’ensemble des formules bien formées de S

(cid:204) ∑S* )

(FS

(cid:2) Un sous-ensemble récursif AS de FS

( AS

AS est appelé l’ensemble des axiomes de S

(cid:204) FS )

(cid:2) Un ensemble fini R S de relations sur FS appelé l’ensemble

des règles d’inférence (ou règles de déduction ou règles de

dérivation) R S = { r1, r2, …, rn }

suite

ENSI

Logique Mathématique

21

Système formel

Une règle ri est notée

ou

A1, …, Ap

B

ri

A1, …, Ap

B

ri

Ce qui veut dire « à partir des formules A1, …, Ap on déduit

par la règle ri la formule B »

• Les formules A1, …, Ap sont appelées les prémisses

• La formule B est appelée la conclusion

ENSI

Logique Mathématique

22

Système formel

Définition Déduction

On appelle déduction à partir des formules A1, …, An

toute suite finie B1, …, Bp de formules telle que

pour tout i ˛

[1..p] , la formule Bi est :

Publicité

• soit un axiome

• soit l’une des formules A1, …, An

• soit l’une des formules A1, …, An

• soit obtenue par application de la règle rk

˛ R S

à partir des formules Bi0, …, Bim placées avant Bi

On dit que la suite B1, …, Bp est une déduction de Bp à partir

des hypothèses A1, …, An dans le système S

On note : A1, …, An

Bp

S

ENSI

Logique Mathématique

23

˛

˛

˛

˛

˛

˛

Système formel

Déduction

hypothèses

conclusion

A1 . . . An

B1

B2

:

:

Bi

:

:

Bp

  • axiome
  • axiome
  • A1 ou A2 …ou An
  • résultat de la règle rk

ENSI

Logique Mathématique

24

Système formel

Définition Théorème

On appelle théorème du système formel S toute formule A

pour la quelle il existe une déduction à partir du vide (c-à-d

sans hypothèse)

Notation A ou S

S

A

On note par TS

T

l’ensemble des théorèmes de S

S

Remarque

Une déduction à partir du vide est aussi appelée une preuve

(ou une démonstration)

ENSI

Logique Mathématique

25

Proposition

Si A1, …, Ak

A1, …, Ak

Système formel

B1

B2

S

S

:

:

S

A1, …, Ak Bm

et B1, B2, …, Bm

S

C alors A1, …, Ak

C

S

En particulier si A B et B C alors A C

S

S

S

Corollaire

Toute formule déduite à partir d’un théorème est un théorème

ENSI

Logique Mathématique

26

Système formel

Exemple : le jeu des allumettes

« On dispose d’un tas de n allumettes. 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. Un tas de 10 allumettes. Le joueur A commence.

Exemple. Un tas de 10 allumettes. Le joueur A commence.

– A retire 2 allumettes. Reste 8

– B retire 1 allumette. Reste 7

– A retire 3 allumettes. Reste 4

– B retire 2 allumettes. Reste 2

– A retire les deux dernières allumettes. A a gagné

ENSI

Logique Mathématique

27

Système formel

Le Système formel JA

(cid:2) ∑JA = { A, B} U ℕℕℕℕ

(cid:2) FJAJAJAJA = { mots de la forme (A|B)(A|B)k avec k ˛ ℕℕℕℕ}

exemple : AB14, BB3 ...

Sémantique

AB14 : « le joueur A est sûr de gagner si c’est au joueur

AB14 : « le joueur A est sûr de gagner si c’est au joueur

B de jouer et il reste 14 allumettes dans le tas»

Négation

non(AAk) = BAk non(ABk) = BBk

non(BBk) = ABk non(BAk) = AAk

c-à-d. si AAx est vrai alors BAx est faux

(si A gagne alors B perd)

ENSI

Logique Mathématique

suite

28

Système formel

(cid:2) AJA = { AB4, BA4}

(cid:2) R JA = { ABk

r1

AAk+1 , ABk

AAk+2

r2

ABk AAk+3 , ABk ABk+4

ABk AAk+3 , ABk ABk+4

BAk BBk+1 , BAk BBk+2

BAk BBk+3 , BAk BAk+4 }

r4

r6

r8

r3

r5

r7

ENSI

Logique Mathématique

29

Système formel

o Montrons que AA18 est un théorème ( JA

AA18 )

AB4 AB8 AB12

r4

r4

AB16

r4

r2

AA18

Déroulement du jeux :

  • A retire de 1 à 3 allumettes. Par exemple 1. Reste 17
  • B retire de 1 à 3 allumettes. Par exemple 3. Reste 14
  • A retire par exemple 2. Reste 12
  • A retire par exemple 2. Reste 12
  • B retire par exemple 2. Reste 10
  • A retire par exemple 3. Reste 7
  • B retire par exemple 2. Reste 5
  • A doit retirer 1 allumette. Reste 4 (car AB4 est un axiome)
  • Quelque soit le retrait de B (de 1 à 3 allumettes). A retire le reste

et il gagne

o Est-ce que AB25 est un théorème ? Et AB7654 ?

ENSI

Logique Mathématique

30

Système formel

2- Propriétés des Systèmes formels

(cid:2) Un système formel S (comportant le symbole de négation

«  ») est dit consistant (ou non contradictoire), s’il n’existe

aucune formule bien formée A de S telle que A et  A

soient tous les deux des théorèmes de S

c-à-d il ne prouve pas une formule et son contraire

c-à-d il ne prouve pas une formule et son contraire

Dans le cas contraire le système S est dit inconsistant (ou

contradictoire)

(cid:2) Un système formel S est dit cohérent s’il existe des

formules bien formées qui ne soient pas des théorèmes

ENSI

Logique Mathématique

suite

31

Système formel

(cid:2) Un système formel S est dit correct (sound) si TS

˝ T

T étant un ensemble de formules qu’on veut obtenir comme

théorèmes dans la modélisation d’une situation particulière

(cid:2) Un système formel S est dit complet (complete) si T ˝ TS

(cid:2) Un système formel S est dit correct et complet si T = TS

(cid:2) On appelle problème de décision pour le système formel S

(cid:2) On appelle problème de décision pour le système formel S

’’le problème de savoir si l’ensemble TS est récursif ou non’’

c-à-d le problème de savoir si le prédicat

P(t) = « t est un théorème de S » est décidable ou non

Lorsque le problème de décision admet une réponse positive,

le système d’inférence est dit décidable

ENSI

Logique Mathématique

32

Système formel

Quelques résultats

(cid:2) Un système formel correct est forcément consistant

(cid:2) Un système formel consistant et complet est forcément correct

(cid:2) Un système formel incomplet n’est pas décidable (il est

généralement semi-décidable)

(cid:2) Un système formel complet n’est pas forcément décidable (il

(cid:2) Un système formel complet n’est pas forcément décidable (il

peut être semi-décidable)

En effet la complétude dit seulement que « si A est un

théorème alors on est sûr de trouver une preuve » mais ne dit

pas « pour tout A on est sûr de dire si A est un théorème ou

non »

ENSI

Logique Mathématique

33

Publicité

Système formel

Exemple : le jeu des allumettes

Essayons de démontrer si AB7654 est vraie (c-à-d un théorème).

On peut être dans l’une des situations suivantes :

1. on trouve AB7654 vraie et BB7654 (=non(AB7654) ) faux

2. on trouve BB7654 vraie et AB7654 faux

3. on trouve AB7654 vraie, alors qu’en réalité A ne gagne

pas si B commence

(cid:1) dans ce cas le système JA JA JA JA serait non correct

4. on trouve AB7654 et BB7654 tous les deux vraies

(cid:1) dans ce cas le système JAJAJAJA serait inconsistant

ENSI

Logique Mathématique

suite

34

Système formel

5. on n’arrive à démontrer ni AB7654 ni BB7654

(cid:1) dans ce cas le système JA serait incomplet

Dans notre cas :

Dans notre cas :

le système JAJAJAJA est consistant et complet (donc correct)

(cid:1) il ne permet pas de démontrer une formule et son

contraire et il permet de démontrer toutes les formules

(cid:1) on trouve la situation 1 : AB7654 est un théorème

ENSI

Logique Mathématique

35

Système formel

(cid:1) Ce n’est pas toujours le cas pour tous les systèmes formels.

Surtout les systèmes formels « suffisamment complexes »

(modélisant les théories mathématiques)

Théorème d’incomplétude de Gödel

Théorème d’incomplétude de Gödel

ENSI

Logique Mathématique

36

Système formel

3- Algorithme général d’application

Déduire-S (C ,HHHH)

/* déduire dans le système S la formule C

à partir de l’ensemble des hypothèses H */

début

Ω := H

répéter jusqu’à (condition-arrêt)

– choisir

– choisir

  • une règle ri

˛ R S et des formules A1, …, Ak

˛ Ω

telles que A1, …, Ak

ou - un axiome B ˛

˛ AS

B

ri

– Ω := Ω U {B}

fin

ENSI

Logique Mathématique

37

˛

˛

˛

˛

˛

Système formel

Remarques

• Pour montrer qu’une formule est un théorème, on prend

l’ensemble des hypothèses H égal à l’ensemble vide

• L’algorithme précédent peut se trouver dans l’une des

situations suivantes :

1) il termine sur condition d’arrêt

1) il termine sur condition d’arrêt

(cid:1) en particulier si C ˛

˛ Ω alors H

C

S

2) il se bloque (on ne peut plus faire aucun choix)

(cid:1) dans ce cas C n’est pas une conclusion de H

3) Il ne termine pas (tourne indéfiniment)

(cid:1) dans ce cas on ne peut rien dire

ENSI

Logique Mathématique

suite

38

˛

˛

Système formel

• La procédure Choisir joue un rôle important dans la

terminaison. Il faut fixer une stratégie de choix qui permet de

converger rapidement vers la condition d’arrêt. Ceci dépend

du domaine sur lequel on travaille.

• Si le système S n’est pas complet, l’algorithme ne s’arrête

pas tout le temps même lorsque la formule à démontrer est

pas tout le temps même lorsque la formule à démontrer est

un théorème et ceci quelle que soit la stratégie de choix

adoptée. On dit aussi que le système S ne termine pas.

• Un système formel correct et qui termine est forcément

complet

• L’algorithme précédent est appelé un moteur d’inférence

ENSI

Logique Mathématique

39

Exemple : le jeu des allumettes

• Pour montrer que AA18 est un théorème on exécute

Déduire-JA(AA18, Ø)

Dans ce cas l’algorithme s’arrête avec AA18 ˛

˛ Ω

• Déduire-JA(AB25, Ø) ?

• Déduire-JA(AB7654, Ø) ?

ENSI

Logique Mathématique

40

˛

˛

Notions fondamentales

III- Application au calcul des prédicats

Pour montrer

{H1, …, Hn} ╞ C ou ╞ C

Il faut disposer d’un système formel

qui soit correct et complet pour le calcul des prédicats

Soit CP un système formel correct et complet pour le calcul

des prédicats, alors :

{H1, …, Hn} ╞ C

╞ C

ssi

ssi

H1, …, Hn

C

CP

C

CP

ENSI

Logique Mathématique

41

Application au Calcul des prédicats

Correction :

Si

H1, …, Hn

Si

CP

CP

C

alors

{H1, …, Hn} ╞ C

C alors ╞ C

Complétude :

Si

{H1, …, Hn} ╞ C alors H1, …, Hn

C

CP

Si ╞ C

alors

C

CP

ENSI

Logique Mathématique

42

Application au Calcul des prédicats

Il existe plusieurs systèmes formels permettant de faire des

déductions et des preuves dans le calcul des prédicats. Ils se

classent en deux catégories selon le principe de preuve

adopté :

(cid:2) Méthodes déductives

(cid:1) le système de Hilbert (+ règl. et 1 ax.)

(cid:1) le système de Lukaseiwicz (1 règl. et 3 ax.)

(cid:1) le système de Lukaseiwicz (1 règl. et 3 ax.)

(cid:1) le calcul des séquents : système de déduction

naturelle, système de Gentzen ( + règl. et 1 ax.)

(cid:1) …

(cid:2) Méthode réfutationnelle (preuve par contradiction)

(cid:1) le principe de résolution de Robinson

( 2 règ + 0 ax.)

ENSI

Logique Mathématique

43

Application au Calcul des prédicats

Méthode déductive

{ hypothèses }

H1111 . . . Hnnnn

déduction

conclusion

C

ENSI

Logique Mathématique

44

Application au Calcul des prédicats

Méthode réfutationnelle

{ hypothèses } U

{négation conclusion}

H1111 . . . Hnnnn

 C

déduction

déduction

(réfutation)

contradiction

ENSI

Logique Mathématique

45

(cid:128)

(cid:128)

Publicité

(cid:128)

(cid:128)

Notions fondamentales

IV- Théorème d’incomplétude de Gödel

• Soit CP = (∑CP, FCP, ACP, R CP) un système formel correct et

complet pour le calcul des prédicats

• Soit Th une théorie récursive

(c-à-d un ensemble récursif de formules closes)

Th peut être un ensemble de formules formalisant dans une

structure mathématique les axiomes définissant une théorie

mathématique.

Par exemple : la théorie des groupes, des anneaux,

des corps, de l’arithmétique (Peano),

des ensembles (Zermelo-Fraenkel), ...

ENSI

Logique Mathématique

46

Théorème d’incomplétude de Gödel

Pour montrer que C est un théorème de la théorie Th ,

on montre par le système CP que

Th ╞ C c-à-d Th

C

CP

• Soit le système formel suivant :

STh = (∑CP, FCP, ACP U Th, R CP)

STh est construit en ajoutant aux axiomes du système CP

les formules de la théorie Th. On obtient ainsi un

système formel formalisant une théorie. Qu’on appelle

aussi une théorie axiomatique

ENSI

Logique Mathématique

47

Théorème d’incomplétude de Gödel

Nous avons :

Th

CP

C ssi

C

STh

En effet, il est facile de vérifier que Déduire-CP(C,Th) et

Déduire-STh(C, Ø) donnent le même résultat

Remarques

(cid:2) Toutes les propriétés (complétude, consistance, ...) du

système STh s’appliquent à la théorie Th

c-à-d si par exemple le système STh est complet, on dit

aussi que la théorie Th est complète

C est aussi noté STh

C

Logique Mathématique

48

(cid:2)

STh

ENSI

Théorème d’incomplétude de Gödel

Théorème d’incomplétude de Gödel (1931)

1. Tout système formel consistant, et formalisant

l'arithmétique des entiers, est incomplet.

Autrement dit. Dans toute branche des mathématiques

suffisamment complexe (par exemple l'arithmétique), il

existe une infinité de faits vrais qu'il est impossible de

existe une infinité de faits vrais qu'il est impossible de

prouver en utilisant la branche des mathématiques en

question.

2. Aucun système formel consistant, et formalisant

l'arithmétique des entiers, ne peut prouver sa propre

consistance.

ENSI

Logique Mathématique

49

Théorème d’incomplétude de Gödel

(cid:2) La première partie du théorème de Gödel dit qu'il existe

des énoncés sur les entiers dont on ne sait pas démontrer,

en utilisant les seuls axiomes de la logique construisant les

entiers. Ceci même en ajoutant de nouveaux axiomes

Exemple. La conjecture de Fermat :

« Pour tout entier n > 2,

il n'existe aucun triplet d'entiers x,y,z tels que xn+yn = zn »

il n'existe aucun triplet d'entiers x,y,z tels que xn+yn = zn »

Pour n=2, il existe des valeurs évidentes de x,y,z, par exemple (3,4,5)

Les mathématiciens ont essayé de trouver une solution. Puis ils ont cherché

à démontrer qu'il n'y avait aucune solution. Sans résultat.

Or d'après le théorème de Gödel, il était possible que cette conjecture soit

vraie mais indémontrable, autrement dit, que ce soit un axiome à rajouter à

l'arithmétique des entiers. A la fin ils ont abandonné

Andrew Wiles, en 1995, trouva enfin une démonstration. La conjecture

devient ainsi un théorème

ENSI

Logique Mathématique

50

Théorème d’incomplétude de Gödel

(cid:2) La deuxième partie du théorème donne une réponse au

2ème des 23 problèmes qu'Hilbert avait énoncés en 1900 :

« peut-on prouver la consistance de l'arithmétique en

utilisant seulement les axiomes de l'arithmétique ? »

(cid:2) Avec son théorème d’incomplétude; Gödel a mis fin aux

espoirs de Hilbert de créer des théories mathématiques

espoirs de Hilbert de créer des théories mathématiques

formelles et d’utiliser les systèmes formels pour faire des

déductions automatiques ne laissant aucune place à

l'intuition. En effet, la démonstration de théorèmes

mathématiques ne peut pas être que mécanique et que

l'intuition est nécessaire (elle est indécidable)

ENSI

Logique Mathématique

51

Théorème d’incomplétude de Gödel

Kurt GÖDEL (2 avril 1906 - 14 janvier 1978)

Né à Brno (Empire Austro-Hongrois, aujourd'hui situé

en république tchèque). Il fait de brillantes études

secondaires en Allemagne et obtient son titre de

docteur à 23 ans (1929) à Vienne.

Il est le mathématicien qui, de tout le XXè siècle, a le plus révolutionné les

fondements logiques des mathématiques. Il était tellement obsédé par la

fondements logiques des mathématiques. Il était tellement obsédé par la

logique qu'on raconte que, alors qu'il cherchait à obtenir sa naturalisation

américaine(en 1948), il osa démontrer devant le juge la contradiction de

certains articles de la constitution des Etats-Unis. Il était aussi victime

d'une maladie mentale, une paranoïa qui lui faisait croire qu'on cherchait à

l'empoisonner, le poussa à la diète, et le fit mourir à petits feux.

Il est considéré par Times Magazine comme un des 20 scientifiques les

plus importants du XXème siècle.

suite

ENSI

Logique Mathématique

52

Théorème d’incomplétude de Gödel

Sa thèse, et surtout un article publié en 1931 sous le titre "Über formal

unentscheidbare Sätze der Principia Mathematica und verwandter Systeme"

(sur l'indécidabilité formelle des Principia Mathematica et de systèmes

équivalents), donneront à Gödel une réputation internationale.

Gödel a fait aussi des découvertes fondamentales en théorie des ensembles.

Il prouve notamment que l'hypothèse du continu et l'axiome du choix ne sont

pas en contradiction avec les autres axiomes de la théorie des ensembles.

A son arrivée aux États-Unis, Gödel commence à étudier

la relativité, avec son ami de Princeton Albert Einstein, et

les implications philosophiques de ses travaux. Gödel est

ainsi connu parmi les physiciens pour avoir démontré

que le voyage vers le passé est possible dans le cadre

des équations de la relativité générale d'Einstein.

Il est aussi ami avec Von Neumann.

ENSI

Logique Mathématique

53

Théorème d’incomplétude de Gödel

David HILBERT (1862 - 1943)

Mathématicien allemand, l'un des plus grands (le ?) du

20è siècle.

Partisan d'un formalisme rigoureux, ses travaux se situent

dans l'axiomatisation de la géométrie euclidienne (1899,

Grundlagen der Geometrie : fondements de la géométrie),

dans la construction d'espaces vectoriels topologiques et

dans la construction d'espaces vectoriels topologiques et

fonctionnels abstraits(espaces hilbertiens) englobant les

espaces vectoriels euclidiens (en hommage à Euclide) et hermitiens (en

hommage à Hermite), dans le développement de l'analyse fonctionnelle,

de l'algèbre (anneaux de polynômes), de la théorie des nombres. Les

espaces de Hilbert sont un outil essentiel en mécanique quantique et en

calcul tensoriel.

ENSI

Logique Mathématique

suite

54

Théorème d’incomplétude de Gödel

La volonté de Hilbert fut de reconstruire les mathématiques sur des

fondements axiomatiques, indépendamment de la logique ensembliste. Il

réussit la reconstruction de la géométrie euclidienne : cinq groupes de

quatre axiomes, dont quinze équivalent à ceux d‘Euclide. Il est alors

désormais clair que la géométrie euclidienne est consistante. Les problème

de l'arithmétique, de la géométrie algébrique et de la théorie des ensembles

sont beaucoup plus difficiles à reconstruire axiomatiquement. Ils firent l'objet

des célèbres 23 problèmes ouverts cités au congrès de 1900 qui devaient

guider les mathématiciens de notre siècle.

Il publie en 1893 le Zahlbericht : un état complet de la connaissance en

théorie des nombres et, en 1897, une théorie complète des corps de

nombres algébriques.

ENSI

Logique Mathématique

suite

55

Théorème d’incomplétude de Gödel

Les plus célèbres, des 23 grands problèmes ouverts de Hilbert, et les plus

accessibles pour nous :

1/ Démontrer l'hypothèse du continu. Démontrer indécidable par Cohen,1963.

2/ Consistance des axiomes de l'arithmétique. Résolu par la négative,

théorème d'incomplétude de Gödel, 1931.

7/ Transcendance de nombres comme

Partiellement résolu par Gelfond, Schneider et Baker, 1939.

Partiellement résolu par Gelfond, Schneider et Baker, 1939.

8/ Le problème de la distribution des nombres premiers (leur répartition dans

ℕℕℕℕ) et la conjecture de Riemann concernant les nombres ζ(n). Non résolu.

10/ Recherche d'un algorithme permettant de savoir si une équation

diophantienne admet ou non des solutions. Résolu par la négative

indécidable) en 1970 par le mathématicien russe Youri Matiyasevitch.

ENSI

Logique Mathématique

56