RBJ's Work on The Foundations of Mathematics

Overview:

An overview of the work I have done on the foundations of mathematics.
Introduction
Some preliminary observations.
Real Computation
My first recollected interest in foundations arose from a concern for better implementation of real analysis on computers, which lead me to consider (though later put aside) constructive rather than classical analysis.
Post Productions
When I became acquainted with Principia Mathematica it all seemed a bit mushy to me. I set about trying to reduce the foundations of mathematics to post productions.
Reflexive Foundations
As a result of trying to design an intelligent knowledge-based system I decided I needed a reflexive foundation system and set about, first looking for one, then trying to devise one.
Classical Foundations
Having decided that formal specification languages ought to be foundation systems I did some work on well-founded systems suitable for languages like VDM and Z.
Pure Categories
I also made an experiment in building a foundation out of pure categories and functors, using the same techniques I had used for other classical foundation systems.
Mechanisation
I led the implementation of ProofPower, a tool supporting the formal development of theories in Higher Order Logic. I continue to advocate the mechanisation of mathematics through this web site.

Introduction:

Some preliminary observations.

Real Computation:

My first recollected interest in foundations arose from a concern for better implementation of real analysis on computers, which lead me to consider (though later put aside) constructive rather than classical analysis.
on the margin
Even I don't really regard this in any significant sense as work on the foundations of mathematics, but what I am going to mention here are the first stirrings of interest in foundational issues which I can remember.
Minsky
Since about 1967 I had been aware from Minsky ([Minsky67]) of the idea of a computable real, and of the distinction between that and the real reals. In 1972, just before I returned to University to do my first degree in Maths and Philosophy I spent some time ruminating in this area.
Turing, Church, Post
Probably following references from [Minsky67] I obtained copies of seminal papers by Alan Turing, Alonzo Churchand Emil Post relating to computability. I don't think I actually understood much of the detail.
Reals
I came to the view that the inadequacy of the available implementations of real arithmetic (on computers) was partly attributable to the fact that mathematics had been developed using the classical concept of real number and that it would all have been much better if it had been done with computable numbers.
Constructive Mathematics
By these means, before I knew much more mathematics than I learnt at school, I found myself with constructive inclinations. I'm not at all sure that I had even heard of constructive or intuitionistic mathematics at that time. Later I concluded that the problems which concerned me could be remedied within the framework of classical real analysis.
Computing with Reals
My interest, though not a very active one, persists to the present day and gave rise to a few web pages.

Post Productions:

