Les meilleures news - Page 264

./7889> Humm, il serait ptet plus juste de dire que toute propriété arithmétique universelle est intuitivement vraie (=elle est vraie pour les entiers intuitifs).

C'est le cas de la propriété de Gödel (qu'il a construite pour la preuve de son théorème d'incomplétude)

(cross)

./7890 > je me disais bien qu'il y avait un problème , même si je ne l'avais pas vu aussi précisément ça me semblait créer un peu trop de propositions vraies ce raisonnement

--- bon vais vérifier qq chose d'abord ---

http://www.dailymotion.com/relevance/search/sarkozy%2Bfrance3/video/x5yyb9_sarkozy-en-off-sur-france-3_news

on sauve comment les vidéos sur dm, avant qu'elle soit virée?

#squalyl#

./7894 > en les sauvegardant avant qu'elles ne soient virées, puisqu'on aura déjà été informé ( ./7821 )

old #squalyl# is squalyl, j'ai toujours du lag avec les news et triscience m'a dégouté des liens dailymotion

./7889> Bon voilà, derrière tout ça il y a en profondeur une histoire de vérification algorithmique.

Soit (P) une proposition arithmétique universelle, de la forme "Pour tout entier n, P(n)", où, pour chaque n, P(n) est vérifiable en temps fini (ya un algorithme qui termine, toussa toussa).

Supposons que (P) soit indémontrable, alors le programme qui cherche un contre exemple à (P) en faisant une boucle infini ne s'arrêtera jamais, et cela constitue une preuve de la véracité de (P).

Donc pour une telle proposition (P),
(P) indécidable => (P)
(P) indécidable => "(P) indécidable" est indécidable.

De même toute proposition arithmétique existentielle (P), où P(n) est testable en temps fini, est fausse si elle est indécidable, et son indécidabilité est alors elle même indécidable.



Les hypothèses ne s'appliquent pas :
- à l'axiome du choix, l'hypothèse du continu, etc... : on ne peut pas faire un programme qui boucle sur les ensembles ; ce ne sont pas des propriétés arithmétiques.
- à un truc comme le théorème de goodstein, ou la suite de Syracuse : P(n) n'est pas vérifiable en temps fini

Par contre elle s'appliquent :
- à la conjecture de Goldbach
- et sans doute aussi à l'hypothèse de riemann

OK, donc la substantifique moelle du ./7886 était « il existe des propositions indécidables qui sont nécessairement vraies »...
(donc Gödel a prouvé qu'il existe de telles propositions (P) c'est bien ça ?)

bon je n'aime pas les algorithmes qui prouvent des trucs en ne s'arrêtant jamais, donc je reformule : « Supposons que (P) soit fausse, alors l'algorithme trouvera un contre-exemple en temps fini, donc (P) est décidable. » Ça va mieux tout de suite

mais n'empêche que si la proposition est indécidable, ça veut dire que je peux la supposer fausse sans qu'il soit possible d'en déduire une contradiction, donc le système reste cohérent avec cette hypothèse Par conséquent, pourquoi dit-on que la proposition est vraie ?
en fait elle est « intuitivement » vraie sans être « logiquement » vraie ?

...
bon évidemment comme je ne peux pas savoir si elle est indécidable je ne peux pas savoir non plus si j'ai le droit de rajouter cette hypothèse, donc en pratique je ne peux en fait pas le faire...

Sally (./7899) :
mais n'empêche que si la proposition est indécidable, ça veut dire que je peux la supposer fausse sans qu'il soit possible d'en déduire une contradiction, donc le système reste cohérent avec cette hypothèse Par conséquent, pourquoi dit-on que la proposition est vraie ?
en fait elle est « intuitivement » vraie sans être « logiquement » vraie ?

Si tu décrètes qu'elle est fausse elle sera juste fausse sur quelques entiers "bizarres" qui sont inclus dans ton modèle parce que tes axiomes ne modélisent pas bien les entiers "intuitifs".

Mais j'imagine qu'on doit de toute façon pas pouvoir prouver l'indécidabilité avec ces axiomes (ou alors ça voudrait dire que le schéma d'axiomes "pour toute (P) universelle, (P) indécidable => (P)" permet de prouver strictement plus de choses ? quoi qu'il en soit ça ne ferait que repousser le problème d'un cran, parce qu'on ne pourra jamais prouver l'indécidabilité avec ces nouveaux axiomes)

Sally (./7899) :
en fait elle est « intuitivement » vraie sans être « logiquement » vraie ?

Elle est sémantiquement vraie sans être démontrable ( == "logiquement vraie" ), non ?

Ca me retourne quand même bien la tête cette remarque de Sally.

Alors que tout simplement elle doit être vraie pour tout entier standard, et c'est tout.

La France veut construire un deuxième EPR et pousser toujours plus loin le retraitement des déchets nucléaires http://fr.news.yahoo.com/afp/20080703/tsc-energie-nucleaire-environnement-prev-c2ff8aa.html
very > « sémantiquement »
hippo > ben la phrase que j'ai rajoutée ensuite à la fin de mon post m'a aussi aidé à me remettre la tête à peu près à l'endroit, aussi bizarre que ça puisse paraître ^^

Et bien sûr Greenpeace pense que les éoliennes et les barrages c'est mieux, si seulement on avait des torrents partout sur terre pour avoir plein de barrages...

Mais j'y pense, et si on installait des lacs artificiels partout ?

étrangement, ils ne proposent rien en échange typiquement écolo, comme attitude ^^

ben ca coute cher, c'est pas evident, faut avoir de l'eau ( si t'as trois goutes qui s'evaporent .. ), un sol qui_va_bien dans sa composition et sa geographie, ..

Et ca modifie evidemment pas mal l'environement naturel ( les barages filtrent certaines especes et certains trucs aui font que l'eau n'est plus vraiment la meme, ... )

Bref sauf au Quebec ou dans des coins propices c'est pas evident

Sally (./7903) :
very > « sémantiquement »

Ben le vrai et le faux sont des notions semantiques qui sont differentes de notions de prouvabilité ( évidemment quand on construit un modèle on cherche a ce que tout ce qui soit prouvable soit vrai, sauf a vouloir que tout ce qui soit vrai soit prouvable, mais on peut pas avoir les deux à la foi, sauf avec un model incoherent ... )

very (./7906) :
faut avoir de l'eau

Viendez tous habiter en Écosse avec moi, chassons tous ces répugnants moutons couverts de tiques \o/ (ou bouffons-les ! \o/)
./7907 > ah oui ok, c'est ce que j'appelle « intuitivement »

( quoique quand on regarde la theorie des modeles ( l'espect semantique) c'est pas toujours très intuitif au premier abord, mais bon )

The_CUrE (./7904) :
Et bien sûr Greenpeace pense que les éoliennes et les barrages c'est mieux, si seulement on avait des torrents partout sur terre pour avoir plein de barrages...

Mais j'y pense, et si on installait des lacs artificiels partout ?

Ouais, faisons comme en Chine \o/

hippo > c'est quoi au juste un entier standard ?

un entier du modèle standard de l'arithmétique

qui est?

un entier ISO ?

dualmoo (./7914) :
qui est?

T'as le langage de niveau 0, le langage intuitif dans lequel on parle.
On y discute en particulier d'un système arithmétique axiomatique, dont les phrases forment le langage de niveau 1.

Le modèle standard de ce système axiomatique, c'est l'ensemble des entiers du niveau 0.

Flanker (./7915) :
un entier ISO ?

t1 mais...

erf parfois vous êtes vraiment trop geek pour moi

Ah écoute, on a les qualités qu'on peut, hein