著者

Yatabe S.

出版者

Oxford University Press

雑誌

Logic Journal of IGPL (ISSN:13670751)

巻号頁・発行日

vol.22, no.3, pp.482-493, 2014-06-23

被引用文献数

1

---

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.