On the crispness of omega and arithmetic with a bisimulation in a constructive naive set theory
On the crispness of omega and arithmetic with a bisimulation in a constructive naive set theory
复制标题
论构造性朴素集合论中欧米伽和互模拟算术的清晰性
DOI：
10.1093/jigpal/jzt045
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Shunsuke YATABE
中科院分区：
文献类型：
--
作者：
Yatabe;S.;Shunsuke YATABE
我们证明了ω的简洁性在FLew中的构造性朴素集合论CONS中是不可证明的。在证明中，我们利用不动点定理构造了一个循环定义的对象固定点，即后继函数的不动点。
We show that the crispness of ω is not provable in a constructive naive set theory CONS in FLew∀, intuitionistic predicate logic minus the contraction rule. In the proof, we construct a circularly defined object fix, a fixed point of the successor function suc, by using a fixed-point theorem.