Analyse Non Standard

-D hélas non, je suis sur mon tel et allongé, ça me ferait trop mal partout et surtout aux mains.

Mais pour info je peux quand même dire un truc : presque personne ne la connait, elle a été récupérée par des pédagos à un moment, ce qui a probablement eu le don d'agacer les chercheurs (surtout quand les pédagos n'utilisaient que le seul axiome pas franchement jouissif (l’idéalisation) et parlaient sans savoir, enfin bref ...

Le TRUC PRINCIPAL qu'il faut dire est surtout que l'ANS a été attaquée sur TRÈS EXACTEMENT SON POINT FORT qui a été considéré comme un défaut (il s'agit donc d'un big malentendu en fait) : sa conservativité au dessus de ZFC.

Les uns disaient "c'est de la garantie en béton",
les autres disaient "elle ne démontrera jamais rien de plus que ZFC" (c'est ce théorème la conservativité)

Et finalement personne n'a jamais vraiment voulu regarder le taux de raccourcissement des preuves et leur coté intuitif. Mais le temps de la science est un temps long de toute façon et en ce moment la crise ayant tendance à rejeter l'infini, elle n'a pas le vent en poupe.

Mais quand on voit que même les catégories arrivent à fédérer un peu de chercheurs, nul doute que l'ANS fera un jour une ré-entrée importante, faut juste attendre quelques articles de quelques uns qui s'en servent, d'où le temps long vue leur rareté

Merci à Bruno de m'avoir prévenu de ce fil.

1) Je ne connais pas les résultats récents sur la vitesse de preuve comparée, mais je parie à 10 contre 1 que ça n'est pas étudié

2) [small]Mais y a il, peut-il y avoir, des théorèmes d'ANS "pure" (qui ne se ramènent pas à un théorème exprimé dans ZFC) interessants?[/small] Oui bien sur, il y en a plein, mais comme tu rajoutes "intéressant", hum hum, je ne sais trop quoi répondre :-D

Une précision quand-même: tout énoncé clos borné (par des paramètres standards) écrit avec "std" est équivalent à un énoncé sans "std", en suivant l'astuce de traduction suivante:

$\forall x\exists^s y[...]$

---

> $\exists^{fs} F \forall x\exists y\in F$

$\forall^s \exists^s y[R(x,y)]$

---

>$\exists^s f \forall ^s x [R(x,f(x))] $

De même, soit $R(u,x_1,..,x_n)$ une relation contenant comme seules var libres les $u,x_i$ et écrite avec le mot $std$. Il existe (via un procédé de traduction simple et automatique) un énoncé écrit sans "std" de la forme $S(u,v,w,x_1,..x_n)$ vérifiant $$\forall x_1,..,x_n,u: [(R(u,x_1,..)\iff (\exists^s v\forall^s w S(u,v,w,x_1,..))]$$

(Bon j'exagère un poil qui est sans aucune importance pour le contexte, je te détaillerai ça quand je serai moins flemmard)

Précision: $\forall ^s x: A$ veut dire $\forall x: std(x)\to A$ et $\forall ^{fs} $ veut dire "pour tout x fini et standard..."

Oui, je suis privé de tout débat politique (et donc des rubriques où ils ont lieu).

@Shah: histoire de "t'exciter", sache qu'il existe (enfin pour les bons univers) une relation unaire $R(x)$ à une variable libre (écrite avec le prédicat standard) telle que pour tout énoncé clos $e$ écrit sans le prédicat $std$, on a $R(e)\iff e$ est vrai.

Autrement dit l'ensemble vérité de l'univers est définissable avec "std". Ca ne contredit pas ce que j'ai dit au dessus à cause de petits détails que j'ai volontairement omis..

Je te donne la définition vue qu'elle fait 3 lignes:

[P est vraie] = [il existe un inaccessible E, qui contient tous les standards et tel que pour toute formule $R(a,x)$ standard, avec un paramètre standard $a$ est une variable libre, s'il existe dans $E$ un $t$ tel que $R(a,t)$ alors il en existe un qui est standard, et un tel inaccessible vérifie $P$]