A programmatic methodology in semantics streamlines the otherwise grueling process of attempting to develop and test novel semantic theories as well as their corresponding resulting logics. Instead of only developing a model-theoretic version of a semantics and working out the consequence by hand or not at all, the model-checker provides tooling for implementing semantic clauses using Z3‘s python API.

In addition to developing a proof theory for a given semantics where derivations and metalogical theorems are established by hand, the next phase of this project aims to develop the proof-checker which draws on the LEAN proof assistant to provide support for systematically axiomatizing semantic theories. In addition to a domain specific language (DSL) for developing the proof theory and metalogic for a semantics, the proof-checker will allow users to query the model-checker from within LEAN before attempting to write a derivation or establish a logical consequence.

These programmatic methods aim to support the growth and maturity of semantics and logic as a discipline by easing the process of investigating increasingly complex theories as well as exploring the interaction principles within a unified Language of Thought (LoT) that includes many different operators.

Model-Checker

In order to rapidly prototype semantic clauses for the operators included in The Language of Thought (LoT) and adequately describe their interactions, I used Microsoft’s SMT solver Z3 to build the model-checker for developing and implementing semantic theories. The operators currently implemented with the model-checker include:

• neg for negation
• wedge for conjunction
• vee for disjunction
• rightarrow for the material conditional
• leftrightarrow for the material biconditional
• boxright for the must counterfactual conditional
• circleright for the might counterfactual conditional
• Box for necessity
• Diamond for possibility
• leq for ground read ‘sufficient for’
• sqsubseteq for essence read ‘necessary for’
• equiv for propositional identity read ‘just is for’
• preceq for relevance

In addition to the operators above, the model-checker provides a TheoryLib consisting of a library of different semantic theories that users can evaluate and modify as well as contributing their own. You can find more information in the GitHub repository.

Programmatic Semantics

Although computational resources are commonplace, the ability to make use of these resources to develop and explore the implications of novel semantic theories remains limited. For instance, Prover9 and Mace are restricted to first-order and equational statements. However, for the purposes of developing new semantic theories and studying their corresponding logics, it is desirable to: (1) introduce a range of primitive operators; (2) specify semantic clauses for each operator; (3) define the space of models for the resulting language; (4) set up unit tests for easily evaluating which sentences are a logical consequence of which upon making changes to the semantics; and (5) print readable countermodels if there are any. After developing and testing a semantics for a language, the corresponding model theory and proof theory can be developed with a much better sense of the range of theorems before establishing soundness and attempting to complete the logic.

In order to address these aims, the model-checker provides a programmatic semantics for a range of hyperintensional operators as well as a general methodology for declaring primitive operators and providing their semantics. Instead of computing whether a given sentence is a logical consequence of some set of sentences by hand, these resources allow users to search for countermodels or establish logical consequence up to a finite level complexity specified by the user. If finite countermodels exist, users will be able to generate and print those models rather than attempting to do so by hand which is not only time consuming, but prone to include errors.

Although computational systems cannot search the space of all models (typically a proper class), proving that there are no finite models up to a user specified level of complexity provides evidence that the logical consequence in question holds in full generality. The broader the range of models considered, the stronger this evidence. Given sufficient evidence, logical consequences can then be established by hand. In the next phase of this project, I intend to incorporate the LEAN proof assistant into the methodology in order to streamline the process of axiomatizing novel primitives, providing new tooling for pursuing projects in conceptual engineering.