Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization
2026-06-15 • Logic in Computer Science
Logic in Computer ScienceComputational Complexity
AI summaryⓘ
The authors created a detailed formal version of a technical report on how hard it is to solve a logic problem called Multilevel Syllogistic (MLS) on average. They used a proof assistant called Lean 4 to carefully encode the problem, define rules for interpreting it, and implement a decision procedure that is proven to work correctly in some cases. Their work also explores how complex the problem is under certain conditions, with all the technical details and code included. This formalization helps make the theoretical results more precise and checkable by computers.
Lean 4Average-case complexityMultilevel Syllogistic (MLS)Decision procedureFormalizationNP-average completenessStructural axiomsAxiomatic semanticsReischuk-Schindelhauer classes
Authors
Lars Warren Ericson
Abstract
We describe a Lean~4 formalization revisiting NYU Courant Technical Report TR1995-711 on the average-case complexity of Multilevel Syllogistic (MLS). The development encodes Reischuk--Schindelhauer average-case classes, an axiomatic MLS/EMLS semantics layer, a partial Ferro--Omodeo--Schwartz decision procedure with proved soundness and partial completeness on a membership-free fragment, serialization and step budgets, and conditional NP-average completeness and non-AvP hardness corollaries modulo explicitly documented structural axioms. Full Lean sources are inlined in the appendix modules.