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.

翻译：我们提出了一种带“非对称”有向相等关系的一阶逻辑，该相等关系可视为项之间的重写，允许将类型解释为预序。该逻辑配备了源于对偶自然性的精确极性句法系统，用以追踪变量的出现（正极/负极/两者兼有）。我们利用此系统将有向相等刻画为相对左伴随，推广了Lawvere将相等视为左伴随的思想；直观上，“相对性”用于捕捉避免对称性的句法限制。该逻辑及其方差系统的语义通过有向教义的概念在范畴论框架下被刻画，我们证明了该语义相对于句法的可靠性与完备性。此外，我们证明了该有向逻辑的经典片段在预序标准语义下是完备的。