Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Directed First-Order Logic

Andrea Laretto, Fosco Loregian, Niccolò Veltri

TL;DR

This work develops a directed first-order logic that replaces symmetric equality with an asymmetric directed relation interpreted in preorder-like models. It introduces a rigorous polarity/dinaturality system to manage variable occurrences and a left-relative adjoint characterization of directed equality, yielding a precise universal property. Semantics are captured by directed doctrines, enabling soundness and completeness results with the preorder model as a primary instantiation; polarized exponentials and quantifiers extend standard logical connectives under directed constraints. The framework generalizes Lawvere’s equality, positioning directed logic as a robust internal language for directed doctrines, and points to fruitful future work in indexed models, directed spaces, and potential links to directed type theories and concurrent computation.

Abstract

We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as transitions/rewrites between terms, allowing for types to be interpreted as preorders. We then provide a universal property to such "directed equalities" by describing introduction and elimination rules that allows them to be contracted only with certain syntactic restrictions, based on polarity, which do not allow for symmetry to be derived. We give a characterization of such directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint. 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). The semantics of this logic and its system of variances is then captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax.

Directed First-Order Logic

TL;DR

This work develops a directed first-order logic that replaces symmetric equality with an asymmetric directed relation interpreted in preorder-like models. It introduces a rigorous polarity/dinaturality system to manage variable occurrences and a left-relative adjoint characterization of directed equality, yielding a precise universal property. Semantics are captured by directed doctrines, enabling soundness and completeness results with the preorder model as a primary instantiation; polarized exponentials and quantifiers extend standard logical connectives under directed constraints. The framework generalizes Lawvere’s equality, positioning directed logic as a robust internal language for directed doctrines, and points to fruitful future work in indexed models, directed spaces, and potential links to directed type theories and concurrent computation.

Abstract

We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as transitions/rewrites between terms, allowing for types to be interpreted as preorders. We then provide a universal property to such "directed equalities" by describing introduction and elimination rules that allows them to be contracted only with certain syntactic restrictions, based on polarity, which do not allow for symmetry to be derived. We give a characterization of such directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint. 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). The semantics of this logic and its system of variances is then captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax.

Paper Structure

This paper contains 21 sections, 13 theorems, 31 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Variance and dinaturality
  3. Equality, syntactically
  4. Doctrines and equality by Lawvere
  5. Contribution
  6. Related work
  7. Syntax of Directed Logic
  8. (Predicate symbols for formulas.)
  9. (Polarized exponentials.)
  10. (Directed equality.)
  11. (Polarized quantifiers.)
  12. Examples
  13. Doctrinal Semantics
  14. Examples of directed doctrines
  15. Interpretation
  16. ...and 6 more sections

Key Result

Theorem 1

Any variable appearing naturally can be lifted to be dinatural: there is a function on sets of formulas defined by $\mathsf{lift}_{\Theta,\Delta,\Gamma,N,P} := \mathsf{subst}_{\eta_-,\pi_1,\rho_+} : \{ [\Theta,n:N \mid \Delta \mid \Gamma,p:P]\ \varphi \ \mathsf{prop} \} \to \{ [\Theta \mid \Delta,n:

Figures (3)

  • Figure 1: Intuition for syntax and preorder semantics of directed first-order logic.
  • Figure 2: Syntax of directed first-order logic -- types and terms.
  • Figure 5: Derived rules for polarized exponentials.

Theorems & Definitions (47)

  • Definition 1: Signatures and judgements
  • Definition 2: Substitution of terms in formulas
  • Definition 3: Theory
  • Definition 4: Positions in a formula
  • Definition 5: Variance of a position
  • Definition 6: Polarity of a variable
  • Definition 7: Polarized context
  • Remark 1: On admissibility of substitution in entailments
  • Example 1: Derived rules
  • Example 2: Derivations
  • ...and 37 more