![[Télécharger]](/extension/ag_design/design/light/images/html/icon_world_link.png "Télécharger"){kind=icon}
Passer en vue forum
Version d'archive
- Ce site est en lecture seule. Certains liens dynamiques peuvent ne pas fonctionner correctement.
1 + 1 n'est pas forcément égal à 2
5 commentaires
Que cache cette affirmation erronée ? Une question bien plus fondamentale.
Ha ha, démontrer que 1 + 1 = 2, en voilà un exercice qu'il va être rapidement expédié 
Alors ça va être strictement incompréhensible mais tant pis.
Il existe un entier naturel initial qu'on va appeler O
On a une notation qui désigne l'entier suivant d'un entier n , c'est S n
On s'accorde sur le fait que 1 c'est l'entier suivant O , c'est-à-dire S O
C'est le cas bâtard où Coq est super docile et va faire la démonstration pour nous.
Rassurez-vous ça ne se reproduira pas.
Copie d'écran :
C:> coqtop
Welcome to Coq 8.3pl2 (avril 2011)
Coq < Eval compute in S O + S O.
= 2
: nat
On a bien S O + S O = 2 , ce qu'il fallait démonter.
© Ok, je suis pris en flagrant délit d'étalage gerbant de ma culture, car en fait il y avait beaucoup moins pédant :
Coq < Eval compute in 1 + 1.
= 2
: nat
J'allais dire "c'est pas une science exacte comme les maths", mais je suis plus sûr de rien en la matière depuis qu'un prof m'a démontré que 1+1 n'était pas forcément égal à 2.
Aie Aie Aie. Il y aurait donc une démonstration de 1 + 1 ≠ 2.
Ben alors on est bien dans la ( démonstration de ) merde.
Alors les maths détiennent la vérité ?
En voilà une question plus intéressante.
Je vais essayer de rester très borné donc très technique (zéro philosophie, que du matheux psycho-rigidifié).
Je vais considérer (arbitrairement) que la vérité c'est tout ce que je peux démontrer en Coq.
Remarquez: c'est très très limité comme définition. Par exemple Coq ne me dira jamais si le capitaine Dreyfus était coupable de haute trahison ou non.
Mais bon, bon an mal an, si je me satisfais de cette restriction, est-ce qu'au moins je suis certain de n'atteindre que des vérités vraies aussi dures et froides qu'un rail de chemin de fer en Sibérie ?
Coq admet un axiome (une formule qu'on ne peut pas démontrer en Coq) :
⊥ = ∀ q ∈ Ω, q
En français: il est faux que tous les énoncés sont vrais
Conclusion: il vous suffit d'affirmer que cet axiome c'est du pipeau (parce que pas démontré) pour que toute la crédibilité de Coq s'effondre. En quelque sorte le programmeur Coq a la foi que cet axiome est juste . Dans le cas contraire il n'aurait foi dans aucun résultat que lui fournirait Coq.
En résumé: on ne peut pas concevoir que quelque chose est vrai sans avoir foi en quelque chose qui, aussi évident soit-il, n'est pas démontré.
Les derniers commentaires
Putain, je crois avoir compris !!
Ratatusk il y a plus de 11 ans
Bien pensé mais si on suit correctement la démonstration le mec divise un moment par zéro (ce qui est bien évidement interdit), quelqu'un le dit d'ailleurs dans les commentaires, mais c'est quand même putain bien pensé.
Sur ce... Je recommande à toutes les humains de la planète de lire ce magnifique livre intitulé "Les Fourmis" de Bernard Werber auquel le mec qui parle de la démonstration fait référence.
NeoLind il y a plus de 11 ans
Félicitations, tu viens de renverser l'Univers.
Cordialement.
Ertaï il y a plus de 11 ans
Oui, c'est ça qui m'a toujours fasciné dans les mathématiques, c'est que des démonstrations très complexes sont forcément obligées de se baser sur un truc qu'on s'est mis d'accord pour ne jamais remettre en question.
Dans le cas de la démonstration de SpiceGuid, il y en a déjà deux :
Il existe un entier naturel initial qu'on va appeler O
On s'accorde sur le fait que 1 c'est l'entier suivant O, c'est-à-dire S O
Le fait est qu'un mathématicien est incapable de prouver qu'il existe bien un entier naturel initial sans se référer à d'autres axiomes encore plus basiques (du genre "il y a le rien et il y a le quelquechose" ) m'a toujours impressionné.
Au final, l'édifice mathématique entier repose sur de minuscules piliers. Ce piliers sont quasi-insignifiants en eux-mêmes, mais le fait même qu'on ait bâti autant de théories mathématiques qui en dépendent les a rendu inamovibles a posteriori .
Et carton rouge pour la démonstration de Bernard Werber 
Dragoris il y a plus de 11 ans
Donc si j'ai bien compris, on s'est écarté des mathématiques psycho-rigidifiés pour entrer dans la philosophie :
Puisque le programmeur a la foi que tous les énoncés ne sont pas vrais, alors 1 + 1 = 2 est peut-être faux.
Si c'est pas de la philosophie retorse...
|
|
sasacool il y a plus de 11 ans