The undecidability of Grišin's set theory (Q1402586): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 04:13, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The undecidability of Grišin's set theory |
scientific article |
Statements
The undecidability of Grišin's set theory (English)
0 references
28 August 2003
0 references
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.
0 references
set theory
0 references
substructural logic
0 references
contraction
0 references
undecidability
0 references
second recursion theorem
0 references
combinatory logic
0 references
cut elimination
0 references
naive comprehension
0 references