Skolemization In Intermediate Logics
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912205360857088 |
|---|---|
| author | Baaz, Matthias Gamsakhurdia, Mariami Iemhoff, Rosalie Jalali, Raheleh |
| author_facet | Baaz, Matthias Gamsakhurdia, Mariami Iemhoff, Rosalie Jalali, Raheleh |
| contents | Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_15507 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Skolemization In Intermediate Logics Baaz, Matthias Gamsakhurdia, Mariami Iemhoff, Rosalie Jalali, Raheleh Logic in Computer Science Logic Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics. |
| title | Skolemization In Intermediate Logics |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2501.15507 |