Principe d'idéalisation
# Principe d'idéalisation

En analyse non standard, le principe d'idéalisation est un axiome permettant soit d'obtenir des propriétés portant sur tous les ensembles standard finis à partir d'un résultat d'existence, soit au contraire d'obtenir un résultat d'existence à partir de propriétés portant sur tous les ensembles standard finis.

## Énoncé

Le principe d'idéalisation pose l'équivalence entre les deux assertions suivantes :

* Il existe un ensemble y tel que tout ensemble standard x vérifie un prédicat (interne ou externe) q(x,y) ;
* Pour tout ensemble standard fini X, il existe un ensemble y (dépendant de X), tel que tout élément x de X vérifie q(x,y).

## Principe spécialisé d'idéalisation

Parfois posé comme axiome, le principe spécialisé d'idéalisation est un cas particulier de spécialisation. Il affirme l'existence d'éléments non standard dans tout ensemble standard infini. De manière équivalente, un ensemble interne est fini si tous ses éléments sont standards.

Il se déduit du principe précédent en lui appliquant le prédicat $(y\in A)\wedge (y\neq x)$ où A est un ensemble standard infini.

Conséquences du principe spécialisé d'idéalisation :

* La collection des éléments standard d'un ensemble standard infini n'est jamais un ensemble standard ;
* Les nombres naturels infinis sont exactement les entiers naturels non standard ;
* Il existe des nombres réels infiniment petits non nuls.

## Principe non standard de Cantor

Dans tout ensemble standard infini non dénombrable X, il existe un élément (nécessairement non standard) n'appartenant à aucun sous-ensemble standard dénombrable de X. En effet, pour tout ensemble fini F de parties dénombrables de X, il existe un élément y de X n'appartenant à aucun des ensembles de F (leur réunion, étant dénombrable, ne peut être égale à X). Le principe d'idéalisation s'applique, montrant qu'il existe un élément y* de X n'appartenant à aucune des parties dénombrables standard de X.

## Principe de Nelson

Il existe un ensemble fini Y tel que tout ensemble standard en est un élément.

