A few possible worlds. One actual world. Find the right modality.
Use every operator to make the formula true at w₀. Stack operators to nest them.
Each circle is a world. Its labels list exactly the propositional atoms true there; unlisted atoms are false. The mint circle, w₀, is the actual world.
◇φ is true if φ holds at some outgoing neighbor. □φ is true if φ holds at every outgoing neighbor. At a world with no outgoing arrows, □φ is true and ◇φ is false.
Drag your operators to the small carets beneath the formula. Each caret marks the gap just before the symbol to its right; clicking that symbol works too. A slot can hold several operators, read from left to right: □◇p means “at every next world, possibly p.” Operators placed before parentheses apply to the whole parenthesized formula.
You can also select an operator and then click a slot, or use Tab and Enter. Click a placed operator to return it, or drag it to another slot. Esc cancels selection.
¬ means not, ∧ and, ∨ or, and → if…then (false only when its left side is true and its right side false).
Use the exact inventory. A correct answer unlocks the next generated level; any valid solution counts. Your progress is saved in this browser.