Formal Basis

Status: reference (2026-05-28). Grounds the Edge query language in established logic, to be used as a correctness oracle and completeness checklist — not as an implementation to import. The user-facing surface stays domain-specific (QUERY-LANGUAGE); this doc is the semantics underneath it. Written to support a thorough completeness pass (checklist at the end), to be run after the condition-group engine build lands.

Why this doc

While designing the query grammar we kept re-deriving facts that turn out to be textbook logic — most notably that “eventually A and B” is not the same as “eventually A and eventually B.” Rather than keep rediscovering these by hand, we name the formalism we’re actually in, borrow its semantics and its operator inventory, and use it to check our design for gaps, redundancy, and unsound shortcuts.

We do not adopt a general LTL model-checker or a complex-event- processing engine — that would wreck the single-pass replay performance and the usable surface. Theory as oracle, not as dependency.

The object: a game is a finite trace

A game is a finite sequence of positions, one per ply:

$$\pi = s_0, s_1, \ldots, s_{n-1} \qquad (s_i = \text{the board after ply } i)$$

• A position predicate is an atomic proposition evaluated at a state, parameterized by side: $\llbracket P(\text{side}) \rrbracket(s_i) \in \lbrace \text{true}, \text{false} \rbrace$.
• A header predicate is trace-constant (per game): $\llbracket H \rrbracket(\pi)$, independent of $i$.
• The query asks whether π satisfies a formula; the satisfying games form the result set, handed to a reducer (out of scope — see OUTPUT-MODEL).

This is exactly the setting of Linear Temporal Logic over finite traces (LTLf): finite words over the alphabet of position-valuations.

The layers — and which are “real” logic

1. Atomic — predicates (the PREDICATE-LIBRARY).
2. Propositional — ∧ ∨ ¬ over predicates. Standard boolean logic.
3. Side quantifiers — either / both / neither over {white, black}. Finite first-order quantification = pure propositional macro-expansion — no power beyond layer 2:
   • $\text{either } C \equiv C(\text{white}) \lor C(\text{black})$  ($\exists$)
   • $\text{both } C \equiv C(\text{white}) \land C(\text{black})$  ($\forall$)
   • $\text{neither } C \equiv \lnot C(\text{white}) \land \lnot C(\text{black})$  ($\nexists$)
4. Temporal quantifiers — ever / always / never / streak / then / until / at-ply / … over the ply sequence. The only genuinely new logic: LTLf.
5. Output — the reducer. Not part of the logic; aggregates the satisfying (game, ply) set. See OUTPUT-MODEL.

The side “quantifiers” are sugar; the ply quantifiers are LTLf. The two ∃/∀/∄ families are not the same kind of thing.

Operator dictionary

$\pi, i \models \varphi$ = “trace $\pi$ at position $i$ satisfies $\varphi$.” A condition’s window operator is evaluated at $i = 0$ over the whole trace.

Edge	LTL(f)	semantics	regex over π	notes
ever P	F P	∃ j ≥ i : π,j ⊨ P	.* P .*	eventually
always P	G P	∀ j ≥ i : π,j ⊨ P	P{n} (all states)	globally
never P	¬F P = G¬P	∀ j ≥ i : π,j ⊨ ¬P	(¬P)*	dual of ever
at-ply:k P	Xᵏ P	π,k ⊨ P	—	k = absolute ply
from-ply:k P	bounded F	∃ j ≥ k : π,j ⊨ P	—	ever, j ≥ k
until-ply:k P	bounded F	∃ j ≤ k : π,j ⊨ P	—	ever, j ≤ k
streak:N P	F(P ∧ XP ∧ … ∧ Xᴺ⁻¹P)	∃ j : ∀ 0≤m<N, π,j+m ⊨ P	.* P{N} .*	N consecutive; co-safety
then(P,Q)	F(P ∧ X F Q)	∃ i<j : P@i ∧ Q@j	.* P .* Q .*	ordered
until(P,Q)	P U Q	∃ j≥i: Q@j ∧ ∀ i≤k<j: P@k	P* Q .*	P holds until Q
became P	P ∧ ¬YP	π,i⊨P ∧ (i=0 ∨ π,i-1⊭P)	—	past (rising edge)
ceased P	¬P ∧ YP	π,i⊨¬P ∧ π,i-1⊨P	—	past (falling edge)

(X = next, Y = previous, F = eventually, G = globally, U = until.) Future operators are standard LTLf; became/ceased need one step of past (PLTLf) — one carried bit per predicate.

A full condition (C, S, W) is the two-dimensional quantification [S over sides] [W over plies] C(side, ply) — side expands propositionally, ply is the LTLf modality.

Algebraic laws the planner must respect

Determine which lowerings/fusions are sound (PLANNER):

Does NOT distribute (different queries — must not be fused):

• $F(A \land B) \not\equiv FA \land FB$ — “both together, ever” vs “each ever.” Our simultaneous vs independent AND. The central one.
• $G(A \lor B) \not\equiv GA \lor GB$
• $\text{Streak}(A \land B, N) \not\equiv \text{Streak}(A, N) \land \text{Streak}(B, N)$

Does distribute (safe to fuse):

• $F(A \lor B) \equiv FA \lor FB$ — ever over OR
• $G(A \land B) \equiv GA \land GB$ — always over AND

Duality: $\text{never} \equiv \lnot \text{ever}$, $\text{neither} \equiv \lnot \text{either}$, $G \equiv \lnot F \lnot$, $\nexists \equiv \lnot \exists$; cross-dimension $(C, \text{neither}, \text{ever}) \equiv (C, \text{both}, \text{never})$.

