Paradoxe d'Épiménide/tiers exclu
Bonjours à tous !
En cette veille de bac de philo je suis tombé sur ce petit article sur des propositions ni vrais ni fausses.
Pour simplifier les choses on a qu'à dire que les menteurs mentent tout le temps et les véridiques disent tout le temps la vérité.
Autant ils ont raison de dire que Épiménide ne peux pas dire la vérité parce que voila ça nous amène à une contradiction évidente.
Mais par contre j'ai l'impression que ce n'est pas dutout un paradoxe, Épiménide peut très bien être un menteur, et donc la phrase qu'il énonce est fausse donc la négation de cette phrase c'est à dire : "Il existe au moins un crétois qui n'est pas un menteur" est vrai.
Qu'en pensez-vous ?
En cette veille de bac de philo je suis tombé sur ce petit article sur des propositions ni vrais ni fausses.
Pour simplifier les choses on a qu'à dire que les menteurs mentent tout le temps et les véridiques disent tout le temps la vérité.
Autant ils ont raison de dire que Épiménide ne peux pas dire la vérité parce que voila ça nous amène à une contradiction évidente.
Mais par contre j'ai l'impression que ce n'est pas dutout un paradoxe, Épiménide peut très bien être un menteur, et donc la phrase qu'il énonce est fausse donc la négation de cette phrase c'est à dire : "Il existe au moins un crétois qui n'est pas un menteur" est vrai.
Qu'en pensez-vous ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Dans celui que tu montres, s'il ment, alors il existe des Crétois non menteurs, comme tu le dis, et en effet cela n'apporte rien à rien. Un Crétois qui dit "Les Crétois mentent tout le temps" est simplement un Crétois qui s'avère être un menteur.
D'ailleurs comme tu peux le remarquer, le livre justifie sa première affirmation (que la personne qui dit ça ne peut pas dire la verité), mais pas la seconde
La phrase obtenue en recopiant le texte entre guillemets ci-après une fois sans guillemets, suivi d'un deux-points, suivi du même texte entre guillemets et enfin suivi d'un point final, est une phrase fausse: "La phrase obtenue en recopiant le texte entre guillemets ci-après une fois sans guillemets, suivi d'un deux-points, suivi du même texte entre guillemets et enfin suivi d'un point final, est une phrase fausse".
Noter qu'on peut très facilement construire d'autres phrases auto-référentes (et les paradoxes qui vont avec), il suffit de remplacer "fausse" par n'importe quel adjectif ou propriété: "improuvable", "non écrite sur cette page", "improuvable en moins de 100 000 pages", "entraîne l'existence du père noël si elle est vraie", "entraîne l'existence de Superman si elle est prouvable" etc etc.
C'est la réalisation de l'énoncé ci-dessus dans un langage formel (ex: les mathématiques) qui a permis a Gödel d'établir ses célèbres résultats d'incomplétude.
Je rappelle le théorème: en notant cette phrase $A$, on obtient $A=(A\to P)$, donc $A\to (A\to P)$, donc $A\to P$, donc $A$, donc $P$. Autrement dit, sa simple existence suffit à donner une preuve de $P$ (et rappelons que la preuve est intuitionniste, car un préjugé populaire chez de trop nombreux enseignants, énoncé que ça a un rapport avec le raisonnement par l'absurde, or il n'en est rien).
Il y a des fils sur le forum où j'ai éliminé les faiblesses qui restent encore ici et où on voit qu'il n'y a pas de "réponse bisounours" à ces techniques de preuves. Je rappelle rapidement de quoi il s'agit:
Admettons que $W:=(\forall X: (Prouvable (X) \to X ) )$ et $P := Prouvable ( P \to [W \to A] ) $. Alors un exercice routinier et sans rien de caché sous le tapis, prouve que $W\to A$.
Cette version est la partie "efficace"*** du théorème de Cantor-Godel-Russel-Epiménide disons, puisqu'elle montre que c'est un théorème de science qu'il existe des choses à la fois prouvables et fausses** (on n'en a pas encore trouvées d'intéressantes et concrètes, mais on a d'autres chats à fouetter avec le quantique etc par exemple).
** sauf à renoncer à certains attendus de la science que l'on utilise tous les jours.
*** il est trop souvent diffusé sous une forme dégradée qui est que toute théorie (capable de gérer les entiers) exprimant et prouvant sa propre consistance est contradictoire
J'essaie de comprendre ce théorème :
Il existe des énoncés prouvables et faux.
Je suis tombé sur une "preuve" que vous avez fait sur ce forum il y a quelques temps : http://www.les-mathematiques.net/phorum/read.php?2,733122,page=1
Ce que je ne comprend pas trop c'est la supposition de départ :
Il existe un énoncé P équivalent à : il est prouvable que W=> non P
Comment peut on partir de cette supposition ?
Enfin de toute façon pour donner un sens à ça il faudrait donner une définition de la vérité, qui n'existe pas.
C'est un procédé devenu courant et dont Godel a marqué le début. C'est techniquement un peu long à détailler et je surveille le bac (et la canicule a conduit des candidats de nos salles à l'hôpital), mais je te donne le principe général: on peut "programmer" d'une manière qui s'appelle "programmation fonctionnelle", ce qui conduit à utiliser des fonctions de fonctions de fonctions autant qu'on veut et toutes les fonctions s'appliquent à elles-mêmes, etc. On peut "facilement" prouver que cette méthode de programmation est universelle et équivalente aux styles dits plus "impératifs", enfin bref. Une fois tout ça implémenté, tu peux taper:
ce qui te donne une "fonction" (au sens informatique du terme) telle que quand tu prends
tu obtiens que
Ce n'est donc pas ça le problème ou la "magie introduite" dans le raisonnement, car ça, c'est de la routine. Cette routine est d'ailleurs due à un point technique très important, évident aujourd'hui mais que Godel a contribué à diffuser au public, et on n'imagine pas à quel point le public l'ignorait, les époque anciennes sont difficiles à "ressentir", c'est que "être prouvable" est une notion mathématique, parfaitement bien définie et même plus simple que l'ensemble des nombres premiers (ie l'ensembles des preuves est un ensemble bien plus simple que l'ensemble des nombres premiers).
Avant Godel, il y a des tas de gens qui ne pensaient pas (non pas qu'ils le niaient, mais ils ne l'envisageaient pas) que l'ensemble des preuves de maths est un ensemble parfaitement trivial (si on les avait interviewer, plein auraient répondu "ah bah non, l'ensemble des preuves de maths est un ensemble subtil, difficile à cerner"). Même aujourd'hui, d'ailleurs, les non-matheux pensent que l'ensemble des preuves de maths n'est pas "basique", ni programmable. Seuls les matheux savent qu'un logiciel qui arbitre les maths est un truc très simple et qu'il ne existe plein
Ce qui fait la magie du raisonnement, c'est plutôt la présence de $W$ au troisième ordre (second ordre, mais avec un prédicat)
En fait il y a des problèmes quand on veut vraiment formaliser cette preuve.
Par exemple le fait que X->Prouvable(X) qui est douteux (ou alors il faut renoncer au théorème de déduction et inventer une règle d'inférence ad-hoc pour dire que si $\vdash X$ alors $\vdash Prouvable X$.
ait une valeur de vérité, puisque la formule $<<A := Prouvable (A\to (W\to P))>>$, quant à elle, ne pose pas de difficulté.
Par contre, ton histoire de $[ [Prouvable(S)] \to [Prouvable [Prouvable(S)]] $ n'est pas un problème, et d'ailleurs c'est un peu étonnant, toi qui as fait de la correspondance de Curry-Howard récemment, que tu ne le remarques pas (enfin tu as peut-être posté très vite) immédiatement.
<< Z est prouvable >> est juste une abréviation <<il existe E tel que E est évident et E=>Z est évident>> et je te laisse définir "être évident".
Cela dit, je me trompe peut-être sur ton intention (en ayant compris que tu parlais de demX => dem dem X et que tu avais oublié un "dem" en tapant vite), peut-être voulais -tu réellement parler de <<X => prouvable X>>? :-S, mais dans ce cas-là, tu aurais fais une encore plus grosse coquille car je n'ai jamais évoqué ça
Si ta coquille est d'avoir confondu avec ( Prouvable X ) =>X alors je ne vois pas où est le problème, personne n'a jamais parlé de le prouver, c'est une hypothèse bête et méchante.
Bref, je ne sais pas quelle coquille tu as faite, du coup j'ai envisagé celles qui me paraissent les plus probable.
En fait j'ai l'impression que tu fais comme si la théorie étudiée et la "métathéorie" dans laquelle on se place pour faire le raisonnement étaient les mêmes.
Pour ce qui est de la preuve que j'ai déjà donnée maintes fois, je peux te la retaper, mais tu l'avais déjà acceptée dans le passé me semble-t-il?
[[Supposons A.
Supposons W.
Alors Prouvable (A=>(W=>P)) ;
Donc , comme W, donc A=>(W=>P)
Donc, comme A, donc W=>P
Donc, comme W, donc P]]
On vient de prouver que A=>(W=>P) (je te laisse construire le terme du LC correspondant, qui est vraiment très simple)
On a donc Prouvable (A=>(W=>P) ) , c'est à dire A. On peut donc recommencer ce qui précède, mais sans supposer A, puisqu'on l'a.
Finalement W=>P
Le langage de la théorie des ensembles va me servir provisoirement de méta-langue:
considérons:
un ensemble $\mathcal E$ de "formules";
une partie $\mathcal T\subseteq \mathcal E$ appelée mettons "ensemble des théorèmes";
une fonction $\overline{implique}: \mathcal E\times \mathcal E\to \mathcal E$;
une fonction $\overline{prouvable}:\mathcal E\to \mathcal E$;
Si on dit que $X\in \mathcal E$ est prouvable quand $X\in \mathcal T$, alors "prouvable" n'est pas $\overline{prouvable}$ et implique n'est pas $\overline{implique}$.
Et on est en présence de trois choses distinctes:
1°) le méta-énoncé $\forall X\in\mathcal E:X \in \mathcal T \implies \overline{prouvable} (X)\in \mathcal T$.
2°) le méta-énoncé $\forall Y\in \mathcal E: \overline{implique} \left( \overline{prouvable} (Y),\overline{prouvable}\big(\overline{prouvable} (Y)\big)\right) \in \mathcal T$
3°) le méta-énoncé $\forall Z \in \mathcal E: \overline{implique}\left(Z,\overline{prouvable}(Z)\right) \in \mathcal T$
Par exemple dans mon précédent message ce que j'ai voulu dire est que dans les exemples usuels où ces considérations s'appliquent, 1°) est généralement assez trivialement vrai, 2°) est pénible mais vrai.
Mais 3°) ?????
De plus, même s'il existe $W\in \mathcal E$ tel que pour tout $X$, $\overline{implique}\left[W,\overline{implique}\left( \overline{prouvable}(X),X\right)\right]\in \mathcal T$ et qu'il s'avère que pour tout $Y\in \mathcal E$, $\overline{implique}(W,Y)\in \mathcal T$, je ne vois pas comment tu peux en déduire $\mathcal T=\mathcal E$.
J'ajouterai derniers détails (triviaux) d'un PC. Il n'y a aucune metamaths dans ce que j'ai raconté c'est purement formel (j'ai juste laissé en exercice un point sans intérêt).
Mais si ça peut t'aider sache que si je pensais annoncer un GROS truc je le ferai sur HAL pas sur le forum!! Ce que je suppose EST TRES FORT mais cash: l'existence de W. Mais le reste ne pose pas de problème. Bref je ne resumais pas le théorème de Gödel "canal historique" attention à ce malentendu (dont je porte la responsabilité!!)
J'utilise les abréviations suivantes (crochets ont statut de parenthèses, $<<\to>>$ abrège "implique"):
$<<D(X)>>$ abrège $<<Prouvable (X)>>$
$W:= [\forall X: ((D(X))\to X)]$
Je suppose que $A = (D(A\to (W\to \perp)))$
Lemme: A.
Preuve: $D(W\to (A\to (A\to (W\to \perp)))$ donc
$D(W\to (A\to (W\to \perp)))$ donc
$D(A\to (W\to (W\to \perp)))$ donc
$D(A\to (W\to \perp))$
Théorème: $W\to \perp$
Preuve: supposons $W$
on a déjà prouvé A, donc $(A\to (W\to \perp))$ (car $D(A\to (W\to \perp))$)
donc $W\to (A\to \perp)$
donc $A\to \perp$
donc $\perp$ (car $A$).
J'imagine qu'on a $D(W\to[$$D(A\to (W \to \perp)$$ \to A\to (W \to \perp)])$ (pourquoi?) et que cela est censé entraîner: $D(W\to$$A$$\to A\to W \to\perp)$ malheureusement les objets syntaxiques rouges et verts ne sont pas a priori interchangeables.
[size=x-small]j'ai mis la priorité des parenthèses à droite[/size].
Non non j'ai bien supposé A EGAL blabla.
Je detaillerai d'un PC pourquoi ce n'est pas si audacieux que ça. Et je répète je m'étonne que ce ne soit pas W que tu critiques. Car mon traitement de A est "essentiellement" l'apport de Gödel mais je detaillerai.