Logique -- L3 mathématiques-Informatique - semestre 2

Année 2017-2018

• semaine 1 : 15/01/2018
  • Définitions inductives ; exemple, intersection de tous les ensembles ayant une certaine propriété qui passe à l'intersection.
  • Les entiers naturels : vus comme structure définie inductivement ; axiomatisation de l'arithmétique (Dedekind-Peano) ; démonstration par récurrence ; existence et unicité d'une fonction définie par récurrence, corollaire : définition par récurrence avec paramètres : existence et unicité.
  • Polycopié (cours et exercices) : axiomatisation de l'arithmétique (axiomes de Peano).
  • Feuille d'exercice 2 (arithmétique).
  • Feuille d'exercice 1 (ordre et bon ordre).
• semaine 2 : 22/01/2018
  • Définition par récurrence avec paramètre dépendant de l'argument (sans démonstration, voir polycopié).
  • Définition de l'ordre sur ℕ, propriétés usuelles, démonstrations (ordre, totalité, liens vec l'ordre strict associé).
  • Récurrence à partir d'un certain rang, récurrence forte, récurrence bien fondée.
  • Ensemble bien ordonné ou bon ordre ; ℕ est bien ordonné.
• semaine 3 : 29/01/2018
  • Axiomatisation des entiers comme ensemble bien ordonné, tel que tout élément a un successeur, et tout élément non nul est un successeur (sans démonstration).
  • Cardinalité : équipotence (être en bijection, noté ~), subpotence (il existe une injection, notée ≼), subpotence stricte (il existe une injection mais pas de bijection, notée ≺) ; théorème de Cantor-Bernstein.
  • Exemples : ℕ ~ ℤ ~ ℕ × ℕ ~ ℚ ; argument diagonal : aucune fonction ℕ dans ℝ n'est surjective, donc ℝ n'est pas en bijection avec ℕ ; suites de 0 et de 1 ; théorème de Cantor : E ≺ {0, 1}^E (E ≺ 𝒫(E)).
  • Cardinalité et opérations ensemblistes : les opérations ensemblistes usuelles sont compatibles avec la relation d'équipotence, on a en particulier :
    • si A ~ A' et B~B', alors A ⊎ B ~ A' ⊎ B'   et   A × B ~ A' × B'   et   A^B ~ A' ^B'
    • A^{B ⊎ C} ~ (A^B) × (A^C)   et   (A^B)^C ~ A^{B × C}.
  • Un ensemble A est fini s'il existe un entier n tel que A est en bijection avec {x ∈ ℕ | x < n }, dénombrable s'il est en bijection avec ℕ, infini s'il n'est pas fini ; si A est fini, il existe un unique entier n tel que A est en bijection avec {x ∈ ℕ | x < n } (à démontrer).
• semaine 4 : 05/02/2018
  • Cardinalité finie : unicité du cardinal entier, principe des tiroirs de Dirichlet et variantes ; ensemble dénombrable, tout sous-ensemble d'un ensemble dénombrable est fini ou dénombrable.
  • Un ensemble est équipotent à une de ses parties propres si et seulement s'il contient un sous-ensemble dénombrable ; axiome du choix (AC) et axiome du choix dénombrable ; un ensemble est infini (au sens non fini) si et seulement s'il contient un sous-ensemble dénombrable (avec AC) ; une réunion dénombrable d'ensembles dénombrables est dénombrable (AC).
  • Problème à rendre le 26/02/2016.
• semaine 5 : 12/02/2018
  • Lemme de Zorn (AC), (démonstration du lemme de Zorn), application : comparabilité cardinale étant donnés deux ensembles A et B, il existe une injection de A dans B, ou une injection de B dans A. Théorème de Zermelo (tout ensemble peut être bien ordonné) et équivalence avec AC (indications pour le sens direct par Zorn).
  • Jean-Louis Krivine Éléments de théorie des ensembles, cours polycopié, Université de Paris 7 ; ce polycopié est plus complet que ce que nous avons fait en cours, en particulier vous avez les axiomes de la théorie des ensembles de Zermelo (hors programme cette année). Vous y trouvez une autre démonstration du lemme de Zorn et d'autres applications de celui-ci à la cardinalité.
• semaine 6 : 19/02/2018
  • Calcul des prédicats : premier ordre et ordre supérieur ; langage de la logique du premier ordre, signature, termes ; variable libre, variable liée, formule close ; structure associée à une signature ; environnement, définition de la satisfaction dans une structure pour un certain environnement.
  • Polycopié calcul des prédicats (dernière mise à jour le 9/04/2018).
