The Logos is grounded in rigorous academic research in hyperintensional logic, truthmaker semantics, and formal philosophy.
Peer-reviewed publications establishing the theoretical foundations of the Logos.
Benjamin Brast-McKie
Journal of Philosophical Logic, 2026
Develops world states as maximal possible ways for things to be at an instant, with task relations encoding transitions between states. Proposes possible worlds as functions from times to world states, eliminating unnecessary degrees of freedom from model definitions.
Benjamin Brast-McKie
Journal of Philosophical Logic, 2025
Develops a hyperintensional semantics for counterfactual conditionals using bilateral propositions and exact verification, providing a foundation for the Logos dynamical layer.
Benjamin Brast-McKie
Journal of Philosophical Logic, 2021
Explores the relationship between propositional identity and subject matter, contributing to the constitutive foundation of the Logos formal system.
Current research projects exploring new directions in hyperintensional semantics.
Benjamin Brast-McKie
Presents the model-checker as a computational framework treating semantic theories as executable programs with modular semantic clauses. Demonstrates first computational implementation of bilateral truthmaker semantics.
Benjamin Brast-McKie
Develops hyperintensional semantic theory for past-tense causal claims relevant to responsibility attribution. Extends task semantics to better encode explanatory relationships between events.
The intellectual lineage of the Logos system.
Formal operators are refined from natural language through engineering the semantic clauses for the logical operators, removing ambiguities and creating precise truth conditions for the sentences of the language. The Logos distills the conceptual components needed for systematic application, bridging intuitive understanding and formal verification.
Sentences are assigned to bilateral propositions with verifier states (what makes them true) and falsifier states (what makes them false). This hyperintensional semantics distinguishes necessarily equivalent propositions by their verification conditions, enabling fine-grained analysis that possible-worlds semantics fails to capture.
Planning under uncertainty requires comparing alternative temporal evolutions. World histories map times to states, with tense operators tracking evolution within histories and modal operators quantifying over possible histories. This bimodal infrastructure enables the evaluation of competing plans to reason effectively about future contingency.
Counterfactual operators evaluate what would happen under alternative circumstances; causal operators capture productive relationships over time; tense operators shift the time of evaluation. This unified semantics provides resources to counterfactually analyze plans, identifying potential failure points and their future consequences.
First-order and second-order quantifiers bind variables within the hyperintensional framework, with lambda abstraction reducing quantified formulas to property applications. Actuality-restricted quantifiers distinguish what actually exists from what possibly or sometimes exists, enabling precise reasoning about existence claims.
The Reflection Extension enables first-person metacognitive reasoning
through the 'I' operator, which transforms direct expressions into
self-aware epistemic stances. Agents can reason about their own beliefs,
abilities, and progress toward goals, essential for AI systems that must
understand their own capabilities, norms, and epistemic states.
Distance relations are first-class states in the domain---they can be fused with other states and evaluated for possibility, making spatial structure internal. Value quantales provide an abstract algebra of distances, while extended states have located parts with internal geometry capturing pairwise distances. Spatial profiles between bodies compose as bimodules, enabling reasoning about metric constraints and geometric relationships.
Generic statements characterize kinds through paradigmatic instances rather than universal quantification---"Birds lay eggs" is true though male birds do not lay eggs, expressing something distinct from "All birds lay eggs" or even "Most birds lay eggs." Reasoning about arbitrary objects captures how we draw conclusions about kinds without exhaustive enumeration, treating a paradigm instance as representative of its type. These generalizations form defeasible expectations that guide inference while remaining open to revision.
Discover more about our applications and documentation.