Le théorème d'incomplétude de Gödel peut-il nous aider à faire des achats sur Internet ?

[Schrodies-cat]

Comment delimiteriez vous la difference entre une déduction et une démonstration ?

Quand on fait des mathématiques : aucune !

Un énoncée se déduit d'un certains nombre d'énoncés.
Dans une démonstration, on déduit un énoncé des axiomes.

Enfin, c'est ainsi que je vois ces notions.
-----

[Médiat]

En mathématiques on applique des règles, voir par exemple, la présentation en séquents : https://fr.wikipedia.org/wiki/Calcul_des_s%C3%A9quents.

Je vous conseille en particulier le "groupe identité".

On peut toujours mettre des mots dessus, mais seule l'application de ces règles peut vous procurez l'ivresse qui permet de ne plus sentir l'horrible fardeau du temps qui brise vos épaules et vous penche vers la terre.

[PlaneteF]

Bonsoir,

En mathématiques on applique des règles, voir par exemple, la présentation en séquents : https://fr.wikipedia.org/wiki/Calcul_des_s%C3%A9quents.

Je vous conseille en particulier le "groupe identité".

--> Et oui, et avec en premier lieu la règle de déduction "axiome", comme un clin d'oeil à pazuzen

Cordialement

[Schrodies-cat]

(...)
On peut toujours mettre des mots dessus, mais seule l'application de ces règles peut vous procurez l'ivresse qui permet de ne plus sentir l'horrible fardeau du temps qui brise vos épaules et vous penche vers la terre.

Le temps peut-il être véritablement aboli ?
En mathématique, on peut utiliser pour démontrer un théorème un autre théorème qui a été démontré dans le passé, mais pas un théorème qui sera démontré dans le futur .
Tout au plus peut-on travailler sous l'hypothèse d'une conjecture.