When I became acquainted with Principia Mathematica it all seemed a bit mushy to me. I set about trying to reduce the foundations of mathematics to post productions.
Mathematical Proof
By the time I started studying maths as a principle subject at university I was already corrupted. I didn't like the culturally defined notion of mathematical proof and thought it would be much better to do the proofs properly. So, I did foundational studies on the side, trying to get a better idea of what was involved.
Principia Mathematica
I spent some time working through the elementary parts of Principia Mathematica using a different logic (one from [Hunter], see: ). I was dissatisfied with Principia in two ways.
Vicious Circles
The first was that I didn't like the type system. Having learnt a lot about computing before coming to Russell, I didn't like what seemed to me an unduly paranoid attitude towards circularity (notwithstanding Russell's paradox). Here began a dislike of the limitations of "well-founded" foundation systems which is still with me, and has motivated a great deal of my foundational ruminations from then til now.
Mush
It was pretty clear to me that Russell's logical system was defined very poorly.
Sorting Russell with Post
I didn't have much idea about semantics in those days, but I thought a good way of pinning down the syntax would be to define it using post productions. So I spent a fair bit of time during the summer of 1975 working on this problem and had in mind turning it into a final year philosophy project. Towards the end of the autumn term it became pretty obvious that what I was trying to do was to large a project and it got shelved.
Infinite Regress
This was my first confrontation with the problem of infinite regress in defining the foundations of mathematics. I am still interested in this problem, which however I don't regard as a particularly difficult one. My perferred approach these days is to provide "meta-circular" formal definitions supplemented with informal disambiguation and some study of the potential ambiguities and way of formally eliminating them.

Reflexive Foundations:

As a result of trying to design an intelligent knowledge-based system I decided I needed a reflexive foundation system and set about, first looking for one, then trying to devise one.
Artificial Intelligence
I was interested in AI and in about 1983 I managed to get myself into a part of ICL doing "knowledge engineering". I also bought an ICL PC and started in my own time working on the design of an intelligent knowledge based system. This got me into thinking about foundation systems again. In 1985 I wrote a paper discussing this "work" for presentation at an "Appin Workshop on Persistent Databases" in which I took the position that knowlege representation languages must be logic and discuss the question of what kind of logic is suitable for that purpose.
Reflexive Foundations
One of the key requirements which I then identified was that the logic be "reflexive", for which read: allowing self-application of functions, non-well-founded. The motivation at this time was simply that an intelligent system must be capable of introspection, and that the proposed system involved a functional knowledge-base which was invoked by applying a function contained in the knowledge-base to the whole knowledge-base. So I set about looking for a logic which would be suitable for this kind of application. There is no sign that I was aware at this time of any precise distinction between a foundation system and other kinds of logic, though it was foundation systems that I was looking at.
Combinatory Logic
I thought for a while that Combinatory Logic would do the trick. This seemed particularly appropriate because combinators had been introduced as an implementation technique for functional programming languages, and my prototype knowledge base was combinator reduction system. Then I discovered that a foundation system combinatory logic had not been very successful and that the versions of combinatory logic which were known to be consistent were weak. At this point my search for a suitable foundation system turned from "find" to "invent" and I spent many years tugging at this problem until I decided that it wasn't really necessary to have a reflexive foundation system. I do still think it is desirable.
False Dawns
At the beginning of 1986 I switched from relational databases to formal methods, which allowed me to do work which came somewhere near the foundations of mathematics. Shortly after this switch made what I then thought a great breakthrough (and which I now regard as one of my more instructive errors). This resulted in two papers which were published in extremely obscure corners. The first, Logical foundations and formal verification put forward a stunningly simple formal system as a foundation for program verification (for which you may now read mathematics). The second, Creative Foundations for Program Verification provides a more concise rendering of the sense in which the logical system identified is universal, though it was not until some time later that I realised that the sense in which a foundation systems needs to be universal (to be properly so called) is a stronger one.

Classical Foundations:

Having decided that formal specification languages ought to be foundation systems I did some work on well-founded systems suitable for languages like VDM and Z.
VDM Standardisation
While continuing puzzling over reflexive foundations, I was provoked into giving some thought to well-founded systems by becoming involved in the standardisation activity for the specification language for VDM (the Vienna Development Method). This was during for a period starting sometime in 1986 until the VDM88 conference in September 1988, at which I gave a side presentation on the foundational work I had been doing (before putting that on the shelf).
Axes (to grind)
While I was involved in VDM standardisation I had two axes to grind. That we should define a proof system, and that the specification language together with its proof rules should be a mathematical foundation system.
Proof System
I tried to get the standardisation committee to take proof seriously and to include "proof theory" in the standard as well as semantics. By this I meant just that a logical system in which one could reason about the specification should be defined. Hitherto it had been assumed that the logic was something quite distinct from the spefication language, and that some suitable (probably three-valued logic) would be used for that purpose. This didn't make any sense to me, the proof rules have to be proof rules for the specification language, otherwise there would be some translation involved which would be a source of error.
Foundation System
I further, and less successfully, argued that the specification language with its logic should amount to a foundation system, i.e. that it should be strong enough for the development of mathematics by conservative extension alone and similar in proof theoretic strength to ZFC, on the premise that there was no part of mathematics which might not prove necessary for program verification. A definition of the semantic domains for the language had already been developed and this seemed to me unsuitable for mathematical foundation system (e.g. function spaces were continuous).
New Classical Foundations suitable for VDM and Z
New Classical Foundations
Having argued that the VDM specification language should be amount to a mathematical foundation system, I felt that the proposed semantic domains would not be suitable for such a language, and set about devising more suitable domains. It was a constraint in the design of the language that it would not require reflexive semantic domains, and so my work on reflexive foundations could be put aside. I considered what kind of adjustments to classical set theory would be desirable in this more conservative context.
Desirable Features
I identified the following features as being desirable in semantic domains for languages such as VDM and Z:
  1. Polymorphism of the Milner kind.
  2. Features to support modularity and local polymorphic definitions
I also added these personal preferences:
  1. ontology of pure functions rather than sets
  2. logical operators in the domain of discourse (as in STT rather than FOL)
ZFC in HOL
First I axiomatised ZFC set theory in the Cambridge HOL system. This was done in the obvious way by introducing a new type SET and then new axioms which are the naive translations into higher order logic of the axioms of ZFC. Then I developed the theory a bit in HOL roughly following [Hatcher82], stopping before doing arithmetic. The purpose of this was to provide a rich ontology of sets which could be used to constuct the required semantic domains.
Pure Functions
Next the type of pure functions was defined, using sets as representatives. i.e. a new type PF is introduced which is defined as being in one-one relationship with a subset of SET. Roughly the sets concerned were all those which can be reached from the empty set by the process of constructing functions. This is analogous to the way in which the sets are formed from the e

Categories:

I also made an experiment in building a foundation out of pure categories and functors, using the same techniques I had used for other classical foundation systems.

Mechanisation:

I led the implementation of ProofPower, a tool supporting the formal development of theories in Higher Order Logic. I continue to advocate the mechanisation of mathematics through this web site.


UP HOME © RBJ created 1998/10/18 modified 1998/10/22