Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés - 2e edition

Détails du livre

Titre	Introduction à la Logique : Théorie de la Démonstration
Auteur(s)	René David, Karim Nour, Christophe Raffalli, Pierre-Louis Curien (préface)
Éditeur	Dunod
Année	2004
Édition	2e édition
Langue	Français
Pages	368
ISBN	978-2-10-006796-1
Collection	Sciences Sup
Domaine	Logique mathématique, Informatique théorique
Taille	2 MB
Extension	DJVU

Présentation de l'ouvrage

Publié aux éditions Dunod dans la prestigieuse collection Sciences Sup, cet ouvrage signé René David, Karim Nour et Christophe Raffalli — avec une préface de Pierre-Louis Curien — constitue l'une des références les plus solides de la littérature francophone en logique mathématique. Cette deuxième édition, entièrement révisée et enrichie, s'impose comme un cours introductif rigoureux à la théorie de la démonstration, abordée à la fois comme discipline mathématique autonome et comme outil pratique au service du raisonnement formel. L'ouvrage répond à une nécessité pédagogique réelle : apprendre aux étudiants à maîtriser le raisonnement mathématique, souvent absent des cursus classiques d'algèbre ou d'analyse. Il se distingue par la clarté de son exposition et la rigueur de ses formalismes, caractéristiques qui en ont fait un manuel incontournable dans les universités francophones.

L'ouvrage s'organise en deux grandes parties complémentaires. La première partie pose les fondements du raisonnement mathématique formel : elle introduit la syntaxe et la sémantique du calcul des énoncés, puis aborde la logique du premier ordre avec ses quantificateurs, ses formules et ses règles de déduction. Les auteurs exposent ensuite le théorème de complétude de la logique du premier ordre, résultat fondamental qui établit la correspondance entre vérité sémantique et démontrabilité syntaxique. La seconde partie est consacrée plus spécifiquement à la théorie de la démonstration en tant que discipline à part entière : elle traite notamment de la logique intuitionniste, des modèles de Kripke, des calculs des séquents, de la démonstration automatique et des logiques d'ordre supérieur. Ces thèmes, abordés progressivement, permettent au lecteur de construire une vision cohérente et structurée de la logique formelle moderne.

Un des atouts majeurs de cet ouvrage réside dans son approche pédagogique soigneusement pensée. Chaque chapitre est accompagné d'énoncés d'exercices avec leurs corrigés détaillés, au nombre de 170 au total, permettant à l'étudiant de s'évaluer régulièrement et de consolider les notions acquises. Une annexe originale présente le logiciel PhoX, un assistant de démonstration développé par Christophe Raffalli, qui a été utilisé en contexte pédagogique avec des étudiants de licence pour les aider à mieux appréhender les raisonnements formels. Des ressources complémentaires aux corrigés sont également accessibles en ligne sur le site des auteurs. Cette dimension interactive distingue cet ouvrage des manuels purement théoriques et en fait un outil de formation complet, alliant théorie et pratique.

Cet ouvrage s'adresse en priorité aux étudiants de troisième année de licence de mathématiques et d'informatique, ainsi qu'aux candidats aux concours nationaux que sont le CAPES et l'Agrégation. Il constitue également une ressource précieuse pour les étudiants de master souhaitant approfondir leurs bases en logique formelle et en fondements des mathématiques. Les enseignants-chercheurs et les professionnels de l'informatique théorique y trouveront aussi un exposé rigoureux des principaux formalismes logiques. Le niveau requis correspond globalement à une solide formation de premier cycle universitaire en mathématiques, sans nécessité de prérequis spécifiques en logique.

Depuis sa première parution en 2001, cet ouvrage a connu plusieurs rééditions, témoignant de son succès durable dans la communauté académique française. La deuxième édition de 2004 a encore renforcé sa réputation grâce à une révision approfondie du contenu et à l'intégration de nouveaux exercices. Il a depuis inspiré une troisième édition parue chez Dunod en 2025, preuve de la pertinence et de la longévité de ce travail collectif. La préface de Pierre-Louis Curien, directeur de recherche émérite au CNRS et figure de référence de l'informatique théorique française, confère à cet ouvrage un rayonnement scientifique exceptionnel. Ce manuel demeure, plus de vingt ans après sa première publication, une porte d'entrée privilégiée vers la logique mathématique et la théorie des preuves pour les lecteurs francophones.

Points forts de l'ouvrage