La logique mathématique parle des mathématiques (je sais ce n'est pas un énoncé très formalisable).
Elle peut ou non prendre en compte le temps ( au sens que j'ai précisé ci-dessus), selon les besoins .

[Médiat]

En mathématique, on peut utiliser pour démontrer un théorème un autre théorème qui a été démontré dans le passé, mais pas un théorème qui sera démontré dans le futur .
Tout au plus peut-on travailler sous l'hypothèse d'une conjecture.

Ce qui revient bien à utiliser un théorème qui sera démontré dans le futur (ou non, futur hypothétique)

Comme je l'ai déjà écrit ici plusieurs fois, quand un mathématicien démontre , il ne dit rien de , rien de , il ne parle que de

[leon1789]

quand un mathématicien démontre , il ne dit rien de , rien de , il ne parle que de

Quand vous dîtes, "il ne dit rien de A, rien de B", je suppose que vous voulez parler des valeurs de vérité des assertions A et B.
Pour démontrer une implication, il faut bien évoquer les deux assertions dans la relation d'implication, donc pour prouver A => B, il faut parler de A, de B, et montrer le lien de A vers B.

[Médiat]

Quand vous dîtes, "il ne dit rien de A, rien de B", je suppose que vous voulez parler des valeurs de vérité des assertions A et B.
Pour démontrer une implication, il faut bien évoquer les deux assertions dans la relation d'implication, donc pour prouver A => B, il faut parler de A, de B, et montrer le lien de A vers B.

Oui, bien sûr, la démonstration utilise A et B, mais ne permet pas de statuer sur A, et sur B, c'est (A, A => B) qui permet de parler de B (pas (A => B) seul). Et si A est un axiome (ou un théorème déjà démontré) d'une théorie T, alors on peut dire que T démontre B (que B est "vrai" dans la théorie T, pour utiliser le vocabulaire dont je me méfie).

[Schrodies-cat]

Il y a la question de la notion de démonstration pour le mathématicien et pour le mathématicien logicien.
Quand le mathématicien dit qu'il a démontré B, c'est habituellement qu'il a déduit B de A_1,, A₂, ... , A_n où A_1,, A₂, ... , A_n sont des axiomes de la théorie (souvent implicite), dans laquelle il travaille , ceci dans la cadre de la logique classique.
Notes :
pour une déduction particulière, on utilise un nombre fini d'axiomes même si la théorie peut être munie d'une infinité d'axiomes.

On peut néanmoins se poser la question de la théorie dans laquelle on peut démontrer un théorème:
Exemple: l'énoncé du théorème de Fermat-Wiles s'écrit dans le langage de l'arithmétique de péano, est-il démontré/démontrable dans cette théorie.
Wiles, et ceux qui ont démontré auparavant les théorèmes qu'il a utilisés ne se sont bien entendu paslimités strictement à ce formalisme, mais je ne pense pas (oui c'est une opinion !)qu'il y aurait de difficultés majeures à adapter leurs démonstrations à ce formalisme .

On peut même obtenir des théorèmes sans utiliser un seul axiome de ladite théorie qui sont alors appelés tautologies.

Ceci étant précisé , y a-t-il des différences entre une démonstration de mathématicien, et démonstration au sens de la logique mathématique ?
Un mathématicien ne fera pour ainsi dire jamais une démonstration formelle au sens strict.
À mon mon sens, on considèrera que le résultat est démontré si on est convaincu qu'on pourrait tirer de sa démonstration une démonstration formelle sans difficulté majeure, même si ce serait généralement laborieux.

Qu'est ce qu'une démonstration formelle (restons dans le cadre de la logique classique du 1^er ordre)?
Divers systèmes ont été proposés dans le passé, certains étaient peu rigoureux, d'autres inconsistants ou pas assez complet pour rendre compte d'inférences pratiquées couramment par les mathématiciens et considérées comme légitimes ...
Il y a maintenant des systèmes de déductions considérés comme satisfaisants, Médiat à donné un lien sur l'un d'eux un peu plus haut.
Des systèmes de déduction (ou d'inférences) définis différemment peuvent donner des définitions de la déductibilité équivalents (à vérifier au cas par cas).

Enfin, il faut noter que quand il démontre A=>B , un mathématicien peut utiliser un théorème C déja démontré (dans la théorie dont il est question).
Pour faire une démonstration formelle de A=>B uniquement à partir des axiomes de ladite théorie, il faudrait faire non seulement une formalisation de la démonstration du dit mathématicien, mais y intégrer une formalisation d'une démonstration de C, ce qui risque de donner des démonstrations formelles conséquentes pour les théories ayant une longue histoire.
On doit donc en fait considérer un corpus de théorème déjà démontrés qui s'accroit au fil du temps (en espérant qu'il n'y a pas de bourdes dans les démonstrations).
Les théorèmes démontrables ainsi devant bien entendu être les mêmes.

Cela est bien entendu à prendre en compte dans le programme actuel de développement des outils de vérification de preuve.
J'avais tenté sans succès de lancer à se propos un sujet ici.

[Médiat]

On peut même obtenir des théorèmes sans utiliser un seul axiome de ladite théorie qui sont alors appelés tautologies.

Que voulez-vous dire exactement ?

[Schrodies-cat]

Il faut effectivement utiliser au moins un symbole de relation du langage pour former un énoncé, mais pas forcément d'axiome pour le démontrer un tautologie exemple dans l'arithmétique de péano, je sais démontrer que "(pour tout x)(x=x = > x=x)" , je n'ai besoin d'aucun axiome de l'arithmétique, simplement de ceux de la logique.

[Médiat]

Oui mais ce n'est pas lié à Peano, c'est juste une des propriétés de l'égalité, il n'y a aucune raison de nommer une théorie (ce n'est pas faux, mais cela peut engendrer des confusions), toutes les tautologies de la logique s'appliquent à tous les énoncés de toutes les théories.

[Schrodies-cat]

Ce n'est même pas une propriété de l'égalité ! on obtient la même chose en remplaçant = par n'importe-quel symbole de relation !
C'est néanmoins un théorème (sans grand intérêt) de l'arithmétique de Peano.

D'autre tautologies peuvent être plus intéressantes:

Je considère une théorie (disons du premier ordre ...) Définie par les axiomes A₁, A₂, A₃, etc .
Dire que B est un théorème de cette théorie revient à dire que pour un certain n,(( A₁ et A₂ et ... et A_n) => B) est une tautologie ! ( voir les liens entre implication, déduction et démonstration) .

[pazuzen]

**** Inutile ****
Dites moi, est ce que nous sommes ok pour dire que la conjecture de Fermat est une assertion qui s'exprime dans l'arithmétique de peano ?
Si non, les bras des mathematiciens tomberont tous....
A t'elle été demontrée sous Peano ou en utilisant ZFC ?

[Médiat]

Dites moi, est ce que nous sommes ok pour dire que la conjecture de Fermat est une assertion qui s'exprime dans l'arithmétique de peano ?

Oui et même dans le système Q

A t'elle été demontrée sous Peano ou en utilisant ZFC ?

Personnellement, je ne sais pas, mais où voulez-vous en venir ?

[Tryss2]

On sors largement de Peano pour démontrer la conjecture de Fermat

[Schrodies-cat]

La démonstration utilise des notions relatives aux formes modulaires etc.
De l'analyse complexe pas du tout élémentaire donc.

Il y des techniques pour traduire en arithmétiques certaines assertions d'analyse réelle et complexe, par exemple on peut utiliser les réels calculables etc ...
Seraient-elles suffisante pour traduire la démonstration du théorème de Fermat-Wiles et donc aussi celles des théorème qu'il utilise ?
Il est certain que si c'est possible, il y aurait du boulot. Sans doute serait-il nécessaire de se faire assiter par l'ordinateur.

[pazuzen]

Fermat est donc une assertion vraie dans peano, nous sommes toujours ok ?

[pazuzen]

On ne peut pas avoir x^n=a^n+b^n pour tout n>2
Tout le monde est ok ?

[Schrodies-cat]

Vous allez encore énerver Médiat et je le comprends.

Fermat est donc une assertion vraie dans peano, nous sommes toujours ok ?

"Fermat" a été démontré dans ZF, je pense qu'on peut dire cela de façon aussi certaine qu'il est possible.
Fermat est vrai dans le modèle standard de l'arithmétique, je pense ne pas trop m'avancer.
" vrai dans Peano" je ne vois pas trop (cela s'appelle une litote) ce que cela veut dire .

[gg0]

Heu ... la preuve d'Andrew Wiles utilise d'autres axiomes que ceux de Peano (peu utilisés maintenant, la construction des entiers par les ordinaux redonnant ces axiomes comme des théorèmes).
Rien ne t'empêche, Pazuzen, d'aller lire cette preuve pour savoir

[Médiat]

Vous allez encore énerver Médiat et je le comprends.

Merci d'avoir pris le relais, parce que sincèrement, je ne sais plus quoi faire pour faire comprendre quelque chose à pazuzen

[Schrodies-cat]

Pour tout vous dire, sa façon de saturer le débat m'énerve également.
Je crains que ma méthode pédagogique ne s'avère guère plus efficace.

[pazuzen]

Que voulez vous me faire comprendre ?
Fermat est une assertion vraie (prenez un ordinateur et trouvez un seul n qui le démentirait), qui s'exprime dans peano sans que Peano ne puisse le demontrer ou le refuter
On appelle cela un indecidable
Sauf que cette assertion est vraie, vérifiable pour tous les n que vous testerez et uniquement demontrable pzr Zfc
Vous pouvez faire mine de ne pas le comprendre, ce fait est un fait
Hors nième censure, comment affirmez vous l'inverse ?

[pazuzen]

Vous en voulez d'autres ?
Theoreme de Ramsey, theoreme de goodstein..
Les exemples d'enoncés vrais indecidable vous en voulez dans d'autres theories ?
Suffit de demander

[gg0]

Fermat est une assertion vraie (prenez un ordinateur et trouvez un seul n qui le démentirait)

Raisonnement absurde, contre-factuel. Incompréhension totale des mathématiques et aussi de ce que peut faire un ordinateur. Peut-être même incompréhension de l'infinitude des nombres entiers.

Quand on en est à ce niveau de raisonnement, on commence par apprendre les bases ....

Quant à dire que l'axiomatique de Peano ne peut pas le prouver, c'est parler sans savoir, sauf si on a une preuve de ce qu'on dit :

Fermat est une assertion vraie (prenez un ordinateur et trouvez un seul n qui le démentirait), qui s'exprime dans peano sans que Peano ne puisse le demontrer ou le refuter

Pazuzen, tu n'as pas de preuve, tu racontes ce qui t'arrange, tu veux te faire mousser ici, et tout le monde voit que tu n'est rien ...

Même pas capable de mettre la majuscule à Peano !!!

[Schrodies-cat]

Que voulez vous me faire comprendre ?
Fermat est une assertion vraie (prenez un ordinateur et trouvez un seul n qui le démentirait), (...)

Après un nombre considérable de messages ou vous avez utilisé le mot "vrai", vous commencez à expliquer ce que vous entendez par ce mot.
L'idée n'est pas forcément inintéressante, mais elle a ses limites, comme le montre l'exemple suivant:
https://en.wikipedia.org/wiki/Skewes'_number

[pazuzen]

A ma décharge mes explications les plus argumentées sont supprimées ce qui rend difficile de vous signifier ce qu'est, "pour moi" une assertion vraie

Enfin du fonds et enfin des sources...
J'ai lu attentivement l'article, quelles limites y voyez vous ?

Pour ma part, il faut distinguer inférence, implication, déduction et demonstration car ces notions proches ne renvoient pas les mêmes delimitations
De la même manière, il faut distinguer assertion vraie de theoreme de preuve
Là encore il y a des differences

Pour vous répondre, "ma definition "d'assertion vraie" est un énoncé qui s'exprime dans le langage de la theorie, dans sa typographie et dont la question de savoir si elle est vraie renvoie à une réponse unique la conjecture de
Fermat est VRAI
Sous Peano, x^n=a^n+b^n s'exprime dans la theorie et jamais cette égalité ne sera verifiée pour n>2

Le prouver est resté longtemps impossible
Nous pouvions alors penser qu'elle pouvait être une assertion fausse
Et le fait est que la demonstration a necessité de faire appel à une autre axiomatique et une autre theorie qu'est ZFC
Pour tous les mathematiciens, fermat a été demontré et la preuve de la demonstration a été faite
Dans Peano, cette assertion est VRAIE, elle n'est cependant pas prouvable à l'intérieur même de Peano mais par ZFC
Si nous n'avions pas ZFC, cette assertion pourtant vraie (d'ailleurs personne ne peut évidemment demontrer qu'elle est fausse...) serait restée une assertion indecidable
Sauf que par le calcul, nous voyons qu'elle est systématiquement VRAIE et que par la demonstration dans ZFC qui emule Peano, on sait que c'est aussi demontré donc prouvé

[Médiat]

Pour vous répondre, "ma definition "d'assertion vraie" est un énoncé qui s'exprime dans le langage de la theorie, dans sa typographie et dont la question de savoir si elle est vraie renvoie à une réponse unique

Je vous propose une autre définition, plus courte et plus simple : Une assertion vraie est une assertion qui est vraie !

Ah ben non, j'ai encore été optimiste, avec votre définition, dans Peano, l'assertion 1=2 est vraie, puisque " la question de savoir si elle est vraie renvoie à une réponse unique"

[pazuzen]

Cela renvoie d'ailleurs a un autre énoncé lu dans ce fil que "je" considere FAUX

A ete ecrit que le premier theoreme d'incompletude signifiait que nous ne pourrions jamais connaitre tous les theoremes d'une theorie

Ce n'est pas ce que dit Godel

Godel affirme que des assertions mathematiques sont des indecidables
Un indecidable, c'est justement une assertion qu'on ne peut démontrer vraie ou fausse (théorème)
Pourtant cet indecidable est soit vrai soit faux...
Ce que dit Godel, c'est que des assertions mathematiques de la theorie T échapperont toujours aux demonstrations dans T donc aux theoremes de T bien que ces assertions soient VRAIES ou FAUSSES

[pazuzen]

D'après votre theorie ou A->A signifie "A prouve A"
Je pose A- vous énoncez dans ce systeme formel contre vérité sur contre Vérité
Donc A est prouvé....