A simple proof of second-order strong normalization with permutative conversions
A simple proof of second-order strong normalization with permutative conversions
复制标题
使用置换转换的二阶强归一化的简单证明
DOI：
10.1016/j.apal.2005.05.009
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
G. Mints
中科院分区：
文献类型：
--
作者：
M. Tatsuta;G. Mints
给出了一阶和二阶直觉自然演绎的强正规化的一个简单而完整的证明，包括析取、一阶存在和置换转换。本文通过可计算性谓词(可约性)和饱和集来遵循Tait-Girard方法。首先建立了一类新的转换集的强规范化，然后对标准转换进行了推导。使用一种新的逻辑解决了析取带来的困难，其中析取被限制在原子公式中。
A simple and complete proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait–Girard approach via computability predicates (reducibility) and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.