Doctrinal Semantics of Directed First-Order Logic
This work provides a foundational logical framework for directed equality, relevant to category theorists and logicians studying non-symmetric relations.
The authors present a directed first-order logic with an asymmetric notion of equality, formalized via polarities and directed doctrines, and prove its soundness and completeness with respect to categorical semantics and classical preorder semantics.
We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as preorders. The logic is equipped with a precise syntactic system of polarities, inspired by dinaturality, that keeps track of the occurrence of variables (positive/negative/both). We use this to give a characterization of directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint; intuitively, the relativeness is used to capture the syntactic restriction that avoids symmetry of equality. The semantics of this logic and its system of variances is captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax. Moreover, we prove that the classical fragment of our directed logic is complete with respect to a standard semantics in preorders.