An introduction to and an overview of various work in progress.

The scope of deductive reason is considered. First a connection is discussed between the scope of sound deductive inference and the notion of set theoretic truth via the concepts {\it demonstrative} and {\it analytic}. Then the problem of determining the meaning of set theory and the extension of set theoretic truth is addressed.

Various set theoretic definitions of the concept of analyticity are presented and their characteristics consdered. It is noted that certain techniques for abstraction prevent defining the synthetic as complementary to the analytic, and the consequences of this problem are explored, leading to new ways of defining analyticity.

An exercise in classical (possibly even pre-historic) skepticism. Of necessity this exercise has the character of tentative ideas rendered as sketchy notes. These notes document a retreat in which ideas on the scope for objective ontological knowledge are progressively narrowed. The last ditch in this process is the question of how many things it is logically possible that there might be.

A description of the specification and proof tool ProofPower.

Mainly about his {\it lingua characteristica} and {\it calculus ratiocinator}.

A partly autobiographical exhumation of the ideas which have engaged me throughout my life, so far.

A discussion of methods for the formalisation of Physics.

A philosophical tract.

Positivists have often been antipathetic to metaphysics. Here, however. a positive role for metaphysics is sought. Problems about reality which may not be resolved by the methods of the deductive or empirical sciences are considered. In this domain, the identification of meaningful problems, or of plausible methods is itself an achievement, and is the main purpose of this essay.

A discussion of issues in the design of formal logical foundation systems suitable for use in machine supported formal derivations of analytic models. The outlines of a proposed system with a roadmap for turning the outline into a specification for implementation.

A concise presentation of the motivation for, intuition behind, construction of, and conjectured properties of a model for a set theory with a universal set.

A project aiming to contribute to the realisation of Leibniz's lingua characteristica calculus ratiocinator, making use of XML technologies where appropriate.

An assortment of essays I wrote a long time ago.