= Dense-extension filter semantics
{title2=$F\Vdash\phi$}
For a family of <first-order structures>, take <free filters> on the index set as worlds, ordered by inclusion, and product sequences as parameters. Force an atom when its coordinate truth set belongs to the filter. Conjunction is local, implication and negation quantify over filter extensions, and a disjunction is forced when every extension has a further extension forcing one disjunct. Existence is witnessed by a product sequence and universality holds for all sequences at all extensions. With the <axiom of choice>, induction on formulas identifies forcing with membership of the classical coordinate truth set. Equivalently, every ultrafilter extension satisfies the formula in its <ultraproduct>. Thus the semantics validates classical logic. A local disjunction rule would fail this identification: a set and its complement can both be absent from a free filter, while their union is the whole index set.
Back to article page
