Frege's theory of types

TL;DR

This paper reinterprets Frege's theory of types by proposing that first-level function names are better understood as open terms rather than closed function types, offering a more accurate type-theoretic approximation.

Contribution

It introduces an alternative interpretation of Frege's function names as open terms, improving the alignment with simple type theory and extending to second-level functions.

Findings

Frege's Roman markers behave like open terms

The reinterpretation better captures Frege's hierarchy of functions

Extension to second-level functions is natural and consistent

Abstract

It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church's simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose and defend an alternative interpretation of first-level function names in Grundgesetze into simple type-theoretic open terms rather than into closed terms of a function type. This interpretation offers a still unhistorical but more faithful type-theoretic approximation of Frege's theory of levels and can be naturally extended to accommodate second-level functions. It is made possible by two key observations that Frege's Roman markers behave essentially like open terms and that Frege lacks a clear criterion for distinguishing between Roman markers and function names.