• semaine 7 : 26/02/2018
  • Pause UFR de math, mais le cours de logique a lieu de 10h45 à 12h45 même salle (2018 SG) en rattrapage du lundi 2/04 (lundi de Pâques).
  • Formule satisfaisable et formule universellement valide ; conséquence sémantique ; théorie.
  • Morphisme, sous-structure. Formule universelle et existentielle ; la satisfaction des formules closes universelles est stable par sous-structure.
  • Formules universellement valides : tautologies du calcul des prédicats (obtenues par substitution de celles du calcul propositionnel) ; équivalences mettant en jeu les quantificateurs.
• semaine 8 : 05/03/2018
  • Équivalences mettant en jeu les quantificateurs.
  • Axiomes de l'égalité : réflexivité + propriété fondamentale de l'égalité (schéma d'axiomes) ; équivaence avec l'axiomatisation par réflexivité, symétrie, trasitivité et compatibilité pour les fonctions et prédicats de la signature. Une théorie a un modèle en calcul des prédicats égalitaire si et seulement cette théorie augmentée des axiomes de l'égalité possède un modèle en calcul des prédicats pur (où l'égalité est une relation ordinaire).
  • Mise sous forme prénexe ; équisatisfaisabilité et exemple introductif à la skolemisation.
  • Polycopié mis-à-jour (cf. lien ci-dessus).
• semaine 9 : 12/03/2018
  • Skolemisation : symboles de constantes et de fonctions de Skolem, forme de Skolem d'une formule sous forme prénexe ; une formule du calcul des prédicats (sous forme prénexe) possède un modèle si et seulement si sa forme de Skolem possède un modèle.
  • Méthode de Herbrand, introduction, une méthode de semi-décision pour la non-satisfaisabilité, c'est-à-dire qu'elle ne permet de conclure que quand une formule n'est pas satisfaisable.
  • Domaine de Herbrand,structure de Herbrand, base de Herbrand ; une formule universelle est satisfaisable si et seulement si elle est satisfaisable dans une structure de Herbrand.
  • Pour une signature de domaine de Herbrand non vide (au moins un symbole de constante) : une formule universelle est satisfaisable dans une structure de Herbrand si et seulement si l'ensemble de toutes ses particularisations par des termes clos est satisfaisable en calcul propositionnel.
  • Théorème de Herbrand : réduction de la non satisfaisabilité d'un formule universelle close à celle d'un sous-ensemble fini de ses particularisations ; indications informelles de son utilisation pour une méthode de semi-décision ; démonstration : théorème de compacité du calcul propositionnel par complétude de la réfutation par coupures pour les clauses ; démonstration de la complétude esquissée (cas dénombrable), voir le polycopié pour une démonstration plus précise, (cf. lien ci-dessus).
• semaine 10 : 19/03/2018
  • Partiel lundi 19/03/2018 8h30-10h30 salle 0011
• semaine 11 : 26/03/2018
  • Une méthode de semi-décision pour la non satisfaisabilité d'une formule du calcul des prédicats : réduction aux ensembles de clôtures universelles de clauses ; algorithme de semi-décision naïf par énumération des instances par des termes clos et règle de coupure en calcul propositionnel, complétude de l'algorithme par le théorème de Herbrand. Règle de résolution et unification, complétude de la réfutation par résolution en autorisant un unificateur quelconque.
  • Mise à jour du polycopié, (cf. lien ci-dessus).
• semaine 12 : 2/04/2018
  • lundi de Pâques
• semaine 13 : 9/04/2018
  • Unificateur principal ; algorithme de Robinson (par substitution effective) pour l'unification comme réécriture en un système "résolu", terminaison ; corollaire : existence d'un unificateur principal quand le système est unifiable (Une petite erreur dans la démonstration donnée en cours pour l'existence d'un unificateur principal pour un système résolu, voir le polycopié ci-dessus). Lemme de relèvement, complétude de la résolution par réfutation avec unificateur principal. Voir la mise à jour polycopié.
  • Mise à jour du polycopié, (cf. lien ci-dessus).
• Vacances de printemps 14/04/2018 -- 29/04/2018

Calcul de la note finale de session 1 : 1/2 examen + 1/3 partiel + 1/6 CC (où CC est la moyenne des contrôles en TD).

dernière modification : lundi 9 avril 2018 21:23:40 CEST