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