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

la notion de langages mathématiques et de preuves irréfutables




  1. #1
    youhouhou

    la notion de langages mathématiques et de preuves irréfutables

    bonjour,

    j'ai une intuition mais je n'arrive pas à la formuler surtout quand j'essaye de la mettre en relation avec entre autre tous les concepts compliqués de : - logique des propositions, du premier ordre, d'ordre supérieur, - calcul des séquents, déduction naturelle, - arithmétique des Preburger, de Peano, - calculabilité, - incomplétude, - etc.

    si je dis que les mathématiques ont pour objet les preuves irréfutables : étant donné un langage mathématique, des règles de déduction, des axiomes (les axiomes peuvent être encodés sous forme de règle donc on oublie les axiomes), on a un monde mathématique qui est par définition l'ensemble des théorèmes qui admettent (dans ce monde mathématiques) une preuve irréfutable.

    donc pour un certain langage et un certain ensemble de règles de déduction : on a un monde mathématique, qui est l'ensemble des théorèmes qu'on peut générer dans ce langage à partir des règles de déduction.

    le problème de la consistance n'en est alors pas vraiment un : certains mondes mathématiques sont consistants (aucun théorème ne peut être à la fois vrai et faux), d'autres ne le sont pas.

    vu sous cet angle : quel est le langage "méta-mathématique" plus ou moins universel qui permettrait de définir n'importe quel langage mathématique, et n'importe quelles règles de déduction ?

    et comment arriver à dire qu'un théorème peut servir de nouvelle règle de déduction, et que définir de nouveaux éléments de langage et de nouvelles règles de déduction c'est plus ou moins une heuristique pour permettre de vérifier plus facilement/rapidement/efficacement des théorèmes plus complexes ?

    par exemple le concept de nombre premier, qui peut être vu comme un nouvel élément de langage dans l'arithmétique, est associé à des théorèmes qu'on peut aussi voir comme de nouvelles règles (par exemple est premier, n'est pas premier si , tout entier admet une décomposition en facteurs premiers) et définir tout ça c'est une heuristique pour étudier beaucoup plus simplement la notion de diviseur commun, ou pour démontrer dans quels cas .

    est-ce que ma question est claire ou pas du tout ?

    -----

    Dernière modification par youhouhou ; 19/06/2015 à 21h19.

  2. Publicité
  3. #2
    Médiat

    Re : la notion de langages mathématiques et de preuves irréfutables

    Bonjour,

    Citation Envoyé par youhouhou Voir le message
    si je dis que les mathématiques ont pour objet les preuves irréfutables
    Au mieux, un pléonasme, en mathématiques, ou il y a une preuve, ou il n'y en a pas ; la notion de preuve réfutable est "non mathématique".

    Un théorème, ou un axiome n'est jamais une règle de déduction.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  4. #3
    youhouhou

    Re : la notion de langages mathématiques et de preuves irréfutables

    Citation Envoyé par Médiat Voir le message
    Bonjour,
    Au mieux, un pléonasme, en mathématiques, ou il y a une preuve, ou il n'y en a pas ; la notion de preuve réfutable est "non mathématique".
    non j'ai l'impression que je ne me suis pas assez bien exprimé.

    on est d'accord que pour faire des maths on a besoin d'un langage, d'un ensemble d'axiomes, et de règles de déduction ?

    on est d'accord que si on définit un langage, un ensemble d'axiomes, et un ensemble de régles de déductions (comme CoQ qui apparemment utiliserait l'arithmétique de Presbuger et le calcul des séquents) on devra se poser des question compliquées comme "quels théorèmes intéressant je pourrai et je ne pourrai pas obtenir dans ce contexte" ?

    donc pour être tranquille, on se pose la question : quel "méta-langage" permettrait de définir n'importe quel langage mathématique, axiomes et règles de déduction ?

    si on avait un tel "méta-langage" on serait sûr de pouvoir définir tous les raisonnements possibles, donc toutes les mathématiques. justement parce que si on ne peut pas formaliser un raisonnement dans ce cadre langage/axiomes/règles c'est à dire qu'il n'y a pas de contexte où ce raisonnement est irréfutable, alors ce raisonnement n'est pas mathématique.
    Dernière modification par youhouhou ; 19/06/2015 à 23h02.


  5. #4
    polf

    Re : la notion de langages mathématiques et de preuves irréfutables

    Bonjour,
    J'ai l'impression que tu imagines une "super-algèbre" à travers ce "méta-langage", qui permettrait d'aboutir à toutes les expressions que l'on puisse atteindre par les mathématiques.
    Personnellement, ça ne me parle pas du tout, car ce "méta-langage" ferait lui-même partie de l'algèbre, et l'on aurait rien inventé.
    Ne me dîtes pas que je me trompe, dîtes moi quelle est la bonne réponse !

  6. #5
    youhouhou

    Re : la notion de langages mathématiques et de preuves irréfutables

    bonjour, merci tu as parfaitement compris ma question.

    moi je vois un intérêt à ce méta-langage : il est nécessaire pour faire un programme de maths qui vérifie (prouve) voire crée des théorèmes sans être dépendant d'un seul système langage/axiomes/règles de déduction.

    et oui il permet de générer indirectement l'ensemble des mathématiques, et directement de définir n'importe quel ensemble, n'importe quelle fonction/opération, mais j'imagine (j'espère) que ce langage doit néanmoins être très simple, d'où son intérêt ?

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

    Re : la notion de langages mathématiques et de preuves irréfutables

    Citation Envoyé par youhouhou Voir le message
    il permet de générer indirectement l'ensemble des mathématiques, et directement de définir n'importe quel ensemble
    Non, c'est impossible, cf. les théorèmes d'incomplétude de Gödel, ou plus simplement qu'il existe un nombre non dénombrables de sous-ensembles de IN, et seulement un nombre dénombrable de définitions.
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  9. #7
    youhouhou

    Re : la notion de langages mathématiques et de preuves irréfutables

    hein ?

    dans le méta-langage on peut définir n'importe quel ensemble. n'importe quel ensemble définissable ! les ensembles non-définissables n'ont absolument aucun intérêt en mathématiques. on peut toujours s'amuser à ajouter à une théorie un axiome disant que tel ensemble E est un ensemble non définissable, mais à part tester le fonctionnement interne de la théorie mathématique ça ne présente pas spécialement d'intérêt. et de toute façon les théorèmes qu'on obtiendrait ainsi resteraient définissables.

    donc non les mathématiques, les seules qui existent (à part dans les rêves de certains mais ce ne sont pas des rêves mathématiques) sont définissables, dénombrables, énumérables, etc...

    ou alors je n'ai pas compris ce que voulait dire "c'est impossible".
    Dernière modification par youhouhou ; 20/06/2015 à 19h59.

  10. Publicité
  11. #8
    Médiat

    Re : la notion de langages mathématiques et de preuves irréfutables

    Passer de "tous les ensembles sont définissables" ce qui est faux (au mieux) à "tous les ensembles définissables sont définissables" qui est un truisme sans intérêt :
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  12. #9
    youhouhou

    Re : la notion de langages mathématiques et de preuves irréfutables

    c'est drôle qu'un logicien bug sur ça.

    les maths ne traitent pas des objets non définissables !


    et sinon pour avancer, je pense que le lambda-calcul typé est un soit équivalent soit est un sous-ensemble syntaxique du méta-langage dont on parle. je suppose qu'il y a équivalence vu que CoQ l'utilise, c'est qu'ils doivent penser qu'on peut définir à peut près n'importe quel ensemble (définissable..) en lambda-calcul typé ?

    et puis de toute façon je ne comprends même pas la définition des booléens en lambda-calcul typé donc...
    Dernière modification par youhouhou ; 20/06/2015 à 20h24.

  13. #10
    youhouhou

    Re : la notion de langages mathématiques et de preuves irréfutables

    j'aurais du regarder https://en.wikipedia.org/wiki/Proof_assistant avant, je crois qu'il y a une partie des réponses aux questions que je me posais.

Discussions similaires

  1. La notion de dimension "physique" en mathématiques
    Par geometrodynamics_of_QFT dans le forum Mathématiques du collège et du lycée
    Réponses: 28
    Dernier message: 06/12/2014, 12h08
  2. Langages indécicables
    Par hansou dans le forum Mathématiques du supérieur
    Réponses: 1
    Dernier message: 04/05/2014, 12h40
  3. demande renseignement sur la notion de famille et la notion de partie !!
    Par fayyouz dans le forum Mathématiques du supérieur
    Réponses: 2
    Dernier message: 23/09/2012, 13h46
  4. Disparitions de langages
    Par zb1000 dans le forum Epistémologie et Logique
    Réponses: 19
    Dernier message: 19/12/2009, 21h53
  5. Processeurs, IDE, Langages
    Par Toufinet dans le forum Électronique
    Réponses: 10
    Dernier message: 08/03/2007, 14h32