Logique mathématique

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Principia Mathematica, un d'entre les plus importants travaux sur la logique mathématique.

La logique mathématique, logique formelle ou méta-mathématique est une discipline des mathématiques introduite à la fin du XIXe siècle, qui s'est donnée comme objet l'étude des mathématiques en tant que langage.

Les objets fondamentaux de la logique mathématique sont les formules modélisant les énoncés mathématiques, les dérivations ou démonstrations formelles modélisant les raisonnements mathématiques et les sémantiques ou modèles qui définissent le « sens » des formules (et parfois même des démonstrations) comme certains invariants : par exemple l'interprétation des formules du calcul des prédicats dans les structures permet de leur affecter une valeur de vérité.

Sous-domaines de la logique mathématique[modifier | modifier le code]

Au cours du XXe siècle, la logique mathématique s'est ramifiée en sous-domaines[1] :

On peut y ajouter un cinquième grand axe un petit peu plus récent avec les travaux sur la théorie des types.

Histoire de la logique mathématique[modifier | modifier le code]

Article détaillé : Histoire de la logique.

Naissance de la logique mathématique et logicisme[modifier | modifier le code]

La logique mathématique[2] est née à la fin du XIXe siècle 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 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 logique mathématique se fonde sur les premières tentatives de traitement formel des mathématiques, dues à Leibniz et Lambert (fin XVIIe siècle - début XVIIIe siècle). 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 XIXe siècle, 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 véhiculait l'idée apparemment paradoxale, mais qui devait s'avérer spectaculairement fructueuse, que le langage mathématique pouvait se définir mathématiquement et devenir un objet d'étude pour les mathématiciens. Toutefois il ne permettait pas encore de résoudre les problèmes de fondements. Dès lors, nombre de mathématiciens ont cherché à l'étendre au cadre général du raisonnement mathématique et on a vu apparaître les systèmes logiques formalisés ; l'un des premiers est dû à Frege au tournant du XXe siècle.

Les années 1920 et David Hilbert[modifier | modifier le code]

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[modifier | modifier le code]

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 d'algorithme 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 1er problème 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[modifier | modifier le code]

Interactions entre la logique et les mathématiques[modifier | modifier le code]

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 : le développement de la théorie des ensembles est intimement lié à celui de la théorie de la mesure et a donné lieu à un domaine mathématique à part entière, la théorie descriptive des ensembles. La théorie de la calculabilité est l'un des fondements de l'informatique théorique et de la complexité algorithmique.

Plus récemment depuis la fin du XXe siècle 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.

Formalisation[modifier | modifier le code]

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, ont 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 XXe siècle et au début du XXIe siècle des 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. Le doute levé par l'utilisation de l'ordinateur a motivé la formalisation et 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[modifier | modifier le code]

Quelques résultats importants ont été établis pendant la décennie 1930 :

  • 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ée 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 ».
  • L'ensemble des formules prouvables du second ordre n'est pas calculable ; mais contrairement au cas du premier ordre il n'est pas non plus récursivement énumérable. Ceci est une conséquence du théorème d'incomplétude.
  • 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 XXe siècle.

  • 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 Cohen[4].
  • 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.

Système logique[modifier | modifier le code]

Définition[modifier | modifier le code]

