Support de cours Logique Mathématique

1 R publique Alg rienne D mocratique et Populaire Minist re de l'Enseignement Sup rieur et de la Recherche Scientifique Support de cours Logique Math matique cours d stin aux tudiants de 2me ann e licence Informatique Pr par par Dr ADEL n e AISSANOU Karima 2015/2016. 1. A Zahir, Melissa et Table des mati res Table des mati res 1. Introduction 4. 1 Le langage du calcul propositionnel 8. Introduction .. 8. D finition .. 9. Le langage propositionnel .. 9. La syntaxe du langage propositionnel .. 9. Priorit des connecteurs .. 10. S mantique d'un langage propositionnel .. 10. Satisfiabilit .. 13. Satisfiabilit d'un ensemble de formules .. 13. Tautologie .. 13. Cons quence Logique .. 14. Th or me de substitution .. 15.

2 Th or me de remplacement .. 15. Syst me complet de connecteurs .. 15. Forme normale .. 16. Obtention de Forme normale disjonctive (FND) .. 16. Forme normale conjonctive (FNC) .. 16. Conclusion .. 17. Exercices .. 18. 2 Th orie de la d monstration pour le calcul propositionnel 21. Introduction .. 21. Liste des axiomes .. 22. 2. 3. Les r gles ou sch mas de d duction .. 23. R gle de d tachement (ou Modus Ponens) .. 23. R gle de substitution .. 23. R gle S .. 24. R gles I .. 24. R gles II .. 25. R gles III .. 25. R gles IV .. 25. R gles V .. 26. Liste des th or mes .. 27. Exercices .. 28. Corrig s des exercices .. 29. 3 Le langage du calcul des pr dicats du premier ordre 35. Introduction .. 35. D finitions .. 36.

3 Le langage des pr dicats du premier ordre .. 36. Alphabet .. 36. Les expressions du langage .. 37. Priorit des connecteurs .. 37. Champ d'un quantificateur .. 37. Variable libre et variable li e .. 38. Formule close (ferm e .. 38. S mantique de la Logique des pr dicats du premier ordre .. 38. Interpr tation .. 38. Valuation .. 39. Interpr tation d'un terme .. 39. Interpr tation d'une formule .. 39. Satisfiablit d'une formule .. 40. Mod le d'une formule .. 40. Formule valide .. 41. Satisfiabilit d'un ensemble de formules .. 41. Mod le d'un ensemble de formules .. 42. Cons quence Logique .. 42. Table des mati res 4. Renommage .. 42. Normalisation .. 43. Forme pr nexe .. 43. Forme de Skolem (Skolemisation).)

4 44. Forme clausale .. 45. Compl tude et d cidabilit .. 46. Conclusion .. 46. Exercices .. 47. Corrig s des exercices .. 49. 4 Le calcul des s quents 54. Introduction .. 54. Exercices .. 58. Introduction 5. Introduction La Logique math matique est n e la fin du 19ie me si cle au sens philosophique du terme ; elle est l'une des pistes explor es par les math maticiens de cette poque afin de r soudre la crise des fondements provoqu e par la complexification des math matiques et l'apparition des paradoxes. Ses d buts sont marqu s par la rencontre entre deux id es nouvelles : la volont chez Frege, Russell, Peano et Hilbert de donner une fondation axioma- tique aux math matiques ;. la d couverte par George Boole de l'existence de structures alg briques permet- tant de d finir un calcul de v rit.

