X-Logic, as I now see it, is an exercise in developing the formal theory of certain aspects of distributed cognitive systems. As such it is a bit of theoretical Computer Science. However, these ideas have lately come to seem important as a way to make definite and precise some of my recent ideas about analytic methods. As such X-Logic has come to seem central to my conception of philosophy.
It will be desirable to look closer at some of the non-philosophical drivers and potential applications of X-Logic, but since this book is primarily philosophical I will begin by explaining how X-Logic came to seem important to me philosophically.
Last year I was calling myself a ``Metaphysical Positivist'' and espousing a conception of philosophy which seemed to me a natural successor to that of Rudolf Carnap. In fleshing this out I had looked, with more interest than had Carnap, at the historical origins of his philosophy, and particularly at the line of descent which I imagined running, from Socrates through academic and pyrrhonean scepticism, into modern times as mitigated and constructive scepticisms, yielding positivism at the hands of Hume and eventually reaching The Vienna Circle and Rudolf Carnap. The details of this story do not concern us here, but the perceived connection scepticism-positivism-Carnap-Jones is an important element of my mindset in making the philosophical transition to X-Logic.
While Carnap in his youth was a vigorous positivist exhibiting the customary dogmatic fervour on key points, such as the proscription of metaphysics, as he matured a tolerant pluralism emerged, to an extent which made him doubtful of the positivistic label and inclined to fall backl to mere ``empiricist''. My own transient adoption of positivism was possible only because of the direction I supposed it to have been taken by Carnap, and I followed him in considering my contribution to philosophical analysis as centring round a proposal of certain languages, methods and tools for use in philosophical analysis (rather than as lying in some body of philosophical doctrine). I had however been uncomfortable with that description of my position.
It arose because I was using formal methods, and felt the need to give an account of those methods in the hope that this would make it possible for others to understand my formal work. Since this was not a body of doctrine, it seemed that it must be a proposal. But there is no strong reason why anyone else approaching this kind of work should follow in detail the methods I had adopted. For formal work one has to chose a language, one with good tool support, and to chose which tools to use for the formal development. I'm happy to expose the detail of my work, to describe the languages and tools used and any other aspect of the work, but I have no desire to prescribe or even propose how anyone else should go about this kinds of work. These choices are substantially pragmatic, and depend not only upon the kind of problem at hand but also on the knowledge and skills of the persons undertaking the work. There can be considerable time involved in achieving a proficiency in the use of a new language or a new interactive theorem prover.
Further to these considerations, I was not even keen to be proposing the use of formal techniques. Philosophy is of its nature concerned with many problems which are difficult to formalise, or the formalisation of which might be so time consuming as to impede progress in coming to an articulate understanding of the issues. Though I have a broad conception of nomologico-deductive method for use in philosophy (and elsewhere), I have also an interest in trying to get some understanding of how one can gain and communicate an understanding of problems which are beyond the reach of a plausibly sound basis for deductive reasoning.
Carnap was a pluralist as to language, as embodied in his "principle of tolerance", but he was a serial monist as to method. He always seemed to have a single method of analysis in mind, but his conception of what that method was evolved over his life. Carnap had not been exposed to the many headed beast which is theoretical computer science and formal methods for information engineering, but I had, and so was aware how many choices one had to make to articulate a single method of formal analysis. It is now natural to expect that there are and will continue to be a wide variety of languages, methods and tools, and that from them we will select whichever seems appropriate for the task in hand. It is natural to adopt not merely a linguistic pluralism, but also a methodological pluralism.
The adoption of a more comprehensive pluralism obviates the need to make linguistic and methodological proposals.
Here is a list of factors which have contributed to my conception of the requiremenmts.
The following paragraphs provide a first clarification of these sources and of the contribution each of them has made.
I did some thinking about this in 1985, and this was written up as a paper for presentation at a workshop in Appin that year (on persistent databases).
This gives a starting point in the following principles:
This comes from thinking about how formal theorem proving can be made into a linguistically pluralistic distributed collaborative enterprise (that at least is the fragment of the motivation which best makes the philosophical connection).
Not it already is pluralistic, and collaborative and kind of distributed. There are many interactive proof tools being used supporting a diverse range of languages. These things generate communities who build on each others work, so it is a distributed collaborative effort.
But there are very severe limitations. Each used of such a tool recreates in his own private space the entire heirarchy of theories which are needed for his bit of work, and these will normally be all created with the same tool using the same language. Furthermore, it is probable that in recreating the context he has rerun the proofs of all the theorems which form the environment in which he is working. Unlike regular mathematicians he isn't going to use a theorem which has just been published somewhere else, however much he trusts the source. Typically the software he is using just won't let him do it. To make use of the theorem he will have to obtain a proof script from the author, submit it to his tool in the appropriate context so that the tool can convince itself that the alleged theorem is indeed a theorem. The it will let you use the theorem. And if the proof was done with a different bit of software, then the odds are the proof script won't be understood by your tool.
QED never did amount to a project, so much as a proposal and some talking shops. The idea was to do with the formalisation of mathematics, and was an attempt to bring together interested parties into one big formalisation project rather than having a diversity of small unconnected projects.
I regards X-Logic as providing ideas for a context in which the formalisation of mathematics (and a great deal else) can be progressed in a loosely collaborative way.
Roger Bishop Jones 2016-01-07