统一可实现性解释
Uniform Realizability Interpretations
AI总结：
本文提出统一可实现性框架，统一并泛化逻辑中各种可实现性解释，重点处理原子公式和量词，兼顾经典与现代变体。
摘要：
本文介绍了一种新的统一可实现性框架，该框架统一并泛化了逻辑中各种可实现性解释，特别是着重于原子公式和量词的处理。传统的可实现性解释（如克里贝尔的数可实现性）要求存在性量词有显式的见证者。相比之下，新的方法，如第一作者的统一直觉算术、非标准算术的赫尔伯朗可实现性，或在"经典"算术的可实现性中，某些量词被统一处理。所提出的统一可实现性概念抽象了这些差异，通过给定的原子公式处理方式参数化解释，兼顾经典和现代变体。该方法通过几种直觉算术的可实现性解释进行了说明。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
