Accueil

Logique classique (et baroque)

Une version plus détaillée de cette discussion, avec théorèmes et preuves à l'appui, est disponible ici.

Introduction historique.

Au XIXème, les mathématiques deviennent de plus en plus abstraites, et avec cette abstraction viennent des inquiétudes sur les contradictions et paradoxes logiques qui peuvent résulter de situations "pathologiques":

  • En analyse réelle: dans son Cours d'Analyse, Cauchy entreprend de prouver rigoureusement les théorèmes du calcul infinitésimal de Newton et Leibniz, en utilisant une notion de quantité convergeant vers 0. Cette approche sera complétée par Bolzano, qui formalisera cette notion de convergence, et à qui l'on doit les fameuses définitions en $(\varepsilon, \delta)$. Weierstass exhibe alors des exemples pathologiques de fonctions continues mais nulle part dérivables, poussant dans ses retranchement l'intuition de fonction continue comme un graphe "lisse, que l'on peut tracer d'un seul trait". Il milite alors en faveur d'une axiomatisation de l'analyse.
  • En théorie des groupes: Abel et Galois ouvrent la voie à l'algèbre abstraite, basée sur des structures vérifiant certains axiomes, dans leur étude des solutions de polynômes. Ils montrent qu'il n'existe pas de solution générale pour les polynômes de degré plus grand que 4, et, en se basant sur leurs travaux, Lindemann prouve l'impossibilité de la quadrature du cercle à la règle et au compas tandis que Wantzel démontre l'impossibilité de la trisection d'un angle. Ces problèmes, en attente de résolution depuis l'antiquité, démontrent l'extraordinaire puissance de ce type de raisonnement, et inspirent le développement, entre autres, des espaces vectoriels, entraînant la géométrie dans les grandes dimensions et loin de l'intuition.
  • En géométrie: Depuis l'Antiquité, parmi les axiomes d'Euclide, le cinquième, qui stipule qu'étant donné une droite $D$ et un point $p$ hors de cette droite, il existe une unique droite parallèle à $D$ passant par $p$, gêne les géomètres, qui le trouvent moins "immédiat" que les autres (qui exigent des choses telles que "tous les angles droits sont égaux"). Dans les années 1820, après des siècles de tentatives pour le démontrer à partir des autres axiomes, Lobatchevski, Bolyai et Gauss mettent sur pied une géomérie cohérente, vérifiant les 4 premiers axiomes mais pas le 5ème: la géométrie hyperbolique, dans laquelle, par le point $p$ passent en fait une inifnité de droites parallèles à $D$. Plus tard, Riemann introduit la géométrie elliptique, dans laquelle par le point $p$ ne passe aucune droite parallèle à $D$.

Ainsi, au XIXème siècle, il est de bon ton pour un mathématicien de s'interroger sur les axiomes qui fondent son domaine. Et pourquoi pas, de chercher les fondements des maths en général. Avec le développement de la théorie des ensembles et l'axiomatisation de l'arithmétique par Péano, l'affaire semble en bonne voie, mais les systèmes proposés, notamment par Frege, semblaient envahis de paradoxes et de contradictions, comme celui de Russell. Les mathématiques sont alors rendues à un degré d'abstraction si stratosphérique qu'elles flirtent avec la philosophie, au point d'opposer trois écoles de pensées:

  • Les Platonistes, pour qui les objets mathématiques existent réellement en dehors de la pensée humaine. L'objectif des mathématiques est alors de découvrir des vérités sur ces objets; ceux-là, tels les elfes de la Lothlorien, vivent dans un monde enchanté où les automorphismes gambadent en liberté, et ne participent pas à la bataille entre...
  • Les Formalistes, menés par Hilbert, ancrés des deux pieds dans l'esprit de leur temps: pour eux, les mathématiques consistent avant tout en la manipulation de symboles sans signification, en partant d'axiomes tout aussi symboliques et suivant certaines règles "de déduction";
  • Enfin, les Intuitionnistes, menés par Brouwer et dont on reparlera plus loin, pour qui les mathématiques ne font sens que si on les restreint à des opérations concrètes sur des ensembles finis. La preuve, dès qu'on fait autrement, on tombe sur des paradoxes... Mais cette approche oblige à jeter, où au moins à reconsidérer avec suspicion, la plupart des avancées récentes.


Brouwer (à droite)

Hilbert.jpg
Hilbert

