L'analyse non standard

Calli a écrit:

Tout énoncé de la théorie des ensembles prouvé dans ANS est vrai dans ZFC.

Mieux vaut écrire:

Tout énoncé de la théorie des ensembles prouvable dans ZFC+ANS est prouvable dans ZFC seul. (C'est ça la conservativité)

L'idéalisation sans paramètres est pour les ultrafiltres le fait que l'ensemble $\widehat X$ des ultrafiltres d'un ensemble $X$, muni de la topologie engendrée par les $v^X(A):=\{u \in \widehat X \mid A \in u\}$ où $A$ parcourt $\mathcal P(X)$, est compact et que de plus ces parties en question sont fermées (et donc si $(R_i)_{i \in I}$ est une famille de parties de $X$, si l'intersection de toute sous-famille finie des $i\mapsto v^X(R_i)$ est non vide, il en va de même de toute la famille en question par le théorème des ultrafiltres, en explicitant les définitions).

Pour la version paramétrée et bornée (en fait le schéma de réflexion dans l'article en lien sert juste à se débarrasser de la contrainte des quantifications bornées), c'est presque pareil.
Soient $X,Y$ des ensembles. Si $u\in \widehat X$, soit $\widehat f (u):=\{B \subseteq Y \mid f^{-1}(Y) \in u\}$. Alors $\widehat f $ est une fonction continue de $\widehat X$ dans $\widehat Y$.

Soient $A_1,...,A_n,V$ des ensembles. On pose $X:= V \times \prod_{i=1}^n A_i$. Soit $\pi_k: X \to A_k$ la $k$-ième projection pour tout $k$. Soit $(t_1,...,t_n) \in \prod_{i=1}^n \widehat A_i$.

Enfin soit $(S_j)_{j\in J}$ une famille de parties de $X$.

Si pour toute partie finie $J$ de $I$, il existe $w_J \in \bigcap_{j \in J} v^X(R_j)$ tel que $\widehat{\pi_{A_k}} (w_J) = t_k$ pour tous $k\in \{1,...,n\}$, alors il existe également $w\in \bigcap_{i \in I} v^X(R_i) $ tel que $\widehat{\pi_k} (w) = t_k$ pour tous $k\in \{1,...,n\}$. Cela provient à nouveau de la compacité de $X$ et de ce que la famille de fermés $v^X(R_i) \cap \bigcap_{k=1}^n \widehat{\pi_k} ^{-1} \left ( \{t_k\}\right )$ n'a pas de sous-famille finie d'intersection vide.

La projection de $w$ sur $\widehat V$ peut-être vue comme l'élément non standard réalisant la propriété d'idéalisation (prendre garde au fait qu'étant donnés des ensembles $A,B$, si $ u \in \widehat{A \times B} \mapsto \left ( \widehat{\pi_A} (u), \widehat{\pi_B} (u)\right ) \in \widehat A \times \widehat B$ n'est pas injective en général, bien qu'elle soit surjective - exo ).

Noter aussi que pour toute partie $T$ d'un ensemble $X$, si $i_{T,X}:= x\mapsto x:T \to X$ désigne l'injection canonique, alors l'image de $\widehat {i_{T,X}}$ dans $\widehat X$ n'est autre que $v^X(T)$ et de plus $\widehat {i_{T,X}}$ est injective. Ainsi pour tout $Y\subseteq X$, $\widehat Y$ s'identifie à une partie de $\widehat X$ et on a un énoncé du genre:
pour toute $R: I \to \mathcal P(X)$, si pour tout $J\subseteq I$ fini, il existe $w_I$ dans $\bigcap_{j\in J} \widehat {R_j}$ dont les projections sur les $\widehat A_k$ sont égales à $t_k$ pour tout $k$, alors il existe $w$ dans $\bigcap_{i\in I} \widehat {R_i}$ dont les projections sur les $\widehat A_k$ sont égales à $t_k$ pour tout $k$.

Bref on peut ne pas aimer "l'analyse non standard du pauvre avec ultrafiltres" :-D mais la construction d'un exo non traitable par elle mais par l'IST passe par plus qu'un peu d'idéalisation (bornée) à mon avis.

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

Autres propriétés:
le transfert est le constat de ce que l'ensemble des ultrafiltres principaux de $X$ est dense dans $\widehat X$ (et que le complémentaire de $v^X(A) = im \left ( \widehat {i_{A,X}} \right)$ est un ouvert puisque c'est $v^X(X \backslash A)$). Donc si $v^X(A)=\widehat A$ contient tous les principaux, il vaut $\widehat X$.

Pour la standardisation, notons pour $x\in X$, $\delta^X_x$ l'ultrafiltre principal de $X$ engendré par $x$. Si $E$ est une partie de $\widehat X$, soit $A:= \{x \in X \mid \delta^X_x \in E\}$. Alors pour tout $w$ principal dans $\widehat X$, $w\in E$ si et seulement si $w\in \widehat A = im \left ( \widehat {i_{A,X}} \right) = v^X(A)$ (via les identifications précédentes).

Entièrement d'accord avec Foys. Dans ma petite vie je n'ai jamais eu à me demander comment je pourrais esquiver l'idéalisation non std.

Cependant elle induit de fortes diffences d'approche des GC. Je détaillerai.

On peut féliciter Foys qui allie une forte ressource documentaire à son génie mathématique ;-)