Un système logique ou système de déduction est un système formel constitué de trois composantes. Les deux premières définissent sa syntaxe, la troisième sa sémantique :

  • Un ensemble de formules, ou faits ; dans les systèmes de logique classique ou intuitionniste, les formules représentent des énoncés mathématiques exprimés formellement. Les formules sont définies par des moyens combinatoires : suites de symboles, arbres étiquetés, graphes
  • Un ensemble de déductions ; les déductions sont également définies par des moyens combinatoires. Une déduction permet de dériver des formules (les formules prouvables ou théorèmes) à partir de formules de départ (les axiomes) au moyen de règles (les règles d'inférence).
  • Une interprétation des formules ; il s'agit d'une fonction associant à toute formule un objet dans une structure abstraite appelée modèle, ce qui permet de définir la validité des formules.

Syntaxe et sémantique[modifier | modifier le code]

La caractéristique principale des formules et des déductions est qu'il s'agit d'objets finis ; plus encore, chacun des ensembles de formules et de déductions est récursif, c'est-à-dire que l'on dispose d'un algorithme qui détermine si un objet donné est une formule correcte ou une déduction correcte du système.

La sémantique, au contraire, échappe à la combinatoire en faisant appel (en général) à des objets infinis. Elle a d'abord servi à « définir » la vérité. Par exemple, en calcul des propositions, les formules sont interprétées par des éléments d'une algèbre de Boole ; les formules valides sont celles qui sont interprétées par le plus grand élément.

Une mise en garde est de rigueur ici, car Kurt Gödel (suivi par Alfred Tarski) a montré avec son théorème d'incomplétude l'impossibilité de définir mathématiquement la vérité mathématique. C'est pourquoi il est plus approprié de voir la sémantique comme une métaphore : les formules — objets syntaxiques — sont projetées dans un autre monde, plus abstrait, par exemple les algèbres de Boole. Cette technique — plonger les objets dans un monde plus vaste pour mieux raisonner dessus — est couramment utilisée en mathématique et a amplement démontré son efficacité.

Ainsi la sémantique ne sert pas qu'à « définir » la vérité. Par exemple, la sémantique dénotationnelle est une interprétation, non des formules, mais des déductions visant à capturer leur contenu calculatoire.

Systèmes de déduction[modifier | modifier le code]

En logiques classique et intuitionniste, on distingue deux types d'axiomes : les axiomes logiques qui expriment des propriétés purement logiques comme A\lor\lnot A (principe du tiers exclu, valide en logique classique mais pas en logique intuitionniste) et les axiomes extra-logiques qui définissent des objets mathématiques ; par exemple les axiomes de Peano définissent les entiers de l'arithmétique ou les axiomes de Zermelo-Fraenkel définissent la notion d'ensemble. Quand le système possède des axiomes extra-logiques, on parle de théorie axiomatique. L'étude des différents modèles d'une même théorie axiomatique est l'objet de la théorie des modèles.

Deux systèmes de déduction peuvent être équivalents au sens où ils ont exactement les mêmes théorèmes. On démontre cette équivalence en fournissant des traductions des déductions de l'un dans les déductions de l'autre. Par exemple, il existe (au moins) trois types de systèmes de déduction équivalents pour le calcul des prédicats : les systèmes à la Hilbert, la déduction naturelle et le calcul des séquents. On y ajoute parfois le style de Fitch qui est une variante de la déduction naturelle dans laquelle les démonstrations sont présentées de façon linéaire.

Alors que la théorie des nombres démontre des propriétés des nombres, on notera la principale caractéristique de la logique en tant que théorie mathématique : elle « démontre » des propriétés de systèmes de déduction dans lesquels les objets sont des « théorèmes ». Il y a donc un double niveau dans lequel il ne faut pas se perdre. Pour clarifier les choses, les « théorèmes » énonçant des propriétés des systèmes de déduction sont parfois appelés des « métathéorèmes ». Le système de déduction que l'on étudie est appelé la « théorie » et le système dans lequel on énonce et démontre les métathéorèmes est appelé la « métathéorie ».

Les propriétés fondamentales des systèmes de déduction sont les suivantes:

La correction
La correction énonce que les théorèmes sont valides dans tous les modèles. Cela signifie que les règles d'inférence sont bien adaptées à ces modèles, autrement dit que le système de déduction formalise correctement le raisonnement dans ces modèles.
La cohérence
Un système de déduction est cohérent (on emploie aussi l'anglicisme consistant) s'il admet un modèle, ou ce qui revient au même, s'il ne permet pas de démontrer n'importe quelle formule. On parle aussi de cohérence équationnelle lorsque le système admet un modèle non trivial, c'est-à-dire ayant au moins deux éléments. Cela revient à affirmer que le système ne permet pas de démontrer n'importe quelle équation.
La complétude
Elle se définit par rapport à une famille de modèles. Un système de déduction est complet par rapport à une famille de modèles, si toute proposition qui est valide dans tous les modèles de la famille est un théorème. En bref, un système est complet si tout ce qui est valide est démontrable.

Une autre propriété des systèmes de déduction apparentée à la complétude est la cohérence maximale. Un système de déduction est maximalement cohérent, si l'ajout d'un nouvel axiome qui n'est pas lui-même un théorème rend le système incohérent.

Affirmer « tel système est complet pour telle famille de modèles » est un exemple typique de métathéorème.

Dans ce cadre, la notion intuitive de vérité donne lieu à deux concepts formels : la validité et la démontrabilité. Les trois propriétés de correction, cohérence et complétude précisent comment ces notions peuvent être reliées, espérant qu'ainsi la vérité, quête du logicien, puisse être cernée.

Le calcul des propositions[modifier | modifier le code]

Les propositions sont des formules exprimant des faits mathématiques, c'est-à-dire des propriétés qui ne dépendent d'aucun paramètre, et qui donc ne peuvent qu'être vraies ou fausses, comme « il pleut » ou « 3 est un multiple de 4 » (au contraire de « n est un multiple de 4 » qui est vraie ou fausse selon la valeur que l'on donne au paramètre n). Les propositions sont utilisées notamment pour exprimer des principes logiques : par exemple la propriété déjà évoquée que d'une contradiction on peut déduire n'importe quoi s'exprime par la formule propositionnelle (P ∧ ¬P) ⇒ Q. Elles servent également à fonder les systèmes de déductions logiques.

Les propositions élémentaires, appelées variables propositionnelles, sont combinées au moyen de connecteurs pour former des formules complexes. Les propositions peuvent être interprétées en remplaçant chaque variable propositionnelle par un fait. Par exemple une interprétation de la proposition ci-dessus pourrait être « si 3 est pair et 3 est impair alors 0 = 1 ». En général on simplifie en interprétant les variables propositionnelles par la valeur de vérité du fait associé, les connecteurs deviennent alors des opérations booléennes. Le calcul des propositions peut donc être vu comme une formalisation du calcul booléen, ce qui autorise plusieurs types d'applications, notamment son utilisation comme langage de spécification de circuits en électronique.

Articles détaillés : Calcul des propositions et Fonction logique.

Le premier article porte sur les aspects de logique mathématique, tandis que le second porte sur les aspects pragmatiques tels qu'ils sont vus par les électroniciens.

Connecteurs les plus fréquents[modifier | modifier le code]

Les connecteurs sont présentés avec leur interprétation en logique classique.

La disjonction
La disjonction de deux propositions P et Q est la proposition notée PQ ou « P ou Q » qui est vraie si l’une au moins des deux propositions est vraie, et fausse si les deux propositions sont fausses.
La négation
La négation d’une proposition P, est la proposition notée ¬P, ou « non P » qui est vraie lorsque P est fausse et fausse lorsque P est vraie.

À partir de ces deux connecteurs, on peut construire d’autres connecteurs ou abréviations utiles :

La conjonction
La conjonction de deux propositions P et Q est la proposition suivante :
¬((¬P) ∨ (¬Q)) c'est-à-dire non ( (non P) ou (non Q) )
Celle-ci est notée PQ ou « P et Q » et n’est vraie que lorsque P et Q sont vraies et fausse si l’une des deux propositions est fausse.
L'implication
L'implication de Q par P est la proposition (¬P) ∨ Q, notée « PQ » ou « P implique Q », et qui est fausse seulement si P est une proposition vraie et Q fausse.
L'équivalence
L'équivalence logique de P et Q est la proposition ( (PQ) ∧ ( QP) ) ( ((P implique Q) et (Q implique P) )), notée « PQ » ou (P est équivalent à Q), et qui n'est vraie que si les deux propositions P et Q ont même valeur de vérité.
Le ou exclusif
Le ou exclusif ou disjonction exclusive de P et Q est la proposition P ∨∨ Q (parfois aussi notée[5] PQ ou encore[6] P | Q) qui correspond à (PQ) ∧ ¬(PQ), c'est-à-dire en français : soit P, soit Q, mais pas les deux à la fois. Le ou exclusif de P et Q correspond à P ⇔ ¬Q ou encore à ¬(PQ). Cette proposition n'est vraie que si P et Q ont des valeurs de vérités distinctes.

Connecteur universel[modifier | modifier le code]

Une caractéristique du calcul propositionnel dit « classique » est que toutes les propositions peuvent s'exprimer à partir de deux connecteurs : par exemple ∨ et ¬ (ou et non)[7]. Mais d'autres choix sont possibles comme ⇒ (implication) et ⊥ (faux). On sait aussi que l'on peut aussi n'utiliser qu'un seul connecteur, le symbole de Sheffer « | » (Henry M. Sheffer, 1913), appelé « stroke » par son concepteur et appelé aujourd'hui Nand et noté NAND ANSI.svg par les concepteurs de circuits ; on peut aussi n'utiliser que le connecteur Nor (noté NOR ANSI.svg) comme l'a remarqué Charles Sanders Peirce (1880) sans le publier. En somme, en logique classique, un unique connecteur suffit pour rendre compte de toutes les opérations logiques.

Le calcul des prédicats[modifier | modifier le code]

Le calcul des prédicats étend le calcul propositionnel en permettant d'écrire des formules qui dépendent de paramètres ; pour cela le calcul des prédicats introduit les notions de variables, de symboles de fonctions et de relations, de termes et de quantificateurs ; les termes sont obtenus en combinant les variables au moyen des symboles de fonction, les formules élémentaires sont obtenues en appliquant les symboles de relations à des termes.

Une formule typique du calcul des prédicats est « ∀a,b ((p = a.b) ⇒ ((a = 1) ∨ (b = 1)) » qui lorsqu'on l'interprète dans les entiers exprime que le paramètre p est un nombre premier (ou 1). Cette formule utilise deux symboles de fonction (le point, fonction binaire interprétée par la multiplication des entiers, et le symbole « 1 », fonction 0-aire, c'est-à-dire constante) et un symbole de relation (pour l'égalité). Les variables sont a, b et p, les termes sont a.b et 1 et les formules élémentaires sont « p = a.b », « a = 1 » et « b = 1 ». Les variables a et b sont quantifiées mais pas la variable p dont la formule dépend.

Il existe plusieurs variantes du calcul des prédicats ; dans la plus simple, le calcul des prédicats du premier ordre, les variables représentent toutes les mêmes types d'objets, par exemple dans la formule ci-dessus, les 3 variables a, b et n vont toutes représenter des entiers. Dans le calcul des prédicats du second ordre, il y a deux types de variables : des variables pour les objets et d'autres pour les prédicats, c'est-à-dire les relations entre objets. Par exemple en arithmétique du second ordre (en) on emploie des variables pour représenter des entiers, et d'autres pour des ensembles d'entiers. La hiérarchie continue ainsi, au 3e ordre on a 3 types de variables pour les objets, les relations entre objets, les relations entre relations, etc.

Article détaillé : Calcul des prédicats.

Substitution[modifier | modifier le code]

Pour décrire le calcul des prédicats, une opération essentielle est la substitution qui consiste à remplacer dans une formule toutes les occurrences d'une variable x par un terme a, obtenant ainsi une nouvelle formule ; par exemple si on remplace la variable p par le terme n! + 1 dans la formule ci-dessus on obtient la formule « ∀a,b ((n! + 1 = a.b) ⇒ ((a = 1) ∨ (b = 1)) » (qui exprime que la factorielle de l'entier n plus 1 est un nombre premier).

Si P est une formule dépendant d'un paramètre x et a est un terme, l’assemblage obtenu en remplaçant x par a dans P est une formule qui peut se noter P[a/x] ou (a|x)P, ou d'autres variantes de ces notations. et s’appelle formule obtenue par substitution de x par a dans P.

Pour mettre en évidence un paramètre x dont dépend une formule P, on écrit celle-ci sous la forme P{x} ; on note alors P{a} la proposition (a|x)P.

On peut chercher à trouver la (les) substitution(s) qui rend(ent) une formule prouvable ; le problème est particulièrement intéressant dans le cas de formules dites équationnelles, c'est-à-dire de la forme t(x) = t'(x). Le théorie qui cherche à résoudre de telles équations dans le cadre de la logique mathématique s'appelle l'unification.

Les quantificateurs[modifier | modifier le code]

Les quantificateurs sont les ingrédients syntaxiques spécifiques du calcul des prédicats. Comme les connecteurs propositionnels ils permettent de construire de nouvelles formules à partir d'anciennes, mais ils s'appuient pour cela sur l'utilisation des variables.

Article détaillé : Quantificateurs.

Soit une formule du calcul des prédicats P. On construit alors une nouvelle formule dite existentielle notée ∃ x P qui se lit « il existe x tel que P ». Supposons que P ne « dépende » que de x. La proposition ∃ x P est vraie quand il existe au moins un objet a (dans le domaine considéré, celui sur lequel « varie » x) tel que, quand on substitue a à x dans P on obtienne une proposition vraie. La formule P est vue comme une propriété, et ∃ x P est vraie quand il existe un objet ayant cette propriété.

Le signe ∃ s’appelle le quantificateur existentiel.

De même on peut construire à partir de P une formule dite universelle notée ∀ x P, qui se lit « pour tout x P » ou quel que soit x P. Elle signifie que tous les objets du domaine considéré (ceux que x est susceptible de désigner) possèdent la propriété décrite par P.

Le signe ∀ s’appelle le quantificateur universel.

En logique classique les quantificateurs universel et existentiel peuvent se définir l'un par rapport à l'autre, par négation car :

x P équivaut à ¬ ∃x ¬P   et   ∃x P équivaut à ¬ ∀x ¬ P

En effet « il est faux que tout objet possède une propriété donnée » signifie « il en existe au moins un qui ne possède pas cette propriété  ».

Utilisation des quantificateurs[modifier | modifier le code]

Propriétés élémentaires[modifier | modifier le code]

Soient P et Q deux propositions et x un objet indéterminé.

  • ¬(∃ x P) ⇔ (∀ x ¬ P)
  • (∀ x) (PQ) ⇔ ( (∀ x) P ∧ (∀ x) Q )
  • (∀ x) P ∨ (∀ x) Q ⇒ (∀ x) (PQ ) (Implication réciproque fausse en général)
  • (∃ x) (PQ) ⇔ ( (∃ x) P ∨ (∃ x) Q )
  • (∃ x) (PQ) ⇒ ( (∃ x) P ∧ (∃ x) Q ) (Implication réciproque fausse en général)
Propriétés utiles[modifier | modifier le code]

Soient P une proposition et x et y des objets indéterminés.

  • (∀ x) (∀ y) P ⇔ (∀ y) (∀ x) P
  • (∃ x) (∃ y) P ⇔ (∃ y) (∃ x) P
  • (∃ x) (∀ y) P ⇒ (∀ y) (∃ x) P S’il existe un x, tel que pour tout y, on ait P vraie, alors pour tout y, il existe bien un x (celui obtenu avant) tel que P soit vraie.
    L’implication réciproque est fausse en général, parce que si pour chaque y, il existe un x tel que P soit vraie, ce x pourrait dépendre de y et varier suivant y. Ce x pourrait donc ne pas être le même pour tout y tel que P soit vraie.
Propriétés moins intuitives[modifier | modifier le code]
  • ∀x Px ⇒ ∃x Px [8]

Si A est une formule où la variable x n'apparaît pas librement, on a [9]:

  • (A ⇒ ∀x Px) ⇔ ∀x (A ⇒ Px)
  • (A ⇒ ∃x Px) ⇔ ∃x (A ⇒ Px)

Mais aussi :

  • (∀x Px ⇒ A) ⇔ ∃x (Px ⇒ A)
  • (∃x Px ⇒ A) ⇔ ∀x (Px ⇒ A)

L’égalité[modifier | modifier le code]

Le symbole de relation = qui représente l'égalité a un statut un petit peu particulier, à la frontière entre les symboles logiques (connecteurs, quantificateurs) et les symboles non logique (relations, fonctions).

La formule a = b signifie que a et b représentent des objets identiques, et se lit « a est égal à b »

est définie par ab si ¬(a = b)

Axiomes de l'égalité en logique du premier ordre[modifier | modifier le code]

  • x (x = x) (réflexivité de =)
  • x (∀ y) ( (x = y) ⇔ (y = x) ) (symétrie de =)
  • x (∀ y) (∀ z) ( ((x = y) ∧ (y = z)) ⇒ (x = z) ) (transitivité de =)

La relation = étant réflexive, symétrique et transitive, on dit que la relation = est une relation d'équivalence

  • Soit P{x} une formule dépendant d'une variable x. Soient a et b deux termes tels que a = b. Alors les propositions P{a} et P{b} sont équivalentes.
  • Soit F(x) une fonction contenant une variable libre x. Soient a et b des termes tels que a = b. Alors les termes F(a) et F(b) (obtenus en remplaçant respectivement x par a et x par b dans F(x)) sont égaux.

Ces deux dernières propriétés expriment intuitivement que = est la plus fine des relations d'équivalence.

Définition en logique du second ordre[modifier | modifier le code]

En logique du second ordre on peut définir plus simplement l'égalité par :

  • a = b si et seulement si ∀P (Pa ⇔ Pb)

Autrement dit deux objets sont égaux si et seulement s'ils ont les mêmes propriétés (principe d'identité des indiscernables énoncé par Leibniz)

