Monday, July 26, 2010

Active Zones

In my grand scheme of things there are at present three books in play, rather remote and implausibly ambitious objectives.

The things I am thinking about and "working on" right now are less grandiose, and possibly less implausible.
I hope that these pieces of the elephants might be more intelligible to others and so I thought I would give a short account here.

The thing which has consumed the greatest portion of my time of late has been my attempts to analyse formally (with ProofPower) the substance of Grice's "Vacuous Names".
This is conceived of as a part of my large projected tome of formal philosophy (which I call "analyses of analysis"), but since it is provoked more by the logic of my dialogue with Speranza than the aims of that tome, my conception of the work has gradually been evolving as I get a better idea of how it may be fitted into the historical themes which dominate the volume.
In that context it is an episode in the development of semantics, and is helping me to get my mind around how to address that topic in the larger context.

The Griceian material is an exemplar of a method of analysis with ProofPower, making use of shallow embeddings, and part of what I am trying to do at the same time as the Grice paper is get this method (and the particular languages and tools I do it with) written up in a form which might conceivably be intelligible to some philosophers. To this end I started a chapter on HOL, in which I would like to give an account of the language and logic closely based on the Church paper on his Simple Theory of Types. There is a place to this (to appear) but I have been struggling to find the right approach to this.

The last active zone is nominally X-Logic, but the first bit of the new formal models for X-Logic needs a bit of lattice theory, and the lattice theory may not strictly need, but is nevertheless serving as an excuse for an excursion into Universal Algebra (to appear), which itself has contributed a little impetus to my recent love affair with the proposition. The interest here is in doing Universal Algebra in a type theory in a way which is actually useful in the development of more concrete algebraic theories such as Lattice theory. The danger with high levels of abstraction is that the cost of using the abstract theory is just as large as the cost of doing the work without it. The first test will be in obtaining a sufficient theory of quotient lattices from a more general theory of algebraic quotients. The connection with the proposition is an aspect of the reuse problem. Universal algebra provides more abstract or more general results which subsume some of the results obtainable in specific algebras. What does this relationship between abstract and concrete theories tell us about the notion of proposition?
This is a conceptually simple sandbox for thinking about such matters, relative to the much greater difficulties in making sense of what happens in category theory.

RBJ

The Proposition

"The proposition" is a concept which has for a long time been growing, by stealth, more important in my scheme of things.

For most of that time, I have regarded the nature of the proposition as being determined only relative to a particular description of the semantics of a particular language, and hence as belonging to semantics rather than to metaphysics.

What I now dimly perceive is that the nature of the proposition probably does become an important problem in metaphysics as soon as you try to come up with something less language specific, and that there are many good reasons for attempting to do that.

