 Filtration of a Kripke model

Filtration identifies worlds that force the same formulas in a fixed finite subformula-closed set. With order induced by inclusion of these finite theories, the quotient preserves forcing of every retained formula and has at most $2^n$ worlds for $n$ formulas.