Functorial Frame Logic: Institutions, Indexed Consequence, and Truth-Preserving Translation

Functorial Frame Logic (FFL) is a framework-indexed consequence system for reasoning across contexts in which languages, admissible models, background theories, or criteria of interpretation may vary. Built on institution theory, the framework represents a contextual frame as a signature equipped with a selected model class and a local theory. Cross-frame inference is permitted only through admissible translations that preserve model admissibility, background assumptions, and semantic truth. The associated proof theory combines ordinary local sequent calculi with an explicit transport rule, thereby preventing unlicensed movement of consequences between frames. The paper establishes soundness, completeness from fiberwise completeness, local conservativity, functorial coherence, and a conditional cut-elimination theorem for strict logical translations. It also constructs the Lindenbaum functor and its Grothendieck construction, providing a categorical representation of indexed propositions and cross-frame entailment. Within this framework, objective content is modeled not as an unindexed or frame-free sentence, but as a valid natural family invariant under admissible translations. FFL consequently distinguishes local truth, transportable consequence, and invariant validity without reducing them either to unrestricted relativism or to universal absolutism.