thumb|Principia Mathematica, un des travaux qui ont le plus marqué l'histoire de la logique mathématique.
La logique mathématique ou métamathématique est une discipline des mathématiques inventée à la fin du , qui s'est donné comme objet l'étude des mathématiques en tant que système formel.
Les objets fondamentaux de la logique mathématique sont les formules représentant les énoncés mathématiques, les dérivations ou démonstrations formelles représentant les raisonnements mathématiques et les sémantiques ou modèles ou interprétations dans des structures qui donnent un « sens » mathématique générique aux formules (et parfois même aux démonstrations) comme certains invariants : par exemple l'interprétation des formules du calcul des prédicats permet de leur affecter une valeur de vérité.
Histoire de la logique mathématique
Naissance de la logique mathématique et logicisme
La logique mathématiqueAvant de trouver son nom actuel, attribué à Giuseppe Peano, la logique mathématique s'est appelée « logique symbolique » (en opposition à la logique philosophique), « métamathématique » (terminologie de Hilbert) et « idéographie » (Begriffsschrift) (terminologie de Frege). est née, à la fin du , de la logique au sens philosophique du terme ; elle est l'une des pistes explorées par les mathématiciens de cette époque afin de résoudre la crise des fondements mathématiques provoquée par la complexification des mathématiques et l'apparition des paradoxes. Ses débuts sont marqués par la rencontre entre deux idées nouvelles : la volonté chez Frege, Russell, Peano et Hilbert de donner une fondation axiomatique aux mathématiques ; la découverte par George Boole de l'existence de structures algébriques permettant de définir un « calcul de vérité ».
La logique mathématique se fonde sur les premières tentatives de traitement formel des mathématiques, dues à Leibniz et Lambert (fin - début ). Leibniz a en particulier introduit une grande partie de la notation mathématique moderne (usage des quantificateurs, symbole d'intégration, etc.). Toutefois on ne peut parler de logique mathématique qu'à partir du milieu du , avec les travaux de George Boole (et dans une moindre mesure ceux d'Auguste De Morgan) qui introduit un calcul de vérité où les combinaisons logiques comme la conjonction, la disjonction et l'implication, sont des opérations analogues à l'addition ou la multiplication des entiers, mais portant sur les valeurs de vérité faux et vrai (ou 0 et 1) ; ces opérations booléennes se définissent au moyen de tables de vérité.
Le calcul de Boole introduisait l'idée, apparemment paradoxale mais spectaculairement fructueuse, que le langage mathématique pouvait se définir mathématiquement et devenir un objet d'étude pour les mathématiciens. Cependant, il ne permettait pas encore de résoudre les problèmes de fondements. Ainsi, de nombreux mathématiciens ont cherché à étendre ce concept au cadre général du raisonnement mathématique, ce qui a conduit à l'émergence des systèmes logiques formalisés. L'un des premiers de ces systèmes a été développé par Gottlob Frege au tournant du . Frege a posé les bases de la logique moderne, influençant profondément la philosophie des mathématiques et ouvrant la voie à des développements comme le lambda-calcul d'Alonzo Church et les machines de Turing.
Les années 1920 et David Hilbert En 1900 au cours d'une très célèbre conférence au congrès international des mathématiciens à Paris, David Hilbert a proposé une liste des 23 problèmes non résolus les plus importants des mathématiques d'alors. Le deuxième était celui de la cohérence de l'arithmétique, c’est-à-dire de démontrer par des moyens finitistes la non-contradiction des axiomes de l'arithmétique.
Le programme de Hilbert a suscité de nombreux travaux en logique dans le premier quart du siècle, notamment le développement de systèmes d'axiomes pour les mathématiques : les axiomes de Peano pour l'arithmétique, ceux de Zermelo complétés par Skolem et Fraenkel pour la théorie des ensembles et le développement par Whitehead et Russell d'un programme de formalisation des mathématiques, les Principia Mathematica. C'est également la période où apparaissent les principes fondateurs de la théorie des modèles : notion de modèle d'une théorie, théorème de Löwenheim-Skolem.
La logique à partir des années 1930 et Kurt Gödel En 1929 Kurt Gödel montre dans sa thèse de doctorat son théorème de complétude qui énonce le succès de l'entreprise de formalisation des mathématiques : tout raisonnement mathématique peut en principe être formalisé dans le calcul des prédicats. Ce théorème a été accueilli comme une avancée notable vers la résolution du programme de Hilbert, mais un an plus tard, Gödel démontrait le théorème d'incomplétude (publié en 1931) qui montrait irréfutablement l'impossibilité de réaliser ce programme.
Ce résultat négatif n'a toutefois pas arrêté l'essor de la logique mathématique. Les années 1930 ont vu arriver une nouvelle génération de logiciens anglais et américains, notamment Alonzo Church, Alan Turing, Stephen Kleene, Haskell Curry et Emil Post, qui ont grandement contribué à la définition de la notion dalgorithme et au développement de la théorie de la complexité algorithmique (théorie de la calculabilité, théorie de la complexité des algorithmes). La théorie de la démonstration de Hilbert a également continué à se développer avec les travaux de Gerhard Gentzen qui a produit la première démonstration de cohérence relative et initié ainsi un programme de classification des théories axiomatiques.
Le résultat le plus spectaculaire de l'après-guerre est dû à Paul Cohen qui démontre en utilisant la méthode du forcing l'indépendance de l'hypothèse du continu en théorie des ensembles, résolvant ainsi le de Hilbert. Mais la logique mathématique subit également une révolution due à l'apparition de l'informatique ; la découverte de la correspondance de Curry-Howard, qui relie les preuves formelles au lambda-calcul de Church et donne un contenu calculatoire aux démonstrations, va déclencher un vaste programme de recherche.
Intérêt de la logique mathématique dans les mathématiques
Interactions entre la logique et les mathématiques
L'intérêt principal de la logique réside dans ses interactions avec d'autres domaines des mathématiques et les nouvelles méthodes qu'elle y apporte. De ce point de vue les réalisations les plus importantes viennent de la théorie des modèles qui est parfois considérée comme une branche de l'algèbre plutôt que de la logique ; la théorie des modèles s'applique notamment en théorie des groupes et en combinatoire (théorie de Ramsey).
D'autres interactions très productives existent toutefois : La théorie de la calculabilité est l'un des fondements de l'informatique théorique.
Depuis la fin du on a vu la théorie de la démonstration s'associer à la théorie des catégories et par ce biais commencer à interagir avec la topologie algébrique. D'autre part avec l'apparition de la logique linéaire elle entretient également des liens de plus en plus étroit avec l'algèbre linéaire, voire avec la géométrie non commutative. Plus récemment la théorie homotopique des types crée une connexion riche entre la logique (la théorie des types) et les mathématiques (la théorie de l'homotopie) dont on n'entrevoit que les prémices.
Formalisation
La formalisation des mathématiques dans des systèmes logiques, qui a suscité en particulier les travaux de Whitehead et Russell, a été l'une des grandes motivation du développement de la logique mathématique. L'apparition d'outils informatiques spécialisés, démonstrateurs automatiques, systèmes experts et assistants de preuve, a donné un nouvel intérêt à ce programme. Les assistants de preuve en particulier ont plusieurs applications en mathématique.
Tout d'abord dans la fin du et au début du deux anciennes conjectures ont été résolues en faisant appel à l'ordinateur pour traiter un très grand nombre de cas : le théorème des quatre couleurs et la conjecture de Kepler. Les doutes soulevés par cette utilisation de l'ordinateur ont motivé la formalisation et la vérification complète de ces démonstrations.
D'autre part des programmes de formalisation de mathématiques utilisant les assistants de preuves se sont développés afin de produire un corpus complètement formalisé de mathématiques ; pour les mathématiques l'existence d'un tel corpus aurait en particulier l'intérêt de permettre des traitements algorithmiques comme la recherche par motif : trouver tous les théorèmes qui se déduisent du théorème des nombres premiers, trouver tous les théorèmes à propos de la fonction zeta de Riemann, etc.
Quelques résultats fondamentaux
Quelques résultats importants ont été établis pendant la décennie 1930.
Le théorème de complétude du calcul des prédicats du premier ordre que Gödel a montré dans sa thèse de doctorat, un an avant son célèbre théorème d'incomplétude. Ce théorème énonce que toute démonstration mathématique peut être représentée dans le formalisme du calcul des prédicats (qui est donc complet).
L'ensemble des théorèmes du calcul des prédicats n'est pas calculable, c'est-à-dire qu'aucun algorithme ne permet de vérifier si un énoncé donné est prouvable ou non. Il existe cependant un algorithme qui étant donné une formule du premier ordre en trouve une preuve en un temps fini s'il en existe une, mais continue indéfiniment sinon. On dit que l'ensemble des formules du premier ordre prouvables est « récursivement énumérable » ou « semi-décidable ».
La cohérence (non-contradiction) d'une théorie (ensemble d'axiomes), permettant de formaliser (au moins) l'arithmétique (par exemple les axiomes de Peano) n'est pas une conséquence de ces seuls axiomesSauf si la théorie est incohérente, car du faux on peut déduire toute proposition. Ce principe s'appelle le Ex falso sequitur quodlibet.. C'est le fameux second théorème d'incomplétude de Gödel.
Tout théorème purement logique peut être démontré en n'utilisant que des propositions qui sont des sous-formules de son énoncé. Connu sous le nom de propriété de la sous-formule, ce résultat est une conséquence du théorème d'élimination des coupures en calcul des séquents de Gerhard Gentzen : la propriété de la sous-formule a pour conséquence la cohérence de la logique, car elle interdit la dérivation de la formule vide (identifiée à l'absurdité).
D'autres résultats importants ont été établis pendant la deuxième partie du . L'indépendance de l'hypothèse du continu par rapport aux autres axiomes de la théorie des ensembles (ZF) est achevée en 1963 par Paul CohenCela lui a valu la médaille Fields.. La théorie de la calculabilité se développe. Au tournant de la décennie 1980, la correspondance de Curry-Howard identifie la simplification des démonstrations et les programmes, créant ainsi un pont entre mathématiques et informatique. En 1990, cette correspondance est étendue à la logique classique. La mécanisation, et donc la formalisation, complète de théorème de mathématiques comme le théorème des quatre couleurs ou le théorème de Feit-Thompson.
Au , émergent de nouvelles branches prometteuses comme la théorie homotopique des types.
Système logique Définition
Un système logique (ou une logique) est un système formel auquel on ajoute une sémantique. Un système formel se constitue :
d'une syntaxe (ou langage) dont on lui attribue deux données : un ensemble de symboles servant à la construction de formules. Dans les systèmes de logique classique ou intuitionniste, les formules représentent des énoncés mathématiques exprimés formellement. La deuxième donnée est un ensemble de règles de constructions de formules. Les formules sont définies par des moyens combinatoires à l'aide de ces règles : suites de symboles, arbres étiquetés, graphes…