Research

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 concepts that are better fit for theory building. In order to extend these traditional methods, I have developed a programmatic methodology for working in semantics, drawing on the computational power of a 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 operators including constitutive explanation ("necessary for," "sufficient for," "what it is for," "just is for"), counterfactual and indicative conditionals, causal explanation, relevance and logical subtraction, normative explanation, tense and circumstantial modality, free choice and deontic modality, probability and epistemic operators, and the Boolean operators.

Developing a unified model-theoretic semantics and proof theory for this collection of operators is computationally intractable by traditional hand-derivation methods. The programmatic methodology I have developed instead supports discovery of adequate semantic theories and logics by exploring the interactions between operators computationally, aiming to abstract on my own semantics to provide a general methodology for developing and exploring new semantic systems and their corresponding proof systems.

Verification

This project provides a flexible, unified semantics and logic for tense, modal, counterfactual, and constitutive explanatory operators in order to model system behavior and verify software. Rather than taking possible worlds and times to be primitive, the semantics models evolutions as constrained functions from times to instantaneous world states, with a primitive task relation distinguishing possible from impossible state transitions.

This project aims to unify several logics employed in formal methods — the temporal logics LTL, CTL, and TLA, the dynamic logics DL and PDL, Hoare logic, and separation logic — by providing a common notation in which each may be expressed as a special case of the present semantics' expressive power. Temporal logic (particularly Lamport's TLA+) has emerged as a highly practical tool for modeling programs and systems, with adoption at AWS, Microsoft, and Oracle; this project aims to extend that lineage with the greater expressive power of a hyperintensional semantics.

Interpretability

In order to assist efforts to maintain the alignment of AI-assisted decision-making in socially and morally sensitive sectors, this project develops a semantic methodology to bridge the divide between the opaque parameters of an AI model and the transparent determinations and inferences that may be carried out in human-readable object languages. Rather than directly interpreting model parameters, the approach constructs semantic models (in the sense of model theory) from AI model abstractions in order to evaluate human-readable object languages with counterfactual, causal, relevance, and constitutive explanatory operators — exploring the complex dependencies within AI models and clarifying responses to edge cases relevant to model robustness.

Integrating tense and modal operators enables this approach to capture the dynamic aspects of AI decision-making, explaining how outputs evolve over time or respond to initial conditions. Normative explanatory, epistemic, indicative-conditional, free-choice, and deontic modal operators provide further resources for surveying and maintaining alignment with human values.