Mécompréhension de signes logiques

[Tnak10]

Bonsoir,

Je ne parviens pas à déchiffrer le premier axiome du théorème de Gödel, il y a une notation dont j'ignore le sens ici. Le signe Π n'est pas utilisé dans le sens d'une suite ou d'un produit cartésien. Gödel le définit ainsi "pour tout". x1 (x indice 1) est une variable individuelle et x2 une variable de classe d'individus. fx désigne le successeur de x.
Pouvez-vous m'éclairer sur le sens de la formule suivante ?

x2(0). x1Π(x2(x1)⇒x2(fx2))⇒x1Π(x2(x1)).

Merci à vous.

[Ben314]

Salut,
Si tu donnais une référence, histoire d'avoir le contexte, je pense qu'on pourrait éventuellement faire quelque chose, mais là, une formule avec des tas de symboles, sans le contexte, je vois vraiment pas ce qu'on peut en faire.

P.S. Je suis allé au premier endroit qui me viendrait à l'esprit, c'est à dire sur l'article de Wiki concernant les deux théorèmes d'incomplétude de Gödel (en supposant que c'est d'un de ces deux théorème là dont tu parle...) et j'ai rien trouvé qui ressemble à ça...

[Ben314]

En regardant ton truc, j'ai quand même l'impression que c'est le principe de récurrence, mais avec une faute de frappe :

x2(0). x1Π(x2(x1)⇒x2(fx2))⇒x1Π(x2(x1)).

Tu es sûr que c'est pas plutôt x2(0). x1Π(x2(x1)⇒x2(fx1))⇒x1Π(x2(x1)) ?
Qui, grosso modo, avec un symbolisme plus usuel s'écrirait :

[Tnak10]

Oh ! Merci beaucoup.
Oui, j'ai fait une faute en recopiant la formule, c'est bien fx1 dont il s'agit.
En symboles usuels je comprends mieux, j'aurais dû passer plus de temps à chercher, au temps pour moi.