<一般論文> 循環性を受け入れる : 構成主義における可述性の位置づけの変更とその影響

Abstract

Recently some constructivists try to justify impredicative theories with coinduction which play a very significant role in computer science though it had been thought that predicativity is necessary for constructivity. In this paper we introduce these arguments, by Rathjen and by Coquand, and apply these argument to show a naive set theory CONS in FLew∀, which is intuitionistic logic minus the contraction rule, can be regarded as constructive.