• Présentation rigoureuse et progressive du calcul des énoncés, de la syntaxe à la sémantique formelle.
• Développement complet de la logique du premier ordre, incluant quantificateurs, termes et formules closes.
• Démonstration détaillée du théorème de complétude de la logique classique du premier ordre.
• Introduction approfondie à la logique intuitionniste et à ses modèles de Kripke, peu couverts dans la littérature introductive francophone.
• Présentation du calcul des séquents, formalisme central de la théorie de la démonstration moderne.
• Chapitre dédié aux exemples de théories mathématiques formelles, illustrant concrètement l'usage de la logique.
• Section consacrée aux logiques d'ordre supérieur et à leurs applications en informatique théorique.
• Intégration de 170 exercices avec corrigés complets, répartis en fin de chaque chapitre.
• Annexe pratique présentant le logiciel PhoX, assistant de démonstration développé par l'un des auteurs et utilisé en enseignement universitaire.
• Accès à des ressources et compléments en ligne sur le site des auteurs, enrichissant l'expérience d'apprentissage.
• Préface rédigée par Pierre-Louis Curien, directeur de recherche émérite au CNRS et spécialiste reconnu de la théorie des preuves.
• Ouvrage conçu à partir de l'expérience directe d'enseignement à l'Université de Savoie, garantissant une pédagogie éprouvée.
• Couverture des thèmes au programme des concours nationaux CAPES et Agrégation de mathématiques.
• Publication dans la collection Sciences Sup de Dunod, gage de qualité scientifique et pédagogique reconnue.

À propos des auteurs

René David (né en 1948) était professeur de mathématiques à l'Université de Savoie (Chambéry), où il a exercé pendant de nombreuses années. Ses recherches portaient principalement sur la logique mathématique, la théorie des types et la théorie de la démonstration. Avec Karim Nour, il a co-encadré plusieurs thèses de doctorat portant sur des sujets tels que les propriétés de normalisation des calculs logiques et les types de données en logique du second ordre. Leur collaboration pédagogique à l'Université de Savoie, traduite dans cet ouvrage, est née d'un constat partagé sur les difficultés des étudiants à maîtriser le raisonnement formel dans les cursus classiques de mathématiques. Karim Nour est maître de conférences habilité à diriger des recherches (HDR) à l'Université Savoie Mont Blanc. Ses travaux s'inscrivent dans le domaine de la logique formelle et de la théorie des preuves. Il a notamment dirigé et co-dirigé des thèses portant sur la sémantique des langages de programmation et les systèmes de typage. Christophe Raffalli est chercheur associé au G.A.A.T.I. et enseignant à l'Université de Polynésie française. Il est l'auteur du logiciel PhoX, assistant de démonstration développé dans le cadre de ses activités de recherche et d'enseignement, qui constitue l'une des contributions les plus originales de cet ouvrage.

Pierre-Louis Curien (né en 1953) est directeur de recherche émérite au CNRS, rattaché à l'Institut de Recherche en Informatique Fondamentale (IRIF), unité mixte CNRS et Université Paris Cité. Diplômé de l'École Normale Supérieure de la rue d'Ulm avec une agrégation de mathématiques, il a soutenu sa thèse de troisième cycle à l'Université Paris 7 en 1979, puis une thèse d'État en 1983. Il est cofondateur du laboratoire Preuves, Programmes et Systèmes (PPS), aujourd'hui intégré à l'IRIF, et de l'équipe-projet Inria πr2. Auteur de plus d'une cinquantaine d'articles scientifiques et d'un ouvrage de référence sur les domaines et le lambda-calcul (coécrit avec Roberto Amadio, Cambridge University Press, 1998), il a supervisé une vingtaine de thèses de doctorat. Rédacteur en chef depuis 2016 de la revue Mathematical Structures in Computer Science, membre du jury du Prix Gödel en 2004–2006 et lauréat du Grand Prix Inria–Académie des Sciences, Pierre-Louis Curien est l'une des personnalités les plus influentes de l'informatique théorique française. Sa préface à cet ouvrage témoigne de l'importance qu'il accorde à la diffusion de la logique et de la théorie des preuves auprès des jeunes mathématiciens.

Livres similaires

• Logique mathématique, tome 1 : Calcul propositionnel, algèbres de Boole, calcul des prédicats — René Cori et Daniel Lascar
• Logique mathématique, tome 2 : Fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles — René Cori et Daniel Lascar
• Éléments de logique mathématique — Michel Delorme et Jacques Mazoyer
• Logique pour l'informatique et pour l'IA — Gilles Dowek
• Proofs and Fundamentals: A First Course in Abstract Mathematics — Ethan D. Bloch
• Proof Theory: The First Step into Impredicativity — Wolfram Pohlers
• Basic Proof Theory — A. S. Troelstra et H. Schwichtenberg
• Logic in Computer Science: Modelling and Reasoning about Systems — Michael Huth et Mark Ryan

