A Completeness Result for Inequational Reasoning in a Full Higher-Order Setting

TL;DR

This paper proves a completeness theorem for inequational reasoning in a full higher-order setting with variable-free applicative terms over preorders, extending the understanding of semantic models in this context.

Contribution

It establishes a completeness result for a specific logic of inequational reasoning in full structures, including new rules and extensions for variable-free terms.

Findings

Completeness proven for variable-free applicative terms in full structures.

Additional rules introduced to handle weak completeness properties of base preorders.

Extensions and variations of the completeness theorem are also presented.

Abstract

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.