Uniform Realizability Interpretations
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915833875267584 |
|---|---|
| author | Berger, Ulrich Oliva, Paulo |
| author_facet | Berger, Ulrich Oliva, Paulo |
| contents | This work introduces a novel framework of uniform realizability that unifies and generalizes various realizability interpretations of logic, particularly focussing on the treatment of atomic formulas and quantifiers. Traditional realizability interpretations (such as Kleene's number realizability) require explicit witnesses for existential quantifiers. In contrast, newer approaches, such as in the first author's uniform Heyting arithmetic, Herbrand realizability of non-standard arithmetic, or in the "classical" realizability of arithmetic, (some) quantifiers, are treated uniformly. The proposed notion of uniform realizability abstracts these differences, parametrising the interpretation by a given treatment of atomic formulas, accounting for both classical and modern variants. The approach is illustrated using several realizability interpretations of Heyting arithmetic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_04009 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Uniform Realizability Interpretations Berger, Ulrich Oliva, Paulo Logic in Computer Science F.4.1 This work introduces a novel framework of uniform realizability that unifies and generalizes various realizability interpretations of logic, particularly focussing on the treatment of atomic formulas and quantifiers. Traditional realizability interpretations (such as Kleene's number realizability) require explicit witnesses for existential quantifiers. In contrast, newer approaches, such as in the first author's uniform Heyting arithmetic, Herbrand realizability of non-standard arithmetic, or in the "classical" realizability of arithmetic, (some) quantifiers, are treated uniformly. The proposed notion of uniform realizability abstracts these differences, parametrising the interpretation by a given treatment of atomic formulas, accounting for both classical and modern variants. The approach is illustrated using several realizability interpretations of Heyting arithmetic. |
| title | Uniform Realizability Interpretations |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2603.04009 |