Voir la source de Logique mathématique

[[Image:Russell, Whitehead - Principia Mathematica to 56.jpg|thumb|''[[Principia Mathematica]]'', un des travaux qui ont le plus marqué l'histoire de la logique mathématique{{Note|texte={{Harvsp|Ferreirós|2001}}<ref group=alpha>{{en}} {{Citeref|Ferreirós|2001|José Ferreirós. The Road to Modern Logic-An Interpretation. December 2001. Bulletin of Symbolic Logic 7(04)}}</ref> Section 4.4 : Principia Mathematica {{harv|Whitehead|1910}} a été reconnu comme un moment marquant de l'histoire de la logique moderne. Jusqu'en 1928, c'était la référence la plus importante pour tout étudiant en logique...}}.]]

La '''logique mathématique''' ou '''métamathématique''' est une [[Discipline (spécialité)|discipline]] des [[mathématiques]] inventée à la fin du {{s-|XIX}}, qui s'est donné comme objet l'étude des mathématiques en tant que [[Langage mathématique|langage]]. 

Les objets fondamentaux de la logique mathématique sont les [[Formule (mathématiques)|formules]] représentant les [[énoncés mathématiques]], les dérivations ou [[Démonstration formelle|démonstrations formelles]] représentant les [[Logique et raisonnement mathématique|raisonnements mathématiques]] et les sémantiques ou modèles ou interprétations dans des [[Structure (logique mathématique)|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 ==
{{loupe|Histoire de la logique}}

=== Naissance de la logique mathématique et logicisme ===
{{article connexe|Logicisme}}
La logique mathématique<ref>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 [[David Hilbert|Hilbert]]) et « [[idéographie]] » (''Begriffsschrift'') (terminologie de [[Frege]]).</ref> est née à la fin du {{s-|XIX}} 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|crise des fondements mathématiques]] provoquée par la complexification des mathématiques et l'apparition des [[paradoxe]]s. Ses débuts sont marqués par la rencontre entre deux idées nouvelles :
* la volonté chez [[Gottlob Frege|Frege]], [[Bertrand Russell|Russell]], [[Giuseppe Peano|Peano]] et [[David Hilbert|Hilbert]] de donner une [[fondation des mathématiques|fondation]] [[Axiome|axiomatique]] aux mathématiques ;
* la découverte par [[George Boole]] de l'existence de [[structure (mathématiques)|structures]] [[structure algébrique|algébriques]] permettant de définir un «[[Table de vérité| calcul de vérité]] ».

