Upcoming Events

The next event is on Thursday, January 29th:

LIRa session: Huub Vromen


Speaker: Huub Vromen (Radboud University Nijmegen)

Date and Time: Thursday, January 29th 2026, 16:30-18:00

Venue: ILLC Seminar Room F1.15, Science Park 107 and online.

Title: Lewis on common knowledge: formalizations in Lean 4

Abstract. David Lewis (1969) introduced common knowledge using ‘having reason to believe’ rather than ‘knowledge’. He argues that a state of affairs meeting certain conditions generates an infinite hierarchy of higher-order reasons to believe. Unfortunately, his argument is informal and has gaps.
This talk discusses three formal reconstructions. I first analyze Cubitt and Sugden’s (2003) syntactic approach, treating ‘reason to believe’ and ‘indication’ as primitives governed by axioms. They correctly derive the first steps of the infinite hierarchy but must assume crucial principles (A1, A6) as axioms.
I then analyze Sillari’s (2005) modal-logic approach and present machine-verified counterexamples showing key axioms are invalid and the main theorem either fails or becomes vacuous.
Finally, I present Vromen’s (2024) justification logic approach, representing reasons as syntactic objects. This captures Lewis’s “thereby” condition and derives A1 and A6 as theorems.
All results are formalized in Lean 4, demonstrating how machine verification functions as a discovery instrument — revealing hidden structure, catching errors, and verifying proofs of theorems.

Vromen, H. (2024). Reasoning with reasons: Lewis on common knowledge. Economics and Philosophy, 40(2), 397-418. https://doi.org/10.1017/S0266267123000238

Vromen, H. (2025). Formalizing Lewis’s Theory of Common Knowledge in Lean 4. https://github.com/hjvromen/lewis-common-knowledge-lean4

More upcoming events: