Saved in:
Bibliographic Details
Main Authors: Berger, Ulrich, Oliva, Paulo
Format: Preprint
Published: 2026
Subjects:
Online Access:https://arxiv.org/abs/2603.04009
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of 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.