Cet ouvrage est le contenu d’un cours que l’auteur dispense à l’Université de Lausanne, au niveau Bachelor (nom de la licence en Suisse). Il est quasiment exhaustif, n’omettant que les démonstrations des théorèmes les plus difficiles (de Gödel par exemple), non sans indiquer une ressource bibliographique.
Le Préambule apporte déjà du vocabulaire : « langage », « formule », « syntaxe », « sémantique »…
L’Introduction est, notamment, historique : on y croise aussi bien Aristote que Russell, en passant par Leibniz, Boole, Cantor…
Dans la Partie I : Calcul Propositionnel, le lecteur trouvera des choses connues, mais sous une forme relativement originale : les formules sont présentées sous formes d’arbres, où chaque noeud est un connecteur ; on ne les linéarise qu’ensuite ; les valeurs de vérité sont attribuées grâce à des jeux d’évaluation. Mais plus d’un y découvrira des aspects qu’il ignorait : différences entre les Systèmes axiomatiques, la Déduction naturelle et le Calcul des séquents, entre les logiques minimale, intuitionniste et classique.
La Partie II : Logique modale ouvre les portes d’un monde où dans les formules on rencontre, outre les connecteurs, des opérateurs de modalité, qui selon les modèles seront interprétés comme Certain/Possible, Obligatoire/Autorisé, ou encore l’individu i sait que/croit que…Sémantique.
Avec la Partie III : Logique du premier ordre nous retrouvons un terrain mieux connu, où aux notions de la partie I on adjoint les quantificateurs. Il existe une traduction de la logique modale en logique du premier ordre.
La Partie IV : Récursivité, 2d ordre et Correspondance Preuves-Programmes assure la connexion de la logique avec, d’une part, la théorie des ensembles, d’autre part, l’informatique ; il y est question de décidabilité, des théorèmes d’incomplétude de Gödel, de λ-calcul.
Enfin la Partie V : Annexes se réduit à un chapitre : Une preuve du théorème de compacité par ultraproduit.
Chaque sous-chapitre débute par un résumé, et se termine par la rubrique « Pour aller plus avant » comportant des renvois à l’abondante Bibliographie qui clôt l’ouvrage.