In 1994 I got my first web site. After struggling some time to get web access through ICL, it eventually happened, and with the web access came, through a backdoor an external website. In the Finnish arm of ICL I found an outfit which had an externally visible website, contrary I think to ICL policy on firewalls, and which was willing to cross mount web-space on one of our Sun workstations, making it externally visible.
The primary purpose of this was to put up information about ProofPower, but I also put up my own personal web-space, which was philosophical. I did some experiments with converting philosophical classics into hypertext, of which the modern ancestors (actually not a lot different) are now on rbjones.com. The hypertext classics are not significant. What was significant was the gradual revival of my philosophical thinking, beyond the scope of the foundations of mathematics. This was a very tentative process, evident initially only in the few extended periods away from work (i.e. vacations). Its possible to pursue technical problems in private time (though I can't say the results are spectacular, this is what I have done all my life), but it was much harder to take up philosophy on that basis. I don't actually know when this started, but it was very roughly at the time when I started experimenting with the web.
At the time I got into hypermedia I was very taken by it and utterly convinced that it was the right medium for me. It has taken very many years for me gradually to come to the conclusion that I was wrong.
1994 was also the beginning of the end for the formal methods team in ICL. CESG was running into problems with some of its high security developments and soon there was to be a change of policy and they would simply stop funding this kind of R&D. The hole was partly plugged by safety critical applications but there was not enough of this to keep the formal methods unit going. The honeymoon period for the Defence Technology Centre was past, and the focus was once more on profits. not research.
In 1994 I volunteered for other kinds of work, in the hope that a slimmed down formal methods team would have have a better chance of survival, and believing that such a slimmed unit would have to be headed by someone less senior than myself to be cost effective. For me that was the end of interesting work at ICL, and I decided that on my fiftieth birthday I would go it alone in the hope of finding something more congenial. I then had the sense that I wanted to write, but I had a pretty fluid sense of what I wanted to write. Philosophy, software, ... What I really wanted to do was to find a way to earn a living from creative activities. In particular from doing what I though a good idea rather than what someone else thought a good idea. I had this sense of being handicapped throughout life by this dichotomy between what I was paid to do at work and the more interesting things which I attempted in my own time.
Attempting this at the age of fifty had the additional advantage that I could fall back on a pension from ICL. I did this rather faster than I expected to because the year following ICL changed the rules in a way which gave me an incentive to take the pension sooner rather than later. Gradually the revenues that I was then able to obtain, first from contracts with ICL and later with contracts from Lemma1 has petered out so that we now live on two pensions between us.
From when I left ICL to the present moment is now a period of seven years in which I have failed to get things in order. I have had what I now think of as ``philosophers block'' (if one can be said to have that without any sign of ever having a philosophical capability which might have been blocked), the beginnings of which were almost immediate, and which may just possibly be now disappearing. Notwithstanding this ``block'' there has been quite a bit of intellectual and philosophical development during that period which is hard to trace chronologically.
For me it is important however, to exhume at least some of this stuff, so I shall attempt it in the following without worrying to much about the chronology.
A major theme in this period has lain on the boundaries of artificial intelligence and formal mathematics. This began with something I called ``Engineering Logic'' and progressed first though ``The Global Super-brain'' to ``X-Logic'', all different takes on essentially the same theme, and all engineering projects bound up with philosophy.
I was not attempting to do philosophy when I started ``Engineering Logic'' but I was then seeking to put forward an architecture for, and an approach toward artificial intelligence which was primarily rooted in producing software first which would not be intelligent, in framework which might eventually lead to intelligent software. The rationale for this framework could not be explained without getting into philosophy, and the philosophy proved awkward to explain, because it was old fashioned philosophy, closer to logical positivism than to anything which philosophers did at the time. It was based on tenets which seemed generally discredited (especially in the marginal world of on-line philosophising).
I'm going to say what I can about the engineering side of this in this section, and deal with the more philosophical aspects later.
There are three clearly identifiable stages in my thinking on this topic, which I give the tags:
Each of these stages is best thought of as adding something to what went before, rather than as replacing its predecessors. All of this was conceived of at the time as something like software engineering. I was aware that the rationale for this depended upon certain philosophical doctrines, which when I first started I did not think of as novel, and was only dimly aware of as controversial. So my first inclinations philosophically were perhaps just to run of a position statement which gave the relevant philosophical background. However, I became increasingly aware of the distance between the philosophy on which these architectures are based and the kind of thing which contemporary analytic philosophers are saying. Not just that they were saying different things, but that this whole way of thinking was thought of as having been discredited. At first I didn't even know where the philosophical ideas had come from, but eventually I figured out that it was probably predominantly from Russell and Ayer, modified by my own knowledge and experience of modern logic and computing.
Now I am returning to this, thinking of it as philosophy.
The ideas started with an architectural conception which corresponded to (what I consider) the obvious way of working out from the formalisation of logic, and there is a picture illustrating the scheme at
I've chosen this tag here, even though it was just one element of the ``topography for AI'' which I sketched out, because it was for me the most important element, because I sought to advance the aspects of it which could be regarded as realisable engineering, rather than speculative research. So ``engineering logic'' was the limits of engineering logic based automation of (inter alia but importantly) engineering design.
The idea of engineering logic is simply the idea of automating engineering design through formalisation. This kind of work, not itself conceived of as artificial intelligence was intended to form a basis on which intelligent capabilities might later be established, but which was just a special kind of software engineering, in which logic is applied first to the formalisation and automation of mathematics and thence to science and ultimately to engineering.
Underlying this of course is a story about how one ideally can formalise science and engineering which is in spirit if not in detail similar to what logical positivists such as Carnap were engaged in, inspired to a significant extent by the prior work of Russell in the formalisation of mathematics in Principia Mathematica. Intelligent logic is intended as an ``intelligent'' overlay on engineering logic.
This stage in thinking was to some extent simply connecting in with a popular theme, to some extent it was rethinking in terms of global networks. There is a distinction in the topography of the previous scheme where one crosses the boundary from the domain of the analytic, and hence beyond the scope of logic. This is marked by a change of colour from shades of blue to shades of green, and though the topology shows some subdivision of the green zone I didn't do any significant thinking about this side of things (not even by my own lights).
In the ``super-brain'' stage that distinction is made more prominent, the two parts are called the analytic and the holistic super-brains and the balance gets a bit better (in terms of how much I thought about these different sides of things).
The analytic super-brain was a networked version of intelligent engineering and intelligent logic. The holistic super-brain was the use of global networks to transform the operation of markets. An important part of this was its intended role in achieving greater transparency in the total costs and effects of products and companies upon the issues of greatest importance to us all. This is also about the future of democratic institutions, capitalism and free markets. So in a more concrete way the holistic side connects with the more socially oriented side of philosophy, including ethics and political and economic philosophy.
This last stage in the evolution of these ideas is where I connect the Super-brain with XML.
Now alongside the line of thought about engineering knowledge processing artifacts, I had a more self consciously philosophical line of thinking. This was mainly about the role of formal logic in philosophy, which following Russell, and Carnap I considered crucial.
The distinction between sets and classes has I think always struck me as being arbitrary, but it was only in 2005 while engaged in a discussion on the FOM mailing list that I found an argument to that effect which I considered convincing.
The argument flows from a simplification of the description of the intended domain of well-founded set theory which goes under the headings ``the iterative conception of set'' or ``The Cumulative Hierarchy''. There had been attempts (for example, by Dana Scott and George Boolos) to further explicate this account of set theory using some theory which talked about the stages in the iteration which supposedly lead to the cumulative hierarchy. I found these unconvincing, because these theories seemed to me more complicated than the theory which they sought to explain.
Furthermore, it had begun to dawn on me, that the effect of the classic descriptions should be to simply to make more clear to concept of ``pure, well-founded set'' which one would expect to be co-extensive with the completed cumulative hierarchy. Thinking therefore of the best way to define the concept of a pure well-founded set, I came up with the following definition by transfinite recursion (or induction):
A set is any definite collection of sets.
The reading of this as an inductive definition requires that nothing counts as a set unless its sethood is justified (possibly by some highly infinitary ``proof'' by this definition alone.
Thus one may begin with the empty set, which by any account is definite and which, whatever a set may be, contains nothing else, and from there, after the manner of the interative conception but with more freedom as to order, one may see that subject to some discussion of the meaning of the term definite, any pure well-founded set may be reached.
The term definite here is essential to the definition, for if it is removed the definition engenders contradiction, for the extension of the concept thus defined would be a set, and could be shown both to be and not to be, well-founded.
An inductive definition of a concept yields (or is more fully explicated by) an induction principle which may be used to prove results true of all that falls under the defined concept.
In this case the relevant principle of induction is (sometimes noetherian) induction:
If some property P is:
Using this principle it can be shown that the sets thus defined are:
It also follows directly from the definition that every definite collection of sets is a set, and hence that if there are ultimate collections of sets (which are not themselves members of a set) then these collections are not definite.
Provided the requirement of definiteness is in there, the line of reasoning which might otherwise have obtained a contradiction suffices only to show that the collection of all sets cannot be definite. But the requirement can be very weak indeed.
The effect of this ``idea'' is to give a more concise presentation to the iterative conception of set, in which some inessential features are omitted (in particular the iterative conception proceeds in stages according effectively to the rank of the sets (which is the number of steps or stages which are necessary in its construction), whereas the minimal ordering is in fact that partial ordering which is the transitive closure of the membership relationship. The concision of the definition, makes more transparent the consequences of the definition, in particular the incoherence in the case that the constraint of ``definiteness'' is omitted or made trivial.
In effect, the whole process as described in the iterative conception cannot be completed, as a matter of logical necessity, and a choice must be made, which we might consider to be arbitrary, about where the process is to come to an end.
As a result of futher provocation on the FOM mailing list in January 2010, my understanding of the relationship between the axiom of replacement and the ``limitation of size'' principle was improved 11.1
Let us consider, in the context of the definition of well-founded set in Section 11.4, the alternative ways of defining ``definite'' and the conceptions of set which arise.
First note that the role of the concept ``definite'' here is to separate sets from classes. A collection of well-founded sets is a set if it is definite, and otherwise its not a set, so we'll call it a class. It may be helpful to switch terminology at this point, to emphasise that what's really happening here is that we are making a more-or-less arbitrary choice about when to stop making new sets. So instead of definite we will use the term ``small'', which is familiar to set theorist for making exactly this distinction.
Our definition (of pure well-founded set) becomes:
A set is any small collection of sets.
To make this definite we have to decide where to draw the line, i.e. when to stop making sets. This we do by deciding what small is to mean.
Its worth distinguishing two different things which small might be a property of. The first connects us directly with the iterative conception of set, and is the rank of the collection, the number of stages involved in its construction. If we construe small as a property of the rank of the set, then we are stating the number of stages in the iterative conception that are to be completed.
The most obvious alternative to this is to take ``small'' literally, as referring to the cardinality of the set.
First order set theories do not usually place upper bounds on the size of the universe, either in terms of rank or cardinality. The effect of the axioms is to place lower bounds, their purpose being to ensure that there are sufficient sets for the purposes of mathematics. However, the convenience of the theory depends not only on their being sufficient sets, but also on the universe of sets having strong enought closure properties, so that various kinds of construction can be relied upon always to yield sets.
If our definition of well-founded set is taken as determining a collection of models for set theory, and the collection is to be determined by chosing a particular interpretation of ``small'' the interpretations begin those obtained for values at least that large, then the kinds of theory we get are subtantially different according to whether ``small'' is taken to be a property of rank or of size.
If of rank, then by varying the value of small we can get theories of arbitrarily high strength, but which all have weak closure properties. The universe of sets will not even be known to be closed under the pair constructor. Chosing a large value for ``small'' will result in it being provable that there are sets with good closure properties, but the universe will not have these properties.
On the other hand, if small is a measure of size, then we get replacement, and with it other closure properties.
Roger Bishop Jones 2016-01-07