Whereas semantics and logic are typically developed for formal language consisting of the Boolean operators and a few 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:

• Constitutive explanatory readings of “necessary for,” “sufficient for,” “what it is for,” and “just is for”
• Counterfactual and indicative conditionals
• Causal explanatory operators
• Relevance, logical subtraction, and subject-matter operators
• Normative explanatory operators
• Tense and (circumstantial) modal operators
• Free choice and deontic modal operators
• Probability and epistemic operators
• Boolean 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 and writing derivations all by hand. By contrast, the interactions between the operators given above are readily explored using the programmatic methodology that I have devised in order to support the discovery of adequate semantic theories and proof systems. In the next phase of this project, I aim to extend this methodology to include 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 AI interpretability and formal verification.

Verification

This project provides a flexible, intuitive, and unified semantics and logic for tense, modal, counterfactual conditional, and constitutive explanatory operators in order to model system behavior and verify software. Instead of taking possible worlds (i.e., complete histories of the system) and times to be primitive, the semantics models evolutions as appropriately constrained functions from times to instantaneous world states of the system. In order to interpret hyperintensional operators, world states may be identified with maximal possible states where in general states may be partial and impossible. A primitive task relation is then taken to distinguish possible and impossible state transitions, and is subject to a number of constraints, and further generalizations. Finite evolutions are then defined to be functions from a finite interval of times (integers) to states where there is a task from the state at each time in the interval to its successor (if any).

In addition to providing a general semantic framework for interpreting a range of logical operators, this project aims to unify the following logics employed in formal methods by providing a common notation in which the following may be expressed as special cases:

• The temporal logics LTL (Pnueli 1977), CTL (Clarke 1981), and TLA (Lamport 1994).
• The dynamic logics DL (Pratt 1976) and PDL (Fischer 1979).
• Hoare logic which can be viewed as the fragment of dynamic logic, and a special type of modal logic.
• Separation logic (Reynolds 2002) which bears a natural relation to hyperintensionality.

Temporal logic (in particular, Leslie Lamport’s TLA+) has emerged as a highly practical tool for modeling programs and systems, with adoption and support within major commercial enterprises like AWS, Microsoft, and Oracle. Other tools used in industry, like Microsoft’s Dafny and the Coq formalization of Iris’s higher-order separation logic, rely on Hoare Logic. Hoare logic (at least of the classical variety) is expressively subsumed by dynamic logic, where both dynamic and temporal logic are, at bottom modal systems: the result of enriching a standard extensional deductive logic with modal operators. The aim is to both unify and extend this common lineage, providing an intuitive and general framework in which to gain greater perspective on existing logics used in formal verification as well as affording greater expressive power given the hyperintensionality of the present approach.

Interpretability

In order to assist efforts to maintain the alignment of AI-assisted decision-making in socially and morally sensitive sectors, this project aims to gain insight into the underlying mechanics of AI models by developing a model-theoretic semantics for human-readable object languages in terms of AI model abstractions.

This approach has two main goals. First, it aims to support the challenging task of reverse-engineering AI models. Instead of interpreting model parameters or their abstractions, a semantic methodology seeks to construct semantic models for human-readable object languages from AI model abstractions. In particular, I am interested in studying AI model behavior by interpreting languages with counterfactual, causal, relevance, and constitutive explanatory operators in order to explore complex dependencies and conditional structures within AI models in addition to clarifying responses to edge cases in order to better test for model robustness. Integrating tense and modal operators also enables this approach to capture the dynamic aspects of AI decision-making, explaining how outputs evolve over time or respond to initial conditions. Including normative explanatory operators as well as epistemic, indicative conditional, free choice, and deontic modals provides essential leverage in facing the challenges of surveying and maintain alignment with human values.

The second goal is to support the design of more interpretable AI systems. I am especially interested in architectures that allow for dynamic feedback between an AI model and semantic models for a human-readable object language. 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. More broadly, a semantic approach bridges the opaque aspects of AI models and transparent determinations expressed in a meaningful object language. By analogy, just as perceptual modules inform cognitive reasoning in human agents even without complete transparency (e.g., one does not need to know why a hand appears as a hand to identify it as such), a semantic methodology mediates between AI models and higher-level reasoning about the AI model articulated in an interpreted human-readable object language by drawing on the logic for this language.

Since the success of a theory is ultimately determined by the abductive support that it enjoys, it is important to provide adequate tooling for testing and adapting theories rather than merely defending an existing theory from criticism. These considerations motivated the development of the model-checker for testing the implications of the semantic theories that I have provided. Instead of limiting these tools to the specific languages with which I have been concerned, the version of the model-checker currently under development aims to abstract on my semantic theories, providing a general programmatic methodology for developing and exploring new semantic systems as well as their corresponding logics.

In addition to applying these resources to interpret AI models, I am excited about the advances in scientific methodology that the solutions to the interpretability problem in AI may provide. By training AI models on specific datasets (e.g., DNA sequences, weather, etc.), extracting meaningful counterfactuals and causal hypothesis may provide powerful new methodologies across the sciences.

Papers

