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.
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...).
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