Rather than describing the concepts that we happen to have in natural languages, my research seeks to describe the concepts that we ought to have by abstracting on the patterns of natural reasoning. Just as the material sciences have devised methods for refining the raw materials of the natural world, philosophical logic employs model theory and proof theory in order to engineer the concepts that are better fit for theory building. In order to extend these traditional methods, I have developed a programmatic methodology for working in hyperintensional semantics in order to draw on the computational power provided by any laptop to rapidly prototype and explore the implications of novel semantic theories (see software for details).

Foundations

Whereas semantics and logic are typically developed for language fragments consisting of the Boolean operators and a small number of novel additions in order to limit the computational complexity required to investigate the resulting theory, this project aims at greater conceptual unity, devising a common semantics and logic for the following operators:

Attempting to develop a unified model theoretic semantics and proof theory for the collection of operators given above is computationally intractable given traditional methods of establishing logical consequences or writing derivations by hand. By contrast, the interactions between the operators given above are readily explored using the programmatic methodology that I have developed in order to support the discovery of adequate semantic theories and their corresponding logics. Instead of limiting these tools to the specific languages with which I am concerned, the model-checker abstracts on the details of my semantics, providing a general programmatic methodology for developing and investigating new semantic theories as well as their corresponding proof systems. In the next phase of this project, I aim to extend this methodology to include the LEAN proof assistance so as to streamline the discovery and description of the logics corresponding to each semantic theory.

These methods in conceptual engineering aim to support the development of a unified logical theory with a broad range of applications, including formal verification and AI safety.

Papers

In Progress