The undecidability of Grišin's set theory (Q1402586)

Taking account of the crucial role of contraction in the derivation of Russell's contradiction, Grisin proposed a set theory GS of naive comprehension based on contraction-free logic and showed its consistency by cut elimination. In this paper, the author investigates the system GS in more detail. The main issue is that GS proves a form of the second recursion theorem for predicates, which is applied to an embedding of pure combinatory logic in the system giving rise to the undecidability. Among others, it is shown that the K4-modal extension of GS enjoys Löb's schema. Therefore, the extension of GS by S4-modality in the style of linear logic is not consistent. The author discusses also the so-called Grisin's paradox; naive comprehension is not consistent with extensionality. In fact, GS is shown to be inconsistent with extensionality for the empty set.