La Logique

La logique mathématique ou méta-mathématique est une discipline des mathématiques introduite à la fin du XIXe siècle, qui s'est donné 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é.

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.

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.

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. Plus récemment la théorie homotopique des types (en) 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.

La logique linéaire

En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources.

La logique linéaire est née de l'étude d'un modèle dénotationnel des termes du lambda-calcul typé, c’est-à-dire via la correspondance de Curry-Howard, des preuves de la logique intuitionniste. C'est en effet en développant le modèle des espaces cohérents que Girard a remarqué que l'on peut y définir une notion de fonction linéaire (en un sens très proche des fonctions linéaires entre espaces vectoriels), qui permet de décomposer toute fonction de dans en une fonction non linéaire générique de dans et une fonction linéaire de dans  (  est un espace cohérent associé à dont la construction rappelle celle d'algèbre tensorielle). Cette propriété se résume par la formule fondatrice de la logique linéaire :

où le membre gauche désigne l'espace des fonctions de dans  alors que le membre droit désigne l'espace des fonctions linéaires de dans .

Quelques-unes des principales formules prouvables (par exemple en calcul des séquents) en logique linéaires. Dans ce qui suit le symbole représente l'équivalence linéaire :

Lois de De Morgan

Distributivité

Isomorphisme exponentiel

Remarquons que grâce aux lois de De Morgan, chacune de ces équivalences a une duale, par exemple la négation d'un pourquoi pas est le bien sûr de la négation, le par distribue sur le avec...

Pour finir voici une tautologie linéaire importante, qui n'est toutefois pas une équivalence :Semi-distributivité: 

Bibliographie: 

https://fr.wikipedia.org/wiki/Logique_lin%C3%A9aire