The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, whereas the (...) higher-order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory. (shrink)

It is well known that the circumflex notation used by Russell and Whitehead to form complex function names in Principia Mathematica played a role in inspiring Alonzo Church's “lambda calculus” for functional logic developed in the 1920s and 1930s. Interestingly, earlier unpublished manuscripts written by Russell between 1903–1905—surely unknown to Church—contain a more extensive anticipation of the essential details of the lambda calculus. Russell also anticipated Schönfinkel's combinatory logic approach of treating multiargument functions as functions having other functions as value. (...) Russell’s work in this regard seems to have been largely inspired by Frege’s theory of functions and “value-ranges”. This system was discarded by Russell due to his abandonment of propositional functions as genuine entities as part of a new tack for solving Russell’s paradox. In this article, I explore the genesis and demise of Russell’s early anticipation of the lambda calculus. (shrink)

Frege uses Greek letters in two different ways in his Begriffsschrift. One way is the familiar use of bound variables, in conjunction with variable-binding operators, to mark and close argument-places. The other, which is quite unfamiliar, employs letters to mark places for operators to reach into, without thereby closing these places. Frege thereby invents a powerful and compact notation for functional operations which can be recommended even today. His regrettable double use of Greek letters obscured his invention, and this, together (...) with the fact that in the Grundgesetze he no longer has need of function-valued functions, explains why the device was overlooked and has not passed into general use. (shrink)

In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite (...) recent work, however,has proved valuable not only in the philosophy andfoundations of mathematics, but has also foundpractical application in computer science, where thelanguage of constructivism serves as an implementableprogramming language, and within the philosophy oflanguage.\footnote{Nordstr\"{o}m et al. give an overview of the work in computerscience, whereas Ranta provides an impressiveconstructivist alternative to Montague Grammar usingthe richer type structure of Martin-L\"{o}f in placeof the simple classical type theory of Church.} Mypresentation will be carried out through a contrastwith standard metamathematical work.\footnote{Troelstra and van Dalen give an encyclopedictreatment of the metamathematics of constructivism.}In the course of the development I have occasion tooffer some novel considerations on thenature of proof and inference. (shrink)

Editorial NoteThis lecture was given by Per Martin-Löf at Leiden University on August 25, 2001 at the invitation by Göran Sundholm to address the topic mentioned in the title and to reflect on Dummett’s earlier effort of almost a decade before. The lecture was part of a three-day conference on Gottlob Frege. Sundholm arranged for the lecture to be recorded and commissioned Bjørn Jespersen to make a transcript. The information in footnote 1, which Sundholm provided, has been independently confirmed by (...) Thomas Ricketts in an email to the author. The present version has been edited by Ansten Klev. Following the displayed text there is a lacuna in the original transcript corresponding to a pause in the recording when the tape was changed. The continuous text of the present version is the result of a few additions to the original transcript suggested by Klev and agreed to by the author. (shrink)

Inference versus consequence , an invited lecture at the LOGICA 1997 conference at Castle Liblice, was part of a series of articles for which I did research during a Stockholm sabbatical in the autumn of 1995. The article seems to have been fairly effective in getting its point across and addresses a topic highly germane to the Uppsala workshop. Owing to its appearance in the LOGICA Yearbook 1997 , Filosofia Publishers, Prague, 1998, it has been rather inaccessible. Accordingly it is (...) republished here with only bibliographical changes and an afterword. (shrink)

λ-calculi are of interest to logicians and computer scientists but have largely escaped philosophical commentary, perhaps because they appear narrowly technical or uncontroversial or both. I argue that even within logic λ-expressions need to be understood correctly, as functors signifying functions in intension within a categorical or typed language. λ-expressions are not names but pure viable binders generating functors, and as such they are of use in giving explicit definitions. But λ is applicable outside logic and computer science, anywhere where (...) the notions of complex whole, substitution, abstraction and structure make sense. To illustrate this, two domains are considered. One is somewhat frivolous: the study of flags; the other is very serious: manufacturing engineering. In each case we can employ λ-abstraction to describe substitutions within a structure, and in the latter case there is even a practical need for such a notation. (shrink)