Open Higher-Order Logic (Long Version)

TL;DR

This paper introduces Open Higher-Order Logic, a novel logical framework that interprets formulas as predicates over open objects, enabling natural reasoning about functional concepts like continuity and differentiability.

Contribution

It extends higher-order logic to open objects, providing different variants including relational and local versions for partial domain properties.

Findings

Enables natural reasoning about functional properties.

Provides multiple variants of open higher-order logic.

Facilitates reasoning in partial domain contexts.

Abstract

We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function's domain of definition.