Or, Hilbert (et il n'est pas le seul) tient à ces avancées et aux superbes édifices mentionnés plus haut. Pour les sauver des armées du chaos de Brouwer, il met au point un plan de bataille: battre les intuitionnistes à leur propre jeu. Pour ce faire, il s'agit de prouver, en utilisant des méthodes "finies" que les intuitionnistes devraient accepter, que les mathématiques classiques sont entièrement cohérentes. Il s'agit donc de trouver le bon système d'axiomes qui permet de récupérer des monuments de l'analyse et de la géométrie, en les fondant sur des bases inattaquables, débarrassées des contradictions qui les minent.

Pendant un moment, ce plan, qui suscite l'intérêt de nombreux mathématiciens, semble en bonne voie. C'est alors qu'intervient Gödel, qui démontre ses fameux théorèmes d'incomplétude: premièrement, il existe, dans tout système formel, une phrase vraie qu'on ne peut démontrer, et deuxièmement, aucun système cohérent d'axiomes ne peut prouver sa propre cohérence. Ainsi, le projet de Hilbert est voué à l'échec. (Aparté: L'école pythagoricienne, en activité en Grèce au 6ème siècle avJC, croyait uniquement en l'existence des nombres entiers ou rationnels. Une légende (fausse) rapporte que lorsque l'un des leurs, Hippasus, démontra que la longueur de la diagonale d'un carré de côté 1, $\sqrt 2$, n'était pas rationnelle, les pythagoriciens étouffèrent l'affaire en jetant Hippasus à la mer. Vue sous cet angle, la paranoïa de Gödel, qui craignait d'être empoisonné, n'était peut-être pas tout à fait...dépourvue de fondement.).

Cependant, les mathématiques ont survécu à l'effondrement des défenses de Hilbert. Simplement, il leur a fallu descendre de leur piédestal de vérité absolue et immaculée. En se basant sur une axiomatisation de la théorie des ensembles (la plus populaire étant ZFC, pour Zermelo-Frenkel avec l'axiome du Choix), on peut rendre rigoureux tout ce qui a été obtenu auparavant (le groupe Bourbaki s'est chargé de publier une série de livres absolument imbuvables à cet effet). Il faut admettre que l'on ne peut prouver la cohérence de ce système à l'intérieur de lui-même, ce qui n'empêche pas les mathématiciens contemporains de dormir.

Au cours de cette quête épique, de nombreuses notions fascinantes ont émergé, et avec elles une réflexion approfondie (et mathématique) sur la notion même de raisonnement mathématique. Qu'est-ce qu'un système logique ? Comment séparer le 'sens' des 'symboles', la 'vérité' de la 'démonstrabilité' ? Quand peut-on garantir qu'un système d'axiome est cohérent (i.e. sans paradoxes) ou complet (i.e. on peut montrer tout ce qui est vrai) ? Comment Gödel a-t-il pu montrer qu'on ne peut pas montrer la cohérence d'un système d'axiomes à l'intérieur de lui-même ?

Le suspense est insoutenable, aussi ne le soutiendrons-nous pas:
Un système logique (classique du premier ordre) consiste en

  • un langage formel ou informel, les fameux symboles sans signification des Formalistes
  • un système de règles de déduction, qui donnent les règles pour manipuler ces symboles, et encodent la validité des arguments,
  • une sémantique, qui donne un sens aux symboles (les IA pourront peut-être s'en passer, mais les humains ont encore besoin de ces expédients, sous peine de migraine) et encode la notion de vérité. La notion que l'on verra est issue de la théorie des modèles.

L'objectif des trois premières sections sera de se donner ces trois éléments, et leurs premières propriétés. Ensuite, on s'intéressera au lien entre les déductions abstraites et la sémantique: c'est la méta-théorie. On discutera en particulier des notions de cohérence et de complétude. On parlera ensuite de considérations plus philosophiques sur les liens que ces systèmes logiques entretiennent, au delà des mathématiques, avec le "raisonnement juste" en général.

Ensuite, on ira plus loin encore dans le coupage de cheveux en quatre en étudiant les limites et paradoxes de ce type de logique. On verra qu'il existe d'autres systèmes de logique possibles permettant de les dépasser, et on reparlera en particulier de logique intuitionniste et des mathématiques constructives de Brouwer, entre autres.

Langage formel

En mathématiques, et surtout en algèbre, un moyen commode d'étudier de larges classes d'objets d'un seul coup, et sans avoir à les regarder un par un - car les mathématiciens, habitués à se colleter avec l'infini et au-delà, savent qu'ils n'auraient pas fini à temps pour le thé - est le suivant:

  • extraire les points communs à tous ces objets;
  • formaliser ces points communs en une poignée d'axiomes, c'est à dire une suite de symboles qu'on pourra ensuite interpréter de plusieurs façons;
  • travailler uniquement sur ces axiomes, sans plus se soucier des interprétations.

Ainsi, le signe $+$ s'interprète différemment si on somme des réels, des matrices ou des fonctions $\mathcal{C}^3$; mais on peut décider d'étudier tous les ensembles munis d'une "sorte d'addition", c'est à dire tous ceux tels que

$$ \begin{align} \forall x\ x+0 &= x\\ \forall x \forall y \forall z\ (x+y)+z &= x+(y+z) \\ \forall x \exists y\ x+y&=0\\ \forall x \forall y\ x+y &=y+x. \end{align} $$

Afin d'impressionner quiconque ne le serait pas par ces formules cabalistiques, on dit alors qu'on étudie les groupes abéliens.

L'étape importante, ici, a été de passer d'objets mathématiques spécifiques (l'addition des entiers) à une structure plus générale, en séparant les symboles et les formules de leur sens dans un contexte donné. Plus généralement, c'est le rôle des langages formels.

Un langage formel d'ordre 1 sur $K$, noté $\mathcal L =L1K $ est la donnée d'une collection infinie de symboles, séparés en plusieurs catégories: d'abord, une terminologie non-logique $K$, constituée des éléments suivants

  • Un ensemble de constantes, notées $\{a,a_1,b_{32},...\}$;
  • Pour chaque entier $n$, un ensemble de symboles de fonctions d'arité $n$ (c'est à dire admettant $n$ arguments). On les notera, par exemple $f^n_{1}, f^n_{2},\dots$
  • Pour chaque entier $n$, un ensemble de symboles de prédicats d'arité $n$: On les notera, par exemple $R^n_{1}, R^n_{2},\dots$.

et d'autre part des symboles logiques

  • Un ensemble dénombrable de variables $Vars=\{x,x_1,x_2,...y,y_1,\dots\}$
  • Des parenthèses: (,).
  • Le symbole d'égalité $=$.
  • Des connecteurs: $\neg, \&, \vee, \rightarrow$.
  • Deux quantificateurs: $ \forall, \exists$.

Les symboles de prédicats d'ordre 0 sont, en substance, des phrases se suffisant à elles-mêmes; ceux d'ordre 1 (prédicats monadiques) serviront à énoncer des propriétés (eg "est rouge"), ceux d'ordre 2 (prédicats binaires) énonceront des relations binaires (eg "est plus grand que"); mais cela n'interviendra que lorsqu'on se sera donné une sémantique. D'ici là, comme le nom l'indique, ce ne sont que des symboles.

Par exemple, pour étudier les groupes abéliens, on pourrait considérer le langage sur $K=\{0,+\}$. Si l'on souhaite un symbole spécial $-$ pour l'opposé d'un élément, on peut considérer $K'= \{0,+,-\}$; ou encore, on pourrait adopter une notation multiplicative: $K''=\{1, \cdot\}$. En fait, en laissant libre cours à notre créativité, on peut même faire l'étude des groupes en utilisant les symboles $K_{n'imp}= \{\clubsuit, \star\}$.

Pour parler de langage, il nous faut définir des mots; plus précisément, des éléments formés à partir du langages que l'on pourra utiliser pour désigner des objets. C'est ce que l'on appelera des termes: un terme des $L1K$ est une suite finie de symboles $t$ qui est

  • soit un symbole de constante $a$;
  • soit une variable $x$;
  • soit de la forme $f t_1\dots t_n$, où $f$ est un symbole de fonction d'arité $n$ et les $t_i$ sont des termes.

Considérons par exemple $K=\{\bar0,\bar1, \bar2,\dots,+,<\}$, un langage muni d'un symbole pour chaque entier, un symbole de fonction binaire $+$ et un symbole de prédicat binaire $<$. Alors $\bar3$, $+\bar 2 \bar 5$ et $+ \bar 4 +x \bar 1$ sont des termes. Pour améliorer la lisibilité des symboles binaires (de fonctions comme de prédicats), on adoptera, pour les deux derniers, la notation plus familière $\bar 2 + \bar 5$ et $ \bar 4 +(x+\bar 1)$.

Il nous reste à former des phrases dans notre langage; ainsi, pour reprendre l'exemple précédent, on souhaite que

$$ (x<\bar3) \vee (x=y)$$

soit une formule valide, mais pas

$$x(\rightarrow \bar3 <. $$

Pour formaliser cela, on va procéder récursivement. On commence par les formules les plus simples:

Définition: Si $V^n$ est un symbole de prédicat et $t_1...t_n$ des termes de $K$, alors $Vt_1...t_n$ est une formule atomique de $L1K$. De plus, pour tous termes $t_1$ et $t_2$, $t_1=t_2$ est une formule atomique.

Par exemple, $R^1x, R^3aab, y= f^2t_1t_2$ sont des formules atomiques. On peut alors définir récursivement les formules de via les clauses suivantes:

  • Les formules atomiques sont des formules;
  • (Négation) Si $\theta$ est une formule, $\neg \theta$ est une formule;
  • (Conjonction) Si $\theta$ et $\varphi$ sont des formules alors $(\theta \& \varphi) $ aussi;
  • (Disjonction) Si $\theta$ et $\varphi$ sont des formules alors $(\theta \vee \varphi) $ aussi;
  • (Condition) Si $\theta$ et $\varphi$ sont des formules alors $(\theta \rightarrow \varphi) $ aussi;
  • Si $\theta$ est une formule et $v$ une variable alors $\forall v \theta$ est une formule;
  • Si $\theta$ est une formule et $v$ une variable alors $\exists v \theta$ est une formule;
  • Toutes les formules se construisent ainsi.

On dispose alors d'un outil de démonstration très puissant: la récurrence sur la complexité d'une formule, c'est à dire le nombre de clauses utilisées pour l'écrire. On démontre ainsi, par exemple, que toute formule de $L1K$ a le même nombre de $($ et de $)$.

On distingue deux types de formules: les énoncés (ou propositions), auxquels on pourra, plus tard, attribuer une valeur de vérité bien définie; et les formules ouvertes, qui "dépendent" de la valeur donnée aux variables.

Posons par exemple $K_{nt}=\{0,S,+,\cdot\ ,E,<\}$ le langage de la théorie des nombres, auquel on reviendra souvent. La formule

$$\forall x \forall y (y < x) \vee ((x=y) \vee (x < y)) $$

est un énoncé (qui, avec l'interprétation adéquate, affirme que, étant donnés deux entiers, soit l'un est plus petit que l'autre, soit l'inverse, soit ils sont égaux); tandis que

$$ x < SS0 $$

est une formule ouverte: elle peut être vraie ou fausse, suivant la valeur de $x$ (en l'occurrence, dans une interprétation raisonnable, selon si $x$ est plus petit ou plus grand que 2).

Pour formaliser cela, on définit récursivement la notion de "dépendre de la valeur d'une variable":

Soit $x$ une variable et $\phi$ une formule. On dit que $x$ est libre dans $\phi$ si

  • $\phi$ est atomique et le symbole $x$ apparaît dans $\phi$;
  • $\phi$ est de la forme $\neg \alpha, \alpha\&\beta, \alpha\vee \beta$ ou $\alpha \rightarrow \beta$ et $x$ est libre dans $\alpha$ ou $\beta$;
  • $\phi$ est de la forme $\forall u \alpha$ ou $\exists u \alpha$, $x$ n'est pas $u$ et $x$ est libre dans $\alpha$.

Alors, un énoncé de $L1K$ est une formule ne contenant aucune variable libre.

Déduction

On souhaite maintenant donner un sens à la notion de preuve. Maintenant que toutes les pièces ont été définies proprement, il s'agit de définir les règles du jeu: comment passer d'une formule à une autre, d'une façon qui reflète un raisonnement; plus précisément un raisonnement mathématique, où l'on part de prémisses supposés connus et l'on souhaite en tirer une conclusion, qu'on pourra ajouter à la liste des affirmations justifiées (et donc, on pourra l'utiliser comme prémisse à son tour).

Un système déductif sur $L1K$ est donné par un ensemble de formules $\Lambda$ dont les éléments sont qualifiés d'axiomes logiques, et un ensemble de paires $(\Gamma, \phi)$ appelées règles d'inférence, où $\Gamma$ est un ensemble fini de formules et $\phi$ une formule.
Soit $\Sigma$ une collection de formules, $D=\{ \phi_1\dots,\phi_n\}$ un ensemble fini de formules. On dit que $D$ est une déduction de $\phi_n$ à partir de $\Sigma$ si, pour tout $1\leq i\leq n$,

  • soit $\phi_i \in \Lambda$
  • soit $\phi_i \in \Sigma$,
  • Soit il existe une règle d'inférence $(\Gamma, \phi_i)$ où $\Gamma \subset \{ \phi_1,\dots,\phi_{i-1}\}$.
Dans ce cas $\phi_n$ est la conclusion, les autres $\phi_i$ sont appelées des prémisses. On notera $\Sigma \vdash \phi$.

Deux remarques:

  • Différents choix pour les axiomes logiques et les règles d'inférence donnent lieu à différents types de logiques. On va ici donner le système déductif donnant lieu à la logique classique, ou de premier ordre, qui est la plus communément utilisée; on verra des alternatives ultérieurement.
  • Si $\Lambda=\emptyset$ et $\Sigma=\emptyset$, on ne peut rien déduire de $\Sigma$. Autrement dit, il nous faut au moins des axiomes logiques pour démarrer (Apparemment, cela irritait beaucoup Russell).

On introduit maintenant une règle permettant de remplacer des variables libres par des termes:
Soit $u$ un terme, $x$ une variable et $t$ un terme; on appelle $u(x|t)$ le terme défini par

  • si $u$ est une variable différente de $x$ ou une constante, alors $u(x|t) = u$;
  • si $u$ est $x$, alors $u(x|t)=t$;
  • si $u=f^n u_1\dots u_n$, alors $u(x|t)= f^nu_1(x|t)\dots u_n(x|t)$.
Soit $\phi$ une formule, $x$ une variable et $t$ un terme; on appelle $\phi(x|t)$ la formule définie par
  • Si $\phi$ est $t_1 = t_2$, $\phi(x|t)$ est $t_1(x|t)=t_2(x|t)$;
  • Si $\phi$ est de la forme $Rt_1\dots t_n$, $\phi(x|t)$ est $R t_1(x|t)\dots t_n(x|t)$;
  • si $\phi$ est $\neg \alpha$ alors $\phi(x|t)$ est $\neg \alpha(x|t)$;
  • si $\phi$ est de la forme $\alpha \vee \beta$, $\phi(x|t)$ est $\alpha(x|t) \vee \beta(x|t)$; il en va de même pour les connecteurs $\&$ et $\rightarrow$;
  • si $\phi$ est de la forme $\forall v \alpha$, $\phi(x|t)$ est $$ \begin{cases} \phi \text{ si $x$ est $v$,}\\ \forall v\ \alpha(x|t) \text{ sinon.} \end{cases} $$

Inversement, on définit la substitution d'un terme à une variable d'une façon qui ne perturbe pas les quantificateurs:

Soit $\phi$ une formule, $x$ une variable et $t$ un terme; on dit que $t$ est substituable pour $x$ dans $\phi$ si:

  • $\phi$ est atomique;
  • $\phi$ est de la forme $\neg \alpha$, $\alpha \vee \beta$, $\alpha\& \beta$, $\alpha\rightarrow \beta$ et $t$ est substituable pour $x$ dans $\alpha$ et $\beta$;
  • $\phi$ est de la forme $\forall y \ \alpha$ ou $\exists y \alpha$ et soit $x$ n'est pas libre dans $\phi$, soit $y$ n'apparaît pas dans $t$ et $t$ est sustituable à $x$ dans $\alpha$.

Ceci posé, on se donne les axiomes logiques suivants:

  • (E1) Pour tout terme $t$, $t=t$ est dans $\Lambda$.
  • (E2) Pour tout symbole de fonction $f^n$, et pour tous $n$-uplets de variables $(x_1,\dots,x_n)$ et $(y_1,\dots,y_n)$, $[(x_1=y_1) \& \dots \& (x_n = y_n)] \rightarrow f^nx_1\dots x_n = f^ny_1 \dots y_n$ est dans $\Lambda$.
  • (E3) Pour tout symbole de prédicat n-aire $R^n$, et pour tous $n$-uplets de variables $(x_1,\dots,x_n)$ et $(y_1,\dots,y_n)$, $[(x_1=y_1) \& \dots \& (x_n = y_n)] \rightarrow (R^nx_1\dots x_n \rightarrow R^ny_1 \dots y_n)$ est dans $\Lambda$.
  • ($\forall$ E) Pour toute formule $\phi$, variable $x$ et terme $t$ tel que $t$ est substituable à $x$ dans $\phi$, $\forall x\ \phi \rightarrow \phi(x|t)$ est dans $\Lambda$.
  • ($\exists$ I) Sous les mêmes hypothèses, $\phi(x|t) \rightarrow \exists x\ \phi$ est dans $\Lambda$.

On va définir les règles de déductibilité par récurrence.

  • (As) ("Rule of assumption") Si $\phi$ est dans $\Gamma$ alors $\Gamma \vdash \phi.$
  • ($\&$I) Si $\Gamma_1 \vdash \theta$ et $\Gamma_2 \vdash \psi$ alors $\Gamma_1, \Gamma_2 \vdash (\theta \& \psi).$
  • ($\&$E) Si $ \Gamma \vdash (\theta \& \psi)$, alors d'une part $\Gamma \vdash, \theta$ et d'autre part $\Gamma \vdash \psi$.
  • ($\vee$I)Si $\Gamma \vdash \theta$ alors $\Gamma \vdash (\theta \vee \psi).$ Si $\Gamma \vdash \theta$ alors $\Gamma \vdash (\psi \vee \theta).$
  • ($\vee$E) Si $\Gamma_1 \vdash (\theta \vee \psi)$, $\Gamma_2, \theta \vdash \phi$ et $\Gamma_3, \psi \vdash \phi$ alors $\Gamma_1, \Gamma_2, \Gamma_3 \vdash \phi$.
  • ($\rightarrow$I) Si $\Gamma, \theta \vdash \psi$ alors $\Gamma \vdash (\theta \rightarrow \psi)$.
  • $(\rightarrow$E) (Modus Ponens) Si $\Gamma_1 \vdash (\theta \rightarrow \psi)$ et $\Gamma_2 \vdash \theta$ alors $\Gamma_1, \Gamma_2 \vdash \psi$.
  • ($\neg$I) Si $\Gamma_1, \theta \vdash \psi$ et $\Gamma_2, \theta \vdash \neg\psi$ alors $\Gamma_1, \Gamma_2 \vdash \neg \theta$. Autrement dit, on veut que $\psi$ et $\neg \psi$ soient incompatibles. Remarquons que de cela et 1, on peut déduire $\{A\} \vdash \neg\neg A$, mais pas l'inverse. Pour cela, on introduit la règle d'élimination des double négation. Cette règle est l'une des nombreuses choses que Brouwer et son armée d'Intuitionnistes rejettent.
  • ($\neg$E) Si $\Gamma \vdash \neg\neg \theta$ alors $\Gamma \vdash \theta$.
  • De là, on peut montrer qu'on obtient la loi du tiers exclus $\vdash (A \vee \neg A)$.
  • (EFQ) (Ex falso quodlibet) Si $\Gamma_1 \vdash \theta$ et $\Gamma_2 \vdash \neg \theta$ alors pour toute phrase $\psi$, $\Gamma_1, \Gamma_2 \vdash \psi$. Cette règle, en substance, énonce que d'un ensemble de formules contradictoires, on peut déduire n'importe quoi. Quoique très commode, cette règle peu intuitive est remise en cause dans certains systèmes logiques, notamment la logique de la pertinence ("relevance logic").
  • ($\forall$I) Pour tout terme $t$, si $\Gamma \vdash \theta(v|t) $, alors du moment que $t$ n'est pas dans $\Gamma$ ou $\theta$, on a $\Gamma \vdash \forall v \theta$.
  • C'est la base de la notion d'élément arbitraire en maths.
  • ($\exists$E) Pour tout terme $t$, si $\Gamma_1 \vdash \exists v \theta$ et $\Gamma_2, \theta(v|t) \vdash \phi$, alors $\Gamma_1, \Gamma_2 \vdash \phi$, pourvu que $t$ n'apparaisse pas dans $\phi, \Gamma_2$ ou $\theta$.
  • C'est là aussi une inférence commune lorsque l'on traite d'objets arbitraires en maths.
  • (TAF) Ce sont les seules manières d'obtenir des déductions.

Deux remarques:

  • Dans tous ces cas, on obtient des paires $(\Gamma, \phi)$ que l'on ajoute aux règles d'inférence. Une façon alternative de procéder consiste à définir une notion de conséquence propositionnelle à partir de tables de vérités pour les différents connecteurs.
  • Comme l'indique l'indexation des règles, chaque connecteur et quantificateur donne lieu à deux règles: une qui introduit le symbole (I) et une qui l'élimine (E).

Comme précédemment, la dernière règle ("That's all folks") permet de raisonner par récurrence sur les règles utilisées pour obtenir un argument. Si une propriété est vérifiée par les arguments dont la conclusion est un axiome, ou obtenue par la règle (As), et est préservée par toutes les autres règles, alors tout argument possède cette propriété. On montre ainsi, par récurrence sur le nombre de règles utilisées, que si $\Gamma_1 \vdash \phi$ et $\Gamma_1 \subset \Gamma_2$, alors $\Gamma_2 \vdash \phi$.

Ce lemme, utilisé constamment en maths, dit qu'en ajoutant des hypothèses, on peut prouver au moins autant de choses qu'avant. Mon chef de thèse appelait cela QPPPM (Qui Peut le Plus Peut le Moins). On prouve ce résultat par récurrence sur le nombre $n > 0$ de règles d'inférence utilisées pour obtenir $\Gamma_1 \vdash \phi$ (voir le pdf pour plus de détails).

De la règle (TAF), on déduit que $\Gamma \vdash \phi$ si, et seulement si il existe un sous ensemble fini $\Gamma' \subset \Gamma$ tel que $\Gamma' \vdash \phi$. Autrement dit, toute déduction est établie en un nombre fini d'étapes.

On peut en fait déduire ex falso quolibet du reste du système: Supposons que $\Gamma_1 \vdash \phi$ et $\Gamma_2 \vdash \neg \phi$. Alors par le lemme QPPPM, on peut rajouter des hypothèses: $\Gamma_1, \neg \psi \vdash \phi$ et $\Gamma_2, \neg \psi \vdash \neg\phi$. En utilisant ($\neg$I), on obtient donc $\Gamma_1, \Gamma_2 \vdash \neg \neg \psi$ et, par élimination des doubles négations, $\Gamma_1, \Gamma_2 \vdash \psi$; et ce, pour n'importe quelle phrase $\psi$. C'est probablement ce qui a poussé certain logiciens à mettre en place des systèmes sans élimination des doubles négations.

Par la même méthode de récurrence sur le nombre d'étapes, on obtient aussi que si $\Gamma_1 \vdash \psi$ et $\Gamma_2, \psi \vdash \theta$ alors $\Gamma_1, \Gamma_2 \vdash \theta$.

Ce théorème nous permet d'enchaîner les inférences, et notamment d'utiliser des théorèmes déjà démontrés pour en démontrer de nouveaux. Dans certains systèmes logiques, c'est un résultat profond, et dans d'autres, il n'est carrément pas valide. Le système déductif introduit ici est en partie conçu pour obtenir facilement cette propriété.

Un peu de jargon:

  • Si $\Gamma \vdash \theta$, on dit que $\theta$ est une conséquence déductive de $\Gamma$, et que l'argument $\langle \Gamma, \theta \rangle$ est dit valide.
  • Un ensemble de formules $\Gamma$ est cohérent s'il n'existe pas d'énoncé $\theta$ tel que $\Gamma\vdash \theta$ et $\Gamma \vdash \neg \theta$. Donc, par (EFQ), $\Gamma$ est cohérente s'il y a au moins une formule $\theta$ telle qu'on n'ait pas $\Gamma \vdash \theta$.
  • Une collection de phrases $\Gamma$ est dit maximalement cohérent si $\Gamma$ est cohérent et si l'ajout de toute phrase qui n'est pas déjà dans $\Gamma$ le rend incohérent. Si $\Gamma$ est maximalement cohérent, alors $\Gamma \vdash \theta$ ssi $\theta$ est dans $\Gamma$. Le lemme de Lindenbaum montre que tout ensemble cohérent est contenu dans un ensemble maximalement cohérent.

Sémantique.

On s'intéresse (enfin!) au sens que l'on peut donner aux symboles du langage formel. Considérons par exemple le langage de la théorie des nombres introduit plus haut, le langage de premier ordre basé sur

$$ K_{nt}=\{0,S,+,\cdot\ ,E,<\}. $$

La question est de savoir quelle interprétation on peut donner à ces symboles. Puisqu'on a vendu la mèche en l'appelant "langage de la théorie des nombres", il semble qu'il n'y ait pas de question à se poser: les variables parcourent l'ensemble $\mathbb N$, $0$ devrait être l'entier $0$, $S$ la fonction suivant qui à un entier $n$ associe $n+1$, la fonction binaire $+$ doit représenter l'addition, $\cdot$ la multiplication, $E$ la mise en exposant, etc. Il s'agit là d'une interprétation, certes particulièrement raisonnable.

Mais on peut aussi interpréter ces symboles comme représentant l'arithmétique modulo 2: les variables vivent dans $\{0,1\}$, $S(0)=1$ et $S(1)=0$, $+$ et $\cdot$ sont l'addition et la multiplication modulo 2, etc.

Si l'on se sent d'humeur taquine, on peut considérer que ce langage porte sur les objets $\{$ Motörhead, Papaye, Matrix Reloaded $\}$, avec $0$ interprété comme Papaye, $S$ la fonction constante égale à Motörhead, $<$ l'égalité et $+$ et $\cdot$ les fonctions constantes égales respectivement à Matrix Reloaded et Papaye.

Le choix de l'une ou l'autre interprétation a évidemment un impact sur la vérité d'énoncés tels que $\forall x\ \neg Sx=0.$

Ainsi, dans la première interprétation, cet énoncé signifie qu'aucun entier ne vient avant 0, et est donc vrai. Dans la deuxième, il est faux puisque $S(1)= 0$. Dans la dernière, il énonce que Mötorhead n'est pas une papaye, ce qui est aussi vrai (à ma connaissance).

Définition: Soit $K$ un ensemble de terminologie non-logique. Une interprétation $M$ du langage $L1K$ est la donnée d'un ensemble non-vide $d$ appelé domaine, ou univers du discours, ainsi que:

  • pour chaque constante $c$ de $K$,un élément $c^M$ de $d$;
  • pour chaque symbole de fonction $f^n$, une fonction $f^M: d^n \rightarrow d$;
  • pour chaque 0-symbole de prédicat $P^0$, une valeur de vérité;
  • pour chaque $n$-symbole de prédicat $P^n$, un sous-ensemble $P^M$ de $d^n$.

Le domaine a pour fonction, en gros, de déterminer de quoi parle le langage, quels sont les objets dont il parle. Ce sera l'habitat naturel des variables. Ainsi, on peut noter:

$$ \mathfrak{N}=(d=\mathbb N, 0, S, +,\cdot, E, <) $$

l'interprétation "naturelle" du langage de la théorie des nombres $L1K_{nt}$.

Exemple: Structures de Henkin
Considérons un langage de premier ordre $\mathcal L$ basé sur la terminologie non-logique $K=\{0,f,g,R\}$, où $0$ est une constante, $f$ une fonction unitaire, $g$ une fonction binaire, et $R$ un symbole de prédicat d'arité 3. On considère l'interprétation $M$ dont le domaine est donné par $d=\{$ termes de $\mathcal L$ sans variable$\}$ et telle que $$ \begin{align*} 0^M &=0 \in d\\ f^M: t \in d & \mapsto ft \in d \\ g^M:(t,s) \in d^2&\mapsto fts \in d \end{align*} $$ et on prend pour $R^M$ un sous-ensemble quelconque de $d^3$.
Cette interprétation, construite à partir du langage lui-même, peut se généraliser à n'importe quel langage du premier ordre $L1K$. On appelle cela des interprétations de Henkin; elles joueront un rôle-clé dans la preuve du théorème de complétude.

On dit que $s$ est un assignement des variables sur une interprétation $M$, si $s$ est une fonction des variables vers le domaine $d$ de $M$.
A partir un assignement donné $s$, on construit un assignment de termes $\bar s$, qui est une fonction de l'ensemble des termes du langage dans $d$ défini récursivement par

  • si $t$ est une variable, $\bar s(t) = s(t);$
  • si $t$ est une constante $c$, $\bar s(t) = c^M$;
  • si $t$ est $f^nt_1\dots t_n$, $\bar s(t) = f^M(\bar s(t_1),\dots,\bar s(t_n))$.

Puisque dans le cas général, la vérité ou la fausseté d'un énoncé dépend de l'interprétation, on va définir la "vérité"" relativement à un modèle donné. Soit $\phi$ une formule de $L1K$, $M$ une interprétation et $s$ un assignement de variables sur $M$. On va définir la relation $M$ satisfait $\phi$ sous l'assignement $s$, noté $M,s \models \phi$, de façon récursive sur la complexité de $\phi$.

  • Si $t_1$ et $t_2$ sont des termes, $M,s \models t_1 = t_2$ si $\bar s(t_1)=\bar s(t_2)$ (autrement dit, si les deux termes désignent la même chose.)
  • SI $P^0$ est une lettre de prédicat à 0 places,$M,s \models P$ ssi $P^M$ est "vrai".
  • Si $S^n$ est un symbole de prédicat $n$-aire et $t_1,\dots, t_n$ des termes, alors $M,s \models St_1\dots t_n$ ssi $(\bar s(t_1), \dots, \bar s(t_n)) \in S^M \subset d^n$.
  • $M,s \models \neg \theta$ ssi on n'a pas $M,s \models \theta$.
  • $M,s \models (\theta \& \psi)$ (resp, $M,s \models (\theta \vee \psi)$) ssi on a $M,s \models \theta $ et (resp ou) $M,s \models \psi$.
  • $M,s \models (\theta \rightarrow \psi)$ ssi on n'a pas $M,s \models \theta$, ou si $M,s \models \psi$.
  • $M,s \models \forall v \theta$ ssi $M,s' \models \theta$ pour tout assignement $s'$ identique à $s$ sauf peut-être en $v$.
  • $M,s \models \exists v \theta$ ssi $M, s' \models \theta$ pour au moins un assignement $s'$ identique à $s$ sauf peut-être en $v$.

Sous ces règles de satisfaction, l'interprétation donne donc le sens qu'on attend aux connecteurs et quantificateurs logiques: $\&$ encode "et", $\vee$ encode "ou",etc.

Remarquons que $\rightarrow$ encore l'implication logique: on considère que $P$ implique $Q$ si $P$ est faux, ou alors si $Q$ est vrai. Cette définition ne fait pas consensus, en particulier parce qu'elle n'implique pas de relation particulière entre $P$ et $Q$. Par exemple (dans l'interprétation habituelle du langage !) on a ainsi "Toutes les girafes sont bleues implique que la Terre est ronde". C'est à ces "paradoxes de l'implication" que la "logique de la pertinence" (relevance logic) tente de répondre.

  • Soit $M$ une interprétation du langage $L1K$ et $\theta$ une formule. Si pour tout assignement de variables $s$, $M,s \models \theta$, on dit que $M$ est un modèle de $\theta$, et on note $M\models \theta$.
  • Si de plus $\theta$ est un énoncé, alors $M\models \theta$ ssi $M,s \models \theta$ pour au moins un assignement $s$. On dit dans ce cas que l'énoncé est vrai dans $M$.

Considérons par exemple l'interprétation standard de l'arithmétique: $$ \mathfrak{N}=(\mathbb N, 0, S, +,\cdot, E, <) $$ accmpagné de l'assignement de variables $$ \begin{align*} s: \text{Vars} = \{v_0, v_1,\dots\}&\rightarrow \mathbb N\\ v_i \mapsto 2i \end{align*} $$ On considère la formule $\phi(v_1):(v_1+v_1=SSSS0)$. Montrons que $\mathfrak{N}, s \models \phi$. En effet, on a d'une part $$ \begin{align*} \bar s(v_1 + v_1)&= +^\mathfrak{N}(s(v_1), s(v_1))\\ &=+^\mathfrak{N}(2, 2)\\ &=4, \end{align*} $$ et d'autre part $$ \begin{align*} \bar s(SSSS0)&=S^\mathfrak{N}(S^\mathfrak{N}(S^\mathfrak{N}(S^\mathfrak{N}(0^\mathfrak{N}))))\\ &=4. \end{align*} $$ Dans cette interprétation, les termes $v_1+v_1$ et $SSSS0$ ont le même sens: donc $\mathfrak{N}, s \models \phi$.

Considérons maintenant un énoncé: soit $\sigma$ l'énoncé $$ \forall v_1 \exists v_2(v_1=v_2+v_2) $$ qui dit que tout nombre est pair. Au risque d'enfoncer des portes ouvertes, montrons que cet énoncé est faux dans l'interprétation standard de l'arithmétique.
D'après nos règles de satisfaction, on a $\mathfrak N \models \sigma$ ssi $\mathfrak N,s \models \sigma$ pour n'importe quel assignement $s$. Soit donc $s$ un assignement quelconque. Alors $\mathfrak N,s \models \sigma$, noté aussi $\mathfrak N \models \sigma[s]$, ssi $$ \begin{align*} &\mathfrak N \models (\forall v_1 \exists v_2(v_1=v_2+v_2))[s] \\ \text{Pour tout $a$ dans le domaine } \mathbb N,\ &\mathfrak N \models \exists v_2(v_1=v_2+v_2))[s(v_1|a)] \\ \text{Pour tout $a$ dans le domaine, il existe $b$ tel que } &\mathfrak N \models (v_1=v_2+v_2))[s(v_1|a)(v_2|b)] \\ \end{align*} $$ Clairement, pour $a=3$, on ne peut pas trouver de tel entier $b$; ainsi $\mathfrak N \nvDash \sigma$.

On dit qu'une déduction $(\Gamma, \theta)$, où $\Gamma$ est l'ensemble des prémisses et $\theta$ la conclusion, est valide, ce que l'on note $\Gamma \models \theta$, si pour toute interprétation $M$ du langage telle que $M \models \psi$ pour tout $\psi$ dans $\Gamma$, alors $M \models \theta$.
Une formule $\phi$ est valide si $\emptyset \models \phi$.
Un énoncé $\theta$ est satisfaisable s'il existe une interprétation $M$ telle que $M\models \theta$. On étend cette notion à un ensemble de phrases $\Gamma$, et on dit alors que $M$ est un modèle de $\Gamma$.

Ainsi, un argument est valide s'il est impossible pour ses prémisses d'être tous vrais et la conclusion fausse. C'est la contrepartie sémantique de la déductibilité. Comme on le verra, la satisfaisabilité est la contrepartie sémantique de la cohérence.

Quelques exemples:

  1. On sait déjà que la formule "$x=x$"" est valide. Montrons que ni $x=y$ ni $\neg(x=y)$ ne sont valides. Soit $M$ une interprétation du langage de domaine $d=\mathbb N$. Soit $s_0$ un assignement de variables tel que $s_0(x)=342$, $s_0(y) = 56$. Alors on n'a pas $M,s \models x=y$ pour tout assignement $s$ ($s_0$ est un contre exemple); donc $M \nvDash x=y$. On obtient $M \nvDash \neg(x=y)$ en utilisant cette fois un assignement $s_1$ tel que $s_1(x)=42$, $s_1(y)=42$.
    Remarquons que cela dénote une différence fondamentale entre les notions de validité et de déductibilité: on n'a pas ici de tiers exclus" qui marche dans toutes les interprétations.
  2. Considérons un langage sur $K=\{P\}$, où $P$ est un symbole de prédicat binaire, et montrons que l'énoncé $\sigma$ donné par $$ (\exists y\ \forall\ x\ Pxy) \rightarrow ( \forall\ x\ \exists y\ Pxy) $$ est valide. Soit $M$ une interprétation quelconque de domaine $d$, $s: \text{Vars} \rightarrow d$ un assignement quelconque. Il s'agit de montrer que $M,s \models \sigma$.
    D'après la règle sur l'interprétation de $\rightarrow$, si $M,s \nvDash \exists y\ \forall\ x\ Pxy$, alors $M,s \models \sigma$. Supposons donc que $M,s \models \exists y\ \forall\ x\ Pxy$. Cela signifie qu'il y a un élément $a\in d$ tel que $M \models(\forall\ x\ Pxy)[s(y|a)]$, c'està dire qu'il y a un élément fixe $a \in d$ tel que pour tout $b\in d$, $M \models (Pxy)[s(y|a)(x|b)]$. En d'autres termes, pour tout $b\in d$, $(b,a)\in P^M \subset d^2$.
    Il s'agit de montrer $M,s \nvDash \forall\ x\ \exists y\ Pxy$, autrement dit, que pour un élément quelconque $c\in d$, $M \nvDash (\exists y\ Pxy)[s(x|c)]$. Il s'agit donc de trouver $e\in d$ tel que $M \nvDash (Pxy)[s(x|c)(y|e)]$, c'est à dire tel que $(c,e)\in P^M$. Or, on sait que $(c,a) \in P^M$. On a donc bien $M,s \nvDash \forall\ x\ \exists y\ Pxy$.
    Ceci étant vrai pour toute interprétation $M$ et assignement associé $s$, on a bien obtenu que la formule $\sigma$ est valide.

Méta-théorie

Correction. Les systèmes sémantique et déductifs introduits dans les deux précédentes questions ont été construits pour refléter les règles d'argumentation du langage naturel, de deux façons différentes: d'une part le système déductif donne des règles pour passer d'un assortiment de symboles à un autre, sans s'occuper de ce que cela signifie; d'autre part, le système sémantique traduit les symboles logiques (connecteurs, égalité, quantificateurs) en leur attribuant le sens le plus...sensé.

Etant donné un ensemble de formules $\Gamma$, on peut en tirer, d'une part, l'ensemble des formules que l'on peut déduire de $\Gamma$ dans notre système déductif, noté Thm$(\Gamma) = \{\phi | \Gamma \vdash \phi\}$ ; d'autre part, l'ensemble $V = \{\phi | \Gamma \models \phi\}$ des déductions valides dans notre système sémantique.

On s'attend donc à ce que les notions de déductibilité et de validité ne soient pas complètement sans rapport. En premier lieu, on aimerait ne pouvoir prouver que des choses vraies; c'est ce qu'on appelle la correction d'un système logique. Et de fait, on a:

Théorème : Correction
Pour tout énoncé $\theta$ et collection de formules $\Gamma$, si $\Gamma \vdash \theta$, alors $\Gamma \models \theta$. Autrement dit, Thm$(\Sigma) \subset V$.
Par conséquent, Si une collection de phrases $\Gamma$ est satisfaisable, alors $\Gamma$ est cohérente.

On ne change pas une équipe qui gagne, et donc, ce résultat se prouve par récurrence sur le nombre $n$ d'étapes nécessaires à pour établir $\Gamma \vdash \theta$. Voir ici pour les détails.

Complétude: On pourrait avoir l'impression que la réciproque de ce corollaire est tout aussi facile à établir; c'est à dire, que pour tout ensemble d'énoncés qui ne raconte pas n'importe quoi, on peut trouver une interprétation qui les rende vrais. C'est ce que l'on appelle la complétude d'un système logique: si $\Gamma \models \phi$ alors $\Gamma \vdash \phi$. Or, en y réfléchissant, ce n'est pas si facile: il se pourrait tout à fait qu'on manque de règles d'inférence pour établir tous les arguments valides (En fait, c'est justement l'objet des théorèmes d'incomplétude mentionnés en introduction, les armes de destruction massive avec lesquelles Gödel a réduit en cendres les espoirs de Hilbert). Il s'agit, en fait, de résultats profonds de logique mathématique.

Théorème de complétude de Gödel
Soit $\Gamma$ une collection de phrases. Si $\Gamma$ est cohérente, alors $\Gamma$ est satisfaisable.
Ainsi, pour chaque phrase $\theta$ et collection de phrase $\Gamma$, si $\Gamma \models \theta$, alors $\Gamma\vdash \theta$.

Idée de preuve: Soit $\Gamma$ une collection cohérente d'énoncés, on cherche à construire une interprétation $M$ qui satisfasse $\Gamma$. Pour cela, on va s'inspirer des interprétations de Henkin introduite plus haut. On va commencer par étendre le langage en lui ajoutant des constantes qui pourraient manquer, et, dans ce nouveau langage $\mathcal L'$, former une famille maximalement cohérente $\Gamma'' \supseteq \Gamma$. Enfin, suivant le modèle des structures de Henkin, on construira une interprétation $M$ du langage étendu telle que $M \models \sigma$ ssi $\sigma\in \Gamma''$. Une fois encore, les détails sont ici.

Pourquoi étendre le langage $L$ ? Tout d'abord, il se pourrait que $K$ ne contienne aucune constante, donc que le domaine $d$ des termes sans variables soit vide. D'autres $K$ pathologiques pourraient ne contenir qu'une seule constante $c$ et un symbole de prédicat unitaire $P$; alors $\Gamma=\{\exists x Px, \neg P(c)\}$ est cohérente, mais aucune interprétation de domaine $\{c\}$ ne peur modéliser $\Gamma$, et on ne peut pas imiter les structures de Henkin pour conclure.

Les théorèmes de correction et de complétude assurent l'équivalence de la déductibilité et de la validité pour les arguments, et de la cohérence avec la satisfaisabilité pour les collections de phrases. On peut ainsi passer des aspects issus de la théorie des modèles à ceux issus de la théorie de la preuve.

Une autre méta-propriété d'intérêt est la compacité, qui se déduit facilement des théorèmes précédents:

Théorème de compacité
Une collection de phrase $\Gamma$ est satisfaisable ssi tout sous-ensemble fini de $\Gamma$ l'est.

Preuve: Si $M$ satisfait chaque membre de $\Gamma$, alors $M$ satisfait tout sous ensemble fini. Réciproquement, su pposons que $M$ ne soit pas satisfaisable. Alors un certain sous-ensemble fini ne l'est pas: en effet, par complétude, $\Gamma$ est incohérent, donc un sous-ensemble fini est incohérent par le théorème de finitude, et par le corollaire du théorème de correction, ce sous ensemble n'est pas satisfaisable.

C'est cette notion de compacité qui va mettre en lumière certaines limites de la logique de premier ordre:

  • Modèles non-standard de l'arithmétique
    Comme l'introduction le laisse entendre, une activité très à la mode parmi les mathématiciens du début du 20ème siècle est d'axiomatiser toutes sortes de domaines. Dans le cas de l'arithmétique, on a une interprétation préférée $\mathfrak N$ du langage $L_{NT}$ de la théorie des nombres, et on se demande s'il existe un ensemble d'axiomes qui caractérisent cette interprétation.
    En d'autres termes, existe-t-il un ensemble d'énoncés $\Sigma$ tel que $\mathfrak N \models \Sigma$ et si $M \models \Sigma$, alors $M$ est "semblable à $\mathfrak N$? Plus rigoureusement, on demande que $M$ soit isomorphe à $\mathfrak N$, c'est à dire, qu'il existe une bijection $i:d_M \rightarrow d_\mathfrak{N}$ telle que $$ \begin{align*} i(c^M)&=c^{\mathfrak N} \text{ pour toute constante $c$}\\ i(f^M(a_1,\dots,a_n))&=f^{\mathfrak N} (i(a_1),\dots,i(a_n))\\ (a_1,\dots,a_n)\in R^M &\text{ ssi } (i(a_1), \dots,i(a_n)) \in R^\mathfrak{N}. \end{align*} $$ Hélas, on ne peut trouver de tels axiomes. En effet, si $\Sigma$ est un candidat, considérons le langage étendu $\mathcal L = L_{NT} \cup \{c\}$ et la collection d'énoncés $$ \Theta = \Sigma \cup \{0 < c, S0 < c,SS0 < c\dots\}. $$ Montrons que $\Theta$ est satisfaisable. Si $\Theta_0$ est un sous-ensemble fini de $\Theta$, alors il existe un $n$ tel que $\Theta_0 \subset \Sigma \cup \{0< c, S0< c,SS0< c\dots, \underbrace{SS\dots S}_{n \text{ fois }}0< c\} $. Cet ensemble d'énoncés a un modèle $\mathfrak N_n$, dont le domaine est $\mathbb N$, les opérations ont leur sens usuel et $c^{\mathfrak N_n}=n+1$. Par compacité, $\Theta$ a un modèle $M'$, que l'on peut restreindre en une interprétation de $L_{NT}$ en "oubliant" $c^{M'}$; mais cette interprétation n'est pas isomorphe à $\mathfrak N$, puisqu'elle comporte un élément en relation "<"" avec une infinité d'éléments du domaine, ce qui n'est pas le cas de $\mathfrak{N}$. $M$ est un modèle non-standard de l'arithmétique. En prenant (n'y allons pas de main morte) $\Sigma=$Th$(\mathfrak{N}) = \{\phi\ |\ \mathfrak{N} \models \phi\}$ (ce que l'on appelle la théorie de $\mathfrak N$), on obtient néanmoins que Th$(M)$ = Th$(\mathfrak N)$. Autrement dit, le langage $L_{NT}$ ne peut exprimer d'énoncé vrai dans $\mathfrak{N}$ et faux dans $M$, ou le contraire. Cela est dû au fait que $L_{NT}$ n'est pas équipé pour "parler" de l'élément non-standard $c^{M'}$, qui est pourtant bien là!
  • Analyse non-standard. Avant que Cauchy ne tente d'assainir le calcul différentiel et intégral à grand renfort de $\varepsilon$ et $\delta$, Newton et Leibniz ne se posaient pas tant de questions et travaillaient avec de mystérieuses quantités ``infinitésimales'', plus petites que tout réel sans pour autant être tout à fait nulles. Les fantômes de ces quantités hantent les manuels sous forme de $dx$ et de $dt$ privés de leur sens sulfureux.
    La rigueur est venue au prix de contorsions et de calculs de limites que d'aucuns, dont A. Robinson, trouvent inconfortables. Il développa donc un cadre logiquement cohérent qui autorise les infinitésimaux. Pour cela, il construisit un langage $L_\mathbb R$ qui comporte une constante $\dot r$ pour chaque réel $r$, un symbole de fonction $\dot f$ pour toute fonction $f: \mathbb R^n \rightarrow \mathbb R$, et un $n$-prédicat $\dot R$ pour chaque $n-$relation $R$ sur $\mathbb R^n$. Un gros langage, donc. Il en construit ensuite une interprétation $\mathfrak R$ de domaine $\mathbb R$ qui interprète chaque symbole comme le réel/fonction/relation qui lui a donné naissance (A ce stade, on a l'impression de tourner en rond, mais patience). On étend alors le langage en $L' = L_\mathbb R \cup \{c\}$, et on considère la collection d'énoncés $$ \Theta = \text{Th}(\mathfrak R) \cup \{\dot 0 \dot < c\} \cup \{c \dot < \dot r | r \in \mathbb R, r>0\}. $$ Par la compacité, on montre que $\Theta$ admet un modèle $A$, dans lequel $c$ joue le rôle d'un infinitésimal. Le domaine $d_A$ se décompose en trois types d'éléments: des réels standards, qui donnent une copie de $\mathbb R$ dans $d_A$; des éléments purement non-standard, comme $c^A$, et des éléments "hybrides" preovenant de l'interprétation de, par exemple $\dot{42}\dot + c$. On peut alors faire de l'analyse en utilisant $c$; ainsi, par exemple, on peut définir $f'(a)$ comme la partie standard de $\dfrac{f(a+c)-f(a)}{c}$.
    Tout ceci peut sembler capillotracté, mais c'est en fait un domaine fructueux, qui a permis de prouver de nouveaux résultats en analyse !

La seule bonne logique ?

Du fait de ses règles simples et intuitives et de ses bonnes propriétés de complétude et de correction, la logique classique a souvent été considérée comme la meilleure pour guider le raisonnement.

On en a cependant vu certaines limites, et d'autres types de logiques ont été défendues, telles que la logique intuitionniste, ou des extensions permettant d'encoder la dénombrabilité. Un mouvement de pluralisme logique défend que plusieurs logiques peuvent, sans contradiction, guider le raisonnement.

Plus en profondeur, la question de savoir comment les notions mathématiques de validité logique, et autres propriétés des langages formels, sont liées aux notions épistémologiques de "raisonnement correct" est une instance du problème plus large de l'application des mathématiques à une réalité non-mathématique.

Un aspect de ce questionnement est le rapport entre langages formels et langages naturels. A ce sujet, plusieurs vues s'affrontent.

  • La première (Montague, Lycan) défend que les langages formels possèdent des propriétés de certains fragments du langage naturel. Les phrases déclaratives du langage naturels auraient ainsi une forme logique sous-jacente, montrées par les formules du langage formel. Ainsi, les composantes d'une logique fournissent la structure sous-jacente au raisonnement correct.
  • Une autre vue (Frege, Laibniz) soutient qu'en raison de leurs multiples ambiguïtés, les langages naturels devraient être remplacés par les langages formels pour permettre le raisonnement. Dans ce cas, les propriétés de déductibilité et de validité sont des idéalisations du raisonnement correct en langage naturel.
  • On peut aussi remarquer que mathématiciens et philosophes raisonnenet en langage naturel et recourent à des formuels du langage formel pour clarifier leur propos, le faisant apparaître comme un ajout au langage naturel. Que disent alors les notions précises de validité du langage formel sur le raisonnement en général ?
  • Enfin (Corcoran, Shapiro), le langage formel peut être interprété comme un modèle mathématique du langage naturel: il idéalise certains aspects, en ignore ou en simplifie d'autres. Ainsi, les arguments valides sont des modèles de raisonnement correct.

Logiques baroques

Jusque-là, on s'est intéressé à la logique du premier ordre, et, à ce stade, elle semble à la fois

  • enfoncer des portes ouvertes
  • avoir d'excellentes propriétés: correction, complétude; et plus philosophiquement, formaliser efficacement le raisonnement rationnel
  • poser un certain nombre de paradoxes et limitations.
  • Ce sont ces paradoxes et limitations qui ont donné lieu à toutes sortes de logiques "alternatives", visant à y répondre. Mentionnons en deux:

    Logique du second ordre: La logique du second ordre généralise celle du premier ordre, en autorisant des énoncés portant non seulement sur les variables $x$, mais aussi sur les propriétés du premier ordre $X$. L'application la plus immédiate est de formaliser le principe d'induction en arithmétique: si une propriété est vraie pour 0, et "passe" d'un entier à son successeur, alors elle doit être vraie pour tout entier: en logique du second ordre, où $X$ est une variable parcourant l'ensemble des propriétés, ceci s'écrit $$ \forall X [(X(0)\ \&\ \forall y\,(X(y) \rightarrow X(Sy))) \rightarrow \forall x X(x)]. $$ Si on ajoute à cet énoncé les axiomes $\forall x\, \neg Sx=0$ et $\forall x\, \forall y\ (Sx =Sy \rightarrow x=y)$, alors cet ensemble d'axiomes caractérise $\mathfrak N$, ce qu'on ne pouvait pas faire avec des axiomes du premier ordre.

    Un autre exemple est la propriété de complétude de l'ordre sur les réels: $$ \forall X\, [(\exists y\, X(y) \& \exists z\, \forall y (X(y) \rightarrow y \leq z))\rightarrow \exists z\,\forall y\,(\exists u \, X(u) \& y\leq u)\vee z \leq y] $$ Si l'on ajoute cet énoncé aux axiomes du premier ordre définissant les corps ordonnés, alors ceci caractérise les réels dans l'interprétation usuelle, à isomorphisme près.

    Logique intuitionniste: La logique intuitionniste, en gros, rejette la propriété d'élimination des doubles négations ($\neg$E) et surtout le principe du tiers exclus $A \vee \neg A$ qui en découle (Mick Jagger est un intuitionniste célèbre: de "I can't get no satisfaction", on ne peut pas déduire qu'il est satisfait). Il peut sembler absurde, à première vue, de rejeter des règles de raisonnement si évidentes. Ce qui froisse les intuitionnistes, c'est que ces règles autorisent le raisonnement par l'absurde: pour montrer qu'une propriété $P$ est vraie, par élimination des doubles négations, il suffit de montrer qu'elle n'est pas pas fausse, ou encore que si elle n'est pas fausse, on a une contradiction.

    On peut ainsi montrer que des objets mathématiques existent en montrant qu'on serait bien embêtés, logiquement parlant, s'ils n'existaient pas, ce qui, du point de vue de Brouwer, n'est pas très...constructif. Hilbert, à l'opposé du ring, considérait que "priver le mathématicien du principe du tiers exclus serait comme de priver l'astronome de son télescope, ou le boxeur de ses poings". La logique intuitionniste, obtenue en "jetant" toutes les règles de déduction qui pourraient nous amener au maudit tiers exclus, sont à la base des mathématiques dites constructives, dont le slogan est qu'une preuve de l'existence d'un objet doit donner une façon d'obtenir cet objet.

    Plus de détails sur le type de maths qui résulte de cette privation de poings de boxeur par ici.