Quel est le formalisme de la traduction de Gödel ?

[invite6754323456711]

Bonjour,

Il existe une traduction de Gödel qui permet de transformer toute démonstration classique d’un théorème classique en une démonstration intuitionniste d’un théorème intuitionniste

La notion de traduction relève telle d'une logique ? Peut-on la réfuter ?

Patrick
-----

[Médiat]

Essaye les exercices : http://www.labri.fr/perso/retore/LL/nonnon_sujet.pdf
Et des explications : http://www.labri.fr/perso/retore/LL/...ndications.pdf
Le deuxième pdf utilise clairement la déduction naturelle "à la Hilbert" ; je ne trouve pas sur le net, mais je me souviens d'avoir vu la traduction explicitée en utilisant le formalisme du -calcul.

[Médiat]

la déduction naturelle "à la Hilbert"

Ooops, faute de frappe (quelle pauvre excuse), il fallait lire "à la Gentzen".

Pour le -calcul, j'ai trouvé : http://www.lsv.ens-cachan.fr/~goubault/Lambda/s4.pdf mais ce n'est pas l'article auquel je pensais.

[invite6754323456711]

Ooops, faute de frappe (quelle pauvre excuse), il fallait lire "à la Gentzen".

Pour le -calcul, j'ai trouvé : http://www.lsv.ens-cachan.fr/~goubault/Lambda/s4.pdf mais ce n'est pas l'article auquel je pensais.

Merci.

Je me rend compte que plus amont ce n'est pas encore clair pour moi.

Je m'interroge sur la formalisation du discours des mathématiques dans lequel on évacue tous ce qui a du sens (vrai ou faux).

Un système formel du premier ordre est composé d'un langage (sur un alphabet) d'axiomes (expression bien formé dans le langage) et de règles de déduction /dérivation pour former des expressions bien construites.

La logique classique et intuitionniste partagent elle le même langage (langages des prédicats) ?

Ce qui diffère c'est les axiomes et les règles de déduction ?

Peut on construire un même modèle (donne un sens au formalisme) ensembliste à partir des deux logiques ?

Patrick

[A voir en vidéo sur Futura]

[Médiat]

La logique classique et intuitionniste partagent elle le même langage (langages des prédicats) ?

Ce qui diffère c'est les axiomes et les règles de déduction ?

Oui

Peut on construire un même modèle (donne un sens au formalisme) ensembliste à partir des deux logiques ?

La logique intuitionniste utilise plutôt les modèles de Kripke (grossièrement c'est une famille de modèles au sens classique), comme les logiques modales.

[invite6754323456711]

La logique intuitionniste utilise plutôt les modèles de Kripke (grossièrement c'est une famille de modèles au sens classique),

Comme on peut transformer toute démonstration classique d’un théorème classique en une démonstration intuitionniste d’un théorème intuitionniste peut on en déduire que tout modèles construit à partir de la logique intuitionniste peut aussi être construit à partir de la logique classique ?


Patrick

[Médiat]

Comme on peut transformer toute démonstration classique d’un théorème classique en une démonstration intuitionniste d’un théorème intuitionniste peut on en déduire que tout modèles construit à partir de la logique intuitionniste peut aussi être construit à partir de la logique classique ?

Je ne comprends ce que veut dire cette expression, d'autant plus que dans un cas on a un modèle (au sens classique) et dans l'autre une famille de modèles (au sens classique) pour faire un modèle intuitionniste.

Si le sujet t'intéresse, il faut que tu cherches "sémantique de Kripke", tu vas tomber sur une énorme littérature car beaucoup de (sinon toutes les) logiques modales admettent des modèles de cette forme.

[invite6754323456711]

Je ne comprends ce que veut dire cette expression, d'autant plus que dans un cas on a un modèle (au sens classique) et dans l'autre une famille de modèles (au sens classique) pour faire un modèle intuitionniste.

Si le sujet t'intéresse, il faut que tu cherches "sémantique de Kripke", tu vas tomber sur une énorme littérature car beaucoup de (sinon toutes les) logiques modales admettent des modèles de cette forme.

DESHOUILLERS Jean-Marc parle de traduction aussi plutôt que construction http://www.canalu.tv/themes__1/scien...in_d_un_espoir

Patrick

[invite6754323456711]

DESHOUILLERS Jean-Marc parle de traduction aussi plutôt que construction http://www.canalu.tv/themes__1/scien...in_d_un_espoir

Patrick

Paragraphe théorie des groupes. Position curseur temps 50:10

Donne en exemple un modèle ensembliste pour la théorie des groupes.

Ce qui était axiomatique dans le système formel est quelque chose qui dans l'ensemble structuré (groupe) définit devient quelque chose qui est vrai. Cela permet de passer de ce qui est vrai le modèle ensembliste ... il y a une façon de traduire les énoncés que l'on peut écrire dans le langage formel en énoncés qui sont sur le modèle.

Patrick

[Médiat]

Donne en exemple un modèle ensembliste pour la théorie des groupes.

Je viens d'écouter, et je dois d'abord remercier Jean-Marc Deshouillers pour mettre en avant le théorème de complétude de Gödel, et pour bien remettre le mot "vrai" à sa place quand on parle de mathématique (deux de mes chevaux de bataille) ; par contre le choix du mot "traduire" ici ne me convainc pas (il est parfaitement adapté à la "traduction de Gödel"), j'utilise plutôt le mot "interpréter" (on peut remarquer qu'un interprète et un traducteur font des métiers assez proche).