An easy way for me to motivate that process, is just from the pragmatics of formalisation, in which there is a problem, shared with software engineering, of maximising re-use.
In the development of formal theories what one wants to make maximum use of is theorems, what one wants to avoid is having to prove essentially the same result many times over.
This is what polymorphism (and Russell's typical ambiguity) is about, it is what good modular structure is about, it is the principle reason why I think about non-well-founded foundation systems, and it is a central influence on the structure of X-Logic.

There are more connections between my other ideas and the concept of proposition, and now that I am become more aware of how important the notion of proposition might become for me, I shall make a place to discuss it.
This will be a broadening of a skeletal document which I started when I briefly paid some attention to Harvey Friedman's concept calculus.
I can broaden that document to deal more generally with propositions and still have a place in there for some discussion of Harvey's ideas.

RBJ

Wednesday, July 14, 2010

Proving GCH

After a morning disrupted by an early migrain messing up my visual cortex, I ought really to have taken things easy, but something quite entertaining has just happened.

I'll bore you with the chain of events.

First, I have to get my mail fixed, it just stopped yesterday and raising a ticket didn't get it fixed. However, the support guys pointed out that the mail was reaching my mailboxes on the server so it was just the collection which was awry. I found that one account was working, compared its configuration in my client with my main non-working account, noticed a difference and brought them into line. That fixed the problem. Some software which used to accept both ways of configuring the accounts had been upgraded, and no longer supported them both.

So now my mail downloads, and in there is a call for participation in the "Trusted extensions to ITPs" workshop. This reminds me of the last one, in which I had a lengthy disagreement with a logician from MIT (several disagreements, but one in particular) who insisted that it could be proved that all models of set theory have the same structure of ordinals. I insisted they don't all have the same height. After the workshop it occurred to me that he must have been talking about INNER models.
Which do have the same height because its part of the definition that they have "all" the ordinals.
(which is relative to the interpretation of the meta-language).

So the call for participation has got me thinking about set theory.

Now the entertainment. Within minutes I have a "proof" of GCH (the Generalised Continuum Hypothesis)! So it seems.
Must be wrong of course, we know it can't be done don't we?

Well it is a bit of philosophy rather than a bit of mathematics, I know its not provable in any accepted axiomatisation of set theory.

Still, I believe I have a proof, which is really entertaining (if you like that kind of thing), and so I will have to write it up and see what objections people can find to it.
This will be a bit like my proof that V does not exist (if its good).
You post to FOM and some people have a go at trashing it for a while, and fail, and then everything calms down and people carry on as if it had never happened.
Though a convincing proof of GCH would be harder to ignore than one that V does not exist, the consequences of which are more subtle.

So the next stage is to write it up, formalise what can be formalised, and see whether I still believe it.

RBJ

Thursday, July 1, 2010

The Rebirth of Metaphysical Positivism

About 12 months ago I departed from Carnap in the following respect.

Carnap construed himself as putting forward proposals for languages and methods.
For example his definitions of analyticity were not intended as revelations of facts about the meaning of the word "analytic" but as pragmatically motivated proposals for its use.

Similarly to Carnap, I sought to articulate a particular formal analytic method, including the use of partiular methods and tools.
This I also construed as a proposal rather than any factual (or logical) claim.

However, this construal was not true to the facts. for my own pluralism meant that I had no expectation that anyone else would use the same methods.
There is a lot of historical accident in the detail, and even in the fundaments, of the methods which I employ.
I could describe these as examples of the kind of method which I encourage, but I would recommend that everyone look around and chose the particular languages, methods, and tools which are best suited for their work on their particular problems.

So I decided that I should not present myself as putting forward methodological proposals, and as being methodologically as well as linguistially pluralistic.
This lead me to attach importance to comparative methodology.
The idea is to replace advocacy of particular methods by comparisons between methods, making these as solid and objective as possible.

Metaphysical Positivism was the name which I then employed for the position in relation to analytic philosophy which I proposed.
It was not till about six months later that it occurred to me that I no longer had a position.
I had reverted to the search for and articulation of truths, albeit comparative rather than absolute truths.

I still had to make the same kind of choices (languages, methods, tools) in order to progress my work, but these were not proposals for anyone else, and insofar as I want to support their choice of methods, it would be by providing hard comparative facts rather than proposals and advocacy.

This now appears as a yin/yang type vanishing dichotomy.
Should I be stating facts or should I be making proposals?
Yes.

Anyway, thinking that I was not making a proposal, I for a while also thought that I had grown out of having a name for my philosophy, and "Metaphysical Positivism" was abandoned.
But now I see that its just a matter of level.
I do have proposals and I do wish to engage in advocacy, but the level at which this occurs is subject to occasional lifting.
Now, instead of advocating particular formal methods, I advocate comparative methodology.

So I may well stick with Metaphysical Positivism.

RBJ

Good News

You might expect that spending three weeks failing to come up with an abstract for a talk I was keen to give would leave me deflated and dispirited.
To this we can add that I have just now passed my last target for publishing the first edition of "the book" (last known as "Evolution, Rationality and Deduction"), and its reasonable to say that I have not even started properly on writing it.

However, I have now had just enough time, since giving up on the abstract, for my ideas on the way forward to come "clear", and the picture is good.

The single most important feature of this is that in all but detail there is NO CHANGE, but that I now have a rather clearer picture of what the whole consists in and hope that I will be able to present that picture, and make my web site begin to make sense.
The thing that really pissed me off over the last 12 years or so since I gave up the day job, is that I kept abandoning projects as ill-conceived or unachievable.
Now its probably fair to say that they just kept re-emerging in a different forms.
It is so good to feel that the structure of my enterprise is beginning to stabilise.

I may as well enumerate some of the things which remain essentially unscathed and which are therefore likely to get sewn into the structure of my enterprise.

First, at the head of the list is the thing which may or may not turn out to be my opus magnum, or the two perhaps:

(1) Evolution, Rationality and Deduction

My conception of this project is unchanged in its essentials, but I now have some new ideas about how to progress it. The gross structure remains stable.

(2) Analyses of Analysis

That is the last known name for the volume of formal materials which is intended to underpin "Evolution, Rationality and Deduction".
It began after my first forays into formal historical exegesis applied to Plato and Aristotle and provoked by Grice/Code as conveyed to me by Speranza.
It is still there on the books and is the home for all formal modelling related to (1) which will include lots of foundational stuff in relation to "X-Logic" (which term is heading for meaninglessness).

(3) A Conversation between Carnap and Grice

Important to mention on my top level menu, because it's being neglected right now and I don't want JL (Speranza) to think I am loosing interest.
It is waiting for me to make enough progress with X-Logic to see how the comparative analysis of Grice and Carnap which is needed here can be structured, possibly as an exemplar of that method.

(4) Practical Philosophy

(1) and (2) both belong to my conception of analytic philosophy, and I might as well admit that analytic philosophy seems to be occupying a larger proportion of my intellectual space than it used to.
Possibly I will never get round to saying anything much in the practical arena (which I tentatively classify as political/economic, ethical, existential), but I hope not.

Here are some substructures, which I am pleased (this morning) to find myself thinking I will write something about.

2.1 Abstract Semantics (formal side)

My technical work on the foundational side belongs here, this includes ruminations about the semantics of well-founded set theory, and about how to compare the alternatives, it includes my material on non-well-founded set theory, and I hope it will come up a layer above that as well (those three layers were mentioned in my talk at Cambridge, and nowhere else probably, somewhere on the web site. From QED to X-Logic, following the lead of Leibniz, page 22.
And other stuff on set theory.

I'm going to stop there and try come up with something more detailed on the web site.
Maybe some more here on each area.

RBJ