论文标题
在完整的高阶设置中的不合时间推理的完整结果
A Completeness Result for Inequational Reasoning in a Full Higher-Order Setting
论文作者
论文摘要
本文在未经变量的情况下，在预期的语义模型是完整的结构，这是基本类型的预订上的完整类型的层次结构的设置中，获得了无适用术语的不合时性推理的完整结果。语法允许以下规范，即给定符号被解释为单调函数或抗酮函数，或两者兼而有之。有一个自然的五个规则，用于不合时间推理。一个人可以添加变量并添加替代规则，但是我们观察到这种逻辑对于完整的结构是不完整的。这就是为什么本文完整性导致与没有变量的术语有关的原因。由于完整性已经以一般（Henkin）结构的类别而闻名，因此我们对完整的结构感兴趣。我们提出完整的定理。我们的结果不是最佳的，因为我们仅限于完全完整性属性的基础预订：每对元素都有上限和下限。为了补偿，我们向逻辑添加了几个规则。我们还提出了完整性结果的扩展和变化。
This paper obtains a completeness result for inequational reasoning with applicative terms without variables in a setting where the intended semantic models are the full structures, the full type hierarchies over preorders for the base types. The syntax allows for the specification that a given symbol be interpreted as a monotone function, or an antitone function, or both. There is a natural set of five rules for inequational reasoning. One can add variables and also add a substitution rule, but we observe that this logic would be incomplete for full structures. This is why the completeness result in this paper pertains to terms without variables. Since the completeness is already known for the class of general (Henkin) structures, we are interested in full structures. We present a completeness theorem. Our result is not optimal because we restrict to base preorders which have a weak completeness property: every pair of elements has an upper bound and a lower bound. To compensate we add several rules to the logic. We also present extensions and variations of our completeness result.
