Lazi

Représenter une formule dans elle-même

Contexte

Pour des démonstrations à la Gödel, il est nécessaire qu'une formule ait une représentation d'elle-même.

Question

Est-il possible Lazi, qu'une formule ait une représentation d'elle-même ? Si oui, comment.

Étude

Par remplacement de variable

On a déjà un système pour représenter les formules.
On ne peut pas le faire directement car alors on aurait une représentation infinie, car il faudrait mettre la représentation dans elle-même.

On peut définir une fonction rep qui à partir d'une représentation d'une formule retourne la représentation de la représentation de la formule.
Remarquons que pour une représentation de formule rf comportant une variable r, l'on peut définir une fonction
g = $F rf,gr → rf où la variable r est remplacée par gr +f rep rf +f rep gr
où :

  • gr est la représentation de g

Soit alors f une fonction à un argument r, r prendra la valeur de représentation de f r. Soit rf la représentation de f où on représente son argument r par une variable.

Soit g = f \ g rf gr.
Montrons que g = f où r est remplacé par la représenation de f r :

g rf gr retourne rf, il nous reste donc à vérifier que r est remplacé par la bonne valeur. r est remplacé par gr +f rep rf +f rep gr, qui a comme valeur après interprétation g rf gr, qui est donc par récurrence la bonne valeur.

Réponse

Oui, par des remplacement et une fonction de représentation d'une représentation de formule (voir l'étude).