{"id":5538,"date":"2026-01-09T10:51:56","date_gmt":"2026-01-09T09:51:56","guid":{"rendered":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/?p=5538"},"modified":"2026-01-29T20:39:09","modified_gmt":"2026-01-29T19:39:09","slug":"lira-session-huub-vromen","status":"publish","type":"post","link":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/2026\/01\/lira-session-huub-vromen\/","title":{"rendered":"LIRa session: Huub Vromen"},"content":{"rendered":"<p>The <a href=\"https:\/\/video.uva.nl\/media\/LIRa+seminar+on+2026-01-29+by+Huub+Vromen\/0_qq0vpjw1\">recording of this talk is available here<\/a>.<\/p>\n<p>Speaker: <a href=\"https:\/\/www.ru.nl\/en\/people\/vromen-h\">Huub Vromen<\/a> (Radboud University Nijmegen)<\/p>\n<p>Date and Time: Thursday, January&nbsp;29th 2026, 16:30-18:00<\/p>\n<p>Venue: ILLC Seminar Room F1.15, Science Park 107 <strong>and<\/strong>\u00a0<a href=\"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/guidelines-for-online-sessions\/\">online<\/a>.<\/p>\n<p>Title: <strong>Lewis on common knowledge: formalizations in Lean 4<\/strong><\/p>\n<p><em>Abstract.<\/em> David Lewis (1969) introduced common knowledge using &#8216;having reason to believe&#8217; rather than &#8216;knowledge&#8217;. 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.<br \/>\nThis talk discusses three formal reconstructions. I first analyze Cubitt and Sugden&#8217;s (2003) syntactic approach, treating &#8216;reason to believe&#8217; and &#8216;indication&#8217; as primitives governed by axioms. They correctly derive the first steps of the infinite hierarchy but must assume crucial principles (A1, A6) as axioms.<br \/>\nI then analyze Sillari&#8217;s (2005) modal-logic approach and present machine-verified counterexamples showing key axioms are invalid and the main theorem either fails or becomes vacuous.<br \/>\nFinally, I present Vromen&#8217;s (2024) justification logic approach, representing reasons as syntactic objects. This captures Lewis&#8217;s &#8220;thereby&#8221; condition and derives A1 and A6 as theorems.<br \/>\nAll results are formalized in Lean 4, demonstrating how machine verification functions as a discovery instrument \u2014 revealing hidden structure, catching errors, and verifying proofs of theorems.<\/p>\n<p>Vromen, H. (2024). Reasoning with reasons: Lewis on common knowledge. Economics and Philosophy, 40(2), 397-418. <a href=\"https:\/\/doi.org\/10.1017\/S0266267123000238\">https:\/\/doi.org\/10.1017\/S0266267123000238<\/a><\/p>\n<p>Vromen, H. (2025). Formalizing Lewis\u2019s Theory of Common Knowledge in Lean 4. <a href=\"https:\/\/github.com\/hjvromen\/lewis-common-knowledge-lean4\">https:\/\/github.com\/hjvromen\/lewis-common-knowledge-lean4<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>The recording of this talk is available here.<br \/>\nSpeaker: Huub Vromen (Radboud University Nijmegen)<br \/>\nDate and Time: Thursday, January&nbsp;29th 2026, 16:30-18:00<br \/>\nVenue: ILLC Seminar Room F1.15, Science Park 107 and\u00a0online.<br \/>\nTitle: Lewis on common knowledge: formalizations in Lean 4<br \/>\nAbstract. David Lewis (1969) introduced common knowledge using &#8216;having reason to believe&#8217; rather than &#8216;knowledge&#8217;. He argues that a state of [&#8230;]<\/p>\n","protected":false},"author":11,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[14],"tags":[],"class_list":["post-5538","post","type-post","status-publish","format-standard","hentry","category-all"],"_links":{"self":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/5538","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/comments?post=5538"}],"version-history":[{"count":4,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/5538\/revisions"}],"predecessor-version":[{"id":5553,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/5538\/revisions\/5553"}],"wp:attachment":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/media?parent=5538"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/categories?post=5538"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/tags?post=5538"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}