Du bruit au signal (et inversement)

signalement via Lambda the Ultimate

Un récent article de Mark van Atten:
The Development of Intuitionistic Logic

Conférence de Jean-Yves Girard sur Canal-U
le 17/06/2000
La "crise des fondements" s'ouvre en 1897 avec le paradoxe de Burali-Forti, une contradiction dans la toute jeune théorie des Ensembles. Parmi les solutions proposées, le "Programme de Hilbert " (~ 1925) accorde un rôle privilégié à la non-contradiction formelle. Le théorème d'incomplétude de Gödel (1931), qui réfute le programme de Hilbert, a fait le désespoir de tous ceux qui cherchaient une réponse définitive à leurs angoisses fondationnelles. Il a aussi gêné ceux qui cherchaient plus simplement à comprendre la nature des objets mathématiques. Ce n'est qu'avec le développement de l'informatique qu'ont pu se dégager de nouveaux axes de lecture, en rupture de plus en plus nette avec le réductionnisme Hilbertien.

The formal systems that are nowadays called λ-calculus and combinatory logic were both invented in the 1920s, and their aim was to describe the most basic properties of function-abstraction, application and substitution in a very general setting. In λ-calculus the concept of abstraction was taken as primitive, but in combinatory logic it was defined in terms of certain primitive operators called basic combinators. The present article will sketch the history of these two topics through the twentieth century.
.../...
Seen in outline, the history of λ and CL splits into three main periods:  first, several years of intensive and very fruitful study in the 1920s and ’30s; next, a middle period of nearly 30 years of relative quiet; then in the late 1960s an upsurge of activity stimulated by developments in higher-order function theory, by connections with programming languages, and by new technical discoveries.  The fruits of the first period included the first-ever proof that predicate logic is undecidable.  The results of the second attracted very little non-specialist interest, but included completeness, cut-elimination and standardization theorems (for example) that found many uses later.  The achievements of the third, from the 1960s onward, included constructions and analyses of models, development of polymorphic type systems, deep analyses of the reduction process, and many others probably well known to the reader. The high level of activity of this period continues today.
.../...
By Felice Cardone and  J. Roger Hindley, 2006
To be published in Volume 5 of Handbook of the History of Logic, Editors Dov M. Gabbay and John Woods, Elsevier Co.

Article au format PDF

Voir aussi:
Proofs and Types by Jean-Yves Girard, translated and with appendices by Paul Taylor and Yves Lafont
Cambridge University Press, 1989