Les variables, encore elles

Foys

Dans ce fil on tente (qui a dit "à nouveau ?") de donner explicitement le (enfin, un des mais celui-ci est pratique et très souple) mécanisme par lequel maths peuvent s'encoder.

I) Les variables n'existent pas en mathématiques. Il y a des constantes et des artifices grammaticaux.

Prenons un exemple (basé sur ce qui est appelé "niveaux de Bruijn", à rechercher sur le Web).

Soit  $\mathcal C$ un ensemble (contenant en pratique les lettres de l'alphabet et d'autres symboles) et $n$ un entier. Un lambda-terme à $n$ variables (et constantes dans $\mathcal C$)

est une suite de caractères pouvant être obtenue par application répétée des règles suivantes:

1°) les éléments de $C$ et les caractères spéciaux $\fbox{$k$}$ où $k$ est un entier strictement inférieur à $n$ sont des lambda_termes à $n$ variables.

2°) si $\mathbf p$ et $\mathbf q$ sont des lambda-termes à $n$ variables, $\fbox{$a$} \mathbf p \mathbf q$ est un lambda-terme à $n$ variables

3°) si $\mathbf r$ est un lambda-terme à $n+1$ variables, $\fbox{$\lambda$} \mathbf r$ est un lambda-terme à $n$ variables.

Un lambda-terme à $0$ variables sera dit "clos" dans ce qui suit.

II) La formation de lambda-termes sans se tromper peut être fastidieuse mais l'abréviation suivante est utile:

soit $x$ une constante de $\mathcal C$. Soit $n$ un entier. $\mathbf f$ un lambda-terme clos (i.e. à $0$ variables). Soit $\mathbf f'$ le lambda-terme à une variable obtenu de la manière suivante: pour tout entier $k$, si $\fbox{$k$}$ figure dans $\mathbf f$ on le remplace par $\fbox{$k+1$}$. On remplace toutes les occurrences de $x$ par $\fbox{$0$}$. On vérifie qu'il s'agit bien d'un terme à $0$ variables (par récurrence sur la taille des sous-termes mettons). On pose enfin $\lambda x \mathbf f := \fbox{$\lambda$} \mathbf f'$.

La lettre $x$ n'apparaît pas dans $\lambda x \mathbf f$ (l'algorithme formant le terme enlève toutes ses occurrences).

Grâce à cette notation, on peut former des termes en manipulant uniquement des termes clos. On utilise également les parenthèses et autres artifices habituels pour éviter la notation polonaise préfixe (plus haut, $\fbox{$a$}$ est un symbole d'opération à deux opérandes et $\fbox{$\lambda$}$ est un symbole d'opération à un opérande). On écrira simplement $\mathbf p(\mathbf q)$, $(\mathbf p)(\mathbf q)$, $\mathbf p \mathbf q$ etc au lieu de $\fbox{$a$} \mathbf p \mathbf q$.

III) Exemples simples:

1°) $\lambda x  \lambda y \lambda z ((xz) (yz))$ et $\lambda  a \lambda b \lambda c ((ac) (bc))$ sont des lambda-termes clos ET ILS SONT IDENTIQUES!!!.

Ces deux termes sous leur forme non lisibles sont en réalité le terme $\fbox{$\lambda$}\fbox{$\lambda$}\fbox{$\lambda$} \fbox{$a$} \fbox{$a$} \fbox {$0$}  \fbox {$2$} \fbox{$a$} \fbox {$1$} \fbox {$2$}$. Ce terme ne contient aucune lettre (NB: $\fbox{$a$}$ n'a rien à voir avec la lettre $a$, c'est un symbole dédié).

2°) $\lambda s \lambda t (x (st))$ est un lambda-terme clos qui contient une seule lettre ($x$). Il s'agit de $\fbox{$\lambda$} \fbox {$\lambda$} \fbox{$a$} x \fbox{$a$} \fbox{$0$} \fbox{$1$} $. Ce terme est identique au terme $\lambda p \lambda q (x (pq))$. Il est en revanche différent du terme $\lambda p \lambda q (y (pq))$ puisque ce dernier contient la lettre $y$ mais pas la lettre $x$.

IV) Le langage des lambda-termes (le lambda calcul) permet d'exprimer toutes les formules mathématiques. Chaque formule peut être facilement mise sous la forme d'un lambda-terme, $\mathcal C$ étant choisi de sorte que les symboles usuels d'opérations mathématiques soient parmi les éléments de $\mathcal C$.

