Upcoming Events

“Programmatic Semantics” (June 17, 2025: 11am — 12pm) This talk at the Topos Institute presents a programmatic methodology that uses the model-checker to rapidly prototype modular semantic theories for the Logos. This approach leverages the Z3 SMT solver to search for finite countermodels, providing evidence for logical consequences if there are none, making it easier to explore and combine complex semantic theories in a collaborative framework. [ handout, location ]

LOGOS: A Formal Language of Thought

Whereas logic has traditionally focused on small language fragments, I am developing a unified semantics and logic for the Logos which is an extensible formal language of thought to equip AI agents with the capacity for self-reflection and high cognitive reasoning. The operators that have been implemented so far include:

• 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’
• Relevance operators ‘P is wholly relevant to Q’
• Tense operators ‘It always will be P’, ‘It always was P’, ‘It is going to be P’, ‘It was P’
• Eventuality operators ‘Next it will be P’, ‘Previously it was P’, ‘P until Q’, ‘P since Q’
• Modal operators ‘It is possible that P’, ‘It is necessary that P’
• Extensional operators for conjunction, negation, the material conditional, etc.

The next phase of this project will extend the Logos to include causal, epistemic, and deontic operators for reasoning under uncertainty about imperatives, preferences, and responsibility to facilitate cooperation with human and other AI agents. In particular, I aim to implement modular semantic clauses for the following:

• Causal explanation ‘P causes Q’
• Indicative conditionals ‘If P is the case, then Q is the case’
• Epistemic modals ‘It must be that’ and ‘It might be that’
• 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’
• 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 for R’
• 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 responsibility ‘Group G is jointly responsible for it being the case that P’

Given a unified semantics for the Logos, logical consequences may be evaluated with the model-checker. By contrast, attempting to develop a unified semantics and logic makes evaluating logical consequences impractical to carry out by hand. See software for further details on the packages and programmatic methodology that I am developing to support support this project.

Formal Verification

In addition to providing a unified semantic framework for interpreting the Logos, I am working to unify a number of logics employed in formal methods by identifying the following as subsystems of the Logos:

• 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.

Publications

• “Counterfactual Worlds” JPL (2025)  This paper extends Kit Fine’s [1, 2, 3, 4, 5] truthmaker framework to provide a novel task 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, tasks, and times where the task relation encodes the possible transitions between states. Rather than invoking primitive relations for similarity or imposition, 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 motivations for this approach, I will provide the hyperintensional semantics for counterfactuals that is implemented in the model-checker software along with a unified logic for counterfactual, modal, and tense operators. I will then extend the language to include further tense operators in order to analyze forwards, backwards, and backtracking counterfactuals.
• “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

• “Programmatic Semantics” I demonstrate in Brast-McKie (forthcoming) how to define Fine’s [1, 2, 3] imposition relation in terms of the primitives that Fine [4, 5] includes in a modalized state space to provide a logic for counterfactual conditionals which is at least strong. This paper presents this alternative to Fine’s truthmaker semantics as a case study of a programmatic methodology which makes use of the model-checker to implement both semantic theories. By ruling out finite countermodels smaller than a user defined limit, the model-checker provides evidence that a logical consequence under consideration has no countermodels. Rather than a substitute for working in traditional model theory, implementing a programmatic semantics with the model-checker greatly eases the process of prototyping new semantic theories and making novel additions to existing theories. Nevertheless, the computability of a semantics provides an objective measure on the complexity of a theory which may be weighed alongside other theoretical virtues.
• “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.
• “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.
• “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.