Quelques systèmes déductifs[modifier | modifier le code]

La théorie des ensembles[modifier | modifier le code]

Article détaillé : Théorie des ensembles.

La théorie des ensembles est à la base de nombreuses théories mathématiques. Outre les symboles de logique énumérés précédemment, cette théorie utilise le symbole de relation ∈ (appartenance) qu'elle utilise pour définir la notion d'ensemble en mathématique.

L’appartenance[modifier | modifier le code]

La relation d’appartenance permet de définir le lien entre un ensemble et ses éléments.

Le signe de l’appartenance se note à l’aide du signe « ∈ » et représente la relation d’appartenance d’un objet à un autre. Si a et b sont deux objets ab se lit « a appartient à b » ou encore « a est élément de b ».

Cette relation est primitive en théorie des ensembles. Elle est définie implicitement par des axiomes (comme ceux de ZFC).

Définition de la non appartenance[modifier | modifier le code]

La non appartenance représente la relation d'un objet qui n’appartient pas à un autre objet. Elle se définit logiquement à partir de l'appartenance. Le signe ∉ se définit par  : ab si ¬(ab).

L’expression ab se lit « a n’appartient pas à b ».

Égalité de deux ensembles[modifier | modifier le code]

Deux ensembles sont égaux si et seulement s'ils ont les mêmes éléments, ce qui s'écrit : a = b ⇔ ∀x (x ∈ a ⇔ x ∈ b).

