Cours2 : A propos de IL EXISTE

Ou et il existe, même combat

Il existe c'est la variante n-aire de ou, ou plutôt ou, c'est la variante binaire de il existe. Autrement dit il existe est à ou ce que Sigma est à +. Pour il existe comme pour Sigma, on peut penser qu'il y a un ensemble concerné par l'existence considérée. Par exemple dans la théorie des groupes, il existe concerne le groupe dont parle cette théorie. Et dans notre théorie des ensembles (ou des univers) ZF, $\exists x, Px$ signifie qu'il existe un ensemble x dans notre univers qui vérifie la propriété P. Bien sûr il s'agit là d'une sémantique "à la Tarski", qui ne dit pas ce que signifie exister, mais plutôt où cette existence s'applique.

Comme pour la disjonction, on a un point de vue intuitionniste sur l'existence, qui dit que, pour prouver $\exists a, P$, il faut "exhiber" un témoin t puis prouver l'énoncé P [a :=t] obtenu en remplaçant a par t dans P.

L'exemple standard qui met en évidence la divergence entre les points de vue classique et intuitionniste est celui de l"énoncé $\exists a, b \in R -Q, a^b \in Q$. La preuve classique distingue selon que $(\sqrt 2)^{\sqrt 2}$ est rationnel ou non, et traite les deux cas sans s'intéresser à savoir lequel est le bon. Cette preuve est invalide du point de vue intuitionniste, qui pourrait argumenter: "et si $(\sqrt 2)^{\sqrt 2}$ n'était ni rationnel ni irrationnel?".

Dans le cas d'espèce, on sait par ailleurs que $(\sqrt 2)^{\sqrt 2}$ est irrationnel, et même transcendant, mais c'est bien plus compliqué (théorème de Gelfond-Schneider).

Lorsque ça peut les tirer d'affaire, les mathématiciens n'hésitent pas à invoquer l'axiome du choix pour parvenir à leurs fins.Ils passent sans préavis de ZF à ZFC ce qui modifie significativement le sens de l'existence. Tout ça pour dire qu'on ne sait pas bien ce que veut dire il existe et que beaucoup s'en contre-foutent.

Cours3 : A propos des coupures

La règle de coupure réduit un séquent à deux séquents qui seraient plus petits, sauf qu'on leur ajoute à tous les deux une nouvelle formule, une fois à droite et une fois à gauche. C'est un peu la version moderne du modus ponens. Dans sa forme standard, la règle répartit (au gré du prouveur) sans les dupliquer les hypothèses et les conclusions entre les deux prémisses. Dans le contexte classique, la duplication des hypothèses (ou des conclusions, c'est pareil) est autorisée par la règle de contraction. Dans ce cas, on peut reformuler la règle de coupure en dupliquant tout: les deux prémisses s'obtiennent en ajoutant la nouvelle formule A, d'un côté ou de l'autre, à la conclusion. La logique linéaire considère la règle de contraction comme "sensible" puisqu'elle duplique, et s'occupe entre autres de contrôler son utilisation en la limitant drastiquement.

On peut voir la règle de coupure comme une façon de répartir les tâches. Le prouveur se scinde en deux prouveurs qui se répartissent les hypothèses et les conclusions, et restent en communication via la nouvelle formule. Le dogme de l'élimination des coupures dit que c'est une affaire interne, que ça ne change rien pour le monde extérieur (ceux qui jugent/apprécient/contestent la preuve), et que, si on sait prouver avec coupures, on doit aussi savoir prouver sans coupure. Il y a aussi une bonne raison de vouloir éliminer les coupures, puisque ce sont des pas de preuve qui peuvent faire croître la taille du but (la formule A peut être très grosse...).

Cours4 : Jeux et stratégies

Dans un premier temps, on prend la définition suivante de jeu, pour deux joueurs B et N: un jeu est un graphe "bipartite" G, qui est constitué par
  • un ensemble dit des positions P := P_+ \amalg P_- (P_+ pour celles où B doit jouer, P_- pour celles où N doit jouer).
  • un ensemble dit des coups C := C_+ \amalg C_- , avec $C_+ \in P_+ \times P_- $ (les coups de B) et $C_- \in P_- \times P_+$ (les coups de N) .

    Dans ce jeu, une partie est un chemin, c'est-à-dire une suite (éventuellement vide) de coups composables. Il est plus prudent de postuler qu'il y a une partie vide par position. Ainsi toutes les parties ont une position initiale et une position finale.

    Une partie est gagnée par l'un des joueurs lorsque dans sa position finale, c'est à l'autre joueur de jouer, et qu'il n'a pas de coup possible.

    Une stratégie pour B dans la position p \in P_- est un ensemble S de parties