Paradoxe de l'interro surprise
Bonjour et bonne année...
Je m'interroge sur le soi disant paradoxe de l'interro surprise..Le raisonnement classique c'est :si l'interro n'a pas eu lieu vendredi soir alors etc... Mais un si a toujours deux faces, il faut rajouter : si l'interro a eu lieu avant vendredi, eh bien elle était surprise et il n'y a pas de paradoxe.
Où est mon erreur ?
Amicalement.
Jean-Louis.
P.S. Par contre j'aimerais bien une explication "philosophique" des paradoxes de Zénon...
Je m'interroge sur le soi disant paradoxe de l'interro surprise..Le raisonnement classique c'est :si l'interro n'a pas eu lieu vendredi soir alors etc... Mais un si a toujours deux faces, il faut rajouter : si l'interro a eu lieu avant vendredi, eh bien elle était surprise et il n'y a pas de paradoxe.
Où est mon erreur ?
Amicalement.
Jean-Louis.
P.S. Par contre j'aimerais bien une explication "philosophique" des paradoxes de Zénon...
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
-- Schnoebelen, Philippe
En fait là où ça ne marche pas c'est qu'il faut pousser ce raisonnement jusqu'au bout: puisqu'elle ne sera pas une surprise, le prof a menti. Mais en admettant que le prof puisse avoir menti, les élèves n'ont aucun moyen de savoir si elle aura lieu ou non...
Si non, voici un lien vers une présentation du paradoxe de l'interro-surprise :
https://fr.wikipedia.org/wiki/Paradoxe_de_l'interrogation_surprise
[Edit : Paf m'a griller ]
si elle n'a pas eu lieu avant vendredi alors elle ne sera pas une surprise, ce qui est une contradiction.
Donc on peut en déduire qu'elle aura lieu avant vendredi (simple raisonnement par l'absurde, il n'est pas question ici de "si bifaces").
Mais en réitérant ceci on arrive au fait qu'elle n'aura pas lieu, d'où le paradoxe.
La "surprise" change au cours de leur raisonnement en fait. Une fois qu'ils ont raisonné à propos de vendredi, la présence d'une interrogation le vendredi devient une surprise. S'ils n'y avaient pas pensé, faire une interrogation le vendredi ne les aurait pas surpris, et le plan du professeur aurait échoué. Mais puisqu'ils y ont réfléchi, et qu'ils ont éliminé chaque jour, chaque jour devient un potentiel jour de surprise
-premier cas: le prof a dit "tant que l'interro n'aura pas eu lieu, vous ne pourrez pas prouver que ce ne sera pas une interro surprise"
Si elle n'a pas eu lieu avant vendredi, les élèves peuvent prouver qu'elle aura lieu vendredi ou qu'elle n'aura pas lieu, et dans les deux cas ce n'est pas une surprise.
En réitérant l'argument, ils peuvent prouver que l'interro ne sera pas une surprise. Donc ils peuvent prouver une contradiction: la théorie du prof est contradictoire. En particulier, elle ne leur apprend rien sur ce qui va vraiment se passer.
-deuxième cas: le prof a dit "tant que l'interro n'aura pas eu lieu, vous ne pourrez pas être certains que ce ne sera pas une surprise". Cette fois-ci, les élèves ne peuvent pas être certains que le prof n'a pas menti...
deux vidéos youtube que j'avais trouvées assez claires sur le sujet :
épisode 1
épisode 2.
En 2017, je ne comprends pas pourquoi trop de personnes disent encore des phrases comme ça ne marche pas à propos d'un paradoxe de maths. Tout marche, même celui de Zénon. Il faut juste accorder au raconteur du paradoxe (voir à ses lecteurs) leurs hypothèses.
Dire "ça ne marche pas" sous-entend qu'on essaie d'identifier UNE des hypothèses qui serait plus douteuses que les autres. Mais je trouve que ce n'est pas tellement à encourager comme réflexe puisque, parfois, 4 ou 5 hypothèses peuvent être autant douteuses et peu douteuses. L'exemple typique en maths, c'est AD et AC. Ce sont deux axiomes incompatibles, mais dont il est très difficile de réellement dire lequel on a envie de garder au détriment de l'autre. Et là, il n'y a pas d'affaire de "paradoxe" pour les enfants, mais bel et bien un pur théorème et une pure hésitation finale.
Bien sûr beaucoup de gens préfèrent aujourd'hui AC, pour cause de popularité, mais bon.
Dans le présent paradoxe, c'est un peu pareil, vous avez une preuve de 0=1 à la fin et tout plein d'hypothèses. Je l'aime bien parce qu'il n'y en pas tellement une qui est spécialement "plus une escroquerie" que l'autre. J'ai souvent donné d'ailleurs une version améliorée de ce paradoxe sur le forum, mais orienté vers les maths. Le revoici pour la énième fois:
Un père de famille négligent ne surveille pas son enfant. L'enfant tombe à l'eau et hélas, un crocodile magique habite l'étang. Il capture l'enfant et dit au père: $<<$ tu dois dire une phrase, et si elle est fausse je te rends ton enfant, sinon, je ne te le rends pas$>>$.
Il est classique que si le père dit $<<$ tu vas me rendre l'enfant$>>$, le crocodile ne pourra pas respecter sa propre règle. C'est le paradoxe bien connu "cette phrase est fausse" mais présentée dans un contexte où on évite l'auto-référence et où on n'utilise que des phrases sans problème. Ici ce qui fait marcher le truc est que le père utilise le futur.
Très bien. Alors si c'est le futur qui est en cause, corsons la tâche du père. Le crocodile dit $<<$ tu n'as PAS le droit d'utiliser le futur, de manière directe ou indirecte. tu dois dire une phrase dont la vérité ne dépend pas de ce que je ferai$>>$.
Avec une telle contrainte, on a bien l'impression que le crocodile pourra DANS TOUS LES CAS respecter sa propre règle.
Et bien non... Le père dit
$<<$ je peux prouver que en utilisant comme hypothèse que tout ce qui est prouvé est vrai (et si ça concerne le futur, que ça arrivera), et bien sûr que tu es invincible à ce jeu que tu ne vas pas me rendre l'enfant $>>$.
Le crocodile ne peut évidemment pas répondre puisque le père a respecté la règle. Et bien le crocodile rend l'enfant au père (et admet pour le coup qu'il existe des choses qui sont prouvables et fausses), sinon il ne respecte pas sa règle.
Il n'existe aucune échappatoire** à ce paradoxe (j'en ai donné maintes versions formelles dans des fils moins "vulgarisant"), ou bien il existe des choses prouvables et fausses ou bien la dernière phrase évoquée et prononcée par le père dépend .... du futur. Dans les deux cas la conclusion est pour le moins .. surprenante. A noter que ça fait longtemps d'ailleurs que ce théorème est APPLIQUE (sans vraiment le dire comme ça, mais c'est le même terme informatique qui réalise sa substance) dans diverses branches de la science (en MQ et dans les "algèbres de Johnsson")
** cela provient non pas de la vérité des hypothèses, mais du fait qu'il n'y en pas UNE plus qu'une autre qui est facile à rejeter.
(Bon c'était juste une remarque en passant. Pour la vidéo1, il est clair sociologiquement que la plupart des gens diront "bin si mettre le joker en deuxième carte est une surprise". Je les regarderai entièrement si des intervenants interviennent en faveur de ces vidéos, je ne voudrais pas avoir loupé quelque chose)
(Moi je dirais "rends l'enfant sinon c'est la cc".)
S
De mon téléphone
De mon téléphone (Pi est "je mets le DST le i ieme jour")
Si la seule contrainte est de dire une phrase fausse, il suffit de déclarer par exemple "Tu es une lampe à souder."
@axone : bien sur que non les axiomes peuvent être faux et pour ceux qui utilisent des règles de déduction elles peuvent bugguer. Dans le cas présent (celui du fil) tu en as d'ailleurs un parfait exemple. La plupart des béotiens voient un paradoxe et commettent la GROSSE FAUTE math d'essayer de le résoudre alors qu'on est face à un théorème et sa preuve tous deux pourtant limpides. Le dirlo donne l'interro le jour 4 alors que ses étudiants posent sur son bureau le matin même une preuve (dans T * ) que le DST aura lieu et viole ainsi sa propre promesse. J'aimerais que tu me dises en quoi on dispose d'une preuve scientifique générale que les dirlos ne mentent pas ou tiennent leurs promesses.
La théorie T est constituée des promesses du dirlo +quelques techniques formelles incontestables sur les propriétés du prédicat "est prouvable". Par ailleurs le dirlo a tout à fait le loisir de tenir une de ses promesses : ne pas donner le DST (mais il viole alors celle qu'il en donnera un). La notion de "surprise" je le répète n'a rien à faire ici elle permet juste de commenter psychologiquement les impression que "T est fausse"
DE MON TÉLÉPHONE
Si j'ai bien lu, un intervenant a posté "le prof a menti". A part ça, il ne les effleure pas que etc.
On peut très bien (d'ailleurs c'est ce que tu répètes sans arrêt avec ton petit programme bleu) considérer chaque règle comme un axiome et faire des preuves qui n'utilisent que le modus ponens. Donc s'il existe une phrase prouvée mais pas vraie alors soit il existe un axiome pas vrai, soit effectivement c'est le modus ponens qui déconne. Et ça c'est valable pour n'importe quel théorie, pas juste celle de l'interro surprise (qui n'est pas cohérente, donc bon).
Autrement dit, si ton petit slogan est vrai, n'importe quel système d'axiome suffisamment expressif est faux... (mais alors même parler de vrai et de faux n'a plus tellement de sens me semble-il).
1) Quand je dis "ne les effleure pas", cela signifie juste que les gens présentent ça comme un paradoxe qu'il faut "résoudre" et ne le formalisent pas, ou alors le formalisent mal
2) La plupart du temps, ils font référence, quand ils formalisent, aux axiomes: $non(P_7)$, donc $P_1\vee P_2...\vee P_6$, donc $nonP_6$, etc et c'est ça qui leur fait dire que le dirlo a menti (donc il font une faute de "formalisation", le dirlo n'ayant jamais promis ces choses-là
3) Le modus ponens est juste un mot pour dire que $(A\to
4) Comme tu peux d'ailleurs le voir, aucun des liens (wikipedia dit à peu près n'importe quoi, et le gars mis en lien par michael tombe encore plus gravement dans le HS) ne fournit d'analyse correcte de cette contine. De plus, le gars de michael "en profite" pour faire le pédago qui prétend tenir là un "raisonnement par récurrence" (il faut tout de même rappeler que pour prouver que $7 \in \N$ on n'en a pas besoin (de l'axiome de récurrence) )
5) Puisque je suis sur un pc, je donne une explicitation avec $4$, flemme d'aller jusqu'à 7. J'abrège par $D$ "est prouvable" et je traduis les promesses du prof (pardon je l'ai appelé le dirlo dans mes posts d’avant car je connaissais la version sous la forme d'un directeur d'école qui donne une interro) dans la version précise qu'on m'a raconté (wiki ne se donne même pas la peine et l'orateur du lien de michael non plus, c'est bien tristounet en maths).
5.1) En français le dirlo dit: $<<$ j'annule le DS si vous venez me voir le matin avec une preuve que je vais le mettre l'après-mdi (commentaire: au nom de l'adage "ce ne serait pas une surprise") $>>$
5.2) C'est ç ale contrat (en plus de la promesse de faire une et une seule fois une interro )
5.3) La traduction FIDELE est donc:
a) $P_1\vee P_2\vee P_3\vee P_4$
b) $(dem [non(P_1\vee P_2\vee P3) \to P_4]) \to non(P_4)$
c) $(dem [non(P_1\vee P_2) \to P_3]) \to non(P_3)$
d) $(dem [non(P_1) \to P_2]) \to non(P_2)$
e) $dem(P_1)\to non(P_1)$
f) Tous les axiomes habituels de fonctionnement de $D$ (donc entre autre $D(X\to Y) \to [D(X)\to D(Y)]$, etc
5.4) Exercice: produire une preuve (formelle) dans cette théorie que $non(P_2)$. Aller la poser sur le bureau du prof le mardi. Attendre. S'il met un DST alors il trahit les élèves.
Maintenant, libre à chacun de considérer qu'il ne promet pas tant, etc, etc. Mais je le répète, l'exercice est un exercice DE MATHS et il est facile à faire. Et je le répète aussi, la promesse du dirlo n'est pas
$$[non(P_1\vee P_2) \to P_3] \to non(P_3)$$
mais bel et bien
$$(dem [non(P_1\vee P_2) \to P_3]) \to non(P_3)$$
Le discours e wikipedia est donc de particulièrement mauvaise qualité sur ce coup-là, car il évoque un "raisonnement" pas du tout valable qu'un gamin ferait dans sa tête sans rapport avec la promesse. De plus, tout change si le dirlo dit "attention, vous ne pourrez me proposer qu'une seule fois de lire votre preuve"
Exactement, c'est d'ailleurs bien connu et exprimable sous plusieurs formes + ou - équivalentes phisophiquement.
formes possibles ou "adages" (ce n'est pas un slogan, c'est prouvé) alternatifs:
1) pas de liberté et de complétude en même temps (liberté au sens de groupe libre), sauf à se limiter au fini.
2) l'axiome "tout ce qui est prouvable est vrai" entraine tout ce qu'on veut, sauf dans les théories peu expressives où godéliser n'est pas possible
3) Tout algèbre de Boole se plonge dans une algèbre de Boole dénombrablement engendrée
4) Presque tout réel est EN DEHORS de l'univers
5) Toute théorie générique (au sens du forcing) affirme qu'il existe des entiers infinis
etc
Menfin ici, je rappelle que la contine du fil ne mobilise pas tout ça non plus. :-D
1) pour tout entier $n: v_n<w_n$
2) pour tout entier $n: v_n$ est la position du lapin à l'instant $u_n$
3) pour tout entier $n: w_n$ est la position du tortue à l'instant $u_n$
4) $u$ est sitrctement croissante
Et l'auteur de Zénon en INFERE que le lapin ne rattrape jamais la tortue. Autement dit, il fait comme si pour tout instant $t: $ il existe un entier $n$ tel que $u_n\geq t$.
Bon là ce n'est pas n'importe quel système qui est faux, mais uniquement ceux qui sont assez intéressant. Donc... rien d'intéressant n'existe?
Ouais, bon, vu ta définition de preuve, tout slogan peut être prouvé (en prenant lui-même comme axiome), donc tu ne m'impressionnes pas.
"Tu ne peux pas me rendre mon enfant" gagne.
Si on craint une entourloupe de l'adversaire, "Tu ne peux pas me rendre mon enfant car tu ne le détiens pas, il est à la maison et joue avec ses copains".
-Il y a deux joueurs Alice et Bob.
-Le perdant s'engage à donner 1 000 euros au gagnant.
-Dimanche Bob donne une enveloppe cachetée à un huissier (réputé infaillible), contenant un jour de la semaine (désigné par x dans la suite). Le jeu se déroule toute la semaine suivante.
-Le jour x de la semaine choisi par Bob, l'huissier annonce publiquement "le jour choisi par Bob est aujourd'hui".
-Alice doit, un jour de la semaine (désigné par t dans la suite), annoncer à l'huissier un jour de la semaine de son choix (désigné par y dans la suite... Alice a droit à une seule proposition et perd si elle n'en fournit pas).
-Alice gagne si t<x et si x=y. Sinon Bob gagne.
1°) Quelles sont les stratégies optimales pour les deux joueurs?
2°) Alice peut-elle gagner infailliblement?
3°) Comment modifier les règles de ce jeu pour qu'il corresponde à la situation du paradoxe dit de "l'interrogation surprise", i.e. pour qu'Alice puisse gagner infailliblement?
Il me semble (avis personnel) qu'une "vraie" situation d'interro surprise, c'est ce qui est décrit dans le jeu ci-dessus.
Le plus dégourdi fronce les sourcils et dit :
- M'sieur vous mentez !
- Ah bon Octave ? Et pourquoi donc ?
- Parce que (il a quand même fait de la logique (classique) des séquents et connaît la règle d'élimination du "ou"), soit vous ne faites pas l'interrogation et vous mentez, soit vous la faites, et je peux le savoir, donc vous mentez dans tous les cas !
- Ah Bon ? Et si je la fais, comment peux-tu le savoir ?
- Mais M'sieur ! ... Parce que vous avez commencé par dire que vous la ferez !
La matinée passe, à la pause midi les enfants rassurés s'empiffrent de nuggets au lieu de réviser, et l'après-midi, c'est bien sûr l'interrogation. Le prof a-t-il menti ?
Bien sûr que non !
Moralité de l'histoire, qui peut servir aussi aux grandes personnes :
À l'instant t, ne pensons pas savoir qu'un événement E se produira à un instant ultérieur t' uniquement parce que quelqu'un nous l'a dit, fût-il professeur, voire pire, homme politique !
C'est une expression étrange qui est normalement utilisé quand quelqu'un te dit dans un bar "wech Roger, tu vas voir, je suis capable de tenir en équilibre sur un seul doigt" :-S
Encore heureux qu'en rappelant ces banalités, je ne t'impressionne pas, c'est le contraire qui serait surprenant. Mais tout de même, je tiens à répéter que les vulgarisations du godélisme sont parfois trop insistantes sur des détails et pas assez sur l'essentiel. Par exemple, on force les gens à retenir que Gödel a prouvé $non(D(nonD(\perp))$ au lieu de leur dire qu'il a prouvé "essentiellement" $\exists X: [D(X)\wedge non(X)]$, ecs rappels ne sont donc pas inutiles (beaucoup de personne croient que c'est "un slogan" quand je rappelle le deuxième point, à cause justement, du fait qu'on diffuse trop le premier, peu significatif)
@foys: je redis que la première fois que j'ai entendu cette histoire, elle était présentée avec une précision quand-même plus sérieuse que ce qu'on lit dans le fil et ses liens. J'ai un peu la flemme, mais ça donnait: $<<$ un dirlo va mettre une interro un (et un seul !!) jour de la semaine prochaine entre Lundi et Samedi inclus. Il promet aussi que chaque matin, si le délégué de classe se présente avec une preuve (qui admet les promesses présentes comme axiomes bien sûr) que le DST aura lieu l'après-midi même, il annule ledit DST$>>$
Cette version, plutôt formelle, permet de conclure, qu'on peut prouver à partir de la promesse faite que pour chaque jour de la semaine, il existe une preuve que le DST aura lieu ce jour. Et c'est tout. La récurrence n'a rien à voir la dedans (clin d’œil superficiel au mieux), il n'y a pas "d'erreur" dans le fait que si le dirlo met le DST le mercredi, le certificat posé sur son bureau le matin par le délégué "ne devrait pas être là" non plus. C'est vraiment une banale illustration de la différence entre "certificats" et réalités. Dire que c'est un paradoxe est aussi un peu exagéré, car on a une théorie formellement contradictoire.
[Kurt Gödel (1906-1978) prend toujours une majuscule ! AD]
[Inutile de recopier l'avant dernier message. Un lien suffit. AD]
-$dem(W\to (P\to \perp))$ contient strictement plus de caractères que $P$ donc ne peut pas lui être égale (bon, équivalente suffit certes).
-La plupart des théories de maths sont du premier ordre. Celles d'ordre supérieures font intervenir des types, des sortes etc et des problèmes aparaissent.
-Dès qu'on met le moindre typage dans le formalisme, la rédaction de cette preuve devient irréalisable (comment construire le point fixe associé?); impossible d'appliquer les objets qu'on veut à d'autres objets qu'on veut.
Si on s'autorise des souplesses formelles par militantisme ("mais vous savez, la cause est juste"), pas besoin d'aller chercher aussi loin: on balance "si cette phrase est vraie alors il y a des éléphants volants autour de la tour Eiffel" et le tour est joué. Bon j'ai vérifié, il n'y en a pas; le formalisme mathématique a vocation à valider des énoncés qui se produisent en vrai... Si des gens travaillent à produire des formalismes bridés c'est dans ce but et non pas par avachissement personnel.
Le discours humain peut potentiellement décrire de la magie mais le monde n'est pas magique.
chistophe c, si tu exhibes enfin une fois pour toutes dans les règles ce fameux type vide qui est non vide, les gens te croiront (moi aussi). Mais les "ils sont tous bêtes" et autres "acceptez mes abus de langage" n'ont pas à être crus sur parole.
Mais il n'en reste pas moins que tu passes à cote du fait majeur malgré ça que c'est la réalisation de l'absence de futur face à l'objection du crocodile (voir plus haut) autrement dit ton "... Éléphants.." est fautif comme objection. Il y a un progrès entre la première phrase du père et la deuxième. Tu as sauté ce point la en beauté.
Quant à ta reformulation, c'est au mieux une interprétation subjective, si ce n'est une déformation.
Autre chose: $\mathbb N$ est un modèle de PA dans lequel tout ce qui est prouvable est vrai... Alors...
On peut aller plus loin: ce que tu montres, c'est qu'en admettant certains axiomes, il existe un axiome faux... Bon ben la conclusion est assez évidente ce me semble: tu as admis un axiome faux.
Moi qui croyais que c'était justement ça, un paradoxe.
Pour la devinette des yeux verts, je me souviens que c'était sur un fil qui parlait de MQ. Flemme de chercher, mais je peux le reposter (mais plus tard).
http://www.les-mathematiques.net/phorum/posting.php
concernant $\exists X: (D(X) \wedge non(X))$, je te (et je vous) laisse "tirer dessus" autant que vous voulez après tout, ce n'est pas à moi de décréter que vous devriez (foys, toi, etc) en faire un "livre de chevet" :-D
Par contre, j'ai peur qu'à tirer, vous ne passiez à côté de choses que justement vous-mêmes ne voudriez pas forcément négliger, à un autre moment de votre vie.
Encore une fois, (je vais me forcer à te répondre un peu différemment qu'à foys, comme ça, il y aura deux choix de réponses), en disant "toi cc qui décides que... mais Godel...", je pense que tu peux empêcher des lecteurs de prêter attention au caractère uniforme de son argument, alors même que c'est bien la seule chose qui en fasse un résultat "à vie" pour la science. Ma présentation, certes abstraite, est peut-être un peu "violente", mais elle ne fait que rappeler cette uniformité** (et elle se programme très bien et se réalise très bien en CCH).
Merci pour avoir retrouvé le lien en tout cas, je pense que les lecteurs qui ne connaissaient pas ton histoire vont se régaler.
** il y a un $\forall theorie\ T: ....$
Je t'invite aussi à lire ce que j'ai répondu à foys.
Certes, on peut répondre ça à n'importe quelle argumentation. Ce n'est pas mon propos. Mon propos est de dire que les hypothèses suivantes:
H1) $\forall X: D(X)\to X$ (je l'abrège par $W$)
H2) $\exists P: P=D(non(W\wedge P))$
sont contradictoires avec des axiomes que tout le monde accepte concernant $D$.
L'objection de foys n'est d'ailleurs pas du tout la même que toi. Il dit juste qu'il ne sait pas plonger dans un système connu ce calcul.
Je te propose de me dire, non pas, que ce n'est pas une preuve dans Peano ou dans ZFC, mais quel(s) axiome(s) tu estimes faux.
Remarque: j'ai des cartouches que je n'ai jamais publiées sur le forum car assez longues: je sais remplacer "D", par "A" où D(X) signifie "X est prouvable" et A(X) signifie "X est un axiome", et ce depuis des années que j'ai "fait tourner" ce truc sous caml. (Attention, le remplacement change aussi ce qu'on utilise, ie, je ne fais bien sûr pas fonctionner A comme D). Mais en gros, le "doute" ne se situe:
a) ni dans le fonctionnement de D
b) ni dans l'existence de P (c'est l'informatique triviale)
Il ne reste pas grand chose, car dire "W n'existe pas" (ie s'autoriser à affirmer ou même à écrire H1) revient au même que dire ce que je dis. Concernant "l'audace" que j'utilise dans ce formalisme, contrairement à ce que vous avez l'air de dire foys et toi par exemple, il n'y a absolument rien qui ne soit déjà présent comme même types d'audaces dans nos pratiques habituelles (peano, ZF, etc). La seule chose qu'on ne peut que constater sans avoir d'explication c'est que pour l'heure ils n'ont pas été cassés, mais certainement pas qu'ils n'utilisent pas les mêmes "audaces" ou "auto-références". Mais je suis ouvert à tout.
Concernant ta remarque sur Peano prouve truc alors IN models truc, ça n'a rien à voir. Si tu veux faire la comparaison, il faut parler de la plus petite théorie récursive $T$ qui contient Peano, ainsi que tous les énoncés $(T\vdash X)\to X$. Et bien cette théorie (parfaitement claire et limpide, etc) est, comme tu le sais contradictoire. Encore une fois, je renvoie au crocodile: on n'est pas face à la même nature de mécanisme quand on remarque que c'est un théorème que $(A\iff (A\to
En fait, ce qu'il se passe, c'est que par exemple si on ajoute ZF à ces axiomes, on obtient une bien réelle contradiction "pure et dure". Mais sinon, il faut remplacer le mot axiome par le mot évidence, si on se limite à l'interprétation "primitive" sans ajout d'objets mathématiques pour analyser. Voici pourquoi:
1) il y a 2 définitions (équivalentes) de théorèmes:
1.1) $<<P$ est un théorème$>>$ abrège $<<$ il existe une suite finie d'axiomes $A_1,..,A_n$ telles que $A_1;..;A_n\vdash P$ est un axiome$>>$
1.2) $<<P$ est un théorème$>>$ abrège $<<$ il existe une évidence $X$ telle que $X\to P$ est évident$>>$
1.Fin) Dans (1.1) tu as besoin de savoir ce que veut dire suite finie. Dans la deuxième ou bien tu considères comme déjà donné ce que veut dire évident et c'est là que tu "as raison", ou bien tu as besoin de donner une définition du mot "évidence", mais tu es alors ramené à enrichir ta théorie de manière à pouvoir le faire: $<<$ ensemble des évidences$>>$ abrège $<<$ plus petit ensemble stable par les conjonctions contenant les axiomes$>>$.
2) Attention, dans ce qui précède, j'utilise l'abus de langage suivant: $<<X;L\vdash Y>>$ est une abréviation de $X\to Q>>$ où $Q$ est la phrase que $L\vdash Y$ abrège. Il n'y a que $\to$ qui est primitif, les autres mots clés sont DEFINIS ou apparaissent accompagnés d'axiomes qui annoncent leurs fonctionnement.
Du coup le mot conjonction signifie:
2.1) ou bien être de la forme $(L\vdash P)\to P$. Dans ce cas on dit qu'on a conjoncté les éléments de la liste $L$
2.2) ou bien être de la forme $\forall xA$, ou de la forme $\forall X:A$
3) Le point sensible est qu'un algorithme qui va vérifier si un énoncé est une évidence peut ne pas terminer: en effet, prenant X en paramètre, il dresse la liste des items conjonctés, puis doit vérifier (récursivement) pour chacun si eux-mêmes sont des évidences.
4) Ton diagnostic, est donc, dit sèchement, "faux" dans le sens que (mais il faut exécuter la CCH sur l'argument pour le voir) qu'en fait il n'y a pas d'axiome faux, mais juste un bouclage sur les énoncés mal fondés dont l'analyse récursive ne parvient pas à falsifier que ce sont des évidences, mais ne terminent non plus définitivement sur la conclusion que c'en sont. C'est ce que foys ressent inconsciemment quand il réagit (il ressent qu'il ne parvient pas à "bien fonder" l'enjeu).
5.1) Mais attention: ces défauts sont exactement les mêmes que ceux déjà présents dans nos théories, c'est à dire qu'aucune de nos théories ne présentent un avantage sur le présent mécanisme et rien d'objectif ne permet d'expliquer pourquoi elles semblent en apparence consistantes alors qu'on a une preuve en quelques lignes de la contradiction de la présente. C'est totalement subjectivo-religieux de croire*** à leur consistance (et expérimentale: elles ont résisté). C'est d'ailleurs initialement pour ça que j'ai inventé cet argument, pas pour améliorer le crocodile.
5.2) Cependant: la version crocodile présente un avantage certain, puisque tout y est parfaitement concret et clair. Et personne n'est capable de trouver un bug, une fois évacué bien sûr, le défaut de l'utilisation du futur. En d'autres termes, cet argument (mais il faut un peu méditer pour le comprendre) est simplement une preuve irréfutable (et formelle) qu'une preuve peut ne pas exister en 1894 mais se mettre à exister en 2049, autrement dit que l'absolu (ou en 1681!!) mathématique "évolue" avec le temps. Mais comme cet aspect de la science n'est évidemment jamais utilisé de manière sensible, les discussions se sont peu développées en dehors des salons philo (où les acteurs ne sont pas compétents techniquement, donc ne font qu'échanger des poncifs vagues)
*** remarque: je n'y crois pas, je pense, je l'ai souvent dit, que Peano est contradictoire.
*** si $A$ est un cas particulier de $B$, alors évidemment $B\to A$ est évident, mais en général la réciproque n'est pas du tout vraie, tu peux très bien avoir que $X\to Y$ soit une évidence ou même un axiome logique sans pour autant que $Y$ soit un cas particulier de $X$.
$<<U$ est un cas particulier de $V>>$ ne signifie pas seulement qu'à partir d'une preuve (avec hypothèses éventuelles) de $V$, on peut mécaniquement construire une preuve de $U$. C'est une abréviation de :
Rappel: $W:= [\forall X: (D(X) \to X)]$ (en français: tout ce qui est prouvable (à partir d'axiomes vrais) est vrai
Tu pourrais le faire seul, mais je fais l'effort (très pénible :-D) de t'écrire la version avec $E$ à la place de $D$, où on souhaite interpréter $E(X)$ comme $<<X$ est évident$>>$.
J'abrège par $\perp$ l'énoncé $\forall X: X$
J'abrège par $W$, maintenant, l'énoncé $\forall X, Y: E(X\to Y) \to (E(X)\to Y)$
et par $P$ l'énoncé $\forall X: (E(X\to (W\to P)) \to (E(X)\to \perp))$
Pour chaque $X$, on a comme cas particulier de $W$ que : $E(X\to (W\to P)) \to (E(X) \to (W\to P))$, donc
$$ W\to [E(X\to (W\to P)) \to (E(X) \to (W\to P)] $$
est évident. Or cet énoncé est l'énoncé:
$$ W\to [E(X\to (W\to P)) \to (E(X) \to (W\to [\forall Y: E(Y\to (W\to P)) \to (E(Y)\to \perp)])] $$
ce qui en abrégeant, je te laisse le faire, donne l'énoncé évident $A$ tel que $A\to (W\to P)$ aussi est évident. Il suit que si $E(A)$ et $E(A\to (W\to P))$ alors $\perp$.
Donc tu es contraint, il n'y a pas de portes de sortie, d'admettre que $E(A\to (W\to P))\to (E(A) \to (W\to \perp))$. De plus, tu ne peux que reconnaitre que prétendre qu'on a juste prouvé $(nonW)\vee(non(E(A)))\vee non(E(A\to (W\to P)))$ serait assez de la mauvaise foi, les deux items de droites (après le non) étant parfaitement et formellement d'une évidence qui se regarde à l'oeil nu sans problème.
Je rappelle que, contrairement aux apparences, $P$ n'est pas une autoréférence*** (dire qu'une fonction constante a un point fixe n'est pas très audacieux). Par contre, bien évidemment, l'énoncé $W$ (sa seule existence même) est sulfureuse.
*** on peut le croire visuellement car je n'ai pas alourdi en mettant les suites de caractères dans un autre alphabet pour signifier qu'on les traite comme telles. Mais l'énoncé $P$ est un banal énoncé arithmétique
Le prof dit à ses élèves: Si ZFC prouve la cohérence de 1)+2), on est ramené au problème précédent et on a vu qu'il est contradictoire. Donc ZFC ne prouve pas la cohérence de 1)+2). Mais alors, les élèves ne peuvent pas faire annuler l'interro, donc 1)+2) est cohérente.
Faut-il comprendre que $dem = D$ :-D ? Et as-tu oublié les axiomes pour $i$ et $j$ quelconques mais différents $P_i \Rightarrow non(P_j)$ pour dire que l'interro n'a lieu qu'une seule fois ?
1/ on a une preuve qu'elle n'a pas lieu le dernier jour.
2/ De cette preuve, on déduit une preuve qu'elle n'a pas lieu l'avant-dernier jour en passant par une preuve que si elle n'a pas eu lieu avant, et comme par (1) elle n'aura pas lieu demain, c'est qu'elle a lieu aujourd'hui
3/ De cette preuve, on déduit une preuve qu'elle n'a pas lieu l'avant-avant-dernier jour en passant ..............
etc etc
98437/ ...... le premier jour.
Il suit qu'on a une preuve qu'elle n'a jamais lieu.
Si le prof décide d'en mettre une le mercredi, et la met, cela signifie qu'il renonce à sa promesse de ne pas en mettre si on lui apporte une preuve qu'elle a lieu le mercredi. Il n'y a rien de bien "mystérieux" ici et je trouve étonnant que ça ait fait tant causer ces dernières décennies.