5 La Logique math matique se fonde sur les premi res tentatives de traitement formel des math matiques, dues Leibniz et Lambert (fin 16ie me si cle - d but 17ie me si cle). Leibniz a en particulier introduit une grande partie de la notation math matique mo- derne (usage des quantificateurs, symbole d'int gration, etc.). Toutefois on ne peut par- ler de Logique math matique qu' partir du milieu du 19ie me si cle, avec les travaux de George Boole (et dans une moindre mesure ceux d'Auguste De Morgan) qui introduit un calcul de v rit o les combinaisons logiques comme la conjonction, la disjonction et l'implication, sont des op rations analogues l'addition ou la multiplication des entiers, mais portant sur les valeurs de v rit faux et vrai (ou 0 et 1) ; ces op rations bool ennes se d finissent au moyen de tables de v rit.

6 Le calcul de Boole v hiculait l'id e apparemment paradoxale, mais qui devait s'av - rer spectaculaires fructueuse, que le langage Logique pouvait se d finir math matique- ment et devenir un objet d' tude pour les math maticiens. Toutefois il ne permettait pas encore de r soudre les probl mes de fondements. D s lors, nombre de math maticiens ont cherch l' tendre au cadre g n ral du raisonnement math matique et on a vu ap- para tre les syst mes logiques formalis s ; l'un des premiers est d Frege au tournant du 20ie me si cle. En 1900 au cours d'une tr s c l bre conf rence au congr s international des math - maticiens Paris, David Hilbert a propos une liste des 23 probl mes [5] non r solus les plus importants des math matiques d'alors.

7 Le deuxi me tait celui de la coh rence de l'arithm tique, c'est- -dire de d montrer par des moyens finitistes la non-contradiction des axiomes de l'arithm tique. Introduction 6. Le programme de Hilbert a suscit de nombreux travaux en Logique dans le premier quart du si cle, notamment le d veloppement de syst mes d'axiomes pour les math - matiques : les axiomes de Peano pour l'arithm tique, ceux de Zermelo compl t s par Skolem et Fraenkel pour la th orie des ensembles et le d veloppement par Whitehead et Russell d'un programme de formalisation des math matiques. C'est galement la p - riode o apparaissent les principes fondateurs de la th orie des mod les : notion de mod le d'une th orie et th or me de L wenheim-Skolem.

8 En 1929 Kurt G del montre dans sa th se de doctorat son th or me de compl tude qui nonce le succ s de l'entreprise de formalisation des math matiques : tout raison- nement math matique peut en principe tre formalis dans le calcul des pr dicats. Ce th or me a t accueilli comme une avanc e notable vers la r solution du programme de Hilbert, mais un an plus tard, G del d montrait le th or me d'incompl tude (publi . en 1931) qui montrait irr futablement l'impossibilit de r aliser ce programme. Ce r sultat n gatif n'a toutefois pas arr t l'essor de la Logique math matique. Les ann es 1930 ont vu arriver une nouvelle g n ration de logiciens anglais et am ricains, notamment Alonzo Church, Alan Turing, Stephen Kleene, Haskell Curry et Emil Post, qui ont grandement contribu la d finition de la notion d'algorithme et au d veloppe- ment de la th orie de la complexit algorithmique (th orie de la calculabilit , th orie de la complexit des algorithmes).

9 La th orie de la d monstration de Hilbert a galement continu se d velopper avec les travaux de Gerhard Gentzen qui a produit la premi re d monstration de coh rence relative et a initi ainsi un programme de classification des th ories axiomatiques. Le r sultat le plus spectaculaire de l'apr s-guerre est d Paul Cohen qui d montre en utilisant la m thode du forcing, l'ind pendance de l'hypoth se du continu en th orie des ensembles, r solvant ainsi le 1er probl me de Hilbert. Mais la Logique math matique subit galement une r volution due l'apparition de l'informatique ; la d couverte de la correspondance de Curry-Howard, qui relie les preuves formelles au lambda-calcul de Church et donne un contenu calculatoire aux d monstrations, va d clencher un vaste programme de recherche.

10 La Logique classique est la premi re formalisation du langage et du raisonnement math matique d velopp e partir de la fin du 19ie me si cle en Logique math matique. Appel e simplement Logique ses d buts, c'est l'apparition d'autres syst mes logiques formels, notamment pour la Logique intuitionniste, qui a suscit l'adjonction de l'adjectif classique au terme Logique . Introduction 7. La Logique classique est caract ris e par des postulats qui la fondent et la diff ren- cient de la Logique intuitionniste, exprim s dans le formalisme du calcul des proposi- tions ou du calcul des pr dicats . La Logique est utilis e en informatique pour mod liser de mani re formelle des objets rencontr s par les informaticiens ; par exemple : Bases de donn es, Bases de connaissances, Pr -post conditions d'une proc dure.