Game-level AND/OR-as-independent is the non-distributed reading by design; push a quantifier through a connective only along the “distributes” lines.

The fragment we deliberately occupy

A flat fragment: one temporal operator per condition, conditions combined by booleans at the game level, side quantifiers expanded, ≤1 step of past.

Why: single forward pass, O(1) state per condition (a counter/flag), early-exit — the replay model. The streaming/co-safety slice of LTLf.

Given up (confirm we don’t need):

• Nested temporal inside one condition (G F P, F G P, nested U) — needs LTLf → DFA (exponential to build, linear to run); not single-pass.
• Unbounded past — only 1-step (transitions) is in.
• Weak-until / releases, unless a use case appears.

Knowing the formalism lets us draw this line deliberately, not by omission.

Equivalent lenses

• Kamp’s theorem: LTL ≡ first-order logic over the linear order of positions ≡ star-free regular expressions over the trace. So streak/then/until are equally “regex over the position stream” (P{5}, P.*Q) — often a more intuitive surface, and a candidate framing for the frontend.
• SQL:2016 MATCH_RECOGNIZE and complex-event-processing engines productize exactly this (match a temporal pattern over an ordered stream with per-row predicates). Useful prior art for surface and evaluation.

References

• Pnueli, The Temporal Logic of Programs (1977) — LTL.
• De Giacomo & Vardi, LTL and LDL on Finite Traces (2013) — LTLf, LTLf→automaton.
• Kamp (1968) — LTL ≡ FO[<]; star-free regular correspondence.
• SQL:2016 row-pattern recognition (MATCH_RECOGNIZE); CEP (e.g. Esper).

Completeness-pass checklist

Run after the condition-group build (#11). Confirm or open a follow-up:

1. Total semantics — every surface operator has an unambiguous entry above?
2. Gaps — missing LTLf operators with chess use? (X/previous, “final ply”, between-ply, weak-until, releases.)
3. Redundancy — any operator derivable from others? (always = streak-all? never = ¬ever? then = restricted until?) Keep an orthogonal core + sugar.
4. Sound lowering — every planner fusion checked against the distributes table; AND defaults to independent, fuses only when F∨ / G∧.
5. Side × window matrix — all S×W combos; (neither,ever) ≡ (both,never) holds.
6. Negative-form eval — neither/never early-exit on first occurrence; positives on first satisfaction. Confirm polarity in code.
7. Edge traces — 0-ply; 1-ply; header-only; sideless pred under side quantifier; streak:N N > length; at-ply:k k ≥ length.
8. Past correctness — became/ceased at ply 0; interaction with streak/then.

Completeness pass — first run (2026-05-28, after the #11 build)

Run against the implemented fragment (engine: streak/ever, always, never, at-ply; sides white/black/either/both/neither; game-level AND). Verified live on the 10.19M-game corpus.

Update (same day): #7 (the ALWAYS ≥1-ply gate) and the #2 easy gaps (from-ply/until-ply/between-ply window bounds) landed right after this run — so #7 is FIXED and those three ops are now BUILT. Condition-level OR/NOT (DNF) since landed too. Remaining #2 gaps: then/until, per-branch headers inside OR-branches. (became/ceased 1-step-past now built — checklist #8 satisfied.)

• #1 total / #3 redundancy / #4 sound lowering — PASS. Implemented ops have unambiguous semantics; the core is orthogonal (always≠streak, then≠until; never=¬ever kept as sugar). No unsound fusion: the engine never fuses across conditions (game-level AND = independent = FA∧FB), and simultaneity exists only within a condition’s composite (F(A∧B)). The F(A∧B) ≢ FA∧FB law therefore holds by construction.
• #5 side×window matrix — PASS (empirical). Duality (C,neither,ever) ≡ (C,both,never) exact (king-castled: 955,532 = 955,532); cross-dimension (either,never) = total − both-ever exact (3,255,047); inclusion-exclusion on white/black/either/both consistent.
• #6 negative-form eval — OPEN (perf). Positives early-exit on first satisfaction ✓. never/neither do not yet early-refute on first occurrence — they scan to game end. Correct but unoptimized. Follow-up: bail a never/neither condition the moment the forbidden event occurs (kills the AND-game early; wins when the event is common).
• #7 edge traces — RESOLVED (ALWAYS gated + 0-ply dropped at index). streak:N>len → unsatisfiable ✓; at-ply:k≥len → no match ✓. But ALWAYS is vacuously true on the ~30,933 zero-ply (aborted) games (LTLf G on the empty trace). Fix: gate ALWAYS on ≥1 evaluated ply, and/or drop 0-ply games at index.
• #8 past — PASS. became/ceased built; Ever(Became(P))==Ever(P) exact; an edge can’t streak:2; prior bit tracked across the ply-range boundary (no spurious boundary edges).
• #2 gaps: from-ply/until-ply/between-ply, became/ceased, and in-engine OR/NOT are now built. Remaining: then(P,Q)/until(P,Q) (binary/ordered temporal — beyond the flat single-window fragment, needs a small per-condition automaton) and per-branch headers inside OR-branches.

Build order: easy gaps (ply bounds) → in-engine OR/NOT → became/ceased → then/until.

Cross-references

• QUERY-LANGUAGE.md — the surface grammar this grounds.
• PREDICATE-LANGUAGE.md — type system + AST.
• PLANNER.md — where sound-lowering applies.
• OUTPUT-MODEL.md — the reduce step.