Langage ensembliste de base avec définitions.

$\newcommand{\s}{\bullet}$
$\newcommand{\o}{\blacksquare}$
$\newcommand{\a}{\mathbf A}$
$\newcommand{\e}{\mathbf E}$
$\newcommand{\d}{\mathbf D}$
Préambule:
Ce fil a pour vocation à présenter une version implémentable (à quelques problèmes de complexité près qui peuvent être problématiques du point de vue de l'informatique mais négligeables du point de vue des fondements) et complète du langage de la théorie des ensembles formelle, avec un nombre de notions de base le plus petit possible.
Conformément à sa conception des mathématiques non comme une nouvelle doctrine (religion ?) à imposer mais comme un service dont les usagers peuvent employer les éléments comme ils le veulent, l'auteur refuse fermement toute forme de militantisme et, pour autant qu'il sache, livre des définitions compatibles avec la théorie des ensembles courante.
La totalité de ce qui est dit dans ce message concerne la logique classique (la seule à ma connaissance qui est vraiment utilisée en théorie des ensembles, les autres, intuitionniste, linéaire étant destinées à d'autres types de fondements -quoi qu'on dise, par exemple, COQ n'est pas une théorie des ensembles- ou bien de façon marginale).

#######################

Dans ce message il n'est question que de définitions de formules et d'éléments syntaxiques. Les systèmes de preuves seront discutés plus tard (des choses telles que "qu'est-ce qu'un théorème" etc, si j'ai le temps/la motivation ...)

######################
Dans ce qui suit, le mot "numéro" désigne exclusivement une suite de symboles destinée à enrichir l'alphabet.
Précisément, un numéro est:
-$\o$
-une suite de caractères constituée de $\s$ et d'un numéro placé à sa droite; la suite obtenue sera appelée "successeur" dudit numéro.
-étant donnés deux numéros $a,b$, si $a$ apparaît dans la liste des étapes de formations de $b$ on dira que "$a$ est inférieur à $b$" (on dira aussi "strictement inférieur à $b$" lorsque de plus $a$ et $b$ ne sont pas identiques).

Si $n$ est un numéro, la notation "$n+1$" pourra également être utilisée pour désigner le successeur $\s n$ de $n$.
De même des notations "familières" telles que "$0$" pour $\o$, "$1$" pour $\s \o$, "$2$" pour $\s \s \o$ pourront être employées.

Exemples: $\o$, $\s \o$, $\s \s \s \o$ sont des numéros (notés habituellement "$0,1,3$").

Dans la suite, le mot "lettre" désignera des lettres de l'alphabet, à l'exclusion de $\a,\d,\e$ qui sont des constantes réservées à un usage ultérieur, ou bien des assemblages syntaxiques de la forme $a_{k}$ où $a$ est une lettre et $k$ un numéro (appelé souvent "indice").

Etant donné un numéro $n$, les $n$-formules sont des suites de caractères obtenues à l'aide des règles suivantes:

1°) si $\bf x,y$ sont des lettres ou bien des numéros strictement inférieurs à $n$, $\e \bf x y$ est une $n$-formule
2°) si $\Psi,\Theta$ sont des $n$-formules, $\d \Psi \Theta$ est une $n$-formule.
3°) si $\Phi$ est une $n+1$-formule, $\a \Phi$ est une $n$-formule.

[size=x-small](NB: apartés techniques
(i) cette manière d'implémenter les variables liées s'appelle "indices de Bruijn". Voyez un moteur de recherche
(ii) toutes les formules dont nous parlons sont donc en notation polonaise. Mais nous introduirons rapidement des notations parenthésées. Il n'y a pas lieu d'écrire les formules sans abréviation -c'est même matériellement impossible au vu des éléments premiers que nous avons choisis ici pour fonder le langage formel tant le nombre de caractères nécessaire pour écrire la moindre formule non triviale serait grand-, mais l'intérêt de faire ce genre de présentation est de dire vraiment au moins une fois ce que sont les objets de base des mathématiques).[/size]

-Certaines simplifications syntaxiques seront utilisées dans la suite. Par exemple lorsque $\bf a$ et $\bf b$ sont des numéros ou des lettres on notera "$(\bf a \in b)$" ou même "$\bf a \in b$" au lieu de $\e \mathbf a \mathbf b$. Cette formule se lit "$\bf a$ appartient à $\bf b$".

-Soit $\Phi$ une $0$-formule et $\mathbf x$ une lettre.
On note $\{\mathbf x:\Phi\}$ la $1$-formule obtenue en remplaçant dans $\Phi$ tous les numéros par leurs successeurs, et toutes les occurrences de $\mathbf x$ par $\o$.
On désigne par $\forall x\Phi$ la formule $\a \{\mathbf x : \Phi\}$. Cette formule se lit "pour tout $\mathbf x,\Phi$".

