基于格的不动点逻辑的建设性规范性
逻辑
2016-03-22 v1
摘要
我们在正规格扩张（normal lattice expansions）的构造性元理论中，证明了两类 -不等式的算法规范性（algorithmic canonicity）。该结果同时推广了 Conradie 和 Craig 基于双直觉双模态语言的 -不等式规范性，以及 Conradie 和 Palmigiano 针对归纳不等式的构造性规范性（限制于正规格扩张以符合页数限制）。除了更高的普遍性，这些脉络的统一理顺了现有的 -公式与不等式规范性处理。特别地，用于此结果的算法 ALBA 的规则与 Conradie 和 Palmigiano 的规则具有完全相同的表述，没有为处理不动点绑定符而添加额外规则。相反，不动点通过针对规则应用的某些限制来考量，这些限制涉及与所应用公式相关的项函数的序论性质（order-theoretic properties）。
引用
@article{arxiv.1603.06547,
title = {Constructive canonicity for lattice-based fixed point logics},
author = {Willem Conradie and Andrew Craig and Alessandra Palmigiano and Zhiguang Zhao},
journal= {arXiv preprint arXiv:1603.06547},
year = {2016}
}
备注
arXiv admin note: text overlap with arXiv:1408.6367