Théorème d'incomplétude de Gödel

[invite78516567821]

Bonjour (la politesse n'est pas optionnelle sur ce site)

A quoi sert de donner une version de 1931 qui utilise des concepts et du vocabulaire complètement démodés, alors que Gödel lui-même a donné une version de ce théorème en terme plus moderne en 1963 ?

Je vous prie humblement d'accepter les plus profondes excuses d'avoir énoncé le théorème de Kurt Gödel tel que l'on me l'a enseigné à la fac.
-----

[inviteb6b93040]

Bon reste du jour

Après la physique peut on appliquer le théorème d'incomplétude de Gödel au problème des bug en informatique ?

la troisième forme de « complexité » informatique provient des limites de la logique elle-même : comme l'a démontré Gödel, aucun système logique ne peut contenir la démonstration de toutes les vérités. Le domaine de la pensée pure est lui aussi complexe puisque aucun système fini ne peut en rendre compte (il résulte du théorème de Gödel qu'il est impossible de mettre au point un programme capable de vérifier tous les programmes).
http://www.volle.com/ulb/031122/limites.htm

[Médiat]

Je vous prie humblement d'accepter les plus profondes excuses d'avoir énoncé le théorème de Kurt Gödel tel que l'on me l'a enseigné à la fac.

Je vous en prie ;

Je continuerai de penser qu'il est dommage d'arrêter l'histoire en 1931 et d'ignorer les travaux de Turing qui ont justement permis à Gödel de l'exprimer d'une façon toujours utilisée aujourd'hui.

[invite78516567821]

Je vous en prie ;

Je continuerai de penser qu'il est dommage d'arrêter l'histoire en 1931 et d'ignorer les travaux de Turing qui ont justement permis à Gödel de l'exprimer d'une façon toujours utilisée aujourd'hui.

Bonjour,
Mais je n'arrête pas du tout l'histoire en 1931 et je connais très bien les travaux d'Alan Turing, d'Alonso Church, sa thèse et son lambda-calculus dont s'est inspiré Mc Carthy pour son langage LISP, ainsi que les travaux de Tarski etc.
Je trouve simplement que l'énoncé original de Gödel est plus riche que ses successeurs. c'est tout.
Amicalement.

[Médiat]

Bonjour,

Je trouve simplement que l'énoncé original de Gödel est plus riche que ses successeurs. c'est tout.

C'est votre droit, bien sûr, et même, vous avez raison dans le sens ou l'-consistance est moins exigeante syntaxiquement que la consistance, mais, a contrario, elle est plus exigeante sémantiquement.
De plus, depuis plus de 45 ans, je n'ai lu aucun article de logique (il est exact que je n'ai pas tout lu) utilisant l'-consistance à la place de la consistance.

[invite78516567821]

Bonjour,


C'est votre droit, bien sûr, et même, vous avez raison dans le sens ou l'-consistance est moins exigeante syntaxiquement que la consistance, mais, a contrario, elle est plus exigeante sémantiquement.
De plus, depuis plus de 45 ans, je n'ai lu aucun article de logique (il est exact que je n'ai pas tout lu) utilisant l'-consistance à la place de la consistance.

Bonjour,
J'étais à la Fac de 1945 à 1958 ! En effet, âgé de 88 ans dès le 9 novembre 2015, je suis de la vieille école mais, jouissant d'une bonne santé physique et intellectuelle, je n'ai jamais cessé mes recherches en logique mathématique avec en plus un bon bagage en mathématiques et en physique.
Voilà qui peut expliquer un certain déphasage intergénération.
Amicalement.

[pm42]

Peut-être mais vous venez de donner raison à votre contradicteur : venir expliquer ce que ce qu'on vous appris en fac il y a 60 ans est toujours la meilleure façon d'expliquer les choses n'est pas vraiment convaincant.

[invite5e279b10]

En tout cas si c'est l'énoncé exact du théorème ça refroidit un peu, je trouve.

[invite82078308]

Si on veut aborder les choses d'un point de vue historique, Allan Turing avait fait sa thèse sur le théorème d'incomplétude de Kurt Gödel.
Il y a donc une filiation entre Gödel et Turing.
Par la suite Kurt Gödel, dans sa correspondance, je crois, a reconnu que les idées de Turing permettaient de présenter sa théorie de façon plus claire, reconnaissant ainsi cette filiation.
Comment interpréter la théorie de Gödel dans la théorie de Turing ? Il faut d'abord faire un travail de codage pour représenter la notion de machine de Turing dans l'arithmétique, et ensuite, avec les facilités de codage que donne la théorie de Turing, tout est plus simple.

[Médiat]

Bonjour,

Cette évolution se voit très bien entre la formulation de 1931 et celle de 1963 (par le même Gödel), la reformulation de 63 et les suivantes s'appuyant bien sur les travaux de Turing (entre autres, le récursivement axiomatisable, qui est une part essentielle et souvent oubliée)

[invite82078308]

Si il fallait ne retenir que deux choses de tout cela:
1 : je dirais que "être une démonstration (formelle)" est récursif, ce qui ouvre la voie aux systèmes de vérification automatiques de démonstrations, domaine en pleine expansion actuellement .
2 : "être un théorème" ( ou être démontrable, si vous préférez ...) est récursivement énumérable, mais en général pas récursif sauf dans le cas de théories élémentaires

[invite82078308]

P.S. ajouter à l'assertion 2 : "ce qui limite les possibilités des systèmes de démonstration automatique"
Trouver une démonstration est bien plus difficile que vérifier une démonstration .

[Médiat]

sauf dans le cas de théories élémentaires

Bonjour,

Je suppose que vous parlez de la décidabilité des théories, et dans ce cas, la théorie des corps réels clos est décidable, elle n'est pourtant pas si élémentaire que cela.

[invite82078308]

C'est une question de point de vue: des choses qui paraissent simples en théorie peuvent être compliquées dans la pratique.
Dans certaines théories , même si un énoncé de longueur n est décidable, le démontrer ou le contredire peut demander une longue démonstration difficile à trouver ...
Un résultat important toutefois de la théorie de Gödel est que l'arithmétique de Peano ne peut en aucun cas être considérée comme une théorie "élémentaire", ce qu'on aurait pu espérer avant.

[Médiat]

Un résultat important toutefois de la théorie de Gödel est que l'arithmétique de Peano ne peut en aucun cas être considérée comme une théorie "élémentaire", ce qu'on aurait pu espérer avant.

Nous sommes bien d'accord là-dessus, je n'ai réagi que parce que le mot "élémentaire" me semblait exagéré, pour certaines de ces théories.

Que l'on dise que les théories décidables soient, au moins en un sens précis^(*), plus "simples" que les théories non décidables, cela ne me choque pas.

^(*) Qu'un ordinateur puisse donner la liste des théorèmes dans un cas et pas dans l'autre est bien une mesure de complexité