This project was edited by Aristotle.

To cite Aristotle:

• Tag @Aristotle-Harmonic on GitHub PRs/issues
• Add as co-author to commits:

Co-authored-by: Aristotle (Harmonic) <[email protected]>

Machine-verified formalizations of three approaches to David Lewis's theory of common knowledge in Lean 4.

Based on: Vromen, H. (2024). Reasoning with reasons: Lewis on common knowledge. Economics & Philosophy, 40(2), 397–418. DOI: 10.1017/S0266267123000238

All proofs are fully formalized and verified in Lean 4 with zero sorry statements.

ITP 2026 version (archived at Zenodo — DOI to be assigned upon publication):

git clone --branch ITP_2026 https://github.com/hjvromen/lewis-common-knowledge-lean4.git
cd lewis-common-knowledge-lean4
lake exe cache get
lake build

Latest development version:

git clone https://github.com/hjvromen/lewis-common-knowledge-lean4.git
cd lewis-common-knowledge-lean4
lake exe cache get
lake build

Note: lake exe cache get downloads pre-built Mathlib artifacts at the exact versions pinned in lake-manifest.json, ensuring reproducibility. lake build then compiles only the project-specific files. Do not run lake update unless you intentionally want to upgrade to newer versions of Lean dependencies (which may introduce breaking changes).

For understanding the theory: See GUIDE.md for mathematical and philosophical background (also available as GUIDE.pdf)

For verifying proofs:

1. Lewis/Cubitt_Sugden_baseline.lean - Syntactic reconstruction with axioms
2. Lewis/Sillari_refutation.lean - Why modal logic fails (counterexamples)
3. Lewis/Vromen_justification_logic.lean - Correct foundation using justification logic
4. Lewis/Vromen_JLModel.lean - Concrete model proving axiom consistency

.
├── README.md                              # This file (project overview)
├── GUIDE.md                               # Comprehensive technical guide
├── GUIDE.pdf                              # Compiled guide
├── Lewis.lean                             # Main entry point (imports all modules)
├── Lewis/
│   ├── Cubitt_Sugden_baseline.lean        # Syntactic approach
│   ├── Sillari_refutation.lean            # Modal logic counterexamples
│   ├── Vromen_justification_logic.lean    # Justification logic solution
│   └── Vromen_JLModel.lean               # Concrete model (axiom consistency)
│
│ plus standard Lean project files (lakefile.toml, lean-toolchain, lake-manifest.json)
└── LICENSE

• Treats "reason to believe" (R) and "indication" (Ind) as primitive relations
• Proves Lewis's theorem for the complete infinite hierarchy (Cubitt and Sugden prove only the first three levels)
• Makes all assumptions explicit as axioms A1 and A6
• Limitation: Cannot explain why A1 and A6 hold

• B3 (Lewis's A1) fails - Machine-verified counterexample
• C4 (Cubitt-Sugden axiom) fails - Machine-verified counterexample
• Lewis's theorem fails - Under local assumptions
• Lewis's theorem is trivial - Under global assumptions
• Root problem: Modal □ cannot capture Lewis's "thereby"

• A1 proven as theorem - direct from application rule
• A6 proven as theorem - one line from E2, E3
• Lewis's theorem proven - Non-trivial structural induction
• No logical omniscience - Only reasons for three tautologies (T1, T2, T3) needed
• Captures "thereby" - Reason composition via multiplication: s * t
• Axiom consistency - Concrete satisfying model provided in Lewis/Vromen_JLModel.lean

Lewis's "thereby" in his definition of indication has been informally understood for decades but never properly formalized. This project shows:

1. Modal logic is inadequate - Cannot capture evidential dependence
2. Justification logic works - Explicit reason terms solve the problem
3. Machine verification matters - Reveals gaps invisible in informal arguments

If you use this formalization in academic work, please cite the associated paper and the archived software artifact.

• ILLC LIRa Seminar, Amsterdam, 29 January 2026
• Logic and Philosophy: Historical and Contemporary Issues, Vilnius University, 22–23 May 2026 — slides: docs/Vilnius_talk_2026.tex (current version).

• Lewis, D. (1969). Convention: A Philosophical Study. Harvard University Press.
• Cubitt, R. P., & Sugden, R. (2003). Common knowledge, salience and convention. Economics and Philosophy, 19, 175–210.
• Sillari, G. (2005). A logical framework for convention. Synthese, 147, 379–400.
• Vromen, H. (2024). Reasoning with reasons: Lewis on common knowledge. Economics & Philosophy, 40(2), 397–418.
• Artemov, S., & Fitting, M. (2019). Justification Logic: Reasoning with Reasons. Cambridge University Press.

MIT License - see LICENSE file

Huub Vromen Department of Philosophy Radboud University, Nijmegen Email: [email protected]