Ce cours d'introduction à la logique est composé de douze vidéos, construites pour être utilisées en classe inversée, c'est-à-dire complétées de séances de questions et de travaux dirigés. L'ensemble des vidéos dure 12h 33mn (la plus courte dure 44mn 28s et la plus longue 1h 24mn 52s). Il a été construit, de janvier à mai 2021, pour les élèves de première année du département d'informatique de l'École normale de Paris-Saclay.

Comme tous les cours de logique destinés aux informaticiens, il met l'accent sur les notions de langage, de démonstration et d'algorithme, davantage que sur les notions de modèle et d'ensemble, mais, même si elles sont inégalement développées, toutes ces notions sont abordées. La théorie de la calculabilité, qui fait l'objet d'un cours séparé, est utilisée, mais ses notions fondamentales ne sont pas introduites. Ce cours suit grosso modo les parties I et III du livre Les démonstrations et les algorithmes.

Merci à David Baelde et Émilie Grienenberger avec qui ce cours a été construit.

1 : La notion de définition inductive. La notion de langage (49mn 13s).

2 : La logique des prédicats (47mn 35s).

3 : La notion de théorie (1h 24mn 52s).

4 : La notion de modèle (1h 22mn 44s).

5 : Les théorèmes d'indédicabilité et d'incomplétude (1h 02mn 01s).

6 : La démonstration automatique (1h 07mn 04s).

7 : L'équivalence entre la déduction naturelle et le calcul des séquents. L'élimination des coupures (1h 14mn 07s).

8 : Des théorie décidable (54mn 22s).

9 : La constructivité (1h 03mn 24s).

10 : La Résolution (58mn 17s).

11 : La complétude de la Résolution (1h 04mn 53s).

12 : La définissabilité (44mn 28s).