Titre original :
Witness Theory: Notes on λ-calculus and Logic
Contenu du livre :
Ce livre porte sur l'analyse mathématique du concept de preuve formelle en logique classique et constitue - en substance - un long exercice de λ-calcul appliqué.
Suivant des expressions familières remontant à L. E. J. Brouwer, les objets d'étude de cette entreprise sont appelés témoins. Un témoin est censé représenter la preuve logique d'une formule classiquement valide, dans un contexte de preuve donné. Les formalismes utilisés pour exprimer les témoins et leur comportement équationnel sont des extensions du λ-calcul typé pur, considérées comme des théories équationnelles.
Formellement, un témoin est généré à partir de variables témoins décorées - ou typées' - représentant des hypothèses, et d'opérateurs témoins représentant des règles logiques d'inférence.
Les spécifications équationnelles servent à définir les opérateurs de témoins.
En général, on peut le faire en ignorant le "typage", c'est-à-dire les formules logiques elles-mêmes.
D'un point de vue théorique, les témoins sont des objets d'un λ-modèle extensionnel de Scott.
L'approche - appelée génériquement "théorie du témoin" - s'inspire des travaux de N. G. de Bruijn sur une théorie mathématique de la preuve, réalisés à la fin des années 1960 et au début des années 1970 à l'université d'Eindhoven (Pays-Bas), et est similaire à l'approche sous-jacente à la correspondance Curry-Howard, bien connue dans la logique intuitionniste.
Dans le cas classique, les décorations - souvent appelées "types" - sont des formules logiques classiques.
Au niveau sans quantificateur, la théorie équationnelle concernée est le λ-calcul avec appariement surjectif' et certains de ses sous-systèmes, décorés de manière appropriée.
L'extension aux quantificateurs propositionnels, de premier et de second ordre, est simple.
Le livre consiste en une collection de notes et d'articles écrits et diffusés au cours des dix dernières années, dans le prolongement de recherches antérieures menées par l'auteur au cours des années quatre-vingt.
Il comprend entre autres une étude des origines de la théorie moderne de la preuve - de Frege à Gentzen - d'un point de vue de la théorie du témoin, ainsi qu'une application caractéristique de la théorie du témoin à un problème de logique pratique concernant l'axiomatisabilité.
Autres informations sur le livre :
| ISBN : | 9781848903265 |
| Auteur : | |
| Éditeur : | |
| Langue : | anglais |
| Reliure : | Broché |
Achat:
Actuellement disponible, en stock.
