The Russell-Prawitz embedding and the atomization of universal instantiation
Logic Journal of the IGPL(2020)
摘要
Given the recent interest in the fragment of system $\mathbf{F}$ where universal instantiation is restricted to atomic formulas, a fragment nowadays named system ${\mathbf{F}}_{\textbf{at}}$, we study directly in system $\mathbf{F}$ new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (i) they hel...
更多查看译文
关键词
Intuitionistic propositional calculus,system F,predicative polymorphism,Russell–Prawitz translation,proof reduction
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要