La suite de mes commentaires sur le systeme deductif du Professeur Prouté :
page 11, section 3.2 :
Toutefois, quelle que soit cette facon, il n’en reste pas moins vrai que le theoreme de Diaconescu demeurera indemontrable [dans la theorie des types de Martin-Lof]"
(rappel : le theoreme de Diaconescu enonce que axiome du choix implique intuitionistiquement le tiers exclus)
A-t-on une PREUVE que ce theoreme n'a pas de demonstration dans la theorie des types de Martin-Lof ? Et si oui, cette preuve utilise quel systeme ? L'avis du Professeur Prouté semble bien tranché alors que bien des questions restent sans reponse.
page 12, avant la section 4:
"Le fond du probleme est donc me semble–t–il le fait que le systeme de Martin–Lof est en contradiction avec le principe de l’unicite du temoin, ou de l’indiscernabilite des preuves. Il en va de meme de tous les systemes de type “Curry–Howard”"
Il est facile de renoncer a toute la theorie des types sur un "me semble-t-il". N'est-ce pas plutot le principe d'indiscernabilite des preuves qui est en contradiction avec Curry-Howard que le contraire ?
On peut continuer ainsi en listant tous les arguments du Professeur Prouté qui ne reposent que sur des affirmations et des arguments purement philosophiques et subjectifs. Le refus de la theorie des types du Professeur Prouté ne tient donc pas.
Bien qu'il soit difficile de confirmer ou d'infirmer, en une nuit, le fondement du systeme deductif du Professeur Prouté, les arguments qu'il avance afin d'ecarter la theorie des types sont fumeux.
Il semble evident que la plupart des arguments qu'il apporte n'ont aucun fondement :
page 5, section 2.1 :
"meme si la facon de demontrer un theoreme peut pour diverses raisons interesser le mathematicien, ce dernier ne se soucie aucunement de la facon dont un theoreme a ete demontre pour l’appliquer."
Les mathematiciens peuvent rester tres deconnectés du monde materiel. Ils ne se soucient donc pas forcement de l'adequation entre les preuves des theoremes et le monde reel. Au contraire, lorsque l'on veut "prouver" que tel avion n'explosera pas en vol, il faut rester beaucoup plus proche de l'implementation effective (le programme informatique). Il faut alors se soucier de la facon dont le theoreme est demontré (ce qui implique de se soucier du sens de demontrer un theoreme)
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique
page 5, section 2.1 :
"Si pour appliquer un theoreme, il fallait tenir compte de la facon dont il a ete demontre, les mathematiques serait beaucoup plus complexes qu’elles ne le sont deja."
On peut (et dans certains cas, il faut) tenir compte de la facon dont un theoreme est demontre, ce que ne font generalement pas les mathematiciens. Il est evident que les mathematiques sont bien plus complexes que ce qui est decrit par les mathematiciens. Cet argument n'est pas fonde non plus.
page 6, section 2.3 :
"On n’ecrit pas non plus [des preuves] de la meme facon pour des mathematiciens chevronnes et pour des etudiants de premiere annee. [...] Les preuves supportent donc l’a peu pres, contrairement aux calculs, qui doivent etre beaucoup plus precis"
Qui peut definir la difference entre ce qu'est un calcul et ce qu'est une preuve ? Et si l'on ecrit plus (en quantité) pour les mathematiciens chevronnes, n'est-ce pas parce qu'ils demandent plus ? Et les etudiants ne sont-ils pas capable de chercher une preuve complete si ils ne sont pas convaincus par leur cours ?
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique.
page 6, section 2.4
"Si les informaticiens avaient autant de chance que les mathematiciens, ils leur suffirait de lire les types des fonctions pour pouvoir les utiliser"
Parce qu'il suffit a un mathematicien de lire un enoncé "vrai" pour en avoir la preuve ? Tout cela depend bien evidemment du systeme deductif considere. Par exemple en Coq, un type peut definir complement le comportement d'une fonction.
page 9, section 3.2 :
"Le systeme de Martin–Lof est consistant. S’il ne l’est pas, il sera de toute facon sans interet. Il semble toutefois que sa consistance absolue ait ete prouvee par les methodes de la normalisation forte (Tait, Girard, Coquant,. . .)."
Le fait que sa non-consistance aneantisse son interet suffit-elle a prouver sa consistance ? Que signifie "consistance absolue" ??? La normalisation forte d'un systeme ne permet que de prouver sa consistance si l'on suppose le meta-systeme consistant. En bref, cette phrase ne semble pas avoir de sens.
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par schount . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. Évalué à 5.
page 11, section 3.2 :
Toutefois, quelle que soit cette facon, il n’en reste pas moins vrai que le theoreme de Diaconescu demeurera indemontrable [dans la theorie des types de Martin-Lof]"
(rappel : le theoreme de Diaconescu enonce que axiome du choix implique intuitionistiquement le tiers exclus)
A-t-on une PREUVE que ce theoreme n'a pas de demonstration dans la theorie des types de Martin-Lof ? Et si oui, cette preuve utilise quel systeme ? L'avis du Professeur Prouté semble bien tranché alors que bien des questions restent sans reponse.
page 12, avant la section 4:
"Le fond du probleme est donc me semble–t–il le fait que le systeme de Martin–Lof est en contradiction avec le principe de l’unicite du temoin, ou de l’indiscernabilite des preuves. Il en va de meme de tous les systemes de type “Curry–Howard”"
Il est facile de renoncer a toute la theorie des types sur un "me semble-t-il". N'est-ce pas plutot le principe d'indiscernabilite des preuves qui est en contradiction avec Curry-Howard que le contraire ?
On peut continuer ainsi en listant tous les arguments du Professeur Prouté qui ne reposent que sur des affirmations et des arguments purement philosophiques et subjectifs. Le refus de la theorie des types du Professeur Prouté ne tient donc pas.
En esperant t'avoir obscurci.
PS : les numeros de page et de section correspondent au document
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
[^] # Re: Anubis et les "catégories bicartésiennes fermées"
Posté par schount . En réponse à la dépêche Sortie de la version 2.5 du langage Tom. Évalué à 3.
Bien qu'il soit difficile de confirmer ou d'infirmer, en une nuit, le fondement du systeme deductif du Professeur Prouté, les arguments qu'il avance afin d'ecarter la theorie des types sont fumeux.
Il semble evident que la plupart des arguments qu'il apporte n'ont aucun fondement :
page 5, section 2.1 :
"meme si la facon de demontrer un theoreme peut pour diverses raisons interesser le mathematicien, ce dernier ne se soucie aucunement de la facon dont un theoreme a ete demontre pour l’appliquer."
Les mathematiciens peuvent rester tres deconnectés du monde materiel. Ils ne se soucient donc pas forcement de l'adequation entre les preuves des theoremes et le monde reel. Au contraire, lorsque l'on veut "prouver" que tel avion n'explosera pas en vol, il faut rester beaucoup plus proche de l'implementation effective (le programme informatique). Il faut alors se soucier de la facon dont le theoreme est demontré (ce qui implique de se soucier du sens de demontrer un theoreme)
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique
page 5, section 2.1 :
"Si pour appliquer un theoreme, il fallait tenir compte de la facon dont il a ete demontre, les mathematiques serait beaucoup plus complexes qu’elles ne le sont deja."
On peut (et dans certains cas, il faut) tenir compte de la facon dont un theoreme est demontre, ce que ne font generalement pas les mathematiciens. Il est evident que les mathematiques sont bien plus complexes que ce qui est decrit par les mathematiciens. Cet argument n'est pas fonde non plus.
page 6, section 2.3 :
"On n’ecrit pas non plus [des preuves] de la meme facon pour des mathematiciens chevronnes et pour des etudiants de premiere annee. [...] Les preuves supportent donc l’a peu pres, contrairement aux calculs, qui doivent etre beaucoup plus precis"
Qui peut definir la difference entre ce qu'est un calcul et ce qu'est une preuve ? Et si l'on ecrit plus (en quantité) pour les mathematiciens chevronnes, n'est-ce pas parce qu'ils demandent plus ? Et les etudiants ne sont-ils pas capable de chercher une preuve complete si ils ne sont pas convaincus par leur cours ?
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique.
page 6, section 2.4
"Si les informaticiens avaient autant de chance que les mathematiciens, ils leur suffirait de lire les types des fonctions pour pouvoir les utiliser"
Parce qu'il suffit a un mathematicien de lire un enoncé "vrai" pour en avoir la preuve ? Tout cela depend bien evidemment du systeme deductif considere. Par exemple en Coq, un type peut definir complement le comportement d'une fonction.
page 9, section 3.2 :
"Le systeme de Martin–Lof est consistant. S’il ne l’est pas, il sera de toute facon sans interet. Il semble toutefois que sa consistance absolue ait ete prouvee par les methodes de la normalisation forte (Tait, Girard, Coquant,. . .)."
Le fait que sa non-consistance aneantisse son interet suffit-elle a prouver sa consistance ? Que signifie "consistance absolue" ??? La normalisation forte d'un systeme ne permet que de prouver sa consistance si l'on suppose le meta-systeme consistant. En bref, cette phrase ne semble pas avoir de sens.
(au fait, le mot francais est "coherent")
la suite dans le post suivant