Subsections


A. Research Topics

Here are specifically the research topics I considered for a PhD dissertation.


A.1 Keele

A.1.1 Background

The following is a transcription of a note that I made, probably in early 1976, while an undergraduate at Keele University looking for a University to do research towards a PhD.

The professor of mathematics at that time gave me the advice (which now seems to me rather bad advice) that I should avoid doing an MSc and get straight into working on a PhD. So I wrote down the kinds of things I wanted to do research in and sent the note to some Universities to ask them whether I might be able to do that kind of research with them. I think it just went to Oxford and Manchester at first, then Peter Aczel at Manchester said that the Computer Science department at Warwick would be a good place to do that kind of work and suggested I talk to David Park. The copy to Oxford was addressed to Dana Scott, with a covering letter explaining that I didn't want to do the MSc but was looking to get straight into research. He replied very concisely to the effect that he was not able to help me. Later I got a more conciliatory response from Robin Gandy, who invited me to go and talk to him, but by that time I had already agreed to go to Warwick. For more than one reason this was unfortunate, and I would have been much better doing the MSc at Oxford.

A.1.2 Possible Topics for Research in Mathematical Logic, Foundations of Mathematics, and Computer Science

A.1.2.1 High Level Logics

My most consuming ambition in Mathematical Logic concerns the development of ``High Level'' formal systems of logic. By ``High Level'' I do not mean ``Higher Order'', I mean something analogous to the use in ``Higher Level Programming Language''.

The purpose of a high level programming language might be:

(A)
To facilitate the precise formulation of algorithms (possibly in some special problem area, but not necessarily)
(B)
To enable people to make use of the facilities of a complex computer system without needing first to acquire detailed knowledge of the workings of the machine and its software.

The "sine-qua-non" of a programming language is translatability.

By analogy the purpose of a high level formal system of logic might be:

(A)
To facilitate production of completely formal proofs of mathematical theorems (possibly in some particular branch of mathematics but not necessarily)
(B)
To enable mathematicians to produce completely formal mathematical proofs without needing to master all the intricacies of mathematical logic and set theory.

The ``sine-qua-non'' of a formal system of logic is that there be an effective method for verifying proofs (not to mention that it should be consistent!)

The development of such languages is a prerequisite of any extensive practical use of computers for proof finding.

A.1.2.2 The Foundations of Mathematics

Concurrently with work on the above some work on the foundations of mathematics would be necessary. I could of course stick to formalising versions of the tried and tested axiomatisations of set theory, but I have traces of intuitionism lurking within me and would like to investigate other possibilities.

One possibility which interests me is that of basing mathematics on strings rather than sets. Strings however, unless infinite strings were admitted would serve only for a version of constructive analysis.

A.1.2.3 Computing with Reals

The principle source of my intuitionist leanings was the perception several years ago of the disparity between theory as embodied by real analysis and practice found in numerical analysis. When I was familiar with the way mathematicians use numbers on computers the beautiful completeness and simplicity of the real number system seemed a rather shallow pretence. In practice all mathematical computations were approximated using using a subset of the rational numbers. What seemed worse than the understandable failure of numerical analysts to use real numbers was their failure to exploit the full range of computable numbers. It seemed to me that it was just because mathematicians allowed themselves the pretence of real numbers in their theory that they failed in practice to fully exploit the computational capabilities of their machines. It is well known that a wide range of functions are computable, it would be a good thing if computers were could be organised so that any ``computable'' function can in practice and without much difficulty be computed within any specified degree of accuracy (space and time permitting). This is not presently the case. A typical example of the deficiencies of the present techniques is a problem as simple as the inversion of a matrix. Any non-singular matrix with rational entries has a computable inverse and so one could reasonably expect that any substantial computing complex would have facilities to compute any such matrix to any prescribed accuracy. In fact, I doubt that there is any complex which will guarantee to compute any inverse to within 1% accuracy (subject to time and space limitations only). In practice the accuracy of the inversion will depend upon the size of the matrix, and more importantly, on how close to being singular it is. In general we can only guess at how accurate the inversion is.

It would be interesting and valuable (and not trivial) to investigate the software and hardware necessary to render practicable the computation of any ``computable'' function to an arbitrary number of places. On the more purely mathematical side there is the problem of sorting out which of the problems of analysis known to have solutions actually have computable solutions, and the problem of arriving at practical algorithms for obtaining those that are computable. It must be emphasised that the algorithms here referred to are quite different in character to the algorithms used in numerical analysis at present, which are generally algorithms for approximating solutions. There is no way of obtaining solutions of arbitrary and known precision without abandoning present methods of representing numbers in machine memories.

A.2 Other Proposals

Many years later, during my period of formal methods work with ICL, I considered again the possibility of getting a PhD. I talked with Keith Hanna about the possibility of doing a PhD at Kent under his supervision. However, I wanted to do a purely theoretical dissertation, on some logical foundation system, Keith had already adapted other logical foundation systems for use in his Veritas hardware verification tool, so he was not uncomfortable decising new logical systems, but the main point of his work was the development and application of tools for the verification of digital hardware, and he was not willing to supervise a more theoretical foundational enterprise (and may have doubted that the department of Electrical Engineering at Kent would support him).

Since my interest at that time was in foundation systems which were similar to Combinatory Logic, I also talked to Roger Hindley, who was possibly embarassed to have to decline my suggestion that he supervise me in a PhD. In retrospect I imagine that I can see why he did.

I also enquired with the Open University, who said that they had no-one with sufficient competence in the research area I proposed, but that I could do a PhD with them if I could find a suitable external supervisor. I soon realised that the prospects of ever finding one were slender, but only later realised how unlikely success for me in such a project would have been even if I had found a supervisor.

None of the details of my proposals at this time has survived, but I am pretty sure that during this period my interest would have been in devising new logical foundation systems more suitable for use in mechanised mathematics. The single most distinctive feature I was then interested in was what I called reflexiveness meaning the possibility of functions falling within their own domain, in set theoretic terms, non-well-foundedness.

Roger Bishop Jones 2016-01-07