We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part.

翻译：我们提出了一种基于泛代数与高阶抽象GSOS的逻辑谓词系统化方法，从而迈出了迈向逻辑关系统一理论的第一步。首先观察到逻辑谓词是混合变函子上余代数不变量的特例。为支持归纳推理，我们引入给定谓词的局部极大逻辑精化概念，并识别出在该设置下规范存在局部极大逻辑精化的充分条件。最后，通过识别并抽象化高阶GSOS律（特定类）编码系统中逻辑谓词归纳证明的模板化部分，开发了简化此类证明的归纳提升技术。