Constructive proofs for the standard translation of many-sorted to unsorted predicate logic
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909051307163648 |
|---|---|
| author | Oddsson, Hrafn Valtýr |
| author_facet | Oddsson, Hrafn Valtýr |
| contents | It is well known that many-sorted logic can be reduced to unsorted first-order logic by adding predicates for each sort, relativizing quantifiers to these predicates, and adding appropriate axioms governing their behavior. Existing constructive proofs for the correctness of this translation break down when the many-sorted language includes equality and the unsorted target calculus includes the usual rules/axioms for equality. We give an elementary proof in the form of an effective procedure that closes this gap. As an application, we give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic.
We also give a new proof for a claim made by Herbrand in his 1930 dissertation that, in the equality-free case, a sentence is derivable in many-sorted logic iff it is derivable in unsorted logic. Our proof avoids the heavy machinery of later proofs by Schmidt and Wang. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_18216 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Constructive proofs for the standard translation of many-sorted to unsorted predicate logic Oddsson, Hrafn Valtýr Logic 03F25 (Primary), 03F03, 03B10, 03B20, 03B16 (Secondary) It is well known that many-sorted logic can be reduced to unsorted first-order logic by adding predicates for each sort, relativizing quantifiers to these predicates, and adding appropriate axioms governing their behavior. Existing constructive proofs for the correctness of this translation break down when the many-sorted language includes equality and the unsorted target calculus includes the usual rules/axioms for equality. We give an elementary proof in the form of an effective procedure that closes this gap. As an application, we give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic. We also give a new proof for a claim made by Herbrand in his 1930 dissertation that, in the equality-free case, a sentence is derivable in many-sorted logic iff it is derivable in unsorted logic. Our proof avoids the heavy machinery of later proofs by Schmidt and Wang. |
| title | Constructive proofs for the standard translation of many-sorted to unsorted predicate logic |
| topic | Logic 03F25 (Primary), 03F03, 03B10, 03B20, 03B16 (Secondary) |
| url | https://arxiv.org/abs/2603.18216 |