Subsections

4. Foundations

4.1 Principia Mathematica and Post Productions

Having begun with Russell's Introduction to Mathematical Philosophy [WR13] it was natural eventually to come down to (some of) the detail in Principia Mathematica [WR13] and Mathematical Logic as Based on The Theory of Types [Rus08]. Coming to Russell's theory of types from a background in computing, I was immediately inclined to regard the vicious circle principle as heavy handed. The apparent proscription of recursive definitions (though the self reference in well-founded recursion turns out to be eliminable), and the real proscription of self-applicative functions is an enduring problem in the foundations of mathematics.

It was another kind of reservation about Principia Mathematica which lead to my first conception of how the formal foundations of mathematics might be improved. This reservation was about how well the theory of types was defined in Principia Mathematica, which by contrast with the precision with which the syntactic aspects of programming languages were defined seemed very woolly and unclear. I had previously been impressed by the various simple languages for describing Turing computable functions, and it seemed in the spirit of foundationalism to reduce the syntax of the foundation to one of these very simple languages. I chose post productions as the notation most appropriate for the description of syntax and set out briefly as an undergraduate to effect a description of Russell's theory of Types ultimately in post productions. I didn't get very far.

This was the first of a long sequence of forays into the design of foundation systems which continue to the present day.

4.1.1 Reflection in Logical AI

When I graduated with my degree in Mathematics and Philosophy I intended to do a PhD relating to the development of software supporting the formal derivation of mathematics, and went to the Computer Science Department at the University of Warwick with that in mind. Personal problems interfered with this plan, and after less than one year at Warwick I abandoned my studies are took a job in software development. My interest in the foundations of mathematics then lay dormant for several years.

It resurfaced after a period working in ``knowledge engineering'' [Jonb] while I was working on database query software. I then started to think about what kind of logical foundation system would be appropriate for use in a ``knowledge base'' in which the database was logically an suitably structured collection of definitions, query a process of inference in the theory determined by those definitions, and database update a process of extending or modifying these definitions [Jond]. It seemed then to me that in order for this knowledge base to evolve towards intelligent behaviour it would have to be possible for it to reflect upon and modify its methods in the light of experience. The deductive system which maintained the knowledge would have to be stored in the knowledge base, it would represent a functional program operating on a functional data structure which included itself.

In this way I came to seek a logical foundation system which was capable of reasoning about itself, and in particular, which was implemented as a function which was continually applied to an elaborate data structure which included itself. The foundation system would therefore have to admit functions which fell within their own domain.

It was natural to look to combinatory logic for such a foundation system, particularly because combinatory logic had recently become fashionable in the implementation of functional programming languages. I was disappointed when I eventually discovered that combinatory logics were, when not inconsistent, rather weak. There then began a period in which I conceived of myself as in search of strong reflexive foundation systems. Though I might have been happy to adopt one if I could find it, it seemed likely that I would have to devise one for myself, for which task I was ill-equipped.

4.1.2 Foundation Systems for Formal Specification and Verification

Having transferred from databases to the application of formal methods to the development of secure systems my interest in foundation systems developed further.

There were first of all some instructive errors (see: [Jonc,Jona]).

Consistency strength as a key element in a foundation system,

4.1.3 Semantics for Well-Founded Specification Languages

Semantics for VDM and Z. Alternate foundational ontologies.

4.1.4 Set Theories with a Universal Set

Set theories with a Universal Set.

Roger Bishop Jones 2016-01-07