Logos is a formal verification framework in LEAN 4 implementing hyperintensional logics for verified AI reasoning. By combining an axiomatic proof system with recursive semantics, Logos generates unlimited self-supervised training data for AI systems, providing proof receipts for valid inferences and countermodels for invalid ones without relying on human annotation.
The project also includes the Bimodal theory, a fragment of independent interest providing a complete bimodal logic for reasoning about past and future contingency. While the Bimodal theory serves as a methodological testbed for Logos development, it captures fundamental relationships between time and possibility in its own right. See Bimodal Theory for details.
Specifications: Logos | Bimodal
Demo: Bimodal
The Logos theory is an extensible formal language equipped with an axiomatic proof system and recursive semantic theory. The modular architecture extends the expressive power of the language through progressive layer extensions:
┌─────────────────────────────────────────────────────────────────────────────────┐
│ Constitutive Foundation │
│ (hyperintensional base layer) │
└─────────────────────────────────────┬───────────────────────────────────────────┘
│ required
▼
┌─────────────────────────────────────────────────────────────────────────────────┐
│ Dynamical Foundation │
│ (modal, temporal, counterfactual, causal) │
└─────────────────────────────────────┬───────────────────────────────────────────┘
│
┌──────────────┬─────────────────┼────────────────┬──────────────┐
│ optional │ optional │ optional │ optional │ optional
▼ ▼ ▼ ▼ ▼
┌───────────┐ ┌───────────┐ ┌─────────────────┐ ┌────────────┐ ┌───────────┐
│ Epistemic │ │ Abilities │ │ Normative │ │ Choice │ │ Spatial │
│ Extension │ │ Extension │ │ Extension │ │ Extension │ │ Extension │
│ (belief, │ │ (Can,Stit)│ │ (obligation, │ │ (FP, FF, │ │ (location,│ ...
│ knowledge,│ │ │ │ permission, │ │ Ch) │ │ spatial │
│probability│ │ │ │ preference) │ │ │ │ relations)│
└─────┬─────┘ └─────┬─────┘ └────────┬────────┘ └─────┬──────┘ └─────┬─────┘
│ │ │ │ │
└─────────────┴────────────────┼────────────────┴──────────────┘
│ at least one required
▼
┌─────────────────────────────────────────────────────────────────────────────────┐
│ Agent-dependent extensions │
│ ┌─────────────────┐ ┌─────────────────┐ ┌───────────────────────────────┐ │
│ │ Agential │ │ Social │ │ Reflection │ │
│ │ (agent-indexing)│ │ (common ground) │ │ (metacognition, I operator) │ │
│ └─────────────────┘ └─────────────────┘ └───────────────────────────────┘ │
└─────────────────────────────────────────────────────────────────────────────────┘
-
Constitutive Foundation: Provides the hyperintensional base with predicates (
F,G), functions (f,g), variables (x,y), boolean operators (¬,∧,∨,⊥,⊤), lambda abstraction (λ), identity (=), and constitutive operators (propositional identity≡, grounding≤, essence⊑, reduction⇒) over a complete lattice with bilateral propositions (verifier/falsifier pairs). This enables fine-grained distinctions between propositions with identical truth-values and modal profiles but different verification conditions, essential for exact specification of what makes a claim true. -
Dynamical Foundation: Adds quantifiers (
∀,∃), modal operators (□,◇) for necessity and possibility, temporal operators (H,G,P,F,S,U) for reasoning across time, store/recall operators (↓,↑) for temporal reference, actuality (Act) for distinguishing actual from possible, counterfactual conditionals (□→,◇→) for hypothetical reasoning, and causal operators (○→,◌→) for explanatory links. Together these resources enable reasoning about action sequences, future contingency, what would have happened under different circumstances, and causal relationships. -
Epistemic Extension: Introduces epistemic modals (
Mi,Mu), belief (B), probability (Pr), and indicative conditional operators (↪) for reasoning under uncertainty. By extending the semantic framework with credence functions to assign weights to state transitions, agents can track how evidence updates beliefs across time and distinguish what an agent believes from what is actually the case. -
Abilities Extension: Provides ability (
Can) and STIT (Stit) operators for reasoning about capacities. Ability modals express what an agent can bring about through their capacities, with stronger truth conditions than circumstantial possibility since ability entails possibility but not vice versa. This enables reasoning about what agents are capable of accomplishing given their intrinsic capacities and circumstances. -
Normative Extension: Adds obligation (
O), permission (P), and a preference operator (≺) with value orderings over states for reasoning about what ought to be done, what is permitted, and how to rank alternatives. This enables ethical reasoning about alternatives. -
Choice Extension: Introduces free choice permission (
FP) and best choice (Ch) operators for reasoning about permission over alternatives. Free choice modals address the distribution of permission over disjunctive alternatives---intuitively, "you may have an apple or a pear" implies permission for each disjunct. This enables reasoning about which alternatives are permitted and how permissions combine. -
Spatial Extension: Provides location-dependent operators and spatial relations for reasoning about where things are and how they are oriented relative to an orientation basis. This supports navigation, containment reasoning, and location-sensitive planning.
-
Agential Extension: Indexes epistemic and normative operators to specific agents (
B_a,≺,O_a, …), enabling reasoning about what different agents believe, prefer, and are obligated to do. This transforms single-perspective reasoning into multi-agent coordination where agents can model each other's epistemic and normative states. -
Social Extension: Provides resources for common ground construction and group-level reasoning, building upon the Agential Extension to enable reasoning about shared beliefs, build trust in other agents, and coordinate on common goals.
-
Reflection Extension: Adds first-person metacognitive operators (
I) for self-directed reasoning about one's own beliefs, abilities, and progress towards goals. This enables an agent to reason about what it is in a good position to believe given evaluation of its own limitations and track relative to other agents. Essential for AI systems that must understand their own capabilities and benefit from the capacity to learn by the testimony of others.
The Constitutive Foundation and Dynamical Foundation provide essential expressive resources for verified reasoning in an interpreted language. The Epistemic, Abilities, Normative, Choice, and Spatial Extensions are modular plugins that can be combined in any subset. The agent-dependent extensions (Agential, Social, and Reflection) inherit from the layers above and are free to interact with each other.
AI reasoning in the Logos is both verified by proof receipts for all inferences and interpreted by explicit semantic models, providing scalable oversight for sophisticated reasoning.
See Theoretical Foundations below and the Reference Manual for further details.
Value Proposition
- RL Training - Dual verification for self-supervised AI learning
- Motivations - Philosophical foundations for formal reasoning
Architecture
- Layered Architecture - Progressive layer system for modal-temporal logic
- Constitutive Foundation - Foundational predicates, quantifiers, and grounding
- Application Domains - Medical planning, legal reasoning, multi-agent coordination
Status & Usage
- Implementation Status - Current development progress
- Installation - Quick start and setup guides
- Documentation - User guides, development resources, research
Reference
- Theoretical Foundations - Academic papers underlying the semantics
- Bimodal Theory - Intensional logic comparison baseline
- Citation - How to cite this project
- License - GPL-3.0 License
- Contributing - Guidelines for contributors
Training AI systems to reason reliably requires both positive signals (valid inferences) and corrective signals (invalid inferences with counterexamples where the premises are true and the conclusion is false). This dual verification approach offers three key advantages:
- Unbounded: Infinite theorems are derivable from the axiom system
- Clean: Soundness guarantees only valid inferences are derivable
- Justified: LEAN 4 proofs provide verifiable receipts; Z3 countermodels refute invalid claims
By contrast, human reasoning data is limited, inconsistent, and prone to error, providing a poor training source. Beyond pattern matching, reasoning in the Logos provides proof receipts which ensure validity where the semantic theory for the Logos provide interpretability over explicit semantic models, offering scalable oversight for sophisticated forms of AI reasoning with an extensible set of operators.
| Component | Role | Training Signal |
|---|---|---|
| LEAN 4 Proof System | Derives valid theorems with machine-checkable proofs | Positive RL signal |
| ModelChecker | Identifies invalid inferences with explicit countermodels | Corrective RL signal |
The ModelChecker implements the same Logos semantic theory in Python/Z3, providing Z3-based countermodel generation for invalid inferences. Together, ProofChecker (LEAN) and ModelChecker (Z3) form a complete dual verification system---LEAN proves validity while Z3 finds countermodels.
See also: Dual Verification Research | Integration Guide | LogicNotes
Whereas the material sciences have devised methods for refining the raw materials of the natural world into materials fit for building, philosophical logic employs proof theory and model theory (semantics) to engineer formal languages that are fit for theoretical application. Rather than attempting to describe the idiosyncrasies of natural language, stipulating an axiomatic proof system and recursive semantic theory for formal languages provides a well established methodology for engineering the concepts needed for a specific application.
The Logos is an extensible formal language consisting of the logical operators needed for planning and evaluating complex actions in coordination with other agents under the conditions of uncertainty. Whereas the tense operators provide resources for reasoning about the past and future in a given history, the historical modal operators provide resources for reasoning about different possible futures (world-histories). Including tense and historical modal operators in a common language provides the conceptual resources for reasoning about future contingency, quantifying over the possible futures that could transpire from the present moment.
Constructing and evaluating plans amounts to identifying and ranking histories that proceed from the present moment into the anticipated future. The expected value of a plan is a function of its projected value, likelihood of success, and the value of counterfactual alternatives were the plan to fail along its course. Accordingly, robust planning requires counterfactual scrutiny, identifying potential fail points by evaluating the expected cost of the counterfactual histories that proceed from each potential fail point. Rather than relying on human intuition to estimate likely fail points or to rank alternatives, training AI systems to rigorously construct, counterfactually evaluate, and rank plans based on expected outcomes provides an invaluable resource for assisting human agents in effectively navigating future contingency under conditions of uncertainty and high complexity.
In addition to tense, historical modal, and counterfactual operators, effective planning under natural conditions also requires constitutive operators for reasoning about constitution, causal operators for reasoning about causation, epistemic operators for reasoning about belief, likelihoods, and indicative conditionals, and normative operators for reasoning about imperatives and preferences. Accordingly both the proof theory and semantics for the Logos are implemented in layers in order to accommodate an extensible range of operators. The layer architecture enables applications to import precisely the operator combinations needed for a given domain without carrying unused overhead.
See also: Conceptual Engineering | Layer Extensions
The Logos architecture enables domain-specific operator combinations, demonstrating how planned extensions can be composed for specific use cases:
- Constitutive operators: Predicates, functions, quantifiers for representing medical facts and relationships
- Dynamical operators: Modal (
□,◇) + Temporal (G,F,H,P) for treatment timelines, Counterfactual (□→,◇→) for evaluating treatment strategies - Epistemic operators: Probability (
Pr), belief (B) for uncertainty quantification in diagnosis and prognosis - Example:
Prescribe(DrugA) ∧ Taking(MedicationX) □→ F(Normalize(BloodPressure)) ∧ F(Occur(LiverDamage))- Evaluates what would happen under Drug A prescription given current medication
- Distinguishes necessary consequences (
□→) from possible consequences (◇→)
- Constitutive operators: Predicates and functions for representing legal facts and evidence
- Dynamical operators: Modal + Temporal for tracking events and beliefs across time
- Epistemic operators: Belief (
B), epistemic modals (Mi,Mu) for evidence analysis - Normative operators: Obligation (
O), Permission (P) for legal requirements and permissions - Example: Tracking how evidence reveals agent beliefs and motives, constructing narratives connecting motive to action
- Constitutive: Predicates and functions for representing agent properties and relationships
- Dynamical: Modal + Temporal for action timelines and coordination constraints, Counterfactuals for evaluating alternative strategies
- Epistemic: Belief operators for modeling other agents' knowledge states
- Normative: Deontic operators (
O,P) for obligations and permissions in negotiation
See also: Methodology | Layer Extensions | Architecture
The project includes the Bimodal theory, a complete propositional intensional logic combining S5 modal and linear temporal operators. Bimodal captures a fundamental philosophical insight: the deep relationship between time and possibility. The present opens onto multiple possible futures (world-histories) that share a common past. This relationship is formalized through the perpetuity principles (P1-P6), which establish that what is necessary is perpetual and what occurs is possible.
Bimodal provides a well-motivated purely intensional target for developing the formal methodology—axiomatic proof system, recursive semantics, and metalogic—that is then extended to Logos. By validating the methodology at a simpler complexity level (propositional, intensional, world-states as primitives), we gain confidence before scaling to the hyperintensional complexity of Logos (second-order, fine-grained states with parthood, layered extensions).
The patterns developed in Bimodal transfer directly to Logos: task semantics for relating states across time, proof system architecture for deriving valid inferences, soundness proof techniques, and automation strategies. This scaling approach ensures that the foundational machinery is robust before tackling the greater expressivity of hyperintensional reasoning.
The contrast between Bimodal's purely intensional semantics and Logos's hyperintensional foundation demonstrates the advantages of hyperintensional semantics for supporting a wider range of operators including explanatory, epistemic, and normative operators that require distinguishing necessarily equivalent propositions.
For the full presentation of Bimodal and its comparison with Logos, see A Bimodal Logic for Tense and Modality.
For implementation details, see Theories/Bimodal/README.md.
The Logos methodology comprises three components: (1) an axiomatic proof theory for deriving valid inferences, (2) a recursive semantic theory for interpreting formulas in explicit models, and (3) a metalogic establishing the soundness and completeness of the proof theory over the semantics.
For detailed status: Implementation Status | LEAN Registry | TODO
- LEAN 4 v4.14.0 or later
- Lake (included with LEAN 4)
- Git for version control
- ~5GB disk space (for Mathlib cache)
AI-Assisted (Recommended): Use Claude Code for automated installation
Manual Installation:
# Install elan (LEAN version manager)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Clone repository
git clone https://github.com/benbrastmckie/ProofChecker.git
cd ProofChecker
# Build project (first build downloads Mathlib cache, ~30 minutes)
lake build
# Run tests
lake test| Guide | Description |
|---|---|
| Claude Code | AI-assisted installation (recommended) |
| Basic Installation | Manual installation steps |
| Getting Started | Terminal basics, VS Code, NeoVim setup |
| Using Git | Git/GitHub configuration |
For complete setup: Installation Overview
Getting started and working with Logos:
- Tutorial - Getting started guide
- Examples - Modal, temporal, bimodal examples
- Architecture Guide - TM logic specification
- Methodology - Philosophical foundations
- Integration Guide - Model-Checker integration
- Tactic Development - Custom tactic development
Contributing and extending Logos:
- Contributing - Contribution guidelines
- LEAN Style Guide - Coding conventions
- Testing Standards - Test requirements
- Metaprogramming Guide - LEAN 4 metaprogramming
- Module Organization - Project structure
- Quality Metrics - Quality targets
- Phased Implementation - Implementation roadmap
- Directory README Standard - Documentation requirements
- Documentation Quality Checklist - Quality assurance
Current status and tracking:
- Implementation Status - Module-by-module status
- Known Limitations - Gaps and workarounds
- Sorry Registry - Technical debt tracking
- Tactic Registry - Tactic implementation status
- Maintenance - TODO management workflow
- TODO - Active task tracking
Vision and planned architecture:
- Research Overview - Research documentation index
- Dual Verification - RL training architecture
- Layer Extensions - Layers 1-3 specifications
- Proof Library Design - Theorem caching
- Conceptual Engineering - Philosophical methodology
- Documentation Hub - Complete documentation index
- Bimodal Operators - Formal symbols reference
- Logos Glossary - Key concepts and definitions
Logos implements formal semantics developed in recent research:
"The Construction of Possible Worlds" (Brast-McKie, 2025)
- Compositional semantics drawing on non-deterministic dynamical systems theories to provide an intensional semantics for bimodal logics with historical modals and tense operators
- Complete implementation in
Semantics/package (TaskFrame, WorldHistory, TaskModel, Truth evaluation)
"Counterfactual Worlds" (Brast-McKie 2025)
- Hyperintensional semantics for counterfactual conditionals distinguishing necessarily equivalent antecedents
- Foundation for the explanatory layer extension (counterfactual
□→and causal○→operators) - Integrates with task semantics to evaluate counterfactual reasoning across possible world histories
"Identity and Aboutness" (Brast-McKie 2021)
- State-based semantics using verifier/falsifier pairs to capture fine-grained propositional content
- Enables distinctions between necessarily equivalent propositions based on what they are about
- Theoretical foundation for constitutive explanatory reasoning (grounding
≤, essence⊑, and propositional identity≡operators)
If you use Logos in your research, please cite:
@software{proofchecker2025,
title = {Logos: LEAN 4 Proof System for Bimodal Logic TM},
author = {Your Name},
year = {2025},
url = {https://github.com/yourusername/Logos}
}This project is licensed under GPL-3.0. See LICENSE for details.
Contributions welcome! See Contributing Guide for guidelines.
# Install LEAN 4
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Build and test
git clone https://github.com/yourusername/Logos.git
cd Logos
lake build
lake test
lake lint- PascalCase: LEAN source directories (
Logos/,Theories/,Tests/) - lowercase: Non-code directories (
docs/,scripts/,benchmarks/,latex/)
See Directory Naming Convention for details.
- ModelChecker - Parallel implementation of Logos semantic theory in Python/Z3 for countermodel generation and semantic verification. Together with ProofChecker, forms the dual verification architecture for RL training.