IN E11 : INTRODUCTION A LA LOGIQUE

Professeur : Jean-Baptiste Joinet (Université Paris I).

Ce cours constitue une introduction aux résultats les plus classiques de la logique mathématique. Il présente des rudiments de calcul propositionnel et de calcul des prédicats du premier ordre.
Sont étudiés tant l'aspect syntaxique (formules, systèmes de preuves), que l'aspect sémantique (interprétation et évaluation d'un énoncé dans une structure). Les systèmes de preuves présentés sont la "déduction naturelle" et le "calcul des séquents".
Le cours donne des bases pour aborder ensuite les domaines où la logique intervient, en particulier les méthodes de recherche automatique de preuves, la programmation logique et la preuve de programmes à partir de preuves, le typage des langages fonctionnels.

Thèmes abordés:

Morphologie (formules)

Langages (propositionnels, du premier ordre, d'ordre supérieur). Formules propositionnelles. Termes et Formules du premier ordre.

Syntaxe

Systèmes de déduction : déduction naturelle, calcul des séquents. Équivalence des deux systèmes.

La relation de déductibilité et l'équivalence logique

Propriétés générales de la relation de déductibilité. Équivalence logique. Compatibilité du remplacement de sous-formules équivalentes par rapport à l'équivalence logique. Connecteur définissable (Ensembles complets de connecteurs. Ensembles minimaux de connecteurs). Équivalences et implications mémorables (lois de De Morgan, etc). Quotientation de l'ensemble des formules par l'équivalence logique. Structure de l'ordre résiduel induit sur le quotient par la déductibilité (algèbre de Boole de Lindenbaum). Représentation canonique des classes d'équivalence : formes normales prénexes d'une formule. Skolémisation.

Logique et programmation

Preuves normales. Normalisation des preuves. Répresentation des programmes et de leur évaluation par les preuves et leur normalisation. Preuves et programmes typés. Ordre supérieur et polymorphisme. Recherche de preuves. Représentation des programmes et de leur évaluation par une théorie et la recherche de preuves dans cette théorie.

Sémantique

Introduction : Contre-modèle. Incomplétude. Évaluation d'un énoncé propositionnel. Interprétation d'un énoncé du premier ordre dans une structure. Exemples. Modèles d'une théorie. Cohérence d'une théorie, (In)complétude d'une théorie. Exemples. Notion sémantique de Conséquence. Complétude de la sémantique et Correction de la syntaxe. Sémantique intuitionniste (aperçu) Théorème de compacité et applications (Axiomatisabilité au premier-ordre de classes de structures)

Mots-clefs:

Calcul propositionnel, calcul des prédicats, déduction naturelle, satisfaisabilité, tautologie, forme normale, clause, skolémisation.

This document was translated from LATEX by HEVEA.