Après une introduction naïve en termes de tables des valeurs de vérité , on définit la logique propositionnelle (généralisée, intuitionniste et classique) et l’algèbre de Lindenbaum-Tarski en utilisant le calcul des séquents à la Gentzen. Ensuite, on explore la versione algébrique de la logique propositionnelle : les treillis, les algèbres de Heyting et les algèbres de Boole. On entre dans le vif du sujet avec la définition de la notion de modèle, la preuve des théorèmes de validité et de cohérence et la preuve (beaucoup plus élaborée) du théorème de complétude de la logique propositionnelle intuitionniste par rapport aux modèles de Kripke. Le cours se termine par une introduction rapide aux systèmes de quantificateurs et à la logique prédicative.
- Enseignant: Vitale Enrico