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

part of: Advances in Truthmaker Semantics 2
July 29, 2025, 5:00pm - 6:00pm
Ludwig Maximilians University, Munich

Carl-Friedrich-von-Siemens Foundation
Südliches Schlossrondell 23 80638
Germany

Go to conference's page

This event is available both online and in-person

Sponsor(s):

  • The Siemens Foundation
  • The Humboldt Foundation
  • New York University
  • Syracuse University

Organisers:

Syracuse University
Johns Hopkins University
New York University
New York University
Nottingham University
Syracuse University

Details

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.  

Supporting material

Add supporting material (slides, programs, etc.)

Reminders

Registration

No

Who is attending?

No one has said they will attend yet.

Will you attend this event?


Let us know so we can notify you of any change of plan.