Doctrinal Semantics of Directed First-Order Logic
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918494245748736 |
|---|---|
| author | Laretto, Andrea Loregian, Fosco Veltri, Niccolò |
| author_facet | Laretto, Andrea Loregian, Fosco Veltri, Niccolò |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_11225 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Doctrinal Semantics of Directed First-Order Logic Laretto, Andrea Loregian, Fosco Veltri, Niccolò Logic in Computer Science Category Theory 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. |
| title | Doctrinal Semantics of Directed First-Order Logic |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2504.11225 |