Le si est l'axiome d'extensionnalité et le seulement si découle des axiomes de l'égalité disant que deux objets égaux ont les mêmes propriétés.

Bibliographie[modifier | modifier le code]

Manuels universitaires[modifier | modifier le code]

  • Jon Barwise (dir.), Handbook of mathematical Logic, North Holland,‎ 1977 (ISBN 0-7204-2285-X)
Synthèse du savoir sur le sujet au moment de sa parution.
Quasi une encyclopédie se voulant dans la continuité de la synthèse du savoir sur la logique initié par [Barwise 1977 ; ci dessus], avec en 2011, 16 volumes parus.

Histoire et philosophie[modifier | modifier le code]

Bande dessinée[modifier | modifier le code]

Livres[modifier | modifier le code]

Recueils de textes classiques ayant fondé la discipline[modifier | modifier le code]

  • (en) Martin Davis (dir.), The Undecidable : Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions, Dover Publication,‎ 1965
  • (en) Jean van Heijenoort (dir.), From Frege To Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard Univ. Press.,‎ 1977 (1re éd. 1967) (présentation en ligne)
  • (en) Hilary Putnam (dir.) et Paul Benacerraf (dir.), Philosophy of Mathematics: Selected Readings, Cambridge University Press,‎ 1983 (1re éd. 1964) (ISBN 0-521-29648-X)
  • Jean Largeault (dir.), Logique Mathématique : Textes, Armand Colin,‎ 1972
  • François Rivenc et Philippe de Rouillan, Logique et fondements des mathématiques (1850-1914). Anthologie, Payot,‎ 1992

