Logique Mathématique I (EPFL)
Modalités
Professeur : Jacques DUPARC (Jacques.Duparc[at]unil.ch)Assistant : Yann PEQUIGNOT (Yann.Pequignot[at]unil.ch)
Cours : mercredi, 13h15 - 15h00, CM 5.
Exercices : mercredi, 15h15 - 17h00, CM 5.
Objectifs
Ce cours est une introduction aux outils, concepts et résultats de la logique mathématique dont les thèmes sont la vérité, la démonstration et la calculabilité. Bien que son domaine d’étude soit les mathématiques, la logique mathématique est une branche des mathématiques à part entière avec de nombreuses applications, en particulier en informatique.Contenu
- Eléments de théorie naïve des ensembles.
- Calcul des Prédicats :
- Syntaxe : langage, formule et arbres de
décomposition, variable libre vs liée, formule
close, substitution.
- Sémantique : structure et réalisation,
sous-structure et restriction. Homomorphisme et isomorphisme.
Interprétation et satisfaction. Jeu d’évaluation.
Equivalence universelle et conséquence sémantique.
Théorie, modèle et consistance. Système complet de
connecteur, formes normales prénexes et forme de Skolem.
Eléments de théorie des modèles.
Théorème de compacité et modèle non
standard.
- Théorie de la démonstration : systèmes de Hilbert. Déduction naturelle et Calcul des Séquents. Logique classique vs logique intuitionniste. Elimination des coupures et propriété de la sous-formule. Théorème de complétude de la logique classique (Gödel). Modèle de Kripke et théorème de complétude de la logique intuitionniste.
- Eléments de récursivité : fonctions récursives et partielles récursives. Machine de Turing et décidabilité. Machine de Turing universelle et problème de la halte. Hiérarchie arithmétique, fonctions ∑1, ∆1 définissables. Isomorphisme preuves/programmes de Curry-Howard.
Examen
Quatre devoirs seront donnés au cours du semestre, à raison d'un devoir toutes les deux semaines, à partir de la semaine 4. La moyenne des notes des devoirs (MD) peut remonter la note de l'examen (NE).Les devoirs peuvent être rendus sous format pdf.
Les modalités pour le calcul de la note finale (NF) sont les suivantes:
Si NE<3.5, alors NF = NE;
Sinon NF = max {NE, (NE+MD)/2}.
Les étudiants ont droit à une feuille recto-verso, format A4, de notes personnelles.
La table des règles de déduction naturelle et de calcul des séquents sera donnée en annexe de l'examen.
Documents distribués en cours ou en séries (en format pdf)
Séries d'exercices et solutions:
Devoirs
Devoir 1, Solution du devoir 1.Devoir 2
Devoir 3
Notes de cours:
1. Rappels et Syntaxe (modifié le 3.10.2011)2. Sémantique et théorie des jeux
3. Théorie des modèles
4. Théorème de compacité
5. Ordinaux et cardinaux
6. Théorèmes de Löwenheim-Skolem
7. Théorie de la démonstration
8. Théorèmes de complétude
Règles de déduction
Si vous avez des questions, n'hésitez pas à envoyer un mail à Yann.Pequignot@unil.ch, ou à passer au bureau 127.1 du bâtiment internef de l'UNIL.
Bibliographie
- Introduction générale à la logique mathématique :
- René Cori, Daniel Lascar: Introduction à la logique mathématique, vol. 1 et 2, Dunod, 2003
- Karim Nour, René David, Christophe Raffalli, et Pierre-Louis Curien: Introduction à la logique : Théorie de la démonstration, Dunod, 2004
- H.-D. Ebbinghaus, J. Flum, and W. Thomas: Mathematical Logic, Springer, 1996
- Wolfgang Rautenberg: A concise introduction to mathematical logic, Springer, 2006
- Yu. I. Manin: A course in mathematical logic, Springer, 1977
- Joseph R. Shoenfield: Mathematical Logic, AK Peters, 2001
- Elliott Mendelson: Introduction to mathematical logic (4th edition), Chapman & Hall/CRC 1997
- George Boolos, John Burgess, Richard Jeffrey: Computability and Logic (5th edition), Cambridge 2007
- Herbert B. Enderton : A methamtical introduction to logic (2nd edittion), 2000
- Jon Barwise: Handbook of mathematical logic, North-Holland, 1982
- Théorie des ensembles :
- Thomas Jech: Set theory, Springer 2006
- Kenneth Kunen: Set theory, Spirnger, 1983
- Jean-Louis Krivine: Theory des ensembles, 2007
- Patrick Dehornoy: Logique et théorie des ensembles; Notes de cours, FIMFA ENS: http://www.math.unicaen.fr/~dehornoy/surveys.html
- Yiannis Moschovakis: Notes on set theory, Springer 2006
- Karel Hrbacek and Thomas Jech: Introduction to Set theory, (3d edition), 1999
- Théorie des modèles :
- Bruno Poizat: Cours de Théorie des Modèles. Nur alMantiq walMa'arifah, Villeurbanne, 1985
- Wilfrid Hodges: A shorter model theory, Cambridge 1999
- Wilfrid Hodges: Model theory, Cambridge, 2008
- David Marker : Model theory, an introduction, 2002
- Philipp Rothmaler: Introduction to model theory, 2000
- Théorie de la récursion :
- Piergiorgio Odifreddi: Classical recursion theory, vol. 1 and 2, Springer, 1999
- Robert I. Soare: Recursively Enumerable Sets and Degres, A Study of Computable Functions and Computably Generated Sets, Springer-Verlag 1987
- Nigel Cutland: Computability, an introduction to recursive function theory, 1980
- Raymond M. Smullyan: recursion theory for methamathematics, Oxford, 1993
- Théorie de la démonstration :
- Wolfram Pohlers: Proof Theory, the first step into impredicativity, Springer, 2008
- A. S. Troelstra, H. Schwichtenberg, and Anne S. Troelstra: Basic proof theory, Cambridge, 2000
- S.R. Buss: Handbook of proof theory, Springer, 1998
- Résultats de Gödel :
- Raymond M. Smullyan: Gödel's incompleteness theorems, Oxford, 1992
- Peter Smith: An introduction to Gödel's theorems, Cambridge, 2008
- Torkel Franzen: Inexhaustibility, a non exhaustive treatment, AK Peteres, 2002
- Melvin Fitting: Incompleteness in the land of sets, King's College, 2007
- Torkel Franzen: Gödel's theorem: an incomplete guide to its use and abuse, AK Peters, 2005
Contacts
Jacques.Duparc[at]unil.chYann.Pequignot[at]unil.ch
