Formula Game¶
Evaluate a closed quantified Boolean formula as a perfect-information contest in which Existential and Universal assign their variables in prefix order and truth is equivalent to Existential having a winning strategy.
Core Idea¶
The Formula Game turns the truth of a closed quantified Boolean formula into a two-player, finite, perfect-information game. Write the formula in prenex form as a sequence of quantifiers followed by a propositional matrix. Moving from left to right, player E chooses the truth value of each existentially quantified variable and player A chooses each universally quantified variable. After every variable is assigned, E wins exactly when the matrix evaluates to true; A wins otherwise.
This game is not merely an analogy. It is an operational semantics for the quantifiers. An existential quantifier asks whether E has some choice that succeeds against the continuation. A universal quantifier asks whether the continuation succeeds for every choice A can make.
Scope of Application¶
Formula Game belongs to mathematical logic, complexity theory, QBF solving, and the teaching of alternation. It is used as the canonical source problem in reductions showing that planning, puzzles, and two-player perfect-information games are PSPACE-hard. The game presentation also explains why QBF models policies and reactive choices: existential decisions can depend on earlier universal uncertainty but not on future moves.
The identity is narrow by design. Broader game semantics extends verifier/falsifier play to first-order, modal, fixed-point, and program logics; those systems have different arenas and winning conditions. This node retains the Boolean domain and closed prefix game.
Clarity¶
For ∀x ∃y (x ↔ y), A chooses x first and E observes that choice before choosing y=x; E has a winning strategy, so the formula is true. For ∃y ∀x (x ↔ y), E must commit to y before seeing x; A chooses the opposite value and wins, so the formula is false. The propositional matrix is the same, but information order reverses the result.
Manages Complexity¶
The game compresses recursive quantifier semantics into a familiar adversarial procedure. Rather than repeatedly expanding ∀ into conjunction and ∃ into disjunction, one can inspect a game tree: E-nodes require some winning child; A-nodes require all children to remain winning for E.
It also provides a reduction interface. A target problem is PSPACE-hard when a formula game can be encoded so that E's choices correspond to one player's moves, A's choices correspond to the opponent or environment, and satisfaction corresponds to reaching a winning target.
Abstract Reasoning¶
Backward induction. Label terminal assignments by the matrix truth value. At an existential node, label true if at least one child is true; at a universal node, label true only if every child is true. The root label is the QBF truth value.
Strategy extraction. At each winning existential node, record a true child. The collection is an E strategy, potentially represented as Boolean functions of preceding universal variables.
Knowledge Transfer¶
The full abstraction transfers among QBF instances, solvers, proof systems, and complexity reductions. Outside these settings, “an existential player versus a universal player” can illuminate adversarial planning, but it is only a literal Formula Game when the choices encode a closed Boolean quantifier prefix and the terminal matrix determines the winner.
The portable residue belongs to quantifier, zero_sum_game, contingent strategy, and alternation. The domain-specific package fixes their precise Boolean-logic coupling.
Relationships to Other Abstractions¶
Current abstraction Formula Game Domain-specific
Parents (2) — more general patterns this builds on
-
Formula Game is a kind of Zero Sum Game Prime
zero_sum_game: truth for E is falsity for A, with no jointly preferred outcome. -
Formula Game is part of Quantifier Prime
quantifier: existential and universal quantifiers allocate control and define branching semantics.
Hierarchy paths (2) — routes to 2 parentless roots
- Formula Game → Zero Sum Game → Game-Theoretic Strategy → Function (Mapping)
- Formula Game → Quantifier → Predicate → Relation
Neighborhood in Abstraction Space¶
Formula Game sits in a sparse region of the domain-specific corpus (87th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Automata, Model Checking & Formal Semantics (10 abstractions)
Nearest neighbors
- Quantum Game Theory — 0.82
- Mixed Strategy Equilibrium — 0.80
- Matching pennies — 0.80
- Subgame Perfect Equilibrium — 0.80
- Computation Tree Logic — 0.79
Computed from structural-signature embeddings · 2026-09-08