Software

Model-Checker

Whereas intensional semantic theories model propositions by subsets of a set of worlds, hyperintensional state semantic theories model propositions by ordered pairs of sets of states — exact verifier states and exact falsifier states (I motivate and defend such an account in “Identity and Aboutness” and “Counterfactual Worlds”). Although state semantics provides the much richer theory of content needed to give semantic clauses for counterfactual conditional, constitutive explanatory, and relevance operators, the resulting space of models is much more complex than intensional models.

In order to facilitate exploration of the space of hyperintensional models, the model-checker draws on the Z3 SMT solver to provide tooling for finding hyperintensional countermodels and establishing validity over models up to a user-specified level of complexity, for inferences in a propositional language with operators for negation, conjunction, disjunction, the material conditional and biconditional, the must/might counterfactual conditionals, necessity and possibility, ground ("sufficient for"), essence ("necessary for"), propositional identity ("just is for"), and relevance.

Accessible installation instructions are provided in the GitHub repository. If you have any trouble installing or using the model-checker, or find any surprising or unnatural results, feel free to open an issue in the GitHub repository.