On the crispness of ω and arithmetic with a bisimulation in a constructive naive set theory

Abstract

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. © The Author 2013. Published by Oxford University Press. All rights reserved.