Slanted Canonicity of Analytic Inductive Inequalities
Slanted Canonicity of Analytic Inductive Inequalities
复制标题
解析归纳不等式的倾斜规范性
DOI：
10.1145/3460973
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
A. Palmigiano
中科院分区：
文献类型：
--
作者：
Laurent De Rudder;A. Palmigiano
我们证明了一个代数规范性定理正常LE-逻辑的任意签名，在一个广义的设置，其中的非格连接符被解释为操作映射元组的元素给定的格的封闭或开放的元素，其规范的扩展。有趣的是，LE-不等式的句法形式保证了它们在这个广义的设置中的规范性，这与解析归纳不等式的句法形式相一致，这保证了LE-不等式被一个适当的显示演算的解析结构规则等价地捕获。我们表明，这个正规性结果连接和加强了一些最近的正规性结果在两个不同的领域：从属代数，并通过哥德尔-麦肯锡-塔斯基翻译的转移结果。
We prove an algebraic canonicity theorem for normal LE-logics of arbitrary signature, in a generalized setting in which the non-lattice connectives are interpreted as operations mapping tuples of elements of the given lattice to closed or open elements of its canonical extension. Interestingly, the syntactic shape of LE-inequalities which guarantees their canonicity in this generalized setting turns out to coincide with the syntactic shape of analytic inductive inequalities, which guarantees LE-inequalities to be equivalently captured by analytic structural rules of a proper display calculus. We show that this canonicity result connects and strengthens a number of recent canonicity results in two different areas: subordination algebras, and transfer results via Gödel-McKinsey-Tarski translations.