Model Checker

This project 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:

• 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

The hyperintensional semantics is briefly discussed below with links to further resources.

Screenshot

NOTE: Additional images can be found here.

Installation

Install Python 3 and run the following command in the terminal:

pip install model-checker

The project has the z3-solver as a dependency which should be installed automatically. You can confirm that z3-solver is installed with:

pip show z3-solver

In case the dependency did not install automatically, you can run:

pip install z3-solver

More information can be found here.

Updating

Once installed, you can check the current version of the model-checker with:

model-checker -v

For more information, you can run:

pip show model-checker

To update to the latest version, run:

model-checker -u

To receive updates about new releases, click the "Watch" button at the top right corner of this page.

Instructions

NOTE: Users familiar with the terminal can skip to the Usage instructions below.

Terminal

Open the terminal (e.g., Cmd + Space on MacOS) and list the directories with ls. Navigate to your desired location with cd directory/path/..., replacing 'directory/path/...' accordingly. If you do not know the full path, you can change directory one step at a time, running ls after each move.

Alternatively, if you are on MacOS, write cd followed by a space in the terminal but do not hit return. Then you can open the desired project directory in Finder, dragging the Finder window onto the terminal. This should paste the path into the terminal. You can now hit return to change to the desired directory. If you are in the directory in which the test_file.py exists, you can run model-checker test_file.py without specifying the full (or relative) path to that file. Use the 'up'-arrow key to scroll through past commands, saving time when running the same file multiple times.

Files can be edited with your choice of text editor, e.g., run vim test_file.py to edit the named file in the terminal with Vim (for help, run vimtutor). If you do not want to use Vim (exit with :qa), you might consider using this configuration of NeoVim or VSCodium for working with LaTeX, Markdown, Python, etc., or any other editor you like (e.g., TextEdit on MacOS, or PyCharm).

Usage

To generate a test file run model-checker in the terminal without arguments. Alternatively, run model-checker path/to/test_file.py if the test_file.py already exists. A number of examples are provided in the GitHub repository.

Each file may specify the following inputs where the defaults are specified below:

• A list of zero or more premises that are treated conjunctively: premises = [].
• A list of zero or more conclusions that are treated disjunctively: conclusions = [].
• The number of atomic states to include in each model: N = 3.
• The maximum time in seconds to spend looking for a model: max_time = 1.

Optionally, the user can specify a number of additional settings where defaults are provided below:

• Require all sentence letters to express contingent propositions: contingent_bool = False.
• Require all sentence letters to express propositions with disjoint subject-matters: contingent_bool = False.
• Find a model with the smallest number of atomic elements: optimize_bool = False.
• Print all Z3 constraints or unsatisfiable core constraints: print_constraints_bool = False.
• Show impossible states included in the model: print_impossibe_states_bool = False.
• Prompt the user to append the output to the current file or to a new file: save_bool = False.

Users can override these settings from the command line by including the following flags:

• Include -c to set contingent_bool = True.
• Include -d to set disjoint_bool = True.
• Include -o to set optimize_bool = True.
• Include -p to set print_constraints_bool = True.
• Include -i to set print_impossibe_states_bool = True.
• Include -s to set save_bool = True.

Additional flags have been included in order to manage the package version:

• Include -h to print help information about the package and its usage.
• Include -v to print the installed version number.
• Include -u to upgrade to the latest version.

The following section will sketch the underlying semantics. More information can be found in the GitHub repository as well as in this recent manuscript.

Hyperintensional Semantics

