RCF3:通过闭包的映射代码解释
RCF3: Map-Code Interpretation via Closure
摘要:
对于具有高阶对象的(最小)算术理论,即(最小)笛卡尔闭算术理论--具有相应的闭求值--我们在这里将来自[A,B]的代码映射到这些映射“本身”中,作为hom-Objects B^A中的元素(“名称”)。解释(族)使用泛对象U_n的链,一个用于相对于对象的“更高”阶的每个阶层。结合封闭的、公理化的求值,该解释族给出了代码自求值。通过通常的对角线方法,RICHARD的二律背反可以在最小高阶内形式化(笛卡尔封闭)算术理论,并产生这种方式的不一致性,其所有的扩展,特别是集合论的ZF,基本理论的FREYD所考虑的具有自然数对象的(高阶)拓扑,以及LAMBEK和SCOTT所考虑的具有NNO的笛卡尔闭范畴理论。
英文摘要:
For a (minimal) Arithmetical theory with higher Order Objects, i.e. a (minimal) Cartesian closed arithmetical theory -- coming as such with the corresponding closed evaluation -- we interprete here map codes, out of [A,B] say,into these maps "themselves", coming as elements ("names") within hom-Objects B^A. The interpretation (family) uses a Chain of Universal Objects U_n, one for each Order stratum with respect to "higher" Order of the Objects. Combined with closed, axiomatic evaluation, this interpretation family gives code-self-evaluation. Via the usual diagonal argument, Antinomie RICHARD then can be formalised within minimal higher Order (Cartesian closed) arithmetical theory, and yields this way inconsistency for all of its extensions, in particular for set theories as ZF, of the Elementary Theory of (higher Order) Topoi with Natural Numbers Object as considered by FREYD, as well as already for the Theory of Cartesian Closed Categories with NNO considered by LAMBEK and SCOTT.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。