Cours1 : A propos de OU
La logique dominante
Les mathématiques usuelles sont fondées sur ce qu'on peut appeler la logique dominante, qui comporte deux niveaux.
Le premier niveau est purement logique et constitué par la logique classique du premier ordre. Avec cette logique, on peut faire des théories, comme par exemple la théorie des groupes.
Il faut bien voir au passage qu'en théorie des groupes, on ne parle que d'un groupe à la fois, on ne peut par exemple pas parler des morphismes entre deux groupes.
Au deuxième niveau il y a le choix de la théorie, et le choix dominant est la théorie des ensembles ZF, Z pour Zermelo, et F pour Frankel, ou sa variante ZFC, avec C pour l'axiome du choix.
Les logiciens envisagent des tas d'autres formalismes comme par exemple la logique d'ordre supérieur, mais les autres mathématiciens ne se sentent pas concernés.
Le nom "théorie des ensembles" est un peu trompeur. Ce qu'on appelle la théorie DES groupes parle d'UN groupe, qui est un peu n'importe quel groupe, et de ses éventuellement nombreux éléments.
De ce point de vue, la théorie des ensembles parle d'un "ensemble de tous les ensembles", qui n'est pas un ensemble, et qui, si c'en était un, ne serait sûrement pas n'importe quel ensemble, ce serait ce qu'on appelle un univers, c'est-à-dire un ensemble stable par toutes sortes de constructions genre limites et colimites.
Donc si on parle de théorie DES groupes, il faut parler de théories des classes, ou des univers, plutôt que de théorie des ensembles.
La vérité dans la logique dominante
Le théorème d'incomplétude: Gödel dit que dans cette théorie ZF ou ZFC (et dans beaucoup d'autres), on peut numéroter les énoncés de façon que l'énoncé 3 énonce que "l'énoncé 3 n'est pas démontrable", et observe que ni cet énoncé ni son contraire ne sauraient avoir de preuve (si la théorie est cohérente). Il y a donc des énoncés démontrables, des énoncés dont la négation est démontrable, et entre les deux, il y a une sorte d'inquiétant no-man's-land.
Quel est le statut de la vérité dans tout ça?
Pour une théorie T, on a bien une notion de vérité: un énoncé de T est "universellement valide" s'il est vrai dans tous les modèles. Il y a même un théorème de complétude du même Gödel, qui dit que les énoncés universellement valides sont démontrables.
Les modèles dont il s'agit sont des ensembles, donc quand on applique ça avec pour T la théorie des ensembles, on obtient une notion de vérité qui se mord la queue (ça n'est pas dit dans les livres de logique, c'est moi qui dit ça, mais je me le suis fait confirmer oralement par Girard). Tout ça pour dire qu'on n'a pas vraiment une notion de vérité et qu'on préfère s'en passer. Enfin "on", c'est plutôt "ils". Moi je n'ai pas renoncé. Je ne suis pas complètement seul: je signale un travail de Woodin (voir Wikipedia) qui explique en quoi le débat sur l'hypothèse du continu n'est pas clos.
La logique dominante a un autre souci, que les mathématiciens traitent par le mépris: la consistance de la théorie ZF (ou ZFC) est un dogme. Sur ce sujet et dans cette communauté, on doit donner une preuve de Faux ou se taire à jamais.
Le tiers-exclu
Dans une théorie, le sens des constructions est fixé par les axiomes, et c'est pareil pour la logique. Par exemple le sens de "ou" est fixé, entre autres par l'axiome du tiers-exclu : $\forall A, A ou nonA$. Et ce qui précède met en évidence que
la légitimité de cet axiome ne coule pas de source. Le débat sur le tiers-exclu a fait rage au début du siècle dernier, et a donné naissance à la logique intuitionniste, qui rejette cet axiome. En logique intuitionniste, prouver $A \otimes B$, c'est choisir un côté de l'alternative et le prouver. Bien que son inventeur Brouwer ait été voué aux gémonies par Hilbert et ses potes, la logique intuitionniste est, de nos jours, reconnue par les logiciens comme un progrès significatif dans la mesure où elle "contient" la logique classique, et permet d'y définir des preuves dites constructives, et dont on peut extraire des algorithmes. La logique linéaire a un positionnement analogue. Elle "contient" la logique intuitionniste, et permet de distinguer les preuves dites linéaires, celles qui n'utilisent qu'une fois les hypothèses, et qu'on peut donc exécuter sans faire de copie des données.
La stratégie copycat
On a compris que le sens de "ou" pose un problème d'ailleurs pas très bien formulé. Disons qu'on voudrait bien une logique adaptée aux maths de notre temps et où le statut du tiers-exclu soit plus satisfaisant. La stratégie copycat est une piste vers un tel Eldorado.
Pour comprendre cette stratégie, il faut penser à un joueur d'échecs qui joue simultanément sur deux échiquiers, contre deux adversaires, une fois avec les blancs et une fois avec les noirs, et qui ne connaît pas les règles. Sa stratégie consiste à attendre qu'un adversaire joue sur l'un des échiquiers et à reproduire la nouvelle position sur l'autre. Il est sûr d'un bilan honorable (une victoire une défaite, ou deux nuls).
Cette stratégie s'adapte à tout jeu "suffisamment polarisé", et si ce jeu ne connaît pas de partie nulle, elle assure de gagner sur l'un des deux tableaux, sans qu'il y ait forcément une stratégie gagnante sur l'un ou l'autre des deux tableaux.
Où on va
La piste à creuser consiste donc à définir la vérité à travers un jeu dans lequel deux joueurs s'affrontent par exemple autour d'une formule A que l'un veut confirmer et l'autre veut infirmer et où le joueur pourra gérer simultanément deux formules via une stratégie de type copycat. Cette idée impose deux contraintes au jeu logique que l'on cherche: chaque joueur devra gérer non pas une formule mais éventuellement deux, et plus généralement un paquet de formules. De tels paquets de formules logiques s'appellent des séquents.Et puis nos formules devront être polarisées: pour chaque formule A, on devra savoir lequel, du joueur qui veut confirmer A et de celui qui veut l'infirmer, doit prendre l'initiative à propos de A. On va voir que la logique linéaire supporte ces contraintes.