Between Logicism and Metalogic

The project will investigate a critical transition phase in the evolution of mathematical logic. The period in question stretches from the mid 1920s to the consolidation of metalogic in the 1940s. It is marked by a significant reconception of formal logic, i.e. a gradual transformation of its subject matter, its scope, and its boundaries. It eventually leads to the formation of metalogical disciplines such as formal semantics and proof theory as well as to the consolidation of first-order logic as the standard logical system. The principal objective of this project is to provide a systematic and comparative study of work on mathematical logic that immediately preceded these developments. Specifically, the focus will be set on several conceptions and uses of logical type theory (and higher- order logic more generally) between 1925 and 1940. Type theory (henceforth TT) was originally introduced in Russell`s foundational work on mathematics, culminating in his groundbreaking Principia Mathematica (Whitehead & Russell 1910-1913). As has been shown recently (Ferreirs 2001, Mancosu et al. 2009), it was substantially modified in the subsequent development and eventually came to serve as the "natural" logic in the 1920s and 1930s. Moreover, it was no longer conceived exclusively as a "foundational system for mathematics" in the original Russellian sense but rather as a "basic system of logic" useable for a wide spectrum of different, explicitly non- foundational applications in mathematics, the formal sciences, and in philosophy. The current project will be devoted to a historically precise investigation of this post-Principia evolution of TT from 1925 onwards. Specifically, it will explore different applications of it to formal concept formation in mathematics and in metamathematics. It thereby seeks to provide a first comprehensive survey of these non-foundational uses of TT and their conceptual interrelations in the period in question. In the present literature, the "golden age" of TT in the 1920s and early 1930s is usually characterized as a short transition phase between classical logicism and the consolidation of first-order logic that is without deeper relevance for the subsequent evolution of logic and metalogic. This historical picture is limited since it fails to take into account the formative character of work on TT with respect to these later developments, in particular to the formation of formal semantics. The project will present a substantially refined account of the conceptual transformations within mathematical logic after 1925 and of the origins of modern logical metatheory. It also seeks to integrate the historical reconceptions and uses of TT within contemporary debates on the philosophy of higher-order logic, in particular on its formal semantics, its mathematical applications, and its relation to set theory.

The project will investigate a critical transition phase in the evolution of mathematical logic. The period in question stretches from the mid 1920s to the consolidation of metalogic in the 1940s. It is marked by a significant reconception of formal logic, i.e. a gradual transformation of its subject matter, its scope, and its boundaries. It eventually leads to the formation of metalogical disciplines such as formal semantics and proof theory as well as to the consolidation of first-order logic as the standard logical system. The principal objective of this project is to provide a systematic and comparative study of work on mathematical logic that immediately preceded these developments. Specifically, the focus will be set on several conceptions and uses of logical type theory (and higher-order logic more generally) between 1925 and 1940. Type theory (henceforth TT) was originally introduced in Russell's foundational work on mathematics, culminating in his groundbreaking Principia Mathematica (Whitehead & Russell 1910-1913). As has been shown recently (Ferreirs 2001, Mancosu et al. 2009), it was substantially modified in the subsequent development and eventually came to serve as the natural logic in the 1920s and 1930s. Moreover, it was no longer conceived exclusively as a foundational system for mathematics in the original Russellian sense but rather as a basic system of logic useable for a wide spectrum of different, explicitly non-foundational applications in mathematics, the formal sciences, and in philosophy. The current project will be devoted to a historically precise investigation of this post-Principia evolution of TT from 1925 onwards. Specifically, it will explore different applications of it to formal concept formation in mathematics and in metamathematics. It thereby seeks to provide a first comprehensive survey of these non-foundational uses of TT and their conceptual interrelations in the period in question. In the present literature, the golden age of TT in the 1920s and early 1930s is usually characterized as a short transition phase between classical logicism and the consolidation of first-order logic that is without deeper relevance for the subsequent evolution of logic and metalogic. This historical picture is limited since it fails to take into account the formative character of work on TT with respect to these later developments, in particular to the formation of formal semantics. The project will present a substantially refined account of the conceptual transformations within mathematical logic after 1925 and of the origins of modern logical metatheory. It also seeks to integrate the historical reconceptions and uses of TT within contemporary debates on the philosophy of higher-order logic, in particular on its formal semantics, its mathematical applications, and its relation to set theory.