Cours de logique de Licence de l'ENS de Lyon (2004-2005)


Ce cours est assuré par Pierre Lescanne assisté de Vincent Nesme et Stéphane Le Roux.

J'utilise la vidéoprojection

Cette partie du cours est très orienté vers la théorie de la démonstration. Il présente la déduction naturelle et le lambda-calcul pour introduire la correspondance de Curry-Howard. Il contient cependant une petite incursion vers la théorie des modèles non classiques en introduisant les modèles de Kripke. Puis j'introduis le calcul des prédicats, la logique du premier ordre (calcul des prédicats) et l'axiomatique de Zermelo Fraenkel pour la théorie de ensembles.

La présentation du cours a été fortement changée de puis l'année 2003-2004, grâce à l'aide de Jean-Baptiste Rouquier. Pour trouver le nouveau support de cours je vous invite à vous rendre sur le site Formation ENSL intitulé InfoL3_Logique où je mets à jours régulièrement mes notes de cours.

Les transparents de 05-06 et le poly 2004 non remis à jour.

L'examen final 2006 et son corrigé (il s'agit d'une nouvelle version du 26 janvier, la précédente comportait des petites fautes..

Divers
Formulaire d'évaluation
Le formulaire d'évaluation est .
Quelques lectures

Quelques biographies: Hilbert, Church 1 2, Curry, Turing, Russel, Heyting, Brouwer, Kolmogorov, Gentzen

Un article de Jean-Yves Girard.

Deux articles de Wadler sur la correspondance de Curry-Howard.

Un article de Douglas Bridges, paru dans le bulletin de l'EATCS sur ce qu'est la réalité en mathématique. This article introduces three of the twentieth century's main philosophies of mathematics and argues that of those three, one describes mathematical reality, the reality of the other two being virtual.


Pierre Lescanne
Last modified: Thu Jan 26 15:00:10 CET 2006