My book

124

Réponses

  • Martial
    Martial
    @cohomologies : le problème c'est que tu es confronté à deux "niveaux de conscience". Pour reprendre mon exemple ci-dessus avec l'ensemble $X=\{\alpha, \alpha-1,...\}$ qui n'a pas de plus petit élément, il faut distinguer "vision de l'extérieur" et "vision de l'intérieur". Toi, de l'extérieur, tu vois bien qu'il y a un truc bizarre dans ce modèle, puisqu'il a une suite infinie strictement décroissante d'ordinaux, et donc $\omega$ n'est pas bien fondé. L'habitant du modèle, lui, n'y voit que du feu : pour lui la suite décroissante $(\alpha, \alpha -1,...,0)$ a pour longueur $\alpha +1$, qui, toujours pour lui, est un entier naturel comme un autre. Et c'est heureux car son univers satisfait ZFC, en particulier l'axiome de fondation, donc il faut bien que $\omega$ soit bien fondé. Il n'y a pas de contradiction.
  • Martial
    Martial
    Mettons que tu parviennes à discuter avec ce bonhomme (l'habitant du modèle non standard). Tu vas lui dire : "Ton univers est bizarre, ton ordinal $\omega$ est mal fondé". Il va te répondre : "Mais t'es malade, toi ! Donne-moi un exemple".  Tu vois kui sortir l'ordinal $\alpha$ ci-dessus. Là il va te rétorquer : "Mais t'es complètement à côté de la plaque, mon p'tit gars ! Moi je le vois, cet entier $\alpha$, et il n'a rien de bizarre ! Et pis d'abord arrête d'insulter mon $\omega$ !"
    En clair, un modèle non standard est incapable d'identifier sa partie standard.
  • Martial
    Martial
    Je pense aussi qu'il faut que tu arrêtes de parler de "l'ensemble intuitif des éléments de $\omega$". Ce truc ne veut rien dire.
  • Martial
    Martial
    C'est peut-être plus facile à voir avec une ultrapuissance. Soit $\mathscr U$ un ultrafiltre non principal sur $\omega$, et soit $(\mathbb{V}, \in)$ un modèle (standard ou non) de ZFC. On construit l'ultrapuissance $\mathbb{V}^\omega / \mathscr U$ de la façon suivante. Soient $u,v$ deux éléments de $\mathbb{V}^\omega$, i.e. deux suites d'éléments de $\mathbb{V}$. On dira que $u \sim v$ ssi $\{n \in \omega : u_n=v_n\} \in \mathscr U$. On construit alors l'ultrapuissance $\mathbb{V}^\omega$ comme le quotient de $\mathbb{V}^\omega$ par la relation $\sim$. On munit cette ultrapuissance d'une relation $\widetilde{\in}$ (que je note encore $\in$ pour simplifier) définie par $Cl(u) \in Cl(v)$ ssi $\{n \in \omega : u_n \in v_n\} \in \mathscr U$. Par le théorème de Los tu sais que l'ultrapuissance est élémentairement équivalente à $(\mathbb{V}, \in)$, donc en particulier elle satisfait ZFC.
    Maintenant, on identifie chaque entier $n$ avec la classe de la suite constante égale à $n$. Maintenant, on considère la suite $u=(1,2,3,...,n,...)$. Posons $X=\{n \in \omega : u_n >n\}$. On a clairement $X=[n+1,+ \infty[$, donc $X$ appartient au filtre de Fréchet, et en particulier $X \in \mathscr U$. Toujours par le théorème de Los, tu en déduis que $Cl(u)>Cl(n)$. Comme $n$ était arbitraire, $Cl(u)$ est non standard.
    Maintenant, tu considères la suite $v=(0,1,2,...,n-1,...)$, puis la suite $w=(0,0,1,2,...,n-2,...)$, puis $t=(0,0,0,1,...,n-3)$ etc. Le même argument que ci-dessus montre que
    $$Cl(u)>Cl(v)>Cl(w)>Cl(t)>...,$$
    et tu as bien construit une suite infinie décroissante d'entiers.
  • [Utilisateur supprimé]
    [Utilisateur supprimé]
    Modifié (July 2022)
    Martial a dit :
    Je pense aussi qu'il faut que tu arrêtes de parler de "l'ensemble intuitif des éléments de $\omega$". Ce truc ne veut rien dire.
    Merci @Martial pour la démo avec les ultrafiltres.
    Je suivrais ton conseil.
    Et oui, ce mélange entre les deux mondes m'a un peu chamboulé.


  • Foys
    Foys
    Le vrai phénomène choquant avec ces choses n'est pas tant d'avoir des modèles non standard; c'est d'avoir deux modèles élémentairement équivalents avec un "standard" on va dire et l'autre ouvertement non standard. Les habitants des deux mondes ont l'impression de voir la même chose!
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Martial
    Martial
    Modifié (July 2022)
    J'en rajoute une couche. (Pardon à @cohomologies si je mets la zizanie dans son cerveau). Pour moi la standardicité est une notion relative. Si on part du point de vue platonicien selon lequel on vit déjà dans un modèle $(\mathbb{V}, \in)$ de ZFC, d'un point de vue très anthropomorphique on va décréter que notre univers est standard. À partir de là, quand on "voit" un modèle de ZFC un peu chelou, comme l'ultrapuissance décrite ci-dessus, on est capables de décréter que celui-là est franchement non standard. Mais peut-être que juste au-dessus de nous il y a un petit malin qui se gausse bien de nos hures, car pour lui notre univers est non standard.
  • Cyrano
    Cyrano
    Modifié (May 2023)
    Salut Martial,

    Je lis ta section concernant l'intuitionnisme et le raisonnement par l'absurde. Tu dis que LI ne permet pas de prouver que $\neg \neg P \Rightarrow P$ puisqu'on ne dispose pas de la règle de contraposition dans le bon sens. Mais est-on capable de le (méta)prouver ? Autrement dit, a-t-on le métathéorème suivant : Il existe une proposition $P$ telle que $LI \nvdash \neg \neg P \Rightarrow P$ ?Mon idée est de prendre pour $P$ est une variable propositionnelle quelconque $p$ mais je n'arrive pas à le prouver.

    Merci. :-)
  • Alesha
    Alesha
    Cyrano, tu prends un modèle de LI, une proposition P et tu regardes l’interprétation de (non non P implique P) dans ce modèle.
  • Cyrano
    Cyrano
    @Alesha : En effet, je suis bête. Bon c'est juste qu'il faut d'abord démontrer le théorème de complétude de LI.  :D 
  • Foys
    Foys
    Modifié (May 2023)
    @Cyrano: Il existe une sémantique en termes d'espaces topologiques pour la logique intuitionniste. Soit $(X,\tau)$ un espace topologique. Etant donnés deux ouverts $A,B$, on pose $A \wedge B:= A \cap B$; $A \vee B:= A \cup B$ et $A \to B:=$ l'intérieur de $(X\backslash A) \cup B$. On pose $\top := X$, $\bot := \emptyset$ et enfin $\neg A:= A \to \bot$. Avec cette interprétation on peut montrer (par induction sans surprise sur la longueur de la preuve) que pour toutes formules $A_1,...,A_n, B$, s'il existe une démonstration intuitionniste propositionnelle (mettons en déduction naturelle) du séquent $A_1, ... , A_n \vdash B$, alors $A_1 \cap ... \cap A_n \subseteq B$ dans tous les espaces topologiques (et notamment si $B$ est un théorème intuitionniste sans hypothèses alors $B$ est l'espace $X$ tout entier dans l'interprétation ci-dessus).
    La plupart des théorèmes classiques mais non intuitionnistes simples comme $\neg \neg P \to P$ se réfutent en prenant $\R$ avec sa topologie usuelle et des intervalles (ici on prend juste $P:= ]0,+\infty[$).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Alesha
    Alesha
    Ce n'est pas plutôt la correction dont on a besoin? Le théorème de correction devrait dire que si (non non P implique P) était prouvable, alors son interprétation serait R (en considérant le modèle de Foys); or son interprétation n'est pas R.
  • Cyrano
    Cyrano
    Super merci. 

    Tiens autre question : de quoi $A \vee B$ est-il une abréviation en intuitionnisme ? (En supposant, comme le fait Martial, qu'on parte des symboles $\neg$ et $\Rightarrow$)
    En logique classique, si je pars de $\Rightarrow$ et $\neg$ alors $A \vee B := \neg A \Rightarrow B.$ Mais clairement ceci serait bizarre en intuitionnisme. En effet, $LI \vdash (P \Rightarrow P)$ pour toute formule $P$. En particulier $LI \vdash (\neg P \Rightarrow \neg P)$. Mais ceci serait identique à $LI \vdash P \vee \neg P$ avec l'abréviation habituelle. Donc LI prouverait le tiers-exclus. 
  • Foys
    Foys
    Modifié (May 2023)
    @Cyrano à part $\neg X:= X \to \perp$ il n'y a plus aucune de ces abréviations en logique propositionnelle ou du premier ordre (pour les raisons que tu cites; ou alors spécifiquement en théorie des ensembles du premier ordre grâce à des astuces imitant les règles ci-dessous; j'y reviendrai peut-être). En revanche en logique d'ordre supérieure (avec des types; dans les cas où on peut au moins quantifier sur les formules) on peut tout écrire avec seulement $\forall$ et $\to$, de la manière suivante (avec $A,B$ des formules; $Prop$ désignant le type des formules et $T$ un type quelconque):
    1°) $\perp:= \forall P:Prop, P$
    2°) $A \wedge B:= \forall P:Prop, (A \to (B \to P)) \to P$
    3°) $A \vee B:= \forall P:Prop, (A \to P) \to ((B\to P)\to P)$
    4°) $\neg A := A \to \perp$
    5°) $\exists x:T, F (x):= \forall P:Prop, (\forall x:T, (F(x) \to P)) \to P$.
    6°) $\top:= \perp \to \perp$
    7°) $x \overset T = y := \forall F: (T \longrightarrow Prop), F (x) \to F (y)$ (exo: montrer que cette relation binaire est symétrique et transitive)
    Il est instructif (et assez mécanique) de redémontrer toutes les règles d'inférences de la déduction naturelle intuitionniste à partir de ces définitions et des seules règles d'inférence portant sur l'usage de $\to$ et de $\forall$.
    D'autre part le simple axiome suivant entraîne la logique classique avec ces règles ("axiome de Peirce"): $\forall A:Prop, \forall B:Prop, ((A \to B ) \to A) \to A$.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Foys
    Modifié (May 2023)
    Moyen mnémotechnique: si on regarde bien, ces abréviations ont été choisies pour faire marcher les règles d'inférences correspondantes de la déduction naturelle (je ne pense pas que ce soit une coïncidence à ce stade :) ). Par exemple la définition de l'égalité au 7°) est bien sûr basée sur la propriété de Leibniz (deux objets sont égaux s'ils ont les mêmes propriétés; ici on fait figurer l'élimination de $=$ dans la définition même).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Martial
    Martial
    @Cyrano : Sorry, j'arrive un peu après la bagarre. Même si ta question initiale m'était destinée, @Foys, qui est largement plus compétent dans ce domaine, t'a apporté beaucoup plus d'informations que ce que j'aurais pu faire à sa place.
    J'avoue avoir un peu de mal avec ces questions, même si j'y ai consacré une longue section au chap 26 (section 12)... Mais il faut bien dire que @Foys m'a beaucoup aidé à l'époque. (D'ailleurs, je le remercie chaleureusement quelque part).
    En fait, dans tout ce que dit @Foys plus haut, le seul truc que je sais démontrer c'est que LI+Peirce $\vdash LC$. Ça fait pas bézef...
  • Cyrano
    Cyrano
    Modifié (May 2023)
    Ok merci à vous deux.
    Ce que je ne comprends pas Martial, c'est que tu définis les trois axiomes de LI en n'utilisant que $\neg$ et $\Rightarrow$. Foys semble dire que ça n'est pas suffisant du tout.
    Si je me réfère à cette page https://en.wikipedia.org/wiki/Intuitionistic_logic, $9$ axiomes sont utilisés.
  • Foys
    Foys
    En fait avec $\to$ et $\neg$ on ne peut pas exprimer à équivalence près toutes les formules. Regardons ce qui se passe dans les espaces topologiques (ou les énoncés sont interprétés par des ouverts).
    1°) Soit $X$ un espace topologique et $Y$ un ouvert de $X$. $\neg Y = Y \to \perp$ est l'intérieur du complémentaire de $Y$. En particulier si $Y$ est dense, $\neg Y = \perp = \emptyset$ puis $\neg \neg Y = X$.
    2°) Soient d'autre part $A,B$ deux ouverts de $X$;  Alors $B \subseteq A \to B$.
    Ces propriétés entraînent par induction sur la taille des formules propositionnelles que toute formule $F$ écrite sur deux variables propositionnelles $A$ et $B$ (interprétées par des ouverts *denses*) et seulement les connecteurs $\neg$ et $\to$, vérifie après identification l'une des trois conditions suivantes:
    (i) $F=\emptyset$
    (ii) $A \subseteq F$
    (iii) $B \subseteq F$.

    Lorsqu'on prend $X:= \R$, $A:= \R \backslash \{0\}$ et $B:= \R \backslash \{1\}$, on voit donc qu'il est impossible que $A\wedge B$ ($= A \cap B$ après interprétation) soit intuitionnistiquement équivalent à un énoncé écrit uniquement avec $\to$ et $\neg$.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Foys
    Modifié (May 2023)
    En revanche il est possible d'exhiber, pour des sous-ensembles de formules écrites en restreignant l'usage des connecteurs, des systèmes de preuves qui démontrent tous les théorème parmi ces formules. Cela provient de ce que le calcul des séquents intuitionniste possède la propriété d'élimination des coupures (voir un cours de théorie de la démonstration, par exemple David-Nour-Raffali) dont la conséquence importante ici est la suivante: pour toute démonstration (intuitionniste) d'une formule $F$ de logique du premier ordre, il existe une preuve intuitionniste de cette même formule qui ne contient que des sous-formules de $F$ (dans le cas de la logique du premier ordre, sous formule après remplacement de certaines variables par des termes du langage). Ainsi une formule écrite avec juste $\neg$ et $\to$ qui est prouvable, l'est aussi avec des formules écrites uniquement avec $\neg$ et $\to$.

    Un système d'axiomes pour des preuves à la Hilbert pour un tel système (dans cet exemple je traite le cas propositionnel) peut être:
    (i) $(A \to (B \to C)) \to ((A \to B ) \to (A \to C))$
    (ii) $A \to (B \to A)$
    (iii) $(A \to B ) \to ((\neg B ) \to (\neg A ))$
    (iv) $A \to ((\neg A ) \to B )$
    avec pour règles de raisonnement le modus ponens et le remplacement de variables propositionnelles par d'autres formules dans des formules déjà démontrées.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Martial
    Martial
    @Cyrano : ce que tu lis au chap 4 n'est qu'une esquisse de la LI. Les détails sont explicités au chap 26, section 12.
  • Foys
    Foys
    Pour faire bref ce qui est perdu en limitant l'ensemble des connecteurs employés est l'expressivité du langage, mais pas la capacité à prouver.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Cyrano
    Cyrano
    Ok là c'est parfaitement clair.  ;)
  • Cyrano
    Cyrano
    Modifié (May 2023)
    Bonjour,

    Je truste le fil de Martial pour mes questions mais, en même temps, elles me viennent en lisant son livre.  :p 
    Soit $N$ le modèle standard de Peano et $N'$ le modèle non-standard obtenu en rajoutant le symbole $c$ plus grand que tous les autres éléments (argument par compacité). Comment montrer que $N$ et $N'$ sont élémentairement équivalents ? Il me semble clair que $N \vDash \varphi$ implique $N' \vDash \varphi$ car il suffit de recopier la preuve. Mais l'autre sens est moins évident. Il faudrait montrer que le symbole $c$ n'est intervenu à aucun moment dans la preuve de $\varphi$ dans $N'.$
  • Martial
    Martial
    @Cyrano : Il n'y a a priori aucune raison pour que $N$ et $N'$ soient élémentairement équivalents. Notons $Th(\mathbb{N})$ la théorie complète de $\mathbb{N}$, c'est-à-dire l'ensemble de tous les énoncés au premier ordre qui sont vrais dans la structure $N=(\mathbb{N}, 0, S, +, \times, \leq)$. $N$ et $N'$ sont tous deux modèles de Peano, donc ils satisfont toutes les conséquences de Peano. Mais la théorie complète de $\mathbb{N}$ est "beaucoup plus grosse" que l'ensemble des conséquences de Peano. En effet, tu sais par Gödel qu'il existe des énoncés qui sont vrais dans $N$ mais non prouvables dans Peano. Soit $\sigma$ un tel énoncé. Par complétude il existe un modèle de Peano, disons $N''$, qui satisfait $\neg \sigma$. On a donc $N \models \sigma$ et $N'' \models \neg \sigma$, donc $N$ et $N''$ ne sont pas élémentairement équivalents.
    En conclusion tu ne pourras pas démontrer que $N' \equiv N$, puisque c'est faux en général. En fait ce qu'il faut comprendre c'est que l'argument dans la preuve du théorème $39$ est purement modèle-théorique : il te prouve l'existence d'un modèle non standard par compacité, mais ne te donne aucun moyen effectif de construire un tel modèle "à la main". Et il en va de même des constructions à l'aide d'ultrapuissances exposées dans la section suivante... pour la bonne raison que personne ne sait fabriquer à la main un ultrafiltre non principal sur $\mathbb{N}$.
  • Martial
    Martial
    Pour info, j'ai développé un peu l'étude des modèles non standard de Peano au Chapitre 26, à propos de l'analyse non standard : voir la sous-sous-section 15.6.2. Si tu lis la description faite dans ce paragraphe tu comprendras aisément que cela ne doit pas être tout à fait évident de fabriquer de façon effective un modèle non standard de Peano. Toute la difficulté consiste à définir les opérations : il y a $2^{\aleph_0}$ façons de le faire, mais laquelle choisir ?
  • Médiat_Suprème
    Médiat_Suprème
    En fait, c'est impossible : théorème de Tennenbaum.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Poirot
    Poirot
    @Martial Est-ce que tu comptes un jour publier ton livre chez un éditeur ?
  • Thierry Poma
    Thierry Poma
    @Poirot : bonjour. Bonjour à Martial également. Ce serait bien ; je serais l'un des premiers à l'acheter.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Martial
    Martial
    @Médiat_Suprème : Merci pour l'info. Je m'en doutais un peu, même si je n'ai aucune idée de la façon dont ça se démontre. As-tu par hasard une référence sous la main ?
    @Poirot : comme je l'ai dit plus haut mon livre est terminé. J'en suis à la phase relecture, et dès que j'ai fini je me mets en quête d'un éditeur. Ça ne va pas être particulièrement trivial, dans la mesure où à la louche le pavé pèse 2500 pages en pdf. (Donc au mieux il faudrait envisager une publication en 5 ou 6 volumes)...Enfin, si quelqu'un a des pistes éditoriales je suis preneur.
    Bonjour @Thierry Poma. Merci pour ton soutien.
  • Martial
    Martial
    Je viens de réaliser que de la discussion ci-dessus on pouvait dériver une preuve triviale d'un fait dont je connaissais l'existence mais dont j'ignorais la démonstration.
    Fait : Il existe des modèles non standard de Peano qui ne sont pas isomorphes à une ultrapuissance de $\mathbb{N}$.
    Preuve : On sait par le théorème de Los que toute ultrapuissance est élémentairement équivalente à $\mathbb{N}$. Or, le modèle $N''$ auquel il est fait allusion plus haut n'est pas élémentairement équivalent à $\mathbb{N}$, donc il n'est pas isomorphe à une ultrapuissance.
    Cerise sur le gôto : via Löwenheim-Skolem on peut même s'offrir le supplément qu'il existe un tel modèle dénombrable.
  • Cyrano
    Cyrano
    @Martial : Je comprends ce que tu dis mais je posais la question dans le cadre d'un modèle non standard très particulier : $\N$ + un infiniment grand. J'ai toujours entendu dire que ce modèle non-standard ne permettait pas de prouver plus de théorèmes sur le langage de base que $\N$ lui-même.

    Voir par exemple ce fil MSE : https://math.stackexchange.com/questions/3069333/elementary-equivalence-of-standard-and-non-standard-model-of-arithmetic où cette proposition est réaffirmée (mais sans preuve).
  • Médiat_Suprème
    Médiat_Suprème
    Modifié (May 2023)
    Désolé @Martial, mais dans un document que j'avais écrit sur l'arithmétique, je cite ce théorème, avec la remarque : 

    La démonstration est un peu trop technique pour trouver sa place ici, mais on peut la trouver sur le net.

    Il y a des infos là : Tennenbaum's theorem - Wikipedia
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Martial
    Martial
    @Médiat_Suprème : Merci pour le lien.
    @Cyrano : OK, j'ai compris ta question. Tu sais qu'il y a des modèles de PA qui sont non e.e. à $N$, mais tu veux savoir pourquoi le modèle particulier $N'$ l'est. Là, il faut que je réfléchisse à la question.
    En attendant, si j'ai bien compris ce que dit Eric Wofsey, les modèles $N$ et $N'$ ne sont pas e.e. dans le langage étendu par un symbole de constante $c$, mais ils le deviennent dans le langage de base.
  • Thierry Poma
    Thierry Poma
    Modifié (May 2023)
    @Martial : tu peux peut-être envisager de t'entretenir prioritairement avec les éditions Calvage & Mounet, voire avec les éditions Hermann. C'est déjà un bon début.
    Je pense aussi aux relecteurs ; il te faut des relecteurs. Je veux bien être du nombre, sachant que je suis chiant... A toi de décider.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Foys
    Foys
    Modifié (May 2023)
    @Cyrano je ne vois pas trop comment la théorie des modèles aborde directement ce problème (sans passer par la théorie de la démonstration: si $F$ est vraie dans tous les modèles non standards de $\N$ alors $F$ est vraie dans $\N$, qui est conséquence directe de ce qui va suivre) mais le résultat suivant est syntaxiquement évident :
    Peano + $\{c > \mathbf t\mid \mathbf t \in D\}$ (l'arithmétique non standard élémentaire avec $c$ non standard) est conservative sur Peano (ici $c$ est une nouvelle constante ne figurant pas dans le langage de Peano (i.e. $c$ est une lettre et $c\neq 0$ et $c\neq 1$) et $D$ est l'ensemble de tous les termes construits avec $s,+,\times, 0,1$).
    En effet soit $A$ un énoncé dans lequel ne figure pas $c$. Si par exemple $P_1,\dots,P_{389}$ est mettons une preuve en $389$ lignes de $A$ dans
    Peano $+\{c > \mathbf t|\mathbf t \in D\}$ avec $A=P_{389}$, cette preuve n'utilise qu'un nombre fini d'axiomes de la forme $c > \mathbf t$ et par exemple, le plus grand tel $\mathbf t$ apparaissant dans la preuve va être $2481$. On remplace partout dans cette preuve la lettre $c$ par $2482$ et les invocations des axiomes $c> \mathbf t$ employés par des preuves de $2482 > \mathbf t$ et on obtient une preuve en bonne et due forme de $A$ dans Peano.
    Ce résultat de conservativité est en fait algorithmique.
    Smullyan en donne une version amusante et assez géniale dans un de ses livres.
    Vous êtes dans un pays magique avec un ensemble infini dénombrable de banques $B_1,B_2,B_3,B_4,\dots$ Une entreprise vous remet un chèque de 500 000 euros pour avoir accompli un travail particulièrement difficile (par exemple convaincre un quidam "FDP" des bonnes vertus d'une économie de marché libre). Le chèque comporte la mention suivante : "nous garantissons que ce chèque est encaissable dans au moins une banque".
    Afin de récupérer votre paie, vous vous dirigez vers la banque $B_1$ et on vous dit "non Monsieur nous ne faisons pas ce service mais d'autres banques pourront vous aider". Puis $B_2$ : "nous ne payons plus ce genre de chèque". Puis $B_3$ : "Allez vers une autre banque"...
    Après 17687 refus un sentiment fort d'entourloupe vous saisit et vous envisagez plutôt de vous adresser à un juge. Le problème est le suivant.
    Comment vous prouvez que vous vous êtes fait escroquer ?
    Même après 8 millions d'essais infructueux, le chèque pourrait être encaissable à la banque n° $10^{14}$ !!!
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Cyrano
    Cyrano
    @Foys : Ok pour la preuve syntaxique qui est relativement triviale. Merci. :-)
    Par contre je ne comprends pas encore le "paradoxe" des banques. :p
  • Martial
    Martial
    @Foys : Bien joué ! J'avais bien pensé à quelque chose comme le 3ème paragraphe de ton post, mais je n'arrivais pas à le formaliser correctement.
    @Thierry : Merci pour ton aide. Je vais réfléchir à la question.
    @Cyrano : En fait il n'y a pas de paradoxe. Si tu choisis tes banques au hasard et si tu as le temps d'en visiter 778944 avant la fin de validité du chèque, la probabilité que tu encaisses tes sous est de $778944/\infty$, c'est-à-dire $0$. Mais le juge tranchera toujours en faveur de l'entreprise, qui après tout n'a pas menti (en tous cas pas de façon prouvable). En fait c'est de ta faute, tu n'avais qu'à aller frapper tout de suite à la bonne banque.
  • Foys
    Foys
    Modifié (May 2023)
    Foys a dit :
    @Cyrano je ne vois pas trop comment la théorie des modèles aborde directement ce problème (sans passer par la théorie de la démonstration: si $F$ est vraie dans tous les modèles non standards de $\N$ alors $F$ est vraie dans $\N$, qui est conséquence directe de ce qui va suivre) mais le résultat suivant est syntaxiquement évident :
    En fait si il y a un moyen simple... il suffit de contraposer mon affirmation et utiliser le théorème de compacité tout bêtement: si $\neg F + Peano + \{c > k\mid k \leq n\}$ possède un modèle pour tout $n$ alors $\neg F + Peano + \{c > k\mid k \in \N\}$ en possède également un.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Médiat_Suprème
    Médiat_Suprème
    Il y a un principe tout à fait général, quand une théorie possède un schéma d'axiomes pour la définir, de toute façon, chaque démonstration n'utilise qu'un nombre fini des axiomes du schéma (c'est-à-dire un axiome) ; attention, cela ne veut pas dire que toute théorie est finiment axiomatisable.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Rambert
    Rambert
    Bonjour Martial

    Super livre
    Par contre c'est typographié un peu petit 
  • Martial
    Martial
    @Rambert : merci pour ton appréciation.
    Police 12 tu trouves ça petit ? Déjà que le bouquin fait 2700 pages, si j'augmente la taille de la police je vais me faire trucider par n'importe quel éditeur potentiel...
  • Rambert
    Rambert
    Modifié (July 2023)
    Martial 
    Ça devrait aller sur tablette..
    Si je trouve le temps d'en travailler l'entièreté genre 1 ou 2 chapitre(s)/an ça me prendra entre 10 et 20 ans 😊
    [Inutile de recopier le dernier message. AD]
  • Georges Abitbol
    Georges Abitbol
    Modifié (July 2023)
    Déjà que le bouquin fait 2700 pages, si j'augmente la taille de la police je vais me faire trucider par n'importe quel éditeur potentiel...

    Ben, tu n'as qu'à faire une série ! Il y avait les Berger de géométrie, les deux/trois Rudin d'analyse, il y aura les 13 Martial (Martiaux ?)

  • Boécien
    Boécien
    Et pourquoi pas vu la taille tenter une publication sous forme d'un "ebook" en français chez Springer?
  • Martial
    Martial
    @Georges Abitbol : J'envisage une publication en 4 volumes.
    @Boécien : je ne suis pas trop tenté par un ebook. Il y a beaucoup de gens (sur ce forum et ailleurs) qui pour l'instant ont accès gratos à ma prose, mais qui préféreraient avoir dans les mains un livre physique. Le Tout-Numérique n'a pas encore réussi à tuer le vrai livre.
  • Martial
    Martial
    A propos du Tout-Numérique : j'ai un ami qui a acheté la première version du livre de Patrick Dehornoy quand il est sorti, fin 2017. Pendant l'été 2018 il se promène dans Lille et entre par hasard dans une librairie généraliste, i.e. pas spécialisée math. Il y découvre 3 exemplaires de la deuxième version du livre. Il hésite un peu. A tout hasard il parcourt la préface. En conclusion il y découvre la conclusion, où Patrick nous élève, un autre lecteur et moi-même, au statut de "redoutable chasseur de coquilles". Réaction de mon ami : "Il cite Martial, donc j'achète son livre".
    Je ne sais pas pourquoi j'ai attendu un certain temps pour raconter l'anecdote à Patrick. (J'ai dû le faire environ 2 mois avant son décès). Sa réponse a été : "Ton copain est un bon copain". Il s'est ensuite épanché sur le fait que c'était très bien que 3 exemplaires de son livre soient exposés dans une librairie de province. Pour lui c'était beaucoup plus important qu'un traînaillage sur Internet. CQFD.
  • umrk
    umrk
    Modifié (July 2023)
    J'aime à penser qu'il nous regarde, de là-haut ...
    https://vimeo.com/205778279
    D'autres clips, sur sa page perso :
    https://www.lmno.cnrs.fr/archives/dehornoy/perso.html
  • Martial
    Martial
    @umrk : merci pour ces liens.
  • umrk
    umrk
    Modifié (July 2023)
    @Martial : en référence (et en hommage)  à son Clip d'hommage à Jacques Stern ("La Normandie"), j'espère que tu traites en détail la question du "continu restreint de Luzin" !
  • Martial
    Martial
    @umrk : peut-être que je le traite sans le savoir. S'il s'agit du théorème selon lequel les analytiques vérifient HC, alors oui, j'en cause.
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 13

AmadouCongru +11 Invités