自然演绎的自然性（II）：关于原子多态的一些评注
逻辑
2021-01-05 v2 计算机科学中的逻辑
摘要
在先前一篇论文（本文为其续篇）中，我们研究了从自然演绎推导到 System F 的蕴含式翻译中提取证明论性质。我们的关键思想是引入一个扩展的 System F 等式理论，在语法层面编码参数化模型中发现的一些性质。在最近的一系列论文中，提出了一种不同的方法，通过定义通常翻译的谓词变体，将直觉主义命题逻辑嵌入 System F 的原子片段，以提取自然演绎推导的证明论性质。在本文中，我们表明该方法可在我们对二阶自然演绎的等式研究中得到一般性解释，并由参数性提供清晰的语义依据。
引用
@article{arxiv.1908.11353,
title = {The naturality of natural deduction (II). Some remarks on atomic polymorphism},
author = {Paolo Pistone and Luca Tranchini and Mattia Petrolo},
journal= {arXiv preprint arXiv:1908.11353},
year = {2021}
}