IMPORTANT: Noter que $\{\mathbf x : \Phi\}$ et $\forall \mathbf x \Phi$ sont des suites de caractères (lorsque toutes les abréviations sont retirées) où la lettre $\mathbf x$ ne figure pas.

- Les $0$-formules (i.e. les $\o$-formules) seront simplement appelées "formules".

-Etant donné deux formules $P,Q$, la formule $\mathbf DPQ$ est destinée à signifier intuitivement que $P$ et $Q$ ne sont pas toutes les deux vraies; $\d$ se note "Nand" dans un contexte informatique.
On emploiera les notations (abréviations) suivantes pour toutes formules $\Psi,\Theta$ et toutes lettres $\bf z,w,v$:
"$(\Psi|\Theta)$" pour $\d \Psi \Theta$
"$\Psi \Rightarrow \Theta$" pour $(\Psi|(\Theta|\Theta))$ (on dit "$\Psi$ implique $\Theta$")
"$\neg \Psi$" pour $(\Psi|\Psi)$ (on dit "non $\Psi$")
"$\Psi \vee \Theta$" pour $(\neg \Psi) \Rightarrow \Theta$ (on dit "$\Psi$ ou $\Theta$")
"$\Psi \wedge \Theta$" pour $\neg (\Psi | \Theta)$ (on dit "$\Psi$ et $\Theta$")
"$\Psi \Leftrightarrow \Theta$" pour $(\Psi \Rightarrow \Theta) \wedge (\Theta \Rightarrow \Psi)$ (on dit "$\Psi$ équivaut à $\Theta$").
"$\exists \mathbf z \Psi$" pour $\neg (\forall \mathbf z (\neg \Psi))$
"$\mathbf v \notin \mathbf w$" pour $\neg (\mathbf v \in \mathbf w)$.

Exemples: les formules
(1) $\forall x ((x \in a \wedge x \in b) \Rightarrow x \in c)$
(2) $\forall y \neg (y \in x)$
(3) $\exists y \forall x \neg(y \in x)$ (qui signifient respectivement intuitivement que "$c$ contient l'intersection de $a$ et de $b$", "$x$ est vide", "il existe un ensemble vide") sont en fait sous forme non abrégée, les formules suivantes:

$$\a \d \d \d \e \o a \e \o b \d \e \o a \e \o b \d \e \o c \e \o c \tag 1$$
$$\a \d \e \o x \e \o x \tag 2$$
$$\d \a \d \a \d \e \s \o \o \e \s \o \o \a \d \e \s \o \o \e \s \o \o \a \d \a \d \e \s \o \o \e \s \o \o \a \d \e \s \o \o \e \s \o \o \tag 3$$

Remarque: la formule (2) est identique à la formule $\forall t \neg (t \in x)$. La lettre $x$ est la seule qui figure dans cette formule. De même la formule (3) ne contient aucune lettre (à nouveau $\a,\d$ et $\e$ ne sont pas considérées comme des lettres mais sont des constantes du langage) et cette formule est identique, une fois les abréviations enlevées, à $\exists v \forall w \neg (w \in v)$.
Une formule ne "parle" que des lettres qui apparaissent dans elle (!!!).

Autres définitions:

