Many-Sorted First-Order Logic with Quantification over Inter-Sort Functions

Whereas classical first-order logic provides a formal language for describing structures with a single domain of discourse, structures for many-sorted first-order logic come equipped with multiple domains. This is done explicitly in both the syntax and semantics so as to distinguish between different "sorts" of objects externally. Second-order logic is an extension of first-order logic in which we can quantify over not only individuals but also relations on the universe of arbitrary arity too. There is a tradeoff here in that although second-order logic is more expressive than first-order logic, it is neither complete nor compact. It is hence of natural interest to look for logics that are "in-between" first-order logic and second-order logic and that retain the desirable properties of both.
We will introduce a many-sorted first-order logic that allows for quantification over inter-sort functions. Inter-sort functions are simply relations between sorts, and so this is akin to second-order quantification. However, we only allow inter-sort functions from certain sorts into others. This means that we are only quantifying over a fragment of the possible functions between objects. We will motivate the choice of inter-sort functions via models of basic strategy logic, in which inter-sort functions represent strategies for agents. We will then outline the syntax and semantics, followed by metalogical results such as compactness and completeness.