I am a retired software engineer mainly now interested in philosophy and logic.

My main aim at present, both in philosophy and in philosophical and mathematical logic,
is to build beyond the ideas of Leibniz and Carnap, particularly on Leibniz's idea
of a
*lingua characteristica* and associated
*calculus ratiocinator*, and Carnap's desire to make philosophy and science logically rigorous through the
use of formal logical languages.

I am trying to write a monograph supplying a philosophical framework suitable for
a particular approach to the automation of deductive reasoning.
This approach is intended to deliver formal rigour in philosophy, logic, mathematics,
science and engineering and to facilitate deductively sound approaches to the automation
of engineering design.

Alongside this philosophical project I have a connected more technical line of research
concerning the formal foundations of mathematics and, more generally, of abstract
semantics.
This involves establishing a strong illative lambda calculus with a system of type
assignment via a semantics in an infinitary illative combinatory logic, which is itself
defined in a higher order set theory.
I am now working on a formal derivation of a Church-Rosser theorem for this infinitary
illative combinatory logic.

For more, see:

email address