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 the state semantics provides the much richer theory of content that is needed to provide semantic clauses for counterfactual conditional, constitutive explanatory, and relevance operators, the resulting space of models for the language is much more complex than intensional models. In order to facilitate the 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 the following operators:
negfor negationwedgefor conjunctionveefor disjunctionrightarrowfor the material conditionalleftrightarrowfor the material biconditionalboxrightfor the must counterfactual conditionalcirclerightfor the might counterfactual conditionalBoxfor necessityDiamondfor possibilityleqfor ground read ‘sufficient for’sqsubseteqfor essence read ‘necessary for’equivfor propositional identity read ‘just is for’preceqfor 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.