算法逻辑中的稳定性与悖论

无类型逻辑系统被设计用来一致地处理重要的自指实例。一些一致的无类型系统还具有允许某种一般抽象或概括原理的特征，而该原理在朴素集合论中臭名昭著地导致悖论。由于无类型系统拥有这些特征，并避免了在某些语境下被认为不自然的类型层次，它们有潜力在数学基础、类理论（产生比当前集合论与范畴论中使用的更丰富的类概念）、性质理论、自然语言语义、真值理论与理论计算机科学中发挥重要作用。显然，无类型系统必须以某种方式偏离经典逻辑，但对于使用何种无类型系统以及应允许哪些对经典逻辑的偏离，鲜有共识。我们对无类型逻辑的研究方法是考察一个自然出现的无类型系统，我们相信它在某种意义上可作为最终被证明有用的系统的原型。本文所研究的逻辑称为算法逻辑，关乎涉及算法的某些基本陈述及此类陈述间的算法推理规则。本文研究算法逻辑命题性质。后续论文将证明算法逻辑拥有一个一般抽象原理。