Je suis de plus content de voir que ce que j'ai seriné sur le forum des centaines de fois apparait explicitement chez Nelson qui en a besoin en 1985 :-D pour sa preuve. Je me demandais si je trouverais un jour "une application" (si l'on peut dire) de ce radotage. Du coup, je le reproduis dans le présent post pour tout le monde, d'autant que j'oublie souvent le point (5) quand je poste sur le forum.

Les axiomes logiques des maths sont les clôtures universelles (ie les phrases obtenues à partir des suivantes en ajoutant des $\forall$ à gauche pour lier toutes les variables libres):

1/ $(A\to \to ((B\to C)\to (A\to C))$

2/ $A\to ((A\to \to $

3/ $A\to (B\to A)$

4/ $(A\to (A\to )\to (A\to $

5/ $[\forall x: (A\to R(x))]\to (A\to [\forall x: R(x)])$ (quand $A$ ne parle pas de $x$)

6/ $(\forall x: R(x))\to R(a)$

7/ $[\forall x(R(x) \to S(x))]\to [(\forall x: R(x))\to (\forall x: S(x))]$

et la SEULE règle de déduction est le modus ponens.

8/ On ajoute l'axiome du raisonnement par l'absurde (en option) avec : $((A\to tout)\to tout) \to A$

Attention, j'ai déjà expliqué pourquoi je change un poil le système présenté par Nelson page 126. Il me semble important de prévoir une liste qui permet ensuite pour les gens intéressés de répondre par des sous-listes quand ils demandent ce que font les déffiérentes logiques célèbres. Le système de Nelson ne le permet pas, car la duplication d'hypothèses est contenue et mal isolée dans son axiome:

$$ [A\to (B\to C)]\to [(A\to \to (A\to C)] $$

C'est l'axiome de fondation qui garantit ça (ça lui est même équivalent il me semble). Les $R(\alpha)$ sont plutôt notés $V_{\alpha}$ classiquement.

@Poirot : "C'est l'axiome de fondation qui garantit ça (ça lui est même équivalent il me semble)."

Ce n'est pas "il te semble", c'est vrai. (Dans ZFC - AF, évidemment)...

@Calli: Nelson donne une preuve entièrement syntaxique, profite zen.

J'en profite moi pour faire comprendre (enfin tenter) pourquoi la topologie et en particulier les phénomènes de compacité sont "si bien trivialisés".

Soit $E$ un ensemble standard et $Z$ une partie de $E$ définie (qui n'est pas forcément un ensemble donc) sans se brider, avec tout ce qu'on veut comme ingrédient (prédicat standard, etc). Comme par exemple "la partie de IN contistuée des entiers standards et pairs"

Il est facile de voir qu'il existe alors un ensemble standard $A$ et une partie pour le coup standard $R$ de $E\times A^3$, ainsi qu'un élément $a\in A$ (pas forcément standard) tel que pour tout $x\in E$ :

$$ x\in Z\iff \exists^s u\in A\forall^s v\in A: (x,a,u,v)\in R $$

Ainsi à la petite généralisation près que $E\neq A$ et la présence de $a$, on ne dépasse que très peu la notion de compacité sur le principe (enfin de précompacité), et pour être plus précis, la notion de "ne pas être l'infini" pour ce qui concerne les points d'un espace topologique.

Aurtement dit, la seule chose qu'ajoute l'ANS en plus des "vrais ensembles", c'est "la collection des points d'un espace topologique qui ne sont pas à l'infini". Ce slogan résume à epsilon près ce que fait l'ANS.

Un point $x$ n'est pas à l'infini quand il existe un $a$ qui est standard tel que pour tout ouvert $U$ standard qui $\ni a$, on a aussi forcément $x\in U$. Auterment avec mon mot habituel, $x$ n'est pas à l'infini quand il est superproche d'un élément standard.

L'ANS ajoute juste de parler de ces "ensembles intuitifs" de points avec des quantificateurs idoines au fait de parler des "vrais ensembles".

Un truc que je n'ai jamais (en tout cas je ne me le rappelle pas, ou alors j'ai conclu par la négative) vérifié, c'est "l'axiome du choix externe".

Ca peut être un bon exercice dans le présent contexte. De plus il peut être intéressant de traduire l'énoncé en énoncé classique via l'algo de Nelson.

L'énoncé est que pour tout $E$, il existe $F$ et $S$ tel que
pour tout $R\subset E^3$, il existe un UNIQUE $u$ tel que
pour tout $x\in E$ :

si $\exists^sa\forall^s b: (x,a,b)\in R$

alors:

1/ $\exists^s a\forall^s b : (u,a,b) \in R$
et
2/ $\exists^s c\in F\forall^s d\in F: (R,u,c,d) \in S$

$\newcommand{\set}[1]{\left \{ #1 \right \}}$

christophe c a écrit:

Attention, dans la gestion routnière des ultrapuissances ou des ultraproduits, tu ne gères JAMAIS tous les ultrafiltres en même temps. C'est assez intéressant du fait qu'il faudrait choisir arbitrairement un ultrafiltre prolongeant le filtre généré par $\{A\times B \mid A \in U; B \in V\}$quand $U$, $V$ sont deux ultrafiltres.

Le filtre $p(U,V):=\set{X\subseteq A \times B \mid \set{i \in A \mid \set {j\in B \mid (i,j) \in X} \in V} \in U}$ fait ça (et c'est bien un ultrafiltre, la vérification est un peu longue mais sans fantaisie; ils appellent ça un "produit d'ultrafiltres" dans les livres).

De toute façon, si $(A_k)_{k \in K}$ est une famille d'ensemble et si pour tout $k\in K$, $U_k$ est un ultrafiltre sur $A_k$, alors l'ensemble des parties de $\prod_{k \in K} A_k$ de la forme $\prod_{k\in K} B_k$ où $B_k\in U_k$ pour tout $k$, est une base de filtre sur $\prod_{k \in K} A_k$ et tout ultrafiltre plus fin a ses projections égales aux $U_k$.

Attention, tu vois bien que ce n'est pas du tout symétrique. Tu as choisi de mettre $U$ "avant" $V$.

L'opération que tu définis est très marrante d'ailleurs car elle permet de prouver en quelques lignes le théorème de Hindman qui dit que si $f$ va de $\N$ dans un ensemble fini, il existe une partie $A$ de $\N$ qui est infinie et $x$ tel que toutes les sommes finies et injectives d'éléments de $A$ sont envoyées sur $x$ par $f$.

Pour ça, il suffit de prouver qu'il existe un ultrafiltre non principal $U$ sur IN tel que $U+U = U$ où $*$ est "quasiment ton" opération.

Et pour prouver que $U$ existe, il suffit de prouver que dans tout compact doté d'une opération associative (ce que $*$ est) ayant certaines propriétés de continuité partielle, il existe $a$ tel que $a*a=a$.

C'est l'archétype d'une preuve "pas très constructive" on va dire :-D

A noter d'ailleurs que Hindman ne nécessite pas de parler de $+$. N'importe quelle opération associative sur $\N$ convient.

Oui, mais par exemple, le théorème de Hindman, lui, est concret, il énonce l'existence d'une branche infinie dans un arbre très simple. On peut d'ailleurs y prendre "la plus petite" branche (la plus à gauche, comme on dit souvent)