Test propositional arguments with truth tables and modal arguments with Kripke-frame search. Build and inspect your own Kripke models in the playground.
A full, classical truth table over ¬, ∧, ∨, →, ↔, for propositional logic. It does not work with modal operators □ or ◇.
Click anywhere on the canvas to place a world. Drag worlds to reposition them.
Countermodels is an interactive tool for exploring logical validity through truth tables and Kripke semantics. It was built to make formal logic more concrete by letting users construct models, search for countermodels, and visually inspect the results.
The project supports both classical propositional logic and modal logic. Propositional arguments can be checked with truth-functional tables, while arguments containing □ (necessarily) or ◇ (possibly) are evaluated using Kripke models.
In modal logic, the truth of a formula can depend on which possible worlds are accessible from the current world.
If a world has no accessible worlds, □P is true vacuously: there is no accessible world at which P fails. In contrast, ◇P is false because there is no accessible world at which P holds.
A Kripke frame consists of a set of worlds together with an accessibility relation between them:
A valuation assigns truth values to propositional variables at each world. Together, a frame and a valuation form a Kripke model.
The checker evaluates formulas at a designated evaluation world, w0. For example, □P is true at w0 exactly when P is true at every world accessible from w0.
To show that an argument is invalid, it is enough to find a countermodel: a model in which every premise is true while the conclusion is false.
The Kripke Search tab generates frames satisfying the selected modal system's frame conditions, generates valuations, and checks the resulting models for counterexamples.
The Kripke Search performs an exhaustive search over the finite model space specified by the selected number of worlds.
For example, with four worlds and an unrestricted accessibility relation, there are 16 possible ordered accessibility pairs, so there are:
The search also considers different valuations of the propositional variables at each world. Because both the number of frames and the number of valuations grow rapidly, larger searches can become computationally expensive.
Finding no countermodel within a finite search space does not, by itself, establish validity over every possible Kripke frame. A finite search establishes the result only for the models that were actually searched, unless a separate completeness or finite-model argument justifies the bound.
Different modal systems impose different conditions on the accessibility relation.
These conditions restrict which Kripke frames are included in the search.