Cher karlp,
Les deux premiers types sont normaux, la nécessité de démontrer un axiome à l'intérieur de la théorie dont il est un axiome n'étant pas franchement établie, même la deuxième est normale, quant à la troisième, la réaction que vous décrivez me fait penser à la réaction d'un croyant face à un blasphème (et du coup j'ai envie d'ajouter : QED)
Dernière modification par Médiat ; 29/03/2016 à 13h50.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Quand on pense qu'un theoreme est le résultat d'une démonstration mathématique donc une assertion pouvant être établie comme vraie au travers d'un raisonnement logique à partir d'axiomes...
Et que ces profs définissent l'axiome précisément comme un théorème...
si des palanquées de mathematiciens se sont penchés sur le 5eme axiome de la géométrie d'Euclide pour tenter d'en faire une démonstration, c'est évidemment pas parce qu'il se déduit des autres dans l'axiomatique dont il fait partie !
J'avoue être estomaqué...
Prenons à present l'implication mathématique qui est un autre sujet ayant été evoqué
Il s'agit d'un connecteur logique.
A implique B ne signifie pas que A demontre B ni que B est prouvé par A
A implique A n'est pas davantage une preuve...
Prouver que A implique B ne prouve pas que B est vrai
Si blanche neige est reine du royaume uni alors elle est aussi reine d'australie
Cette implication est vraie sauf que blanche neige n'est pas reine d'australie...
On ne demontre pas B par A
Toujours aucune information sur ce que vous appelez "raisonnement", donc ... continuez d'être estomaqué, cela ne changera rien à la logique mathématique et aux théories de la démonstration.
Pour le 5eme axiome de la géométrie d'Euclide, ce que vous décrivez est la démonstration de l'indépendance d'un axiome par rapport aux autres, c'est à dire son indécidabilité dans la théorie privé de l'axiome dont on veut montrer l'indépendance : cela n'a donc RIEN à voir avec la question en cours, encore votre manie de tout déformer !
Pour l'implication :
Avez-vous lu les 3 démonstrations de PlaneteF qui n'utilise pas l'implication comme connecteur logique, mais un séquent !
Avez-vous entendu parler du Modus Ponens, qui permet aussi de démontrer A à partir de A ? J'ai l'impression que non !
Dernière modification par Médiat ; 29/03/2016 à 14h14.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Le modus ponens concerne l'implication
L'implication n'est pas une démonstration ...
A implique A n'est pas la démonstration que A soit Vrai !
Mais que si on a A alors.. On a A...même si A est faux
C'est une tautologie reflexive, non une démonstration...
Les matheux ont eu pour objectif de prouver l'énoncé du 5ème axiome dans la théorie "engendrée" par les 4 premiers, et cette théorie avec les 4 axiomes n'est pas théorie de la géométrie euclidienne (vous l'avez bien souligné dans vos précédents messages : il y a d'autres géométries...).Envoyé par pazuzen
oui.
Mais si A est un axiome de la théorie, c'est bien une preuve que B est vrai dans la théorie : comme vous l'avez dit, ce petit raisonnement qui se base sur des axiomes présumés vrais (A), sur une logique élémentaire (l'implication). Donc B est prouvé, non ?
Certes, je suis bien d'accord, mais "blanche neige est la reine du royaume uni" n'est pas un axiome de ma théorie.
Ca tourne un peu en rond là.... il est vrai qu'il est question de "A entraîne A" qui est ce qu'on appelle un raisonnement circulaire (court).
Non, mais (A, A ==> A) en est une mais bon cela vous échappe depuis si longtemps ... On peut même se demander si (A) tout seul n'est pas une démonstration, comme se le demandait leon1789 (question qui n'a pas lieu d'être avec le formalisme des séquents).
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
En fait vous ne parlez pas de la même chose. Médiat a raison de dire que si A est un axiome alors c'est un théorème. Mais pazuzen se réfère (je pense) à la démarche d'un étudiant à qui on a demandé de montrer telle proposition et qui bien sûr doit faire attention à ne pas la supposer vraie d'emblée (une erreur qu'on voit bien souvent). Je soupçonne vaguement Médiat d'avoir compris la source de la confusion mais de faire la sourde oreille... (il va s'insurger c'est certain).
Seulement pour la forme car il a bon fond.
Moi ignare et moi pas comprendre langage avec «hasard», «réalité» et «existe».
si A est une démonstration.. Non A est aussi une démonstration...
Que concluez vous de ce système ou A comme non A seraient inclus car tous deux sont démontrés ?
Juste une question parce que, encore une fois, le second theoreme de Godel traite dans une certaine mesure de ce sujet
Comment comprenez vous ce theoreme ?
Pazuzen, etes vous d'accord sur le fait que si A est un axiome, et qu'on a A=>B, alors par le modus Ponens, on a démontré B?
oui, Pazuzen .A implique B ne signifie pas que A demontre B ni que B est prouvé par A
Prouver que A implique B ne prouve pas que B est vrai
Mais si A est un axiome de la théorie, c'est bien une preuve que B est vrai dans la théorie : comme vous l'avez dit, ce petit raisonnement qui se base sur des axiomes présumés vrais (A), sur une logique élémentaire (l'implication). Donc B est prouvé, non ?
Je ne nie pas avoir, parfois, un certain aspect pervers (il suffit de lire ma signature), mais ce n'est pas à cela que je pensais, mais à une vision des mathématiques datant d'Euclide et que l'on ne retrouve plus aujourd'hui, même chez les platoniciens extrémistes et dont karlp, avec plus de mansuétude que moi, datait la fin au 19ème siècle.
Dernière modification par Médiat ; 30/03/2016 à 06h04.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Si A vrai (axiome ou theoreme)
Si A implique B
Alors B est vrai
On est OK sur le caractère demonstratif ci dessus
(Ouf c'est déjà bien )
Mais,
La preuve de B porte précisément sur la démonstration de l'implication relationnelle de A vers B
Ce lien d'implication ne se décrète pas a priori
Mais A=>A est toujours vrai ! Donc si on pose B=A, on a bien démontré A
ok.
Certes, une implication quelconque ne se décrète pas a priori. Mais l'implication "A => A" est validée a priori , non ?
Leon, tryss, excellentes remarques
Je vous remercie de la qualité sur le fonds de nos derniers échanges
Je vais vous répondre
Une assertion vraie dans une théorie repose sur ses axiomes, dont nous discutons (et j'y reviendrai) et sur la logique de premier ordre avec lesquels nous appuyons des démonstrations.
Le fameux Godel, justement, a demontré dans son théorème de completude à la fois la consistance et la completude de cette logique de premier ordre comme le calcul propositionnel dans le cadre de la logique classique et je sais, pour vous lire, qu'on sera d'accord sur la pertinence de cette logique de premier ordre pour effectuer des démonstrations dans une theorie (c'est d'ailleurs ce que vous faites en utilisant le signe d'implication)
Bien...
Tout systeme axiomatique cohérent (non contradictoire) va donc "produire ses propres démonstrations" à partir des définitions d'objets mathematiques (ex : un point, une droite, un plan....), à partir des axiomes initiaux considéré a priori comme VRAI et à partir des règles définies dans la logique de premier ordre.
Ces vérités produites par le systeme formel, on les appelle des théorèmes.
Ces théorèmes reposent donc tous sur une demonstration au sein même de la théorie à partir d'une matière première considérée vraie et à partir de la logique de premier ordre referente considérée
Je vous fais remarquer qu'ici va se trouver notre désaccord concernant le premier theoreme d'incomplétude qui considère indecidable certains énoncés si fait qu'aucune theorie "complexe" ne peut être complète quels que soient les axiomes employés
J'y reviendrai...
Mais revenons à notre histoire d'axiome....
L'axiome est donc d'une part la brique élémentaire de la théorie, il n'y a pas de recursivité possible pour utiliser la logique de premier ordre et descendre à des énoncés plus fondamentaux
D'autre part, ces axiomes sont considérés VRAI a priori (contrairement aux theoreme produits par la logique de premier ordre de la theorie)
Ils ne sont 'produits' par rien, ils sont simplement considérés vrai sans demonstration, sans preuve, sans matière plus fondamentale et sans utilisation de regle logique
Ils sont natifs
Je vous ai fait remarquer la difference entre l'implication et la demonstration....
Oui l'axiome A implique l'axiome A par simple convention
Mais l'axiome A ne demontre pas l'axiome A car la demonstration est le résultat de l'utilisation de règles logique predefinies
Pas de matière plus fondamentale, pas de regles logique dont ils sont issus
Si A implique A, ce n'est pas une preuve, pas une demonstration, c'est juste la confition sine qua non de cohérence sans laquelle une chose et son contraire serait possible
Nulle preuve, nulle demonstration
Un autre jour j'evoquerai les limites de l'autoreferentialité dans un systeme y compris unitaire comme l'axiome
L'impossibilité de s'auto demontrer est un peu au coeur du second theoreme d'incompletude mais etant en désaccord deja sur le premier je remets ce sujet a plus tard
J'aimerais que vous me disiez ce que vous interpretez de ce deuxième theoreme
J'aimerais developper les problèmes d'auto referentialité
Ensuite je m'adapte...
Merci pour votre etat d'esprit d'échanges
Toujours pas de définition de la démonstration : tout ce laïus n'a donc aucun intérêt !
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Je ne vois pas où on n'aurait pas utilisé des règles logiques prédéfinies.
Nous étions, il me semble, d'accord sur le fait que "[A axiome] et [A => B]" prouvait B .
Pourquoi ne serait-ce plus vrai lorsque B est l'énoncé de A ??
Dernière modification par leon1789 ; 29/03/2016 à 18h56.
Leon, nous sommes dans le coeur du sujet
Y compris par les liens entre ce sujet A implique A et Godel
Je n'ai pas la possibilité de répondre aujourd'hui mais je vous promets de donner suite
Pour mediat bien noté la question de spécifier la demonstration
J'en parlerai après ce premier sujet
Bonne journée à tous
Pazuzen , Si les axiomes ne sont pas démontrables comment expliqueriez vous que "A1 ouA2" soit un théorème démontrable bien qu'il soit équivalent à A1 (dans la théorie admettant A1 et A2 comme axiomes) .
J'ai dix minutes, je developperai l'argumentation demain mais je vous donne l'argument principal
L'auto referentialité...
J'ai déjà evoqué le premier argument à savoir que l'axiome est, par definition, la seule assertion vraie non recursivement demontrable par des objets mathematiques plus fondamentaux que lui
A1 ou non A2 entend opérer une opération logique entre deux axiomes différents
Le résultat en est une demonstration logique au sein du système
A1 implique A1 est ce qu'on appelle une proposition autoreferentielle
Si je vous propose de faire comme vous, soit :
A1 - mon énoncé est faux
J'utilise la meme autoreferentialité
Et en effet, que mon énoncé soit faux implique que mon énoncé soit faux
Est ce une demonstration ?
C'est un axiome a priori vrai, à ce stade, tout va bien
Sauf que, si je developpe, si mon énoncé est faux, c'est donc qu'il est faux qu'il soit faux, donc que l'énoncé est vrai, donc cet énoncé est faux...
L'autoreferencialité est le chemin vers l'indecidabilité
J'y reviendrai
Toujours pas de définition de ce qu'est une démonstration, mais quelques erreurs de plus :
La commutativité est indécidable dans la théorie des groupes, je n'y vois pas l'ombre d'une trace d'autoréférentialité.
A1 ==> A1 n'a rien à voir avec l'autoréférentialité cette implication ne parlant pas d'elle-même !
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Quelle confusion !
Confondre la notion d'autoréférence avec la notion d'implication, c'est vraiment ne pas avoir vraiment réfléchi
"A1 implique A1 est ce qu'on appelle une proposition autoreferentielle" N'importe quoi. C'est une tautologie. ""A1 implique A1" ne parle pas de lui-même.
Il n'y a aucune autoréférence dans "mon énoncé est faux donc mon énoncé est faux".
Il reste que prendre comme "axiome" la phrase "mon énoncé est faux" est assez aberrant; on ne sait même pas quel est cet énoncé. Et si on prend pour A1 l'énoncé autoréférent "je suis un énoncé faux", on a choisi de se mettre dans une difficulté connue, pour rien.
mais ça n'a rien à voir avec le fait que ""A1 implique A1" est tout à fait valide.
Mais on attend toujours que Pazuzen dise ce que c'est qu'une démonstration. Tout le monde est d'accord sur ce que c'est, sauf lui. Et tout le monde le relie à l'application de règles logiques, lui dit non. Qui est l'inconséquent ??
On devrait référencer cette discussion comme l'exemple parfait des bêtises qui peuvent être dites par celui qui se confine dans le baratin; qui de ce fait parle sans savoir et finit par raconter n'importe quoi.
Dernière modification par gg0 ; 30/03/2016 à 12h13.
Il faut dire qu'on trouve n'importe quoi sur le net :
Par exemple dans le modèle ({0}, +), où + est définie par 0 + 0 = 0, selon la phrase précédente "nous sommes obligés d'admettre sans preuve" que l'axiome de l'élément neutre est bien vérifié (et même que l'on a un groupe).Ils [Les axiomes] sont un ensemble d'énoncés sur notre modèle que nous admettons sans démonstration. Ce sont souvent des énoncés qui nous semblent évidents dans le modèle que l'on veut étudier. Cependant, évidents ou non, nous sommes obligés de les admettre sans preuve pour qu'ils servent de base à des déductions.
je vous laisse deviner où j'ai trouvé cela
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Rapidement en passant...
Que l'autoreferentialité mène à l'indecidabilité ne signifie pas que l'indecidabilité n'est provoquée que par l'autoréférentialité...
Je veux bien qu'on confonde application et bijection mais ce n'est pas la même nature de relation...
Par ailleurs l'autoréférentialité consiste à proposer une relation à un groupe dont on fait soi même partie
Epimenide le Crétois déclare que tous les crétois sont des menteurs
Or Epimenide est Crétois
Donc cela implique qu'il il ment et les cretois disent la vérité
Donc il dit la vérité
Donc les crétois sont des menteurs
Donc il ment...
A implique A est une relation logique du type ´implication'
A est inclu dans A
Donc A implique A est une relation autoreferentielle
Et pour cause...
L'axiome de depart est A
Le "théorème" de sortie est A
Et la relation ne concerne que A de l'entrée à la sortie
Plus autoreferentiel que ça...
Pour Mediat, il existe une theorie de la demonstration qui est à elle seule une branche des metamathematiques donc je n'ai pas pour intention de developper un dossier complet mais d'en extraire l'essentiel
grossièrement, toutes les techniques de demonstration vont viser à apporter la preuve qu'une assertion mathematique définie est VRAIE dans une theorie consistante (ou par conséquent la preuve de l'assertion inverse est impossible)
Il ne faut cependant pas confondre assertion vraie et preuve car chaque preuve démontre le caractère VRAI de l'assertion mais chaque assertion VRAIE ne peut-être systématiquement prouvée (toujours la difference entre application et bijection)
Si fait qu'il existe des conjectures vraies concernant des assertions dans la theorie mais qui ne sont pas demontrées par la theorie et donc des assertions vraies dans la theorie qui ne sont démontrables qu'en sortant de la theorie (Connes en donne un exemple dans l'article de "la recherche" que j'avais linké)
J'ai donc parlé de démonstration mais en pratique cette dernière ne nécessite pas d'être formalisée en système syntaxique
C'est même rare qu'une demonstration mathematique se fasse de manière totalement formelle
La nature de la demonstration prend généralement une forme adaptée au public en considérant des énoncés connus pour être vrais et en enchaînant des modes de raisonnements eux aussi de la logique de premier ordre pour établir des déductions
Dans tous les cas, on ne trouvera jamais aucune demonstration mathematique autoreferentielle excepté celles qui traitent des limites de l'autoreferentialité des systemes formels
Les theoremes d'incompletude de Godel sont de ceux la
En générant des propositions autoreferentielles inherentes aux theorie consistantes supérieures à celles contenant en leur sein l'arithmétique de Robinson, ces theoremes demontrent :
D'une part qu'aucun systeme consistant ne pourra jamais être complet même en ajoutant comme axiome les énoncés indecidables (connaissez vous d'ailleurs des theories operationnelles qui contiendraient une infinité d'axiomes ?)
Et d'autre part avec le second theoreme qu'aucune theorie précédemment definie ne peut demontrer sa consistance (sa non contradiction) avec les axiomes contenus dans la théorie
l'autoreferentialité est, pour prouver qu'une assertion est vraie un non sens (modulo les demonstrations dont l'objet porte sur les limites des propositions autoreferentielles - ex : theoremes d'incomplétude)
Si j'ose une analogie avec les limites de l'analogie, c'est du meme acabit que de demander à l'accusé de procéder à son propre jugement
Visiblement pazuzen a plus en vue une carrière de politique que de mathématicien
Il nous dit "si on a [A axiome et A=>B] alors on a démontré B... Sauf si B=A. Mais on ne comprends pas très bien pourquoi, ça doit être un des mystères des maths selon pazuzen
Et après on s'étonne que le monde aille si malVisiblement pazuzen a plus en vue une carrière de politique que de mathématicien
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
pazuzen, une fois de plus je ne vais pas perdre mon temps à relever toutes les erreurs de ce dernier texte, mais :
NON ! (A==>A) n'est pas auto référentiel, (cela le serait si A était la formule A==>A)
C'est en vertu de ce principe idiot que vos assertions sont vraies, mais uniquement en sortant des mathématiques ?assertions vraies dans la theorie qui ne sont démontrables qu'en sortant de la theorie
Toujours pas de définition de ce qu'est une démonstration ; les spécialistes de cette discipline apprécieront les avis de pazuzen sur leur science
La coupe à trolls est pleine, mais il y a encore de la place dans la poubelle à trolls : les prochains messages qui ne respecteraient pas la charte (pas de théorie personnelle) seront effacés !
Dernière modification par Médiat ; 31/03/2016 à 07h31.
Je suis Charlie.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
