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的逻辑谓词系统化方法，从而为逻辑关系的统一理论迈出第一步。首先观察到逻辑谓词是混合变元函子上余代数不变量的特例。随后引入给定谓词的局部最大逻辑精化概念以支持归纳推理，并确定了在该整体设定下局部最大逻辑精化规范存在的充分条件。最终发展出up-to归纳技术，通过识别并抽象化系统编码为（特定类别的）高阶GSOS律时的模板化部分，简化基于逻辑谓词的归纳证明。