Répondre à la discussion
Affichage des résultats 1 à 10 sur 10

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



  1. #1
    invite6754323456711
    Invité

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


    ------

    Bonjour,

    Citation Envoyé par Médiat Voir le message
    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

    -----

  2. Publicité
  3. #2
    Médiat

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

    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.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  4. #3
    Médiat

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

    Citation Envoyé par Médiat Voir le message
    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.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  5. #4
    invite6754323456711
    Invité

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

    Citation Envoyé par Médiat Voir le message
    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

  6. A voir en vidéo sur Futura
  7. #5
    Médiat

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

    Citation Envoyé par ù100fil Voir le message
    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

    Citation Envoyé par ù100fil Voir le message
    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.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  8. #6
    invite6754323456711
    Invité

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

    Citation Envoyé par Médiat Voir le message
    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

  9. Publicité
  10. #7
    Médiat

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

    Citation Envoyé par ù100fil Voir le message
    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.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  11. #8
    invite6754323456711
    Invité

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

    Citation Envoyé par Médiat Voir le message
    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

  12. #9
    invite6754323456711
    Invité

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

    Citation Envoyé par ù100fil Voir le message
    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

  13. #10
    Médiat

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

    Citation Envoyé par ù100fil Voir le message
    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).
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

Discussions similaires

  1. Réponses: 13
    Dernier message: 26/01/2009, 23h09
  2. Exercice de proba: est-ce que je respècte bien le formalisme mathématiques?
    Par neokiller007 dans le forum Mathématiques du collège et du lycée
    Réponses: 2
    Dernier message: 22/04/2008, 14h54
  3. Quel est le soft qui est vérolé?
    Par slaytanic dans le forum Logiciel - Software - Open Source
    Réponses: 13
    Dernier message: 29/03/2007, 13h15