La logique mathématique se fonde sur les premières tentatives de traitement formel des mathématiques, dues à [[Gottfried Wilhelm Leibniz|Leibniz]] et [[Johann Heinrich Lambert|Lambert]] (fin {{s-|XVII}} - début {{s-|XVIII}}). Leibniz a en particulier introduit une grande partie de la [[Notation (mathématiques)|notation mathématique]] moderne (usage des [[Quantificateur (logique)|quantificateurs]], [[Intégration (mathématiques)|symbole d'intégration]], etc.). Toutefois on ne peut parler de logique mathématique qu'à partir du milieu du {{s-|XIX}}, 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 logique|conjonction]], la [[Disjonction logique|disjonction]] et [[Implication (logique)|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ème formel|systèmes logiques formalisés]]. L'un des premiers de ces systèmes a été développé par [[Frege|Gottlob Frege]] au tournant du {{s-|XX}}. 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 [[Machine de Turing|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 [[Problèmes de Hilbert|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ème axiomatique|systèmes d'axiomes]] pour les mathématiques : les [[axiomes de Peano]] pour l'[[arithmétique]], ceux de [[Ernst Zermelo|Zermelo]] complétés par [[Thoralf Skolem|Skolem]] et [[Abraham Adolf Fraenkel|Fraenkel]] pour la [[théorie des ensembles]] et le développement par [[Alfred North Whitehead|Whitehead]] et [[Bertrand Russell|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 Cole Kleene|Stephen Kleene]], [[Haskell Curry]] et [[Emil Post]], qui ont grandement contribué à la définition de la notion d'''[[Algorithmique|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 ==

=== 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 : {{Passage non pertinent|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.

Depuis la fin du {{s-|XX}} 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émonstrateur automatique de théorèmes|démonstrateurs automatiques]], [[système expert|systèmes experts]] et [[assistant de preuve|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 {{s-|XX}} et au début du {{s-|XXI}} 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 [[Kurt Gödel|Gödel]] a montré dans sa thèse de doctorat, un an avant son célèbre [[théorème d'incomplétude de Gödel|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 axiomes<ref>Sauf si la théorie est incohérente, car du faux on peut déduire toute proposition. Ce principe s'appelle le [[Principe d'explosion|''Ex falso sequitur quodlibet'']].</ref>. 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 de Gentzen|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 {{s-|XX}}. 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]]<ref>Cela lui a valu la [[médaille Fields]].</ref>. 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 {{s-|XXI}}, é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<ref>{{Ouvrage|auteur1=Étienne Bonheur|titre=Élements de mathématiques pour le {{s-|XXI}}, volume 1|éditeur=Paysages Mathématiques|date=2019|isbn=1-0928-9748-8|isbn2=978-1-0928-9748-8|isbn3=1-9833-0785-8|oclc=1328050475|lire en ligne=https://www.worldcat.org/oclc/1328050475|commentaire=La définition donnée ici est partiellement issue de ce livre (page 42).}}</ref>. 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 [[logique intuitionniste|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 : [[suite]]s de symboles, [[Arbre (combinatoire)|arbre]]s étiquetés, [[Théorie des graphes|graphes]]…

* d'un système de [[déduction logique|déduction]] (ou d'un système d'''inférence,'' ou encore d'un ''calcul'') disposant d'un ensemble d'[[Axiome|axiomes]] et de [[Règle d'inférence|règles d'inférence]]. 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'').
La sémantique sert à attribuer à chaque formule construite à partir d'un système formel un sens, voire une valeur de vérité. Cette attribution se fait au moyen d'une  ''[[Interprétation (logique)|interprétation]]'' (ou ''valuation'') des formules; il s'agit d'une [[fonction (mathématiques)|fonction]] associant à toute formule un objet dans une structure abstraite appelée ''modèle'', ce qui permet de définir la ''validité'' des formules. Elle permet ainsi d'interpréter les formules d'un système formel dans un contexte donné. Dans le cadre de la logique classique, il s'agit d'attribuer à chaque formule la valeur ''Vrai'' ou la valeur ''Faux,'' qu'on peut même respectivement identifier à donner la valeur ''1'' ou la valeur ''0'' (voir [[Algèbre de Boole (logique)|Algèbre de Boole]]). 

Il arrive parfois que l'on puisse définir la syntaxe comme étant le système de déduction, et qu'on appelle calcul le système formel entier, voire le système logique entier. De ce fait, il est courant d'utiliser le nom de ''calcul des propositions'' pour désigner ce qu'on devrait appeler ''logique des propositions,'' de la même façon qu'on peut confondre ''calcul des prédicats'' et ''logique des prédicats.''

=== Syntaxe et sémantique ===

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 [[ensemble récursif|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. L'étude de logique du point de vue des formules et des expressions s'appelle la ''syntaxe''.

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 exemple, par des éléments d'une [[Algèbre de Boole (logique)|algèbre de Boole]].

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 justifier mathématiquement la rigueur mathématique dans les mathématiques. 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. Cette technique — plonger les objets dans un monde plus vaste pour raisonner sur eux — est couramment utilisée en mathématique et est efficace.

Cependant, 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 ''[[correspondance de Curry-Howard|contenu calculatoire]]''.

=== Systèmes de déduction ===

En logiques [[logique classique|classique]] et [[logique intuitionniste|intuitionniste]], on distingue deux types d'[[axiome]]s : les ''axiomes logiques'' qui expriment des propriétés purement logiques comme <math>A\lor\lnot A</math> ([[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]] tandis que les axiomes de Zermelo-Fraenkel définissent les [[théorie des ensembles|ensembles]]. 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 pour la déduction naturelle|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ème]]s ». 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 la [[Correction (logique)|correction]], la [[cohérence (logique)|cohérence]], la [[complétude]] .

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. 

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 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 ==
{{Article détaillé|Calcul des propositions}}

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<ref>Sans qu'on soit capable d'affirmer quelle alternatives s'avère.</ref>, comme « 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'') ou  {{citation | les zéros non triviaux de la fonction zêta de Riemann ont tous pour partie réelle 1/2}}. 

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 une proposition. Par exemple une interprétation de la proposition 
<math>(P\wedge \neg P)\implies Q</math> pourrait être ''« si 3 est pair et 3 est impair alors 0 = 1 »''. 

=== Connecteurs les plus fréquents ===
Les connecteurs sont présentés avec leur interprétation en [[logique classique]].

La [[Disjonction logique|disjonction]] de deux propositions ''P'' et ''Q'' est la proposition notée <math>P\vee Q</math> ou « ''P'' ou ''Q'' » qui est vraie si au moins une des deux propositions est vraie; elle est donc fausse uniquement si les deux propositions sont fausses.

La négation d’une proposition ''P'' est la proposition notée '''¬''P''''', ou « non ''P'' » qui est vraie lorsque ''P'' est fausse; elle est donc fausse lorsque ''P'' est vraie.

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

La [[Conjonction logique|conjonction]] de deux propositions ''P'' et ''Q'' est la proposition suivante :
:{{retrait|<math>\neg((\neg P)\vee(\neg Q))</math> c'est-à-dire non ( (non ''P'') ou (non ''Q'') )}}
Celle-ci est notée '''''P'' ∧ ''Q''''' ou « ''P'' et ''Q'' » et n’est vraie que lorsque ''P'' et ''Q'' sont vraies et est donc fausse si l’une des deux propositions est fausse. 

L'[[Implication (logique)|implication]] de ''Q'' par ''P'' est la proposition <math>(\neg P)\vee Q</math>, notée « <math>P\implies Q</math> » ou « ''P'' implique ''Q'' », et qui est fausse seulement si ''P'' est une proposition vraie et ''Q'' fausse.

L'[[équivalence logique]] de ''P'' et ''Q'' est la proposition <math>\bigg((P\implies Q)\wedge (Q\implies P)\bigg)</math> ( ((''P'' implique ''Q'') et (''Q'' implique ''P'') )), notée « <math>P\iff Q</math> » 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]]'' ou ''disjonction exclusive'' de ''P'' et ''Q'' est la proposition <math>P\;\underline{\vee}\;Q</math> (parfois aussi notée<ref>Ce symbole ⊕ est utilisé pour noter le ou exclusif par les concepteurs de circuits et les [[Réseau de Feistel|cryptographes]], il ne faut pas le confondre avec la ''disjonction additive'' de la [[logique linéaire#Syntaxe|logique linéaire]].</ref> P ⊕ Q ou encore<ref>À ne pas confondre avec le symbole de Sheffer.</ref> P | Q ou par les concepteurs de circuits [[Image:XOR ANSI.svg|30px|alt=signe XOR]]) qui correspond à <math>(P\vee Q)\wedge \neg(P\wedge Q)</math>, 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 à ¬(''P'' ⇔ ''Q''). Cette proposition n'est vraie que si ''P'' et ''Q'' ont des valeurs de vérités distinctes.

=== Connecteur universel ===

Une caractéristique du calcul propositionnel dit « [[logique classique|classique]] » est que toutes les propositions peuvent s'exprimer à partir de deux connecteurs : par exemple ∨ et ¬ (''ou'' et ''non'')<ref>Cette propriété n'est plus valable en logique intuitionniste.</ref>. Mais d'autres choix sont possibles comme ⇒ (implication) et ⊥ (faux). On peut n'utiliser qu'un seul connecteur, le ''symbole de Sheffer'' « | » ([[Henry M. Sheffer]], 1913), appelé ''« stroke »'' par son concepteur et appelé aujourd'hui ''[[fonction NON-ET|Nand]]'' et noté [[Image:NAND ANSI.svg|30px|alt=signe NAND]] par les concepteurs de circuits ; on peut aussi n'utiliser que le connecteur ''[[Fonction NON-OU|Nor]]'' (noté [[Image:NOR ANSI.svg|30px|alt=signe NOR]]) 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 ==
{{Article détaillé|Calcul des prédicats|Logique d'ordre supérieur}}

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 <math>\forall a,b \; \bigg((p=a\times b)\implies (a=1)\vee (b=1)\bigg)</math> 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 ''p'' 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]] 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.

=== Substitution ===
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 « <math>\forall a\forall b((n!+1=a\cdot b)\implies ((a=1)\vee (b=1))</math> » (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 <math>P[a/x]</math> ou <math>(a\mid x)P</math>, 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)''. La théorie qui cherche à résoudre de telles équations dans le cadre de la logique mathématique s'appelle l'[[unification]].

=== Les quantificateurs ===

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é|Quantificateur_(logique){{!}}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 
{{Centrer|<math>\forall x\; P</math> équivaut à <math>\neg \exists x\; \neg P</math> &nbsp; et &nbsp; <math>\exists x\; P</math> équivaut à <math>\neg \forall x\; \neg P</math>}}
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 ====

===== Propriétés élémentaires =====

Soient ''P'' et ''Q'' deux propositions et ''x'' un objet indéterminé.
*<math>\neg(\exists x\; P)\Leftrightarrow (\forall x\;\neg P)</math>
*<math>(\forall x)(P\wedge Q)\Leftrightarrow ((\forall x)P\wedge(\forall x)Q)</math>
*<math>(\forall x)P\vee (\forall x)Q\Rightarrow (\forall x)(P\vee Q)</math>
{{retrait| (Implication réciproque fausse en général)}}
*<math>(\exists x)(P\vee Q)\Leftrightarrow ((\exists x)P\vee (\exists x)Q)</math>
*<math>(\exists x)(P\wedge Q)\Rightarrow ((\exists x)P\wedge (\exists x)Q)</math>
{{retrait| (Implication réciproque fausse en général)}}

===== Propriétés utiles =====

Soient ''P'' une proposition et ''x'' et ''y'' des objets indéterminés.
*<math>(\forall x)(\forall y)P\Leftrightarrow (\forall y)(\forall x)P</math>
*<math>(\exists x)(\exists y)P\Leftrightarrow (\exists y)(\exists x)P</math>
*<math>(\exists x)(\forall y)P\Rightarrow (\forall y)(\exists x)P</math>
{{retrait|1= 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.<br />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 =====

*<math>\forall x \; Px\implies \exist x Px</math><ref>Ainsi, afin d'avoir le [[Théorème de complétude de Gödel|théorème de complétude]] l'ensemble de base d'une [[Structure (logique mathématique)|structure]] du calcul des prédicats n'est pas vide.</ref>
Si ''A'' est une formule où la variable ''x'' n'apparaît pas [[Variable libre|librement]], on a<ref> Moyen mnémotechnique pour se rappeler ces règles : le '''quan'''tificateur se '''con'''serve sur le '''con'''séquent de l'implication et s'inverse sur l'antécédent.</ref> :
*<math>(A\implies \forall x Px)\Leftrightarrow \forall x(A\implies Px)</math>
*<math>(A\implies \exists x Px)\Leftrightarrow \exists x(A\implies Px)</math>

Mais aussi, ce qui est moins intuitif : 
*<math>(\forall x Px\implies A)\Leftrightarrow \exists x(Px\implies A)</math>
*<math>(\exists x Px\implies A)\Leftrightarrow \forall x(Px\implies A)</math>
Associé à cette dernière règle, voir le [[paradoxe du buveur]].

=== L’égalité ===

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 logiques (relations, fonctions). La formule ''a'' = ''b'' signifie que ''a'' et ''b'' représentent le même objet (ou encore que ''a'' et ''b'' sont des notations différentes du même objet), et se lit « ''a'' est égal à ''b'' ». 

La [[théorie des modèles]] classique se développe le plus souvent dans le cadre du calcul des prédicats avec égalité, c'est-à-dire que les [[théorie axiomatique|théories]] considérées sont égalitaires : la relation d'égalité est utilisée en plus des symboles de la [[Signature (logique)|signature]] de la théorie.

Du point de vue de la déduction, l'égalité est régie par des axiomes, décrits ci-dessous, exprimant essentiellement que deux objets égaux ont les mêmes propriétés (et, en [[logique du second ordre]], que la réciproque est vraie).

La négation de « = » est la relation « ≠ » qui est définie par ''a'' ≠ ''b'' si et seulement si ¬(''a'' = ''b'').

==== Axiomes de l'égalité en logique du premier ordre ====

En [[Calcul des prédicats|logique du premier ordre]] :
*<math>\forall x\;(x=x)</math> (réflexivité de ''='')
*<math>\forall x(\forall y)((x=y)\Leftrightarrow (y=x)</math> (symétrie de ''='')
*<math>\forall x(\forall y)(\forall z)(((x=y)\wedge (y=z))\implies (x=z))</math> (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. Ces axiomes (un par formule ''P''{''x''}) expriment que deux objets égaux ont les mêmes propriétés.
* 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 ====

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 [[Gottfried Wilhelm Leibniz|Leibniz]])

== Notes et références ==
=== Notes ===
{{Références|colonnes=}}
=== Références ===
{{Références|groupe=alpha|colonnes=}}

== Bibliographie ==

=== Manuels universitaires ===
* {{Ouvrage
 |prénom1=Jon
 |nom1=Barwise
 |directeur1=oui
 |titre=Handbook of mathematical Logic
 |éditeur=North Holland
 |année=1977
 |isbn=0-7204-2285-X
}}
  {{Commentaire biblio|Synthèse du savoir sur le sujet au moment de sa parution.}}
* {{Ouvrage
 |prénom1=Dale
 |nom1=Jacquette
 |directeur1=oui
 |titre=A Companion to Philosophical Logic
 |éditeur=Blackwell
 |collection=Companions to Philosophy
 |année=2002
 |pages totales=832
 |isbn=978-1-4051-4575-6
 |présentation en ligne=http://www.blackwellreference.com/public/book?id=g9781405145756_9781405145756
}}
* {{Ouvrage
 |nom1=[[Stewart Shapiro]]
 |directeur1=oui
 |titre=The Oxford Handbook of Philosophy of Mathematics and Logic
 |éditeur=Oxford Scholarship
 |année=2005
 |pages totales=774
 |isbn=978-0-19-514877-0
 |présentation en ligne=http://www.oxfordscholarship.com/oso/public/content/philosophy/9780195148770/toc.html
}}
* {{Ouvrage
 |titre=Handbook of Philosophical Logic
 |éditeur=Kluwer Academic Publishers
 |année=depuis 2001
 |isbn=
 |présentation en ligne=http://www.dcs.kcl.ac.uk/research/groups/gllc/philo/
}}
  {{Commentaire biblio|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 ===

==== Handbooks ====
* [[Dov Gabbay]] et John Woods éditeurs, ''Handbook of the History of Logic'', en au moins 11 volumes, chez [[Elsevier]].
* Dov Gabbay et Franz Guenthner éditeurs,  ''Handbook of Philosophical Logic'', en au moins 16 volumes, chez Springer.

==== Bande dessinée ====
{{Logicomix}}

==== Livres ====
* Geraldine Brady
** ''From Peirce to Skolem: A Neglected Chapter in the History of Logic'', North Holland, coll. Studies in the History and Philosophy of Mathematics, Volume 4, 468 pages, 2000, {{ISBN|978-0-444-50334-3}}. Sur les apports en logique essentiellement de [[Charles Sanders Peirce|Peirce]] mais aussi de [[Oscar Howard Mitchel|Mitchell]]<ref group=note>Auteur d'un article en 1883 intitulé ''{{Langue|en|On a New Algebra of Logic}}'' dans la revue ''{{Langue|en|Studies in Logic}}''.</ref>, [[Ernst Schröder|Schröder]], [[Leopold Löwenheim|Löwenheim]] et [[Thoralf Skolem|Skolem]].
* [[Haskell Curry]],
** {{Ouvrage
 |langue  = en
 |titre   = Outlines of a formalist philosophy of mathematics
 |éditeur = North Holland
 |année   = 1951
 |isbn    = 
}}
** {{Ouvrage
 |titre                  = Foundations of Mathematical Logic
 |éditeur                = [[Dover Publications|Dover]]
 |année                  = 1979
 |année première édition = 1963
 |isbn                   = 
}}
* [[Wang Hao (logicien)|Hao Wang]]
** {{Ouvrage
 |langue  = en
 |titre   = From Mathematics to Philosophy
 |lieu    = Londres
 |éditeur = [[Routledge|Routledge & Kegan Paul]]
 |année   = 1974
 |isbn    = 
}}
** {{Ouvrage
 |langue        = en
 |titre         = Popular Lectures on Mathematical Logic
 |lieu          = New-York
 |éditeur       = Van Nostrand
 |année         = 1981
 |pages totales = 281
 |isbn          = 0-486-67632-3
 |lire en ligne = https://books.google.com/books?id=l4lOBAAAQBAJ&printsec=frontcover
}}
* {{Ouvrage
 |prénom1=Willard Van Orman
 |nom1=Quine
 |lien auteur1=Willard Van Orman Quine
 |traducteur=J. Largeault
 |titre=Philosophie de la logique
 |titre original=Philosophy of Logic
 |lieu=Paris
 |éditeur=[[Éditions Aubier-Montaigne|Aubier Montaigne]]
 |année=1975
 |isbn=
 |année première édition=1970 éd.: Prentice Hall
}}
* {{Citeref| Whitehead|1910|[[Alfred North Whitehead|Whitehead, Alfred North]] & [[Bertrand Russell|Russell, Bertrand]]: ''[[Principia Mathematica]]''. 3 vols, Merchant Books, 2001, {{ISBN|978-1-60386-182-3}} (vol. 1), {{ISBN|978-1-60386-183-0}} (vol. 2), {{ISBN|978-1-60386-184-7}} (vol. 3)}}

==== Recueils de textes classiques ayant fondé la discipline ====
* {{Ouvrage
 |langue=en
 |prénom1=Martin
 |nom1=Davis
 |lien auteur1=Martin Davis
 |directeur1=oui
 |titre=The Undecidable : Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions
 |éditeur=Dover Publication
 |année=1965
 }}
* {{Ouvrage
 |langue=en
 |prénom1=Jean
 |nom1=van Heijenoort
 |lien auteur1=Jean van Heijenoort
 |directeur1=oui
 |titre=From [[Frege]] To [[Gödel]]: A Source Book in Mathematical Logic, 1879-1931
 |éditeur=Harvard Univ. Press.
 |année=1977
 |année première édition=1967
 |isbn=
 |présentation en ligne=http://mathgate.info/cebrown/notes/vonHeijenoort.php
}}
* {{Ouvrage
 |langue=en
 |prénom1=Hilary
 |nom1=Putnam
 |lien auteur1=Hilary Putnam
 |directeur1=oui
 |prénom2=Paul
 |nom2=Benacerraf
 |lien auteur2=Paul Benacerraf
 |directeur2=oui
 |titre=Philosophy of Mathematics
 |sous-titre=Selected Readings
 |éditeur=[[Cambridge University Press]]
 |année=1983
 |année première édition=1964
 |isbn=0-521-29648-X
 |éditeur original=Englewood Cliffs {{!}} N.J.: Prentice-Hall <!--PARAMETRE 'éditeur original' N'EXISTE PAS -->
}}
* {{Ouvrage
 |prénom1=Jean
 |nom1=Largeault
 |lien auteur1=Jean Largeault
 |directeur1=oui
 |titre=Logique Mathématique
 |sous-titre=Textes
 |éditeur=[[Armand Colin]]
 |année=1972
 |isbn=
}}
* {{Ouvrage
 |prénom1=François
 |nom1=Rivenc
 |prénom2=Philippe
 |nom2=de Rouilhan
 |lien auteur2=Philippe de Rouilhan
 |titre=Logique et fondements des mathématiques (1850-1914). Anthologie
 |éditeur=[[Payot (éditions)|Payot]]
 |année=1992
 |isbn=
}}
* ''Le raisonnement en mathématiques et en sciences expérimentales'', éditions CNRS, 1958, 140 pages, L005890128.
** Ouvrage faisant suite au Colloque international de logique mathématique de septembre 1955, avec pour intervenants comme rapporteurs ou interlocuteurs, [[Thoralf Skolem|Skolem]], [[Evert Willem Beth|Beth]], [[Alfred Tarski|Tarski]], [[Paul Bernays|Bernays]], [[Andrzej Mostowski|Mostowski]], Arnold Schmidt, [[Roland Fraïssé|Fraïssé]], [[Arend Heyting|Heyting]], Krasner, [[Roger Martin (logicien)|Martin]] et [[Ferdinand Gonseth|Gonseth]].

==== Recueils de textes sur un auteur précis ====
* Alfred Tarski,
** {{Ouvrage
 |prénom1=Alfred
 |nom2=Tarski
 |lien auteur2=Alfred Tarski
 |titre=Logique, sémantique, métamathématique, 1923-1944
 |sous-titre=Sélection de textes par [[Gilles Gaston Granger]] ''et al.''
 |volume=1 et 2
 |lieu=Paris
 |éditeur=[[Armand Colin]]
 |année=1974
 |isbn=
}}
* Kurt Gödel, 
** ''Collected Works'', posthume.

=== Manuels et ouvrages généralistes de référence ===
==== En anglais ====
Nous ne mentionnons pas ici les ouvrages de référence 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é]].

* {{Ouvrage
 |langue=fr
 |prénom1=Alonzo
 |nom1=Church
 |lien auteur1=Alonzo Church
 |titre=Introduction to mathematical logic
 |lieu=Princeton
 |éditeur=[[Princeton University Press]]
 |année=1956
 |année première édition=1944
 |pages totales=378
 |isbn=0-691-02906-7
 |lire en ligne=https://books.google.com/books?id=JDLQOMKbdScC&printsec=frontcover
}}
* [[Stephen Cole Kleene]]
** {{Ouvrage
 |titre=Introduction to Metamathematics
 |éditeur=Ishi Press International
 |année=1952
 |lire en ligne=https://books.google.com/books?id=HZAjPwAACAAJ
}}
** {{Ouvrage
 |langue=fr
 |langue originale=en
 |traducteur=[[Jean Largeault]]
 |titre=Logique mathématique
 |titre original=Mathematical Logic (John Wiley - Dover 1967)
 |lieu=Paris
 |éditeur=Armand Colin (1971) ou Gabay (1987)
 |année=1987
 |pages totales=412
 |isbn=978-2-87647-005-7
 |isbn2=2-87647-005-5
 |lire en ligne=http://worldcat.org/oclc/523472
 |isbn original=0486425339 <!--PARAMETRE 'isbn original' N'EXISTE PAS -->
}}
* {{Ouvrage
 |nom1={{Lien|Elliott Mendelson}}
 |titre=Introduction to mathematical logic
 |éditeur=D. Van Nostrand
 |année=1964
 }}
* {{Ouvrage
 |prénom1=J. R.
 |nom1=Schoenfield
 |titre=Mathematical Logic
 |éditeur=[[Addison-Wesley]]
 |année=1967
 }}
* {{Ouvrage
 |nom1    = [[Jean-Yves Girard]]
 |prénom2 = Yves
 |nom2    = Lafont
 |prénom3 = Paul
 |nom3    = Taylor
 |titre   = Proofs and types
 |éditeur = [[Cambridge University Press]]
 |année   = 1989
 |isbn    = 
}}
* {{Ouvrage
 |nom1                   = {{Lien|langue=en|fr=Dirk van Dalen}}
 |titre                  = Logic and Structure
 |lieu                   = Berlin Heidelberg
 |éditeur                = [[Springer Science+Business Media|Springer-Verlag]]
 |année                  = 2004
 |année première édition = 1994
 |isbn                   = 
}}

==== En français ====

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 :

* {{Ouvrage
 |prénom1      = René
 |nom1         = Cori
 |lien auteur1 = René Cori
 |prénom2      = Daniel
 |nom2         = Lascar
 |titre        = Logique mathématique, tomes 1 {{détail des éditions|Référence : Logique mathématique 1(Cori-Lascar)}} et 2 {{détail des éditions|Référence : Logique mathématique 2 (Cori-Lascar)}}
 |éditeur      = Masson
 |année        = 2003
 |isbn         = 
 |année première édition = 1993 
}}
* {{Ouvrage
 |langue=fr
 |prénom1=René
 |nom1=David
 |prénom2=Karim
 |nom2=Nour
 |prénom3=Christophe
 |nom3=Raffalli
 |titre=Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés
 |lieu=Paris
 |éditeur=[[Éditions Dunod|Dunod]]
 |année=2001
 |pages totales=352
 |isbn=2-10-006796-6
}}
* {{La Logique ou l'art de raisonner (Delmas et Lalement)}}
* {{Ouvrage
 |prénom1=Roland
 |nom1=Fraïssé
 |lien auteur1=Roland Fraïssé
 |titre=Cours de logique mathématique
 |lieu=Paris
 |éditeur=[[Gauthier-Villars]]
 |année=(3 vol.) 1971-1975
 |année première édition=1967
 |isbn=
}}
* {{Ouvrage
 |prénom1=René
 |nom1=Lalement
 |titre=Logique, réduction, résolution
 |éditeur=Masson
 |année=1990
 |isbn=
}}
* {{Ouvrage
 |langue=fr
 |prénom1=Michel
 |nom1=de Rougemont
 |prénom2=Richard
 |nom2=Lassaigne
 |titre=Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul)
 |lieu=Paris
 |éditeur=Hermes Science Publications
 |année=1997
 |pages totales=248
 |isbn=2-86601-380-8
}}

=== Liens bibliographiques externes ===
* {{en}} {{pdf}} [http://www.ucl.ac.uk/philosophy/LPSG/Ch22.pdf Bibliographie de philosophie des mathématiques] de la [http://www.ucl.ac.uk/philosophy/LPSG/ London Philosophy Study Guide].

=== Notes bibliographiques ===
{{Références|groupe=note}}

== Annexes ==
{{Autres projets
  | Wikiversity = Logique (mathématiques)
}}
=== Articles connexes ===
* [[Fondements des mathématiques]]
* [[Logique classique]]
* [[Logique non classique]], dont : [[logique intuitionniste]], [[logique minimale]], [[logique linéaire]], [[logique infinitaire]]
* [[Syllogisme]]
* [[Idéographie]]
* [[Lambda-calcul]]
* [[Logiques multi-valuées]]
* [[Logique de description]]
* [[Logique et raisonnement mathématique]]
* [[Métathéorie]]

{{Palette|Logique}}
{{Portail|mathématiques|logique}}

[[Catégorie:Logique mathématique|*]]