The semantics is hyperintensional insofar as sentences are evaluated at states which may be partial rather than total as in intensional semantic theories. States are modeled by bitvectors of a specified length (e.g., #b00101 has length 5), where state fusion is modeled by the bitwise OR operator |. For instance, #b00101 | #b11001 = #b11101. The atomic states have exactly one occurrence of 1 and the null state has no occurrences of 1. The space of states is finite and closed under fusion.

States are named by lowercase letters in order to print readable countermodels. Fusions are printed using . where a.b is the fusion of the states a and b. A state a is part of a state b just in case a.b = b. States may be either possible or impossible where the null state is required to be possible and every part of a possible state is possible. The states a and b are compatible just in case a.b is possible. A world state is any state that is both possible and includes every compatible state as a part.

Sentences are assigned verifier states and falsifier states where both the verifiers and falsifiers are required to be closed under fusion. A sentence is true at a world state w just in case w includes a verifier for that sentence as a part and false at w just in case w includes a falsifier for that sentence as a part. In order to ensure that sentence letters have at most one truth-value at each world state, a fusion a.b is required to be impossible whenever a is verifier for a sentence letter A and b is a falsifier for A. Additionally, sentence letters are guaranteed to have at least one truth-value at each world state by requiring every possible state to be compatible with either a verifier or falsifier for any sentence letter.

A negated sentence is verified by the falsifiers for the sentence negated and falsified by the verifiers for the sentence negated. A conjunctive sentence is verified by the pairwise fusions of verifiers for the conjuncts and falsified by falsifiers for either of the conjuncts or fusions thereof. A disjunctive sentence is verified by the verifiers for either disjunct or fusions thereof and falsified by pairwise fusions of falsifiers for the disjuncts. Conjunction and disjunction are dual operators obeying the standard idempotence and De Morgan laws. The absorption laws do not hold, nor does conjunction distribute over disjunction, nor vice versa. For a defense of the background theory of hyperintensional propositions, see this paper.

A necessity sentence Box A is true at a world just in case every world state includes a part that verifies A and a possibility sentence Diamond A is true at a world just in case some world state includes a part that verifies A. Given a world state w and state s, an s-alternative to w is any world state to include as parts both s and a maximal part of w that is compatible with s. A must counterfactual conditional sentences A boxright B is true at a world state w just in case its consequent is true at any s-alternative to w for any verifier s for the antecedent of the counterfactual. A might counterfactual conditional sentences A boxright B is true at a world state w just in case its consequent is true at some s-alternative to w for some verifier s for the antecedent of the counterfactual. The semantic theory for counterfactual conditionals is motivated and further elaborated in this accompanying paper. This account builds on Fine 2012 and Fine2012a.

A grounding sentence A leq B may be read 'A is sufficient for B' and an essence sentence A sqsubseteq B may be read 'A is necessary for B'. A propositional identity sentence A equiv B may be read 'A just is for B'. A relevance sentence A preceq B may be read 'A is wholly relevant to B'. The semantics for ground requires every verifier for the antecedent to be a verifier for the consequent, any fusion of a falsifier for the antecedent and consequent to be a falsifier for the consequent, and any falsifier for the consequent to have a part that falsifies the antecedent. The semantics for essence requires every fusion of a verifier for the antecedent and consequent to be a verifier for the consequent, any verifier for the consequent must have a part that verifies the antecedent, and every falsifier for the antecedent to be a falsifier for the consequent. The semantics for propositional identity requires the two arguments to have the same verifiers and falsifiers. The semantics for relevance requires any fusion of verifiers for the antecedent and consequent to be a verifier for the consequent and, similarly, any fusion of falsifiers for the antecedent and consequent to be a falsifier for the consequent. Whereas the first three constitutive operators are interdefinable, relevance is definable in terms of the other constitutive operators but not vice versa:

• A leq B := neg A sqsubseteq neg B := (A vee B) equiv B.
• A sqsubseteq B := neg A leq neg B := (A wedge B) equiv B.
• A equiv B := (A leq B) wedge (B leq A) := (A sqsubseteq B) wedge (B sqsubseteq A).
• A preceq B := (A wedge B) leq B := (A vee B) sqsubseteq B.

Instead of a Boolean lattice as in extensional and intensional semantics theories, the space of hyperintensional propositions forms a non-interlaced bilattice as described in this paper, building on Fine 2017.

Code Architecture

Conclusions are negated and added to a list which includes the premises. The sentences in the list are then tokenized and converted to lists in prefix form so that the operator is the first entry. Each prefix sentence is then passed to the semantics which evaluates that sentence at a designated world, returning a corresponding Z3 constraint. These constraints are then combined with a number of frame constraints and added to a Z3 solver. Z3 looks for a model, returning the unsatisfiable core constraints if none is found. Otherwise, the elements of the model is stored in a class, drawing on these elements to print an appropriate output. Settings are provided to include the Z3 constraints in the printed output, as well as prompting the user to save the output in a new file.