Par exemple quand on veut faire de la logique on peut fixer des symboles $\mathbf A$, $\mathbf E$, $\mathbf O$, $\mathbf N$, $\mathbf C$ et étant donné un entier $n$, appeler "énoncé de théorie des ensembles à $n$ variables" et "terme de théorie des ensembles à $n$ variables" tout lambda-terme obtenu par application répétée des opérations suivantes (et de rien d'autre):

1°) Si $\mathbf x$ et $\mathbf y$ sont des termes de théorie des ensembles à $n$ variables,$\fbox{$a$} \fbox{$a$} \mathbf A \mathbf x \mathbf y$ est un énoncé de théorie des ensembles à $n$ variables

2°) si $\Phi$ et $\Psi$ sont des énoncés de théorie des ensembles à $n$ variables, $\fbox{$a$} \fbox {$a$} \mathbf O \Phi\Psi$ et$\fbox{$a$} \mathbf N \Phi$ sont énoncés de théorie des ensembles à $n$ variables

3°) si $\Theta$ est un énoncé de théorie des ensembles à $n+1$ variables alors $\fbox {$a$} \mathbf E \fbox{$\lambda$}\Theta$ est un énoncé de théorie des ensembles à $n$ variables

4°) les lettres et les symboles $\fbox{$k$}$ avec $k<n$ sont des termes de théorie des ensembles à $n$ variables

5°) si $\Xi$ est énoncé de théorie des ensembles à $n+1$ variables, $\fbox{$a$} \mathbf C \fbox{$\lambda$}\Xi$ est un terme de théorie des ensembles à $n$ variables.

Les notations moins lourdes suivantes sont souvent utilisées:

(i) $\mathbf x \in \mathbf y$ au lieu de $\fbox{$a$} \fbox{$a$} \mathbf A \mathbf x \mathbf y$

(ii) $\Phi \vee \Psi$ (resp. $\neg \Phi$) au lieu de $\fbox{$a$} \fbox{$a$} \mathbf O  \Phi\Psi$ (resp. $\fbox{$a$} \mathbf N \Phi$)

(iii) $\exists x \Gamma$ au lieu de $\fbox{$a$} \mathbf E (\lambda x \Gamma)$

(iv) $\{y \mid \Delta \}$ au lieu de $\fbox {$a$} \mathbf C (\lambda y \Delta)$

Le reste est comme vous imaginez:

$\Phi \Rightarrow \Psi$ est une abréviation de $(\neg \Phi) \vee \Psi$,

$\forall x \Sigma$ est une abréviation de  $\neg (\exists x \neg \Sigma)$,

$\Phi \wedge \Psi$ est une abréviation de $\neg ((\neg \Phi) \vee \neg \Psi)$,

$\Phi \Leftrightarrow \Psi$ est une abréviation de  $(\Phi \Rightarrow \Psi) \wedge (\Psi \Rightarrow \Phi)$

$x=y$ est une abréviation de $\forall z (z \in x \Leftrightarrow z \in y)$ (où $z$ est une lettre qui n'apparaît ni dans $x$, ni dans $y$),

"$x$ est un ensemble" est une abréviation de $\exists y (x=y)$ ($x$ est un terme, pouvant être de la forme $\{...|...\}$ et $y$ n'apparaît pas dans $x$. En théorie des ensembles, certains termes de la forme $\{...\mid ...\}$ ne peuvent désigner des ensembles sous peine de contradiction - songer au terme de Russell: $\{x \mid \neg (x\in x)\}$ - cependant les lettres devant des quantificateurs désignent toujours des ensembles),

$\{a,b\}$ est une abréviation de $\{x\mid x=a \vee x=b\}$ (la lettre $x$ n'apparaissant ni dans $a$, ni dans $b$), $\{a\}$ abrège $\{a,a\}$,

$(a,b)$ est une abréviation de  $\{\{a\}, \{a,b\}\}$,

$a\times b$ est une abréviation de $\{x\mid \exists y \exists z, y\in a \wedge (z \in b \wedge (x,y)=z)\}$ (les lettres $x,y,z$ étant distinctes et n'apparaissant pas dans $a$ ni dans $b$),

$x\subseteq y$ est une abréviation de $\forall z (z \in x \Rightarrow z \in y)$ (la lettre $z$ n'apparaissant pas dans $x$ ni dans $y$),

$\mathcal P(x)$ est une abréviation de $\{y \mid y \subseteq x\}$ (la lettre $y$ n'apparaissant pas dans $x$).

$\bigcup x$ est une abréviation de $\{y \mid \exists z, y \in z \wedge z \in x\}$ (les lettres $y$ et $z$ étant distinctes et n'apparaissant pas dans $x$)

$f(x):= \bigcup \{y \mid (x,y) \in f\}$ (où $y$ n'apparaît ni dans $x$ ni dans $f$. C'est une notation pour les fonctions: on peut montrer sous les axiomes ensemblistes usuels que si $f$ est une fonction et si $x$ est dans son domaine, que $f(x)$ est l'unique ensemble $z$ tel que $(x,z)\in f$)

Et ainsi de suite.