From Profiles to Behaviors: What Elimination Leaves in S4

Abstract

Formal elimination can remove a vocabulary without erasing the structure required to sustain its distinctions. In finite propositional S5, complete modal content collapses to an actual valuation and the valuations realized in its accessibility cluster, encouraging a flat, extensional picture of possibility. We show that this collapse is exceptional. Finite S4 models can share their actual and accessible valuations yet differ over the possibilities available from those alternatives. To identify what survives, we replace flat profiles with a coalgebraic tower of finite behavioral types. S5 stabilizes after one modal step, whereas no uniform finite depth classifies all finite S4 behavior. We put the established one-step S4 construction into an explicit deletion form that tests realizability at each depth. Our main synthesis identifies each round of successor refinement with one round of modal generation from a finite Boolean reduction base. At stability, this construction gives both the least modal repair of the base and its largest compatible bisimulation. The repair takes one round on the canonical S5 carrier but has unbounded depth across finite S4 models. A graded Boolean function-ring presentation encodes each finite layer using atomic and successor-behavior coordinates without restoring formula-indexed variables. The residue is neither a complete world graph nor a mere inventory of categorical possibilities, but a language-relative behavioral organization that can be minimized and recoordinatized without being discarded. Formal eliminability therefore demonstrates representational economy, not by itself metaphysical reduction, grounding, or fundamentality.