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

[invite757adee6]

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 ?
-----

[Médiat]

Bonjour,

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.

[invite757adee6]

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.

[invite5161e205]

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é.

[A voir en vidéo sur Futura]

[invite757adee6]

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 ?

[Médiat]

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.

[invite757adee6]

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".

[Médiat]

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 :

[invite757adee6]

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...

[invite757adee6]

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.