Formalizing Lewis's Theory of Common Knowledge in Lean 4

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

Key Results

Approach	A1 Status	A6 Status	Lewis's Theorem	Status
Cubitt-Sugden	AXIOM	AXIOM	✓ Proven	A1 and A6 assumed as primitive axioms
Sillari	✗ FAILS	No analogue	False / Trivial	Modal logic cannot capture "thereby"
Vromen	✓ THEOREM	✓ THEOREM	✓ Proven	A1 and A6 derived from AR + T1–T3; no logical omniscience

On shared assumptions. All three approaches take Lewis's four base conditions (C1–C4: publicity, reflexivity, target indication, shared standards) as hypotheses of the theorem — that is part of what it means to be a basis for common knowledge, and is not what distinguishes the approaches. The contrast is in what the inference apparatus (A1, A6) requires:

• Cubitt–Sugden introduces A1 and A6 as primitive axioms alongside C1–C4, without further explanation.
• Vromen replaces A1 and A6 with a different primitive apparatus — the Application Rule (AR) plus three tautology witnesses (T1, T2, T3) — from which A1 and A6 are derived as theorems. C1–C4 remain hypotheses.

So Vromen's contribution is not "fewer assumptions" in an absolute sense; it is a shift in the primitive commitments, from opaque inference axioms to a compositional reason-term structure that explains why A1 and A6 hold.

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

Quick Start

Installation

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).

Reading Guide

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 — Trivial model proving axiom consistency
5. Lewis/Vromen_FittingModel.lean — Non-trivial Fitting model with genuine reason-tracking

Repository Structure

.
├── 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               # Trivial model (axiom consistency)
│   └── Vromen_FittingModel.lean          # Non-trivial Fitting model
├── docs/
│   ├── Lewis_paper_main.tex / .pdf        # ITP 2026 paper
│   ├── C_review_Lewis.tex / .pdf          # Review document
│   ├── Vilnius_talk_2026.tex / .pdf       # Vilnius conference slides
│   └── speaker_notes.md / .pdf           # Speaker notes
│
│ plus standard Lean project files (lakefile.toml, lean-toolchain, lake-manifest.json)
└── LICENSE

Main Contributions

1. Cubitt-Sugden Baseline

• Treats "reason to believe" (R) and "indication" (Ind) as primitive relations
• Takes C1–C4 (publicity, reflexivity, target indication, shared standards) as the base conditions of a basis for common knowledge
• Introduces A1 (detachment) and A6 (indication propagation) as additional primitive axioms governing the inference apparatus
• Proves Lewis's theorem for the complete infinite hierarchy (Cubitt and Sugden prove only the first three levels and assert the rest)
• Limitation: A1 and A6 are stipulated rather than explained

2. Sillari Refutation

• 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 logic of Sillari's form cannot capture Lewis's "thereby"; stronger modal resources may but at a cost comparable to justification logic

3. Vromen's Justification Logic

• A1 proven as theorem — direct from the application rule
• A6 proven as theorem — one line from E2, E3
• Lewis's theorem proven — non-trivial structural induction (C1–C4 remain as hypotheses, as in Cubitt–Sugden)
• Captures "thereby" — reason composition via multiplication: s * t
• No logical omniscience — reasons for three tautologies (T1, T2, T3) suffice; agents do not automatically believe all logical consequences of their reasons
• Axiom consistency — concrete satisfying model provided in Lewis/Vromen_JLModel.lean
• The shift: Cubitt–Sugden's opaque inference axioms A1 and A6 are replaced by a compositional reason-term apparatus (AR + T1–T3) from which they follow as theorems

4. Model Theory

Two models establish consistency and expressiveness of the justification logic axioms:

Trivial model (Vromen_JLModel.lean): Sets rb r i φ := φ — every reason justifies every true proposition. Proves the axiom system (AR, T1–T3) is consistent (satisfiable). Simple but the reason parameter is irrelevant.

Fitting model (Vromen_FittingModel.lean): A non-collapsing model inspired by Fitting (2005) where reasons carry genuine information:

