自然演绎的自然性（II）。关于原子多态性的几点注记
The naturality of natural deduction (II). Some remarks on atomic polymorphism
摘要：
在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。
英文摘要：
In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models. In a recent series of papers a different approach to extract proof-theoretic properties of natural deduction derivations was proposed by defining predicative variants of the usual translation, embedding intuitionistic propositional logic into the atomic fragment of System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification provided by parametricity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
