Philosophy of Mathematics

We mention philosophy because in a sense Nuprl embodies a philosophy of mathematics. It demonstrates that it is possible to conduct a "mathematical discourse" with a computer. We can trace backwards from the interactions to the principles of physics and information science that determine the outcome of that interaction. So, we can reduce explanations of mathematical discourse to basic principles. This is a contribution to an analysis of the foundations of mathematics, which is a philosophical matter.

We also notice that the potential for more elaborate and extensive mathematical discourse with Nuprl is apparently unlimited. As we push forward into the more complex realms of this interaction, we will see what else can be reduced to these same primitives. This enterprise means that we will always be engaged in a philosophical as well as a scientific investigation.

Context

A simplistic view of the philosophy of mathematics says that there are four schools of thought: Platonism; Logicism; Formalism; and Intuitionism. Actually there are many variations and distinctions, but we will not elaborate beyond a simple model for now. These schools can be summarized as follows.

Platonism
Based on Plato's notion that there is an ideal world of concepts and objects. For example, there is an ideal notion of number or line. We perceive only "shadows" of the ideal world projected on the walls of a cave. But these ideal notions are the objects of philosophy and science. They are the immutable eternal reality. In the case of mathematics, modern Platonists like Gödel believe that objects like sets exist in this ideal world, and our task is to discover their properties. This is a powerful and coherent view of foundations and it is subscribed to by such giants as Gödel.
Logicism
Takes the view that the basic concepts of mathematics can be defined from the universal principles of logic. Frege and Russell developed this view extensively. Its power can be seen in the single example of the notion of the ancestral relation. If we define the notion of x is the mother of y and from its transitive closure as the relation x is the ancestor of y, then we can see that if u and v are ancestors of x, then either u is an ancestor of v or v is an ancestor of u. This to Frege is a principle of logic. From it and a few other principles that he saw as parts of logic (including the notion that there are an infinity of objects), the notion of number, function and sequence can be defined, and from them all of mathematics.
Intuitionism
Elaborates the view of Kant that the structure of the human mind implies that it comprehends intuitively the notions of space, time and number. The truths about these concepts are truths of how the mind works. L. E. J. Brouwer elaborated on these ideas in his philosophy of Intuitionism. Chomsky has traced mathematical ability to what he believes is an innate "hardwired" capacity of the human mind to process natural language.
Formalism
The view that mathematics is a meaningless game of manipulating symbols. Certain "games" are more interesting than others because of their social use. Otherwise the rules are quite arbitrary, and there is no meaning to mathematical activity.

Contributions

Our work shows that we can communicate mathematics to computers endowed with a certain physical structure, say electronic digital computers that can implement universal computers in the sense of Turing and Church. It suggests that meaning can arise out of mental capabilities. In this sense the ideas of Kant, Brouwer and Chomsky seem to shed light on the enterprise. The Platonic notion is perhaps not so useful. Formalism does not seem to recognize the fact that certain computational abilities are necessary and are essential parts of the formal language and hence essential parts of an explanation of what enables mathematical discourse. As for Logicism, this might just be a matter of definition. In the case of Nuprl's constructors, we might say that if we remove that natural numbers as primitive but keep recursive type definitions, then we can rebuild the numbers and hence the rest of mathematics. But we need the "higher order" parts of logic, namely functions.