Programmatic truthmaker semantics

Benjamin Brast-McKie (University of Oxford), Miguel Buitrago

This talk presents a programmatic methodology which uses the model-checker software that I developed with help from Miguel Buitrago during his UROP at MIT to rapidly prototype truthmaker semantic theories.    We will begin by presenting a standard methodology in philosophical logic to highlight a number of shortcomings which motivate a programmatic methodology. We will then introduce the model-checker which draws on the SMT solver Z3 to rule out finite countermodels of a user specified size to provide evidence that there are no countermodels to the logical consequence in question. Rather than displacing traditional methods, implementing a programmatic semantics with the model-checker supports the development of a model theory and proof theory for a language.    In order to make the workflow concrete, we will present two case studies, the first of which compares implementations of Fine’s (2012a,b) imposition semantics for counterfactual conditionals with the extension provided in Brast-McKie (2025). After demonstrating the tooling that the model-checker provides for theory analysis and comparison, we will turn to present some of the difficulties faced in attempting to implement Champollion and Bernard’s (2024) unilateral semantics for negation. In addition to the standard theoretical virtues, these case studies will shed light on the computability of a semantic theory which the model-checker makes salient.  In addition to facilitating the study of complex semantic theories, the model-checker provides resources for uploading semantic theories to the TheoryLib to facilitate collaboration. Programmatic semantic theories are also modular, making them easy to combine and compare, allowing users to survey the interactions in languages with many operators. Moreover, the computability of a semantic theory provides an objective measure that may be weighed alongside other theoretical virtues.    Although the model-checker is a general purpose utility for working in semantics, applications in hyperintensional semantics are particularly natural given the increased complexity of these semantic systems. Rather than a deficiency, we will characterize well-motivated forms of theoretical complexity as a sign of the maturity of semantics as a discipline. It is in support of both the future development and accessibility of semantics that the model-checker aims to make a contribution. The talk will conclude by presenting the proof-checker which provides a complementary utility for developing the proof theory and metalogic in the LEAN proof assistant.