非标准函数解释与范畴模型
Nonstandard functional interpretations and categorical models
摘要：
最近，第二作者布里塞伊德和萨法里克介绍了非标准的辩证法，一种功能解释，能够消除非标准算术的熟悉原则的实例-包括溢出，下溢和概括到更高的类型-从证明。我们发现，在一些元理论的假设下，这种解释的属性反映了一阶逻辑在一个建设性的层模型的非标准算术由于Moerdijk，后来由Palmgren开发。在这样做的过程中，我们还得出了一些新的非标准原则之间的联系，并拒绝严格的建构主义的原则。此外，我们引入了迪勒-纳姆解释的一个变体，其中包含两种不同类型的量词（有和没有计算意义），类似于赫内斯特的轻方言解释，并表明人们可以通过削弱计算内容来获得非标准的方言。存在量词--我们称之为herbrandisation的过程。我们还定义了一个建设性的层模型，反映了这种新的功能解释，并表明herbrandisation的过程中有一个明确的意义，这些层模型。
英文摘要：
Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and generalisations to higher types - from proofs. We show that, under few metatheoretical assumptions, the properties of this interpretation are mirrored by first order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren. In doing so, we also draw some new connections between nonstandard principles, and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of the Diller-Nahm interpretion with two different kinds of quantifiers (with and without computational meaning), similar to Hernest's light Dialectica interpretation, and show that one can obtain nonstandard Dialectica from this by weakening the computational content of the existential quantifiers -- a process we call herbrandisation. We also define a constructive sheaf model mirroring this new functional interpretation and show that the process of herbrandisation has a clear meaning in terms of these sheaf models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
