Research

My research develops a unified hyperintensional semantics and logic for a Language of Thought (LoT). 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 addition to these traditional methods, I have developed a programmatic methodology for implementing semantic theories with the model-checker in order to rapidly prototype and explore novel semantic theories (see software for further details, and this handout from a recent talk).

Foundations

Whereas logic has traditionally focused on small language fragments, I am constructing a unified hyperintensional semantics and logic for the Language of Thought, which includes a wide variety of logical operators with which to reason. I have developed a semantics and logic for the following:

• Constitutive explanatory ‘P is necessary for Q’, ‘P is sufficient for Q’, ‘P just is for Q’
• Counterfactual conditionals ‘If P were the case, Q would be the case’
• Causal explanatory ‘P causes Q’
• Relevance and subject-matter operators ‘P is wholly relevant to Q’
• Tense operators ‘It always will be P’, ‘It always was P’, ‘It will be P’
• Modal operators ‘It is possible that P’, ‘It is necessary that P’
• Boolean operators

In addition to the operators above, I aim to include epistemic operators for reasoning under uncertainty as well as normative operators for reasoning about relative values and imperatives to support alignment with other agents. For instance, here are some of the operators that I intend to include:

• Epistemic modals ‘It must be that’ and ‘It might be that’
• Indicative conditionals ‘If P is the case, then Q is the case’
• Knowledge ‘S knows that P’ and ‘S knows how to P’
• Belief ‘S believes that P’ (relative to a credence threshold)
• Default reasoning ‘Typically, P’ and ‘Usually, P’
• Probability ‘It is probably the case that’ (relative to a confidence threshold)
• Comparative probability ‘P is more likely than Q’
• Group knowledge ‘It is common knowledge that P’
• Deontic modals ‘It ought to be that’, ‘It is permissible that’, ‘It is forbidden that’
• Reason for ‘P is a reason for Q’
• Defeat ‘P defeats Q as a reason’
• Preference ‘P is better than Q’, ‘P is equally good as Q’
• Ability ‘S can bring it about that P’
• Responsibility ‘S is responsible for it being the case that P’
• Collective ‘Group G is jointly responsible for it being the case that P’

Given a unified semantics for the LoT operators, logical consequences may be evaluated using formal methods as demonstrated by the model-checker. By contrast, attempting to develop a unified semantics and logic without implementing the semantics programmatically makes evaluating logical consequences impractical to carry out by traditional methods, writing semantic proofs by hand. See software for further details on the programmatic methodology that I have developed to support the development of a unified semantics and logic for the LoT operators.

Verification

In addition to providing a unified semantic framework for interpreting LoT operators, I am working to unify the logics employed in formal methods by identifying the following as subsystems that may be expressed in the LoT:

• Temporal logics: LTL (Pnueli 1977), CTL (Clarke 1981), TLA (Lamport 1994)
• Dynamic logics: DL (Pratt 1976), PDL (Fischer 1979)
• Hoare and separation logics: (Hoare 1969, 1997), (Reynolds 2002)

In addition to modeling system behavior and verifying software, this project is motivated by applications in AI safety. In analogy, formal verification is to generative AI as the critical mind is to the creative. By working to integrate these counterpoising elements, I aim to contribute to the development of trustworthy AI systems that will support rather than thwart a safe digital future.

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. Given models trained on specific datasets — DNA sequences, weather, and so on — methods for extracting meaningful counterfactuals and causal hypotheses may provide powerful new methodologies with applications across the sciences.

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.

The semantic models constructed from AI model abstractions may be thought of as an abstract form of memory. By interpreting human-readable object languages, logical reasoning may be carried out in those languages by appealing either to a semantic theory of logical consequence or to a corresponding proof system. I am especially interested in designing architectures that allow for dynamic feedback between an AI model and the semantic models over which human-readable object languages are interpreted. This feedback loop resembles human perception, which both shapes and is shaped by an agent's beliefs, allowing for belief revision given sufficient counter-evidence: just as perceptual modules inform higher cognitive reasoning without complete transparency — one does not need to know why a hand appears as a hand to identify it as such — a semantic methodology mediates between the opaque parameters of an AI model and the transparent patterns of reasoning articulated in a human-readable object language.