Substitution de variables:
Si $n$ est un numéro, $\Psi$ une $n$-formule et $\bf x,t$ deux lettres, on désigne par $(\Psi [\mathbf x:= \mathbf t])$ (parenthèses facultatives si aucune confusion n'est à craindre) la formule obtenue en remplaçant dans $\Psi$, chaque occurrence de $\mathbf x$ par $\mathbf t$.

-Une classe est une 1-formule.

-Si $\Phi$ est une classe et $\mathbf y$ une lettre, $(\Phi(\mathbf y))$ (ou $\Phi(\mathbf y)$ ou même $\mathbf y \in \Phi$ si aucune confusion n'est à craindre) est la formule obtenue en remplaçant dans $\Phi$, chaque numéro par son prédeceseur s'il est non nul, et par $\mathbf y$ s'il est nul. Le prédecesseur du numéro $\s n$ n'est rien d'autre que $n$.

NB: Si $\Gamma$ est une formule et $\bf t,u$ des lettres, $\{\mathbf t : \Gamma\}(\mathbf u)$ est l'énoncé$ \Gamma[\mathbf t:= \mathbf u]$

###############################

Autres abréviations courantes des maths:

A1) Soit $\Phi$ une classe et $\mathbf x$ une lettre.
On abrège par "$ens (\Phi,\mathbf x)$" l'énoncé "$\a \left (\Phi \Leftrightarrow (\o \in \mathbf x) \right )$". Cet énoncé se lit "$\Phi$ est l'ensemble $\mathbf x$".
On voit donc que lorsque $\mathbf z$ est une lettre différente de $\mathbf x$ et ne figurant pas dans $\Phi$ , l'énoncé $ens(\Phi,\mathbf x)$ se réecrit $\forall \mathbf z \left ( \Phi(\mathbf z) \Leftrightarrow \mathbf z \in \mathbf x\right )$
Dans le cas particulier où $\Phi$ est introduite sous la forme $\{\mathbf t : \Gamma\}$ avec $\mathbf t$ une lettre différente de $\mathbf x$ (NB: on peut toujours se ramener à cette situation puisque si $\mathbf s$ est une lettre ne figurant pas dans $\Gamma$ et différente de $\mathbf s$, les classes $\{\mathbf t:\Gamma\}$ et $\{\mathbf s :\Gamma[\mathbf t := \mathbf s]\}$ sont identiques), on voit avec les conventions précédentes que $ens (\mathbf x, \{\mathbf t : \Gamma\})$ est l'énoncé $\forall \mathbf t \left (\Gamma \Leftrightarrow \mathbf t \in \mathbf x\right )$.

A2) On note pour toute classe $\Phi$, $Ens(\Phi)$ l'énoncé $\exists x, ens(\mathbf x,\Phi)$ où $\mathbf x$ est une lettre ne figurant pas dans $\Phi$ (cet énoncé se lit "$\Phi$ est un ensemble").

Un célèbre théorème de logique dû à Russell dit que $\{x : x \notin x\}$ n'est pas un ensemble.

A3): Soit $\Phi$ une classe et $A$ une lettre ou une classe.
On pose $\Phi \in A:=\exists \mathbf z\left (ens(\mathbf z,\Phi) \wedge \mathbf z \in A\right )$ (cf notation bleue plus haut quand $A$ est une classe). Ainsi on a défini $A\in B$ quand $A$ et $B$ sont des lettres ou des classes et on a étendu le langage de la théorie des ensembles. On pourra consulter "Introduction to axiomatic set theory" de Takeuti et Zaring pour un exposé détaillé de cette approche.

A4) si $A$ est une classe, $\Phi$ une formule et $\mathbf x$ une lettre,
$\forall \mathbf x\in A,\Phi$ abrège $\forall \mathbf x, (\mathbf x \in A \Rightarrow \Phi)$ et
$\exists \mathbf x\in A,\Phi$ abrège $\exists \mathbf x, (\mathbf x \in A \wedge \Phi)$.

A5) Soient $A,B$ des lettres ou des classes. (":=" veut dire "on définit ...").
On définit donc:
$A\subseteq B:= \forall x (x \in A \Rightarrow x \in B )$
$A=B:= A \subseteq B \wedge B \subseteq A$
$\{A,B\}:= \{x: x = A \vee x = B\}$
$(A,B):= \{\{A\},\{A,B\}\}$
$\mathcal P(A):= \{x : x \subseteq A\}$
$\bigcup A := \{x : \exists y, y \in A \wedge x \in y\}$
$A \cap B:= \{x: x \in A \wedge x \in B\}$
$A \cup B:= \{x: x \in A \vee x \in B\}$
$A \backslash B:= \{x : x \in A \wedge x \notin B\}$
$\{x\in A\mid \Phi\}:= \{x : x \in A \wedge \Phi\}$ où $\Phi$ est une $0$-formule.
$dom(A):= \{x: \exists y, (x,y) \in A\}$
$im(A):=\{y: \exists x, (x,y) \in A\}$
$Graphe(A):=\forall c \in A, \exists x \exists y, (x,y)=c)$ (NB: en fait par construction, les lettres qui suivent les quantificateurs ne peuvent pas désigner autre chose que des ensembles).
$Fonction\_ensembliste (A):=Graphe(A) \wedge \forall x \forall y \forall z, \left ((x,y) \in A \wedge (x,z)\in A\right) \Rightarrow y = z$.
$A \times B:= \{c:\exists x \in A, \exists y \in B, c=(x,y)\}$
$B^A:= \{f:Fonction\_ensembliste(f) \wedge dom(f)=A \wedge im(f) \subseteq B\}$
$x \in A \mapsto B := \{u: \exists x \exists y(u=(x,y) \wedge x \in A \wedge y = B )\}$ ($x,y,u$ étant distinctes, $x$ ne figurant pas dans $A$, $y$ ne figurant ni dans $A$, ni dans $B$, $u$ ne figurant ni dans $A$, ni dans $B$).