I have almost finished reading Sol Feferman’s excellent book, “In the Light of Logic”, which surveys a number of historical and recent results in Mathematical Logic, particularly Proof Theory, with an eye towards their possible philosophical consequences.  I want to skip ahead to talk about Chapter 13 of the book, “Weyl Vindicated: Das Kontinuum Seventy Years Later”.  In this chapter, Feferman surveys, reconstructs, and reports on his results building on the work of the early-20th-century mathematician Hermann Weyl.  It seems from what Feferman reports that Weyl, while influenced strongly by his doctoral advisor David Hilbert, was nevertheless drawn to the intuitionism of L. E. J. Brower, as providing a better foundation for mathematics than various schemes of axiomatization.  For a prominent example, Russell’s Ramified Theory of Types seemed to require at least one axiom which Computer Scientists would probably describe as a hack: the Axiom of Reducibility was needed to make some things work out, but lacked principled justification.

Weyl set out in his book Das Kontinuum to develop a theory of real-valued functions, including differentiation and integration of continuous functions, on a foundation he found more defensible: a theory of predicatively defined first-order relations on natural numbers. Here, “predicative” means that the definition of a set S (say) is not allowed to refer to a set of sets which contains S.  That is, we cannot base our definition of S on a set of sets containing S.  A simple case of an impredicative definition is defining the set of natural numbers to be the intersection of all sets containing 0 and closed under the successor (“plus 1”) operation.  This definition presupposes the existence of a set U of all sets containing 0 and closed under successor, in order to define the set of natural numbers.  But the set U contains the set of natural numbers — so we are using a set of sets containing the set of natural numbers, in order to define the set of natural numbers.  As Feferman points out, impredicative definitions need not trouble us if our philosophy of mathematics is platonistic: sets of sets really do exist independent of our constructions, so definitions like the one above for the set of natural numbers are simply identifying a set which already exists.  A more constructivist philosophy of mathematics might not allow such a definition, on the grounds that there is no preexisting mathematical reality independent of our constructions, so it is not justified to refer to a set of sets containing N as part of the definition of N.  It is important to note that despite the appeal of Brower’s work, Weyl based his system on classical (2-valued) logic, instead of the intuitionistic logic that came to be identified with Brower’s program.  (As an aside, type theorists Zhaohui Luo and Robin Adams have recently been developing a formalization of Weyl’s project from a type-theoretic perspective; see their “Weyl’s predicative classical mathematics as a logic-enriched type theory“).

Section 8 of Feferman’s chapter on Weyl’s Das Kontinuum is quite interesting for termination analysis.  Feferman presents a theory W, in the spirit of Weyl’s work, in which Weyl’s program (of reconstructing the mathematics of the reals on predicative foundations) can be carried out.  This theory W is essentially a theory of general recursive functions, described by individual terms, and classified by what a Computer Scientist would see as simple types (base type N for natural numbers, function types $S\stackrel{\sim}{\rightarrow} T$ for partial functions from $S$ to $T$, and cartesian production types).  Classification is done with an explicit membership predicate $\in$, and the simple types are expressed as class terms of the language. (So types are not a distinct syntactic category; rather, they are expressed as terms of the language, and the connection with individual terms is given by an atomic formula of the language, using the $\in$ predicate.)

Theory W is based on Beeson’s Logic of Partial Terms (LPT), which has an explicit predicate $\downarrow$ for definedness.  In W, $\downarrow$ is used for termination of general recursive functions.  There are axioms for definition by primitive recursion and search, as well as induction, in the form that if $a\in\mathcal{P}(N)$, and $0\in a$ and $a$ is closed under successor, then every $n\in N$ is in $a$.  Here, $\mathcal{P}(N)$ is defined as $N \stackrel{\sim}{\rightarrow} \{ 0, 1 \}$ (that is, as the class of characteristic functions for subsets of N).  This theory does not allow us to state that a class $T_1$ is a member of another class $T_2$, unless of course the former is representable by an individual term.

Despite its expressivity, W is a conservative extension of Peano Arithmetic.  This is, in a sense, not too surprising (but perhaps I am being naive), since the form of class terms is quite restricted, and induction is just the usual natural-number induction.  Feferman goes on to outline how the theory of analysis of real-valued functions can be developed “at least for separable Banach and Hilbert spaces” in a straightforward way.  On the basis of this, and with some discussion of potential counterexamples, Feferman claims that all of scientifically applicable mathematics (certainly a very large portion of it) can be developed in theory W.

In the end, what is the possible application for Computer Science here?  Theory W is an example of an expressive but proof-theoretically relatively weak theory, in which it is possible to reason about termination of general recursive functions, based on a notion of type (the class terms of W).  So it is an example of the combination of total and partial functions that is of interest for developing dependently typed programming languages with a logically sound notion of proof, or alternatively, for extending total type theories to allow general recursion.  This is the theme, by the way, of a FLoC workshop which I am hoping to submit a paper to.  The workshop is called “Partiality and Recursion in Interactive Theorem Provers“.