LOGOS: A Formal Language of Thought

Responsible human agents engage in planning by reasoning in interpreted languages which include: (1) tense operators for thinking about the past and future along a given course of events; (2) modal operators for reasoning about different courses of events; (3) counterfactual conditional operators for reasoning about minimal changes to a course of events at a given time in order to consider the different futures that may transpire; and (4) causal operators for attributing responsibility. By also reasoning with epistemic and normative operators, human agents are able to cooperate under uncertainty with other agents where the forethought that goes into effective planning remains open to inspection and communication between agents. The Logos seeks to extend these abilities to AI agents to promote verified reasoning in an interpreted formal language that can be both easily audited, providing path towards scalable oversight.

The Logos is designed to train AI systems to conduct verified reasoning in an extensible formal language of thought that is interpreted by explicit semantic models. Including extensional, tense, modal, causal, counterfactual, epistemic, and normative operators in the Logos equips AI systems to perform complex reasoning tasks for planning and evaluating actions in coordination with other agents under conditions of uncertainty. By implementing the axiomatic proof system and recursive semantic theory for the Logos in LEAN 4 and establishes soundness, the proof-checker provides a positive RL signal for training AI systems that is not limited by human annotation or inaccuracy. Implementing the same semantic theory in the model-checker leverages the SMT solver Z3 to find finite countermodels if there are any, providing a negative RL training signal, providing a dual verification architecture.

Whereas logic has traditionally studied small language fragments, the Logos provides a unified semantics and proof system for an extensible range of expressive resources. 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 normative operators for reasoning under uncertainty about imperatives, preferences, and responsibility to facilitate cooperation with human and other AI agents. This includes:

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

See software for further details.

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

• “The Construction of Possible Worlds” (talk | handout) Possible worlds are often taken to be complete histories of everything. Insofar as there are temporary sentences that are true at some times and false at other times, evaluating a sentence at a possible world does not fix its truth-value. Moreover, if possible worlds are taken to be primitive, evaluating sentences at world-time pairs invalidates a perpetuity principle that what is necessarily the case is always the case where imposing model constraints cannot validate these principles without undermining the significance of the truth-conditions for the language. Rather, this paper takes world states to be maximal possible ways for things to be at an instant where the task relation encodes the possible transitions between world states. Possible worlds are then defined as functions from times to world states as constrained by the task relation. Since sentences are assigned truth-values at world states, times are exogenous to the truth-conditions for the language, eliminating unnecessary degrees of freedom from the definition of a model. By evaluating sentences at world-time pairs, the resulting semantic theory validates a logic for tense and modality in which the perpetuity principles are theorems, providing a logical foundation for reasoning about future contingency.
• “Programmatic Semantics” (talk | handout) Formal semantics traditionally relies on hand-verified proofs and countermodels, limiting the range of inferences that can be validated as theories grow in complexity. This paper presents the model-checker, a computational framework that treats semantic theories as executable programs with modular semantic clauses that can be easily imported and combined. By ruling out finite countermodels smaller than a user-defined limit, the model-checker provides evidence that a logical consequence has no countermodels. The framework provides theory-agnostic infrastructure for implementing diverse semantic frameworks, from intensional to hyperintensional approaches, with compositional modularity allowing selective operator loading and systematic reuse. We demonstrate the framework’s capabilities by comparing the Logos semantics for counterfactual conditionals to Fine’s imposition semantics and by comparing the Logos semantics for negation to Bernard and Champollion’s exclusion semantics. A systematic comparative methodology enables controlled theory benchmarking, revealing that the arity of semantic primitives dominates other parameters in determining the computability of a semantic theory. The framework includes TheoryLib for sharing semantic theories in a standardized format. Rather than a substitute for traditional model theory, the framework greatly eases the process of prototyping new semantic theories and making novel additions to existing theories. This paper represents the first computational implementation of bilateral truthmaker semantics and establishes computational tractability as a measurable theoretical virtue alongside logical adequacy.
• “Hyperintensional Causation” This paper develops a hyperintensional semantic theory for past tense causal claims that are critical for attributing responsibility 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 the task semantics developed in “Counterfactual Worlds” (2025) which is better able to encode the explanatory relationships between events. The paper concludes by employing the resulting semantic theory to analyse a number of characteristic causal scenarios.
• “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.