oui tiens d'ailleurs, je n'ai rien à ajouter à ce qu'a dit jobertz à ceci près que je précise que l'encodage est direct, aisé et naturel et ne rencontre jamais le moindre obstacle. Ca fait un peu une différence.

D'une certaine manière on pourrait aussi dire que l'activité mathématique est "encodable" par les entiers (en passant à l'étage au dessus et en regardant les preuves), et même par les équations diophantiennes à cause du théorème de Matiasevic. Par contre, cet encodage-ci n'est ni direct, ni aisé.

Par ailleurs, ne parlons pas trop de ZF. C'est surtout $\in$ qui compte. La "théorie originelle" qui fait tout magiquement est la théorie contradictoire axiome d'extensionnalité + ceux qui disent $\exists a\forall x R(x)\iff x\in a$ appliquée aux R qu'on veut. ZF est ensuite un choix subjectif d'avoir autorisé les "R" seulement qui intuitivement sont considérées comme "contenant peu de choses" (ie choix basé sur le cardinal)

Bonjour,


quelle est la différence entre un théorème et une proposition ???

Pour info, voici un résumé de preuve que 2 modeles pleins sont isomorphes et dedans, je vais pointer le problème évoqué par Dummet (du moins où il se manifeste, mais le fait qu'on sache qu'il se manifeste vient de godeleries)


Pour simplifier, j'évite les opérations + et fois

Soit donc (zero1,E,f,P) et (zero2,F,g,Q) 2 modèles pleins. E,F sont les ensembles base, f,g sont les injections non surjectives (ie les zero de chaque modele n'ont pas d'antecedent et P et Q sont les domaines sur lesquels vaient les variables du second ordre (pour simplifer je ne traite que l'arité 1, ce qui ne change rien ici)

Soit $u(n+1)$ le couple $(x,y)\in E\times F$ obtenu de la manière suivante: en notant $u(n)=(z,t)$ alors $x:=f(z) $ et $y:=g(t)$; partant de $u(0):=(zero1,zero2)$

C'est une définition par récurrence de $u$ qui va de $\N$ (le vrai lol) dans $E\times F$

la partie par exemple de $F$ qui est l'ensemble des $y\in F$ tels qu'il existe $n\in \N, x\in E: u(n)=(x,y)$ est un ensemble $A$ qui contient $zero2$ et qui est stable par $g$

Maintenant, supposer qu'on a affaire à un modèle plein, c'est supposer précisément que $A\in Q$

Il s'ensuit que si $(F,g,Q)$ obéit à l'axiome du second ordre $\forall X: $ si X inductif alors $\forall y: Xy$, en appliquant cet axiome à $A$, on obtient que $\forall y\in F: y\in A$

On fait de même pour $(E,f,P)$ et on obtient alors que l'image de $u$ est la graphe d'un isomorphisme entre les 2 modèles supposés pleins

Mais les supposer pleins a consisté à parler "de l'extérieur" de certains ensembles (et pas du tout construits de manière innofensive,puisque on attend que l'un contienne un ensemble relatif à l'autre, même si je suis passé par un troisième $\N$ on pourrait s'en passer, mais ce dont on ne sait pas se passer, c'est d'affirmer que $Q$ contient une partie de $F$ dont la définition utilise $(E,f,P)$)

Ce que sous-entend Dummet c'est que dans les protocoles de communication, c'est typiquement le genre d'hypothèse qu'on ne peut pas faire (dire que l'un contient bien tous les objets concevables à partir de l'autre), sinon c'est supposer gratuitement qu'on a déjà résolu le problème

De plus, initialement, tu voulais éclaircir un propos deDummett et je pense te l'avoir entièrement reprécisé.

"on aimerait bien communiquer (sous-entendu les vraies choses), mais on ne dispose pas de possibilité de formaliser le second ordre (sous-entendu toute formalisation tombe très loin de ce qui arrive vraiment aux modèles pleins)"

Tu as formulé ta question initiale en disant: "je croyais que 2 modèlespleins de l'arithmétique était isomorphes" et je t'ai répondu, "oui, deux modèles pleins, mais on n'a pas accès aux modèles pleins avec un nombre fini de mots et dénombrable de phrases, de quelque manière qu'on s'y prenne, et du Godélisme divers vient en plus de ça attester irréfutablement que c'est "irrattrapable""

Tu ne semble pas vouloir accepter que c'est ce que Dummett a exprimé (ou souhaité exprimer).

Analogie: c'est comme si tu disais "je ne comprends pas, je ne veux pas d'un modele M de ZF dans lequel IR est dénombrable, je veux raisonner avec le vrai IR, celui qui n'est pas dénombrable" et depuis le début je te dis que TOUT raisonnement que tu feras, aussi biscornu soit-il, ne distinguera pas le vrai IR d'unefoultitude de corps réels clos dénombrables banals qui viennent s'insérer dans ton cadre axiomatique.

Bon, bin tu veux pas, tu veux pas, u'est-e que j'y peux?

La preuve que 2 modeles pleins de l'arith du scd ordre sont isomoprhes est l'analogue de la preuve que IR n'est pas dénombrable, ie étant donné un modèle M de ZF (ou de n'importe quelle théorie qui englobe toutes les maths) cette preuve montre que si f est une sujection de $\N _M\to \R _M$ alors $f\notin M$, c'est tout

Toi tu voudrais avoir accès "au vrai IR" celui qui n'est pas dénombrable, même :D sans parler de modeles ou koi ou kes, genre, même si on demande à Dieu de metter une surjection de IN sur IR, il n'y arrive pas, et bé, je suis pas le père Noel, désolé.