• Reason terms form a free algebra: atomic evidence (unverified), logical constants (self-evident), and composition (modus ponens for reasons)
• fittingRb r i φ holds iff the reason term is grounded (no unverified atoms) and φ is true
• Unverified atoms cannot justify beliefs; logical constants can; composition preserves groundedness
• All four axioms (AR, T1, T2, T3) are satisfied simultaneously and non-trivially
• Non-collapse: ∃ r φ, φ ∧ ¬ fittingRb r i φ — not every reason justifies every truth

Why This Matters

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. Reasons carry genuine information — The Fitting model shows reason-tracking is non-trivial, not just truth-tracking
4. Machine verification matters — Reveals gaps invisible in informal arguments

Reproducing #print axioms Output

Every key theorem in the project includes a #print axioms directive at the end of its source file. When you build the project, Lean prints the axiom dependencies for each checked declaration, confirming that the proofs rely only on the expected foundations.

Steps

1. Build the project (after cloning and fetching the cache — see Quick Start):

   lake build 2>&1 | grep "#print\|axioms\|does not depend"

   Or simply run lake build and look for the info: lines in the output.

2. Expected output. A successful build produces the following axiom reports:

   Vromen justification logic (Lewis/Vromen_justification_logic.lean):

   'JustificationLogic.E1' does not depend on any axioms
   'JustificationLogic.L1' does not depend on any axioms
   'JustificationLogic.E2' does not depend on any axioms
   'JustificationLogic.E3' does not depend on any axioms
   'JustificationLogic.A1' does not depend on any axioms
   'JustificationLogic.A6' does not depend on any axioms
   'JustificationLogic.Lewis' does not depend on any axioms
   

   Cubitt–Sugden baseline (Lewis/Cubitt_Sugden_baseline.lean):

   'L3_aesop' depends on axioms: [propext, Quot.sound]
   'lewis_theorem' does not depend on any axioms
   

   (L3_aesop uses aesop, which introduces propext and Quot.sound — both standard Lean axioms.)

   Trivial model (Lewis/Vromen_JLModel.lean):

   'JLModel.AR_trivial' does not depend on any axioms
   'JLModel.T1_trivial' does not depend on any axioms
   'JLModel.T2_trivial' does not depend on any axioms
   'JLModel.T3_trivial' does not depend on any axioms
   'JLModel.axioms_consistent' does not depend on any axioms
   

   Fitting model (Lewis/Vromen_FittingModel.lean):

   'FittingModel.AR_fitting' does not depend on any axioms
   'FittingModel.T1_fitting' does not depend on any axioms
   'FittingModel.T2_fitting' does not depend on any axioms
   'FittingModel.T3_fitting' does not depend on any axioms
   'FittingModel.fitting_sound' does not depend on any axioms
   'FittingModel.fitting_non_collapse' does not depend on any axioms
   'FittingModel.fitting_reason_discriminates' does not depend on any axioms
   'FittingModel.fitting_not_trivial' does not depend on any axioms
   'FittingModel.axioms_consistent_nontrivial' does not depend on any axioms
   

3. Interpretation. "Does not depend on any axioms" means the proof is purely constructive — it uses no axioms beyond the core type theory of Lean's kernel (not even propext or Classical.choice). This is the strongest possible guarantee: the result follows from definitions and logical rules alone.

   The only exception is L3_aesop, which depends on propext (propositional extensionality) and Quot.sound (quotient soundness). These are standard Lean axioms accepted by the entire Mathlib ecosystem, and are introduced by the aesop tactic rather than by the mathematical content of the lemma.

   None of the theorems depend on Classical.choice, confirming that no classical reasoning is used.

Citation

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

Presentations

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

References

• 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.
• Fitting, M. (2005). The logic of proofs, semantically. Annals of Pure and Applied Logic, 132(1), 1–25.

License

Licensed under the Apache License, Version 2.0. See LICENSE for details.

Author

Huub Vromen Department of Philosophy Radboud University, Nijmegen Email: huub.vromen@ru.nl