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.
[^] # 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