• “Identity and Aboutness” JPL, 50, p. 1471-1503 (2021). This paper develops a theory of propositional identity which distinguishes necessarily equivalent propositions that differ in subject-matter. Rather than forming a Boolean lattice as in extensional and intensional semantic theories, the space of propositions forms a non-interlaced bilattice. After motivating a departure from tradition by way of a number of plausible principles for subject-matter, I will provide a Finean state semantics for a novel theory of propositions, presenting arguments against the convexity and nonvacuity constraints which Fine (Journal of Philosophical Logic, 4545, 199–226  13, 14, 15) introduces. I will then move to compare the resulting logic of propositional identity (PI¹) with Correia’s (The Review of Symbolic Logic, 9, 103–122  9) logic of generalised identity (GI), as well as the first degree fragment of Angell’s (2) logic of analytic containment (AC). The paper concludes by extending PI¹ to include axioms and rules for a subject-matter operator, providing a much broader theory of subject-matter than the principles with which I will begin.
• “A Complete Logic of Ground I: Unilateral Propositions” RSL (R&R)  A proposition is specific just in case there is exactly one way for that proposition to obtain, and one proposition grounds another just in case every way for the former to obtain is a way for the latter to obtain. This paper provides a proof system for a unilateral logic of ground with a specificity operator, establishing soundness and completeness over a state semantics in which propositions are sets of states closed under finite fusion.
• “A Complete Logic of Ground II: Bilateral Propositions” RSL (R&R)  Having established soundness and completeness for a unilateral logic of ground with a specificity operator in a previous paper, this paper extends these results to a bilateral logic where propositions are closed under infinite fusion. By contrast with the Boolean lattices described by extensional and intensional logics, the space of bilateral propositions forms a non-interlaced bilattice. I will conclude by defining the bilateral notions of essence and ground in terms of unilateral ground.

In Progress

• “Counterfactual Worlds” This paper extends Kit Fine’s [1, 2, 3, 4] truthmaker framework to provide a novel semantics for tensed counterfactual conditionals. Instead of taking possible worlds to be primitive elements in a model, possible worlds will be defined in terms of states, parthood, and tasks where the latter encode the possible transitions between states. Rather than invoking primitive similarity or imposition relations, possible worlds will be compared at a time independent of that time’s past and future where the comparison will be carried out in mereological and modal terms. After reviewing the motivations for this approach, I will provide the hyperintensional semantics for counterfactuals that is implemented in the model-checker software for this project. I will then extend the language to include tense operators in order to analyze forwards, backwards, and backtracking counterfactuals.
• “The Varieties of Constitutive Explanation” Constitutive explanations play important roles throughout many domains of inquiry. What is necessary for an atom to be gold? What is sufficient for an action to be wrong? What is it for a number to be prime? These are good question with good answers. This paper provides an account of constitutive explanatory readings of ‘necessary for’, ‘sufficient for’, and ‘what it is for’, arguing that modal regimentations of these locutions fail to track the explanatory relationships that these locutions are typically intended to express. Rather, I present a logic for constitutive explanation which includes operators for essence and ground in addition to the modal operators and the truth-functions. In support of these developments, the majority of the paper is devoted to clarifying the theoretical roles which the different forms of constitutive explanation are intended to play, as well as contrasting the present treatment to related accounts in the literature.
• “Hyperintensional Causation” This paper develops a hyperintensional semantic theory for past tense causal claims such as ‘Throwing the stone caused the window to break’ and ‘The fuse blowing caused the fire to start’. Consideration of where David Lewis’ (1973, 1986, 2000) accounts fail to capture common usage will motivate an extension of Kit Fine’s (2017a,b,c) state semantics that is better able to encode the explanatory relationships between events. After employing the resulting semantic theory to analyse a number of important causal scenarios, the paper concludes by presenting objections and possible extensions to the framework.
• “Relevant Implication and Ground” Given a constitutive explanatory reading of ‘sufficient for’ which I will refer to as ground— or in symbols ‘≤’— it is natural to assume that A ≤ B entails: (1) A strictly implies B; and (2) A is wholly relevant to B. For instance, although A ≤ A ∨ B holds in general, A ∧ B ≤ A does not since B may be unrelated to A. By contrast, relevance logics accept the principle that A ∧ B relevantly implies A. This paper conducts a study of the conceptual targets that guided the development of relevance logics, comparing the results to a logic of ground which is designed to regiment constitutive explanatory readings of ‘sufficient for’. The paper concludes by presenting a unified logic and semantic theory for ground, relevance, and modality.
• “Fundamentality and the Self” This paper investigates the nature of the self. In particular, I will seek to regiment the Upanishadic claim, ‘sa esa neti netyatma’ (NA), which Olivelle (1998, p. 101) translates as, ‘About this self (atman), one can only say ‘not—, not—’.’ After presenting the context of the ´Sakalya Dialogue from the Brihadaranyaka Upanishad in which this claim first occurs, I will regiment NA by means of the following second-order principle: For any way of being, being that way does not strictly ground what it is to be the self (atman). It follows that the self is fundamental on account of failing to have any strict grounds. I will conclude by examining the relationship between the fundamentality of the self and the nature of the absolute (brahman). In particular, given the assumptions that the self (atman) is the absolute (brahman) and that every way of being is to be weakly grounded in the way that the absolute is, it follows that the self is fundamental.