zbMATH — the first resource for mathematics

The undecidability of Grišin’s set theory. (English) Zbl 1039.03040
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.

03E70 Nonclassical and second-order set theories
03D35 Undecidability and degrees of sets of sentences
03B40 Combinatory logic and lambda calculus
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F05 Cut-elimination and normal-form theorems
Full Text: DOI