|
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: |