Recueils de textes sur un auteur précis[modifier | modifier le code]

  • Alfred Tarski,
    • Logique, sémantique, métamathématique, 1923-1944 : Sélection de textes par Gilles Gaston Granger et al., vol. 1 et 2, Paris, Armand Colin,‎ 1974
  • Kurt Gödel,
    • Collected Works, posthume.

Manuels et ouvrages généralistes de référence[modifier | modifier le code]

En anglais[modifier | modifier le code]

Nous ne mentionnons pas ici les ouvrages de références en anglais dans les sous-domaines de la logique mathématique que sont la théorie de la démonstration, la théorie des modèles, la théorie des ensembles ou la calculabilité.

En français[modifier | modifier le code]

La quasi-totalité des ouvrages de référence sont en anglais, néanmoins existent aussi en français, des ouvrages de référence comme ceux listés ci-dessous :

  • Roland Fraïssé, Cours de logique mathématique, Paris, Gauthier-Villars,‎ (3 vol.) 1971-1975 (1re éd. 1967)
  • René Cori et Daniel Lascar, Logique mathématique, tomes 1 [détail des éditions] et 2 [détail des éditions], Masson,‎ 2003
  • René Lalement, Logique, réduction, résolution, Masson,‎ 1990
  • Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul), Hermes Science Publications,‎ 1997 (ISBN 2-86601-380-8)
  • Yannis Delmas-Rigoutsos et René Lalement, La Logique ou l'art de raisonner, Paris, Le Pommier,‎ 2000 [détail de l’édition] (ISBN 2746500353)
  • René David, Karim Nour et Christophe Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod,‎ 2001 (ISBN 2-10-006796-6)

Liens bibliographiques externes[modifier | modifier le code]

Notes et références[modifier | modifier le code]

  1. Cette classification en quatre grands axes, généralement admise, est celle proposée par Jon Barwise éditeur de l'ouvrage collectif Handbook of Mathematical Logic Handbook of Mathematical Logic.
  2. Avant 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).
  3. Sauf 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.
  4. Cela lui a valu la médaille Fields.
  5. Ce symbole ⊕ est utilisé pour noter le ou exclusif par les concepteurs de circuits et les cryptographes, il ne faut pas le confondre avec la disjonction additive de la logique linéaire.
  6. À ne pas confondre avec le symbole de Sheffer.
  7. Cette propriété n'est plus valable en logique intuitionniste.
  8. Ainsi, afin d'avoir le théorème de complétude l'ensemble de base d'une structure du calcul des prédicats n'est pas vide.
  9. Moyen mnémotechique pour se rappeler ces règles : le quantificateur se conserve sur le conséquent de l'implication et s'inverse sur l'antécédent.
  10. Auteur d'un article en 1883 intitulé On a New Algebra of Logic dans la revue "Studies in Logic"

Annexes[modifier | modifier le code]

Sur les autres projets Wikimedia :

Articles connexes[modifier | modifier le code]