A Lean 4 implementation of bimodal logic combining S5 modal operators with linear temporal operators. This project provides a complete formal verification of the syntax, semantics, proof theory, and metalogic for TM logic, establishing soundness, completeness, and decidability.
Paper: "The Construction of Possible Worlds" (Brast-McKie, 2025) - Compositional semantics for bimodal logics with historical modals and tense operators
Specifications: BimodalReference.pdf
Demo: Demo.lean
TM bimodal logic formalizes the deep philosophical relationship between time and possibility: the present opens onto multiple possible futures (world-histories) that share a common past. This relationship is captured through the perpetuity principles (P1-P6), which establish that what is necessary is perpetual and what occurs is possible.
| Result | Statement | Status |
|---|---|---|
| Soundness | (Gamma vdash phi) to (Gamma vDash phi) |
Proven |
| Completeness | valid phi to (vdash phi) |
Proven |
| Deduction Theorem | ((A :: Gamma) vdash B) to (Gamma vdash A to B) |
Proven |
| Decidability | decide phi : DecisionResult phi |
Implemented |
| Symbol | Lean | Reading |
|---|---|---|
Box phi |
box phi |
necessity ("necessarily phi") |
Diamond phi |
diamond phi |
possibility ("possibly phi") |
H phi |
all_past phi |
"phi has always been true" |
G phi |
all_future phi |
"phi will always be true" |
P phi |
some_past phi |
"phi was once true" |
F phi |
some_future phi |
"phi will be true" |
A task frame (W, T, R) consists of:
- W: Set of world-states (metaphysically possible states)
- T: Set of times with linear order
< - R : W -> T -> W -> Prop: Task relation (accessibility across time)
The task relation satisfies nullity (reflexive at each time) and compositionality (forward composition), enabling evaluation of modal and temporal formulas at world-history/time pairs.
Bimodal logic is a fragment of the Logos, a formal language of thought designed to enable AI systems to reason with mathematical certainty. The Logos provides verified synthetic reasoning data of arbitrary complexity through an extensible system of proof theory and semantics. This repository focuses specifically on the bimodal fragment, which is of independent interest due to its completeness and decidability. For more about the Logos project, see logos-labs.ai.
- 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
ProofChecker/
Theories/
Bimodal/ # TM bimodal logic implementation
Syntax/ # Formula types and contexts
ProofSystem/ # Axioms and derivation trees
Semantics/ # Task frame semantics
Metalogic/ # Soundness, completeness, decidability
Theorems/ # Perpetuity principles and derived results
Automation/ # Proof tactics
Examples/ # Demo and pedagogical examples
latex/ # BimodalReference specification document
docs/ # Theory-specific documentation
Tests/ # Test suites
docs/ # Project documentation
specs/ # Task artifacts and planning
- Tutorial - Getting started with bimodal proofs
- Quick Start - Minimal setup guide
- Examples - Worked examples with solutions
- Proof Patterns - Common proof strategies
- Troubleshooting - Common errors and fixes
- Axiom Reference - Complete axiom schemas
- Operator Reference - Formal symbols
- Tactic Reference - Custom tactic usage
- API Reference - Module API documentation
- Contributing - Contribution guidelines
- LEAN Style Guide - Coding conventions
- Testing Standards - Test requirements
- Module Organization - Project structure
- Bimodal Logic - Theoretical foundations
- Dual Verification - RL training architecture
- Proof Library Design - Theorem caching
Bimodal is production-ready with complete metalogic verification.
| Layer | Component | Status |
|---|---|---|
| 0 | Syntax | Complete |
| 1 | ProofSystem | Complete (14 axioms, 7 rules) |
| 2 | Semantics | Complete (TaskFrame, TaskModel, Truth) |
| 3 | Metalogic | Complete (Soundness, Completeness, Deduction, Decidability) |
| 4 | Theorems | Complete (P1-P6 perpetuity principles) |
| 5 | Automation | Partial |
For detailed status: Implementation Status | Bimodal Status
"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 the Semantics/ package (TaskFrame, WorldHistory, TaskModel, Truth evaluation).
"Counterfactual Worlds" (Brast-McKie 2025)
Hyperintensional semantics for counterfactual conditionals distinguishing necessarily equivalent antecedents. Foundation for planned explanatory layer extensions.
"Identity and Aboutness" (Brast-McKie 2021)
State-based semantics using verifier/falsifier pairs to capture fine-grained propositional content. Theoretical foundation for constitutive explanatory reasoning.
- ModelChecker - Python/Z3 implementation of Logos semantic theory for countermodel generation. Together with ProofChecker, forms the dual verification architecture.
If you use this project in your research, please cite:
@software{proofchecker2025,
title = {ProofChecker: LEAN 4 Implementation of Bimodal Logic TM},
author = {Brast-McKie, Benjamin},
year = {2025},
url = {https://github.com/benbrastmckie/ProofChecker}
}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/benbrastmckie/ProofChecker.git
cd ProofChecker
lake build
lake test- PascalCase: LEAN source directories (
Theories/,Tests/) - lowercase: Non-code directories (
docs/,scripts/,specs/)
See Contributing Guide for details.