|High Level Logics||The Foundations of Mathematics||Computing with Reals|
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 facilitiate 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.
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.
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 practive 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 arbitary number of places. On the more purely mathematical side there is the problem of sorting out which if 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 appoximating solutions. There is no way of obtaining solutions of arbitrary and known precision without abandoning present methods of representing numbers in machine memories.