17250016 - Logique

Volume horaire total 24
Volume horaire CM 24

Responsables

Contenu

Master 1 - Semestre 2 - Année universitaire 2018-2019
Cours commun Master 1 mention Philosophie et Master 1 mention Histoire de la philosophie

Enseignant : Jean-Baptiste JOINET

Thème du cours : Axiomatiques et théories. Calculabilité et constructivité

Présentation du cours :
Le cours est organisé en deux chapitres relativement indépendants : Axiomatiques & Théories ; Calculabilité & Constructivité. L’ordre dans lequel ces deux parties sont abordées peut être modifié en début de semestre, en fonction de la composition de l’auditoire et en concertation avec ce dernier.

  • Le chapitre « Axiomatiques & Théories » commence par un bref rappel des acquis de licence en logique propositionnelle et logique du premier ordre. À cette occasion, une extension du langage de cette dernière est présentée, pour inclure les termes d’individus avec symboles de fonction et, dans ce contexte, les règles de la Déduction Naturelle pour l’égalité.

    La sémantique ensembliste des formules du premier ordre est ensuite présentée (en trois étapes en fonction de la richesse du langage : prédicats unaires, relations n-aires, fonctions).

    Le cours se concentre ensuite sur les notions d’axiomatique et de théorie : sur l’équivalence d’axiomatiques ; sur les propriétés d’axiomatiques (cohérence, minimalité, incomplétude) ; et sur la question de l’axiomatisabilité (finitaire ou non) d’une théorie.

    On aborde ensuite la relation entre théorie et ensemble des modèles de celle-ci. Est en particulier abordée l’idée de caractérisation (finitaire ou infinitaire) d’un ensemble de structures par une axiomatique du premier ordre (notion de « propriété du premier ordre »). Des exemples de démonstrations de non caractérisabilité (finitaire ou infinitaire, selon les cas) au premier ordre de propriétés particulières (comme corollaires de la complétude des règles de la logique du premier ordre) sont étudiés.
     
  • Le chapitre « Calculabilité & Constructivité » est centré sur le Lambda-calcul d’A. Church (1934). Une première section aborde la définition du lambda-calcul pur, de sa dynamique, de son pouvoir expressif (et de sa complétude au sens de la thèse de Church-Turing en théorie de la calculabilité). Une seconde section aborde le lambda-calcul simplement typé et la correspondance preuves-programmes (isomorphisme de Curry-Howard). Dans une section conclusive, on aborde de façon plus générale l’idée constructivité logique, et ses enjeux logico-philosophiques.

Bibliographie

Des documents couvrant l’ensemble du programme seront mis à disposition des étudiants inscrits.

Contrôles des connaissances

Crédits ECTS :
Master 1 Philosophie : 4
Master 1 Histoire de la philosophie : 2

Mise à jour : 20 juillet 2018