On the crispness of and arithmetic with a bisimulation in a constructive naive set theory
Shunsuke Yatabe · Logic Journal of IGPL · 2013
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.