Software

The ModelChecker is a tool for rapidly prototyping semantic theories. Developing a semantics ordinarily means computing by hand whether particular inferences hold, which is slow and error prone precisely where the cases become interesting. The ModelChecker automates this work: given semantic clauses for the operators of a language, it compiles an inference into constraints for Z3, either establishing that the inference holds over all models up to a chosen level of complexity or printing a readable countermodel that shows exactly how it fails. Nothing in the program fixes a semantics in advance: users declare primitive operators, provide their semantic clauses, and set up batteries of test inferences, so that each change to a semantics can be evaluated against its logical consequences in seconds. A countermodel rules an inference out conclusively, while the absence of countermodels at increasing levels of complexity builds evidence that the inference holds in general and is worth the effort of proving.

The package may be installed with pip install model-checker. If you have any trouble installing or using it, or find any surprising or unnatural results, feel free to open an issue.

Whereas the ModelChecker refutes inferences, the ProofChecker establishes them, providing an axiomatic proof system for the Logos together with its metalogic in the Lean 4 proof assistant. Every derivation is checked by the assistant rather than by hand, so a result counts as a theorem only once its proof has been verified in full. Because the two programs are developed in tandem for the same semantics, they discipline one another: an inference that survives every search for a countermodel is a candidate for derivation, a countermodel settles that no derivation is to be found, and soundness guarantees that the two verdicts can never collide.

The tense and modal fragment of the Logos is open-sourced as BimodalLogic, which combines S5 modal operators with the linear tense operators Since and Until, developed in Lean 4 with Lake and Mathlib. The soundness, completeness, and decidability results for this system are established there, and the semantics it axiomatizes is presented in The Construction of Possible Worlds, forthcoming in the Journal of Philosophical Logic. The main repository carries the formalization beyond this fragment to the constitutive and dynamical foundations of the Logos, where the metalogic remains under active development.

The ModelBuilder is designed to construct semantic models from descriptions given in natural language: explicit, inspectable representations of a situation that specify which states of a system are possible, how those states may evolve over time, and which agents belong to the system along with what they believe, prefer, and are able to do. A model of this kind interprets the Logos — it settles the truth-value of every sentence in the language — so constructing one closes the gap between an informal description of a situation and something the ModelChecker and ProofChecker can evaluate exactly.

Together, the three programs are intended to support a familiar cycle of scientific reasoning carried out in formal terms: the ModelBuilder proposes candidate interpretations of the available information, the ProofChecker draws verified consequences from each candidate, and testing those consequences against further evidence prunes the candidates that fail while refining those that survive. This applied direction is the focus of Logos Laboratories.