Ads

Télécharger le livre DJVU [2 MB] Aperçu en ligne

Questions fréquentes

Q : Quels prérequis sont nécessaires pour aborder cet ouvrage ?

R : L'ouvrage est conçu pour des étudiants ayant validé les deux premières années d'une licence de mathématiques ou d'informatique. Une familiarité avec les notions élémentaires d'ensembles, de fonctions et de raisonnement par récurrence est suffisante. Aucune connaissance préalable en logique formelle n'est exigée, car les bases sont posées dès les premiers chapitres. Il reste néanmoins exigeant sur le plan de la rigueur mathématique attendue du lecteur.

Q : Qu'est-ce que le logiciel PhoX présenté en annexe et comment peut-on l'utiliser ?

R : PhoX est un assistant de démonstration développé par Christophe Raffalli, l'un des coauteurs de l'ouvrage. Il permet de construire et de vérifier des preuves formelles de façon interactive. Il a été utilisé en enseignement à l'Université de Savoie pour aider les étudiants à mieux comprendre le déroulement d'un raisonnement formel en algèbre ou en analyse. Le logiciel ainsi que des compléments aux corrigés des exercices étaient disponibles sur le site Web des auteurs au moment de la publication.

Q : Cet ouvrage est-il adapté à la préparation du CAPES et de l'Agrégation de mathématiques ?

R : Oui, cet ouvrage est explicitement recommandé pour les candidats au CAPES et à l'Agrégation de mathématiques. Il couvre les notions de logique formelle et de théorie de la démonstration qui figurent dans les programmes de ces concours. La présence de 170 exercices corrigés en fait un outil de révision particulièrement efficace. Les thèmes traités, tels que la complétude de la logique du premier ordre ou la logique intuitionniste, correspondent précisément aux attentes des jurys de ces concours nationaux.

Q : Quelle est la différence entre la deuxième édition de 2004 et la première édition de 2001 ?

R : La deuxième édition de 2004 a fait l'objet d'une révision complète du contenu par rapport à la première édition de 2001. Les auteurs ont revu les exposés théoriques pour les rendre plus clairs et plus rigoureux, enrichi le corpus d'exercices et affiné les corrigés. L'ensemble du manuscrit a été relu et corrigé, et certains chapitres ont été restructurés pour améliorer la progression pédagogique. Cette édition représente donc une amélioration substantielle sur tous les plans par rapport à la version initiale.

Q : Pourquoi la logique intuitionniste est-elle abordée dans un manuel destiné à des mathématiciens classiques ?

R : La logique intuitionniste joue un rôle croissant dans les mathématiques constructives et en informatique théorique, notamment dans la vérification formelle de programmes et la théorie des types. Les auteurs l'incluent car elle offre une perspective complémentaire et fondamentale sur la nature des preuves mathématiques, en distinguant existence effective et existence par l'absurde. Les modèles de Kripke associés fournissent un outil sémantique puissant pour comprendre les différences entre logique classique et logique intuitionniste. Cette approche prépare le lecteur aux développements modernes de l'informatique fondamentale.

Q : Quel rôle joue Pierre-Louis Curien dans cet ouvrage ?

R : Pierre-Louis Curien est l'auteur de la préface de la deuxième édition. En tant que directeur de recherche émérite au CNRS, cofondateur du laboratoire Preuves, Programmes et Systèmes et lauréat du Grand Prix Inria–Académie des Sciences, il est une figure de référence internationale de la théorie des preuves et de l'informatique théorique. Sa préface contextualise l'ouvrage dans le paysage scientifique et pédagogique de la logique francophone. Son nom associé à ce manuel lui confère une légitimité scientifique particulière auprès de la communauté académique.

Q : Une version plus récente de cet ouvrage existe-t-elle ?

R : Oui, une troisième édition a été publiée par Dunod en septembre 2025, toujours dans la collection Sciences Sup, signée par René David, Karim Nour et Christophe Raffalli. Cette nouvelle édition actualise et enrichit le contenu de la deuxième édition, notamment en intégrant les avancées récentes en logique intuitionniste et en démonstration automatique. Elle bénéficie d'une nouvelle préface rédigée par Olivier Laurent. La version de 2004 présentée ici reste néanmoins un document de référence valide pour l'étude des fondements de la logique mathématique.