Logique et permutation

Pour ce problème assez élémentaire, qui sera la question numéro 1050 de "il est facile de",j'ai décidé de ne pas être trop formel afin qu'un max de gens s'y amusent. Attention, je n'ai pas cherché la réponse, je ne la connais pas a priori, même si j'ai une opinion.

Le langage sera un alphabet infini composé de lettres majuscules et minuscules. Les phrases seront ce qu'on obtient en écriture polonaise via $(X,Y) \mapsto \to XY$ (qui signifie $(X)\to (Y)$, $X,Y$ étant des phrases déjà construites) et via $X\mapsto \forall vX$, où la quantification ne peut porter que sur des lettres minuscules.

Les composants atomiques pour les phrases sont les mots commençant par une majuscules et n'ayant que des minuscules ensuite. Un mot sera considéré comme "écrit en colonne" et donc n'occupe qu'une seule place.

Exemple de phrase $\to Axyr Buc$ ou encore $\to \forall eRucse Axex$, qui signifient respectivement en notations humaines:

$(Axyr) \to (Buc)$ ; $ (\forall e: Rucse) \to (Axex)$

Je rappelle ce qu'est la sémantique de la logique du premier ordre. L'arbitre affecte des vrai ou faux à chaque phrase sans quantificateur en respectant la règle de fonctionnement de $\to$ *** . ensuite des joueurs s'affrontent. Le " joueur faux" jouent les lettres commandées par les $\forall x$ qui sont positifs et le "joueur vrai" joue les lettres commandées par les $\forall x$ négatifs.

Une quantification $\forall x$ est positive quand sa place (celle de $\forall$) est impaire et négative quand sa place est paire dans l'écriture polonaise. Je mets des couleurs: Dans la phrase suivante, c'est le "joueur vrai" qui joue les lettres vertes et le "joueur faux" qui joue les lettres rouges. On joue de gauche à droite durantla lecture de la phrase.

[large] [/large]

Toute phrase peut être mise sous forme prénexe de PLEIN de façons différentes. Mais d'abord commençons par INTERDIRE les phrases où une même variables liée apparait plusieurs fois avec des rôles différents comme dans:

$$ \to \forall xAx\forall xBx$$

car ce sont deux joueurs qui devront faire les remplacements. Dans la suite on n'autorisera que les

$$ \to \forall xAx\forall yBy $$

La phrase qui précède a deux prénexations possibles que voici (Attention, il n'y a pas de quantificateurs $\exists$ officiel dans le présent post, il n'y a que des $\forall$, mais la présence dans le préfixe se doit de distinguer qui joue la lettre: pour signaler un jeu par "le joueur vrai", on utilise le symbole $\exists$.

1/ $\exists x\forall y : (\to AxBy)$

2/ $\forall y \exists x: (\to AxBy)$

Attention: les phrases de ce genre ne font pas partie du langage. Je les appellerai des "prénexations".

J'aborde maintenant la question qui va être l'objet du fil:

regardez bien la très mystérieuse phrase : $\to \forall xAx\forall yAy$

(Je rappelle qu'elle dit humainement $(E)\to (E)$ où $E$ exprime $\forall x: A(x)$, rien de plus, elle est donc une "évidence primitive")

Cette phrase a deux prénexations:

1/ $\exists x\forall y : (\to AxAy)$

2/ $\forall y \exists x: (\to AxAy)$

Mais ... seule la deuxième la fait apparaitre "à nouveau" comme une évidence..
Alors que la première forme lui donne un aspect un peu magique (ie ancètre de l'axiome du choix + de l'omniscience).

Je le rappelle la sémantique usuelle demande à l'arbitre de dire AVANT qu'ils ne s'affrontent aux deux joueurs qui est vrai et qui est faux parmi toutes les phrases sans quantificateurs. Il suit que deux joueurs absolument parfaits "ne vont pas voir" la différence entre les difficultés des jeux associés aux prenexations.

On va maintenant changer les règles: l'arbitre ne joue plus avant, mais plutôt APRES la partie et "fait tout" pour faire gagner le "joueur faux".

On obtient ainsi un ensemble intéressant de phrases: l'ensemble des phrases qui ont au moins une prénexation gagnable par le "joueur vrai" avec ces nouvelles règles. On peut de manière équivalente demander si en gardant les anciennes règles et en supprimant l'arbitre on le "joueur vrai" peut s'assurer de terminer la partie sur une tautologie.

Il en va bien sûr ainsi de la phrase de l'exemple $\to \forall xAx\forall yAy$ dont la prénexation

$$ \forall y \exists x: (\to AxAy) $$

est gagnable par "le joueur vrai" comme suit: il regarde la valeur (lettre) $v$ jouée par faux pour $y$, ie au moment où on en est au stade $\exists x: \to AxAv$.

Il fait exprès de recopier, ie de jouer $v$, ce qui donne comme partie terminée la phrase:

$$ \to AvAv$$

qui lui assure la victoire.


Cet ensemble contient tous les axiomes affines.




*** Seul $vrai\to faux$ ne peut recevoir $faux, les autres implications recevant la valeur vraie.