Site home

Make every world true.

Connect possible worlds so every formula holds where it’s written.

Select a world, then its destination. You can also drag.

0Arrows placed

Fewest possible

Your arrows

Arrows will appear here. Select one to remove it.

Finite Kripke models · □ necessity · ◇ possibility Progress stays in this browser.

How to play

Every card is a world. The first line fixes which propositional letters are true there. Add arrows until every formula on every card is true and the relation follows the puzzle’s rule.

◇φ: At least one outgoing arrow leads to a world where φ is true.
□φ: Every outgoing arrow leads to a world where φ is true. This holds if there are no outgoing arrows.
¬φ: φ is false. The symbols ∧, ∨, and → mean “and,” “or,” and “if … then.”

Select a source and a destination by click, tap, or keyboard. Select the same world twice for a loop. You can also drag between worlds. Repeating a connection removes it, and a double arrowhead counts as two arrows. Press Escape to cancel a selection.

Any model that meets the requirements counts. Try to use the fewest arrows shown on the puzzle.