Deduction as Filtering
We have lattices, abstractions, and Galois connections. Now we can talk about what it means to reason within these structures.
Think of logical deduction as filtering out invalid candidates. On the powerset lattice, a deduction function takes a set of possible grids and removes some that violate a constraint — leaving a smaller, more informative set.
Deduction functions can vary in strength. What properties should any reasonable deduction function have?
- Monotone
- Fewer candidates in, fewer candidates out. Deduction shouldn't somehow produce more results from less input.
- Decreasing
- Deduction only removes candidates, never adds them. The result is always ⊑ the input — we only gain information, never lose it.
The best deduction function on the powerset lattice filters out every grid that violates any Sudoku constraint — leaving exactly the valid solutions. This ideal deduction additionally is:
- Idempotent
- Applying it twice gives the same result as once. Once invalid candidates are gone, they're gone.
A function that is monotone, decreasing, and idempotent is called a closure operator (specifically, a lower closure).
Sound abstract deduction
The ideal deduction operates on the expensive concrete lattice. But we've seen that we can work on cheaper abstract lattices instead. Can we define deduction there and still trust the results?
An abstract deduction operator d is sound if it never concludes anything that the ideal concrete deduction d* wouldn't:
In other words: take an abstract state, concretize it, apply d, then abstract back — the result should be at least as precise as what the ideal deduction gives. Whatever d concludes, d* agrees.
Below is the lattice of partial solutions for a puzzle with 7 unknown cells — 128 nodes. Each node is a mini Sudoku grid — colored cells are known, white cells are unknown. The solution sits at the bottom, the starting givens at the top.
Toggle deduction rules to see where each node maps. With no rules enabled, every node maps to itself (self-loops). As you enable rules, the arrows show how deduction pushes each state downward toward the solution: