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