Demonstrations et modeles Theoreme de completude Complements De la verite a la demonstration : le theoreme de completude de G odel Guillaume Brunerie Seminaire mathematique des eleves du lycee Louis-le-Grand 4 fevrier 2009 Guillaume Brunerie Le theoreme de completude de G odel2 Theoreme de completude Theoreme de correction Theoreme de completude 3 Complements Arithmetique non standard Extension a des systemes formels quelconques Demonstrations et modeles Theoreme de completude Complements Sommaire 1 Demonstrations et modeles Termes et formules Demonstrabilite Validite Guillaume Brunerie Le theoreme de completude de G odel3 Complements Arithmetique non standard Extension a des systemes formels quelconques Demonstrations et modeles Theoreme de completude Complements Sommaire 1 Demonstrations et modeles Termes et formules Demonstrabilite Validite 2 Theoreme de completude Theoreme de correction Theoreme de completude Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles Theoreme de completude Complements Sommaire 1 Demonstrations et modeles Termes et formules Demonstrabilite Validite 2 Theoreme de completude Theoreme de correction Theoreme de completude 3 Complements Arithmetique non standard Extension a des systemes formels quelconques Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles Termes et formules Theoreme de completude Demonstrabilite Complements Validite Sommaire 1 Demonstrations et modeles Termes et ...
Demonstrations et modeles
Theoreme de completude
Complements
De la verite a la demonstration : le theoreme
de completude de G odel
Guillaume Brunerie
Seminaire mathematique des eleves
du lycee Louis-le-Grand
4 fevrier 2009
Guillaume Brunerie Le theoreme de completude de G odel2 Theoreme de completude
Theoreme de correction
Theoreme de completude
3 Complements
Arithmetique non standard
Extension a des systemes formels quelconques
Demonstrations et modeles
Theoreme de completude
Complements
Sommaire
1 Demonstrations et modeles
Termes et formules
Demonstrabilite
Validite
Guillaume Brunerie Le theoreme de completude de G odel3 Complements
Arithmetique non standard
Extension a des systemes formels quelconques
Demonstrations et modeles
Theoreme de completude
Complements
Sommaire
1 Demonstrations et modeles
Termes et formules
Demonstrabilite
Validite
2 Theoreme de completude
Theoreme de correction
Theoreme de completude
Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles
Theoreme de completude
Complements
Sommaire
1 Demonstrations et modeles
Termes et formules
Demonstrabilite
Validite
2 Theoreme de completude
Theoreme de correction
Theoreme de completude
3 Complements
Arithmetique non standard
Extension a des systemes formels quelconques
Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Sommaire
1 Demonstrations et modeles
Termes et formules
Demonstrabilite
Validite
2 Theoreme de completude
3 Complements
Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Termes de l’arithmetique
C : ensemble des symboles de constantes, 02C
V : des symboles de variables (in ni)
De nition
L’ensemble des termes surC est de ni par :
T =CjVj STj (T +T )j (T T )
De nition
Un terme qui ne contient pas de symbole de variable est appelle un
terme clos.
Guillaume Brunerie Le theoreme de completude de G odelDemonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Exemples de termes
Exemples
Si c2C et x; y2V,
x Sy + c n’est rien du tout
(0 + (0 Sc)) est un terme clos
(((c + Sy) S(Sx (SS0 + SSSx))) + 0) est un terme.
Guillaume Brunerie Le theoreme de completude de G odelVariables libres : variables non liees par un quanti cateur
Formule close : formule sans variable libre
Theorie : ensemble de formules closes
De nitions
Demonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Formules logiques
De nition
L’ensemble des formules est de ni par :
F =?j (T =T )j:Fj (F_F)j (F^F)j (F!F)j9VFj8VF
Guillaume Brunerie Le theoreme de completude de G odelFormule close : formule sans variable libre
Theorie : ensemble de formules closes
Demonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Formules logiques
De nition
L’ensemble des formules est de ni par :
F =?j (T =T )j:Fj (F_F)j (F^F)j (F!F)j9VFj8VF
De nitions
Variables libres : variables non liees par un quanti cateur
Guillaume Brunerie Le theoreme de completude de G odelTheorie : ensemble de formules closes
Demonstrations et modeles Termes et formules
Theoreme de completude Demonstrabilite
Complements Validite
Formules logiques
De nition
L’ensemble des formules est de ni par :
F =?j (T =T )j:Fj (F_F)j (F^F)j (F!F)j9VFj8VF
De nitions
Variables libres : variables non liees par un quanti cateur
Formule close : formule sans variable libre
Guillaume Brunerie Le theoreme de completude de G odel