Retour à la page du séminaire

9/12/99 : Michel Parigot (Paris 7)
Sur l'interpretation calculatoire du raisonnement par l'absurde.

Résumé

Les calculs associés à la logique classique tels que LambdaC ou LambdaMu donnent un contenu calculatoire a nnA -> A, sous forme de la constante C ou de l'opérateur Mu. On discutera de la possibilité de donner une interprétation "triviale" de nnA -> A, autrement dit d'ajouter au Lambda-calcul typé habituel la règle:

t : nnA
-------
t : A

et du sens calculatoire de cette interprétation.