{"entities":{"Q1902734":{"pageid":1913476,"ns":120,"title":"Item:Q1902734","lastrevid":69239736,"modified":"2026-04-13T05:41:25Z","type":"item","id":"Q1902734","labels":{"en":{"language":"en","value":"Axiom ``collection'' independence of ``DC'' principle in intuitionistic set theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 819974"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1902734$06F74A50-A5F4-4194-B845-B43272153A92","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dde0e66fe04c53c5168fc247cb5d2d24e4b43054","datavalue":{"value":{"text":"Axiom ``collection'' independence of ``DC'' principle in intuitionistic set theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1902734$02281A47-2942-4AEC-AE2E-9BA1E935492B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1a068fd25b22cb187a21988080461cbf137424b7","datavalue":{"value":"0835.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1902734$8B19C9AD-AAC8-4F56-8933-506016382BD9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1e48636b5fa08c10ac39bb80920a584977fb9124","datavalue":{"value":{"entity-type":"item","numeric-id":869789,"id":"Q869789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1902734$57931E8D-1AAF-4F70-844B-FEB08A3B371E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"62318960435ff4e0b6f0bda102e1b989b0fc569e","datavalue":{"value":{"entity-type":"item","numeric-id":268929,"id":"Q268929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1902734$CCD2BA4B-F977-45C0-BF0D-E656E736995E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"825562d8f2afae6a37dc432bafc88c050ff424bd","datavalue":{"value":{"time":"+1995-12-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1902734$13F699C5-4409-434B-BD15-1C28E9BD21C3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7ae116bacfd4ca3854b31a84205a20933ca20b83","datavalue":{"value":"Let \\(\\text{ZFI}_2\\) be the set theory with intuitionistic logic, with two sorts of variables (natural numbers and sets), and including a complete family of set-theoretic axioms (exact formulation is given by the author in Dokl. Akad. Nauk SSSR 252, 1070-1074 (1980; Zbl 0482.03026)). In that paper we obtained a model where ``collection'' and ``DC'' (double complement) are true. Let us cite the precise formulation of ``DC'' in the language of \\(\\text{ZFI}_2\\):  \\[ \\forall a \\exists x \\bigl[ \\forall n (\\neg \\neg n \\in a \\leftrightarrow n \\in x) \\wedge \\forall u( \\neg \\neg u \\in a \\leftrightarrow u \\in x) \\bigr] \\]  (here \\(n\\) is a variable on the natural numbers, and the other ones on sets). It is clear that \\(\\text{ZF} \\vdash \\text{DC}\\). Let us make an effort to weaken \\(\\text{ZFI}_2\\) by means of replacement of the axiom ``collection'' by the axiom of substitution. From the intuitionistic standpoint, the deducibility \\(\\text{ZFI}_2\\) -- ``collection'' + substitution \\(\\vdash\\) ``collection'' is no longer valid [see \\textit{H. M. Friedman} and \\textit{A. \u0160\u010dedrov}, Adv. Math. 57, 1-13 (1985; Zbl 0585.03025)]. It is also clear that \\(\\text{ZFI}_2\\) -- ``collection'' + substitution + ``DC'' is consistent with respect to ZF. There arises the question: whether the scheme ``collection'' remains not deducible in this theory? Here we give the answer and prove the following result concerning the one-sorted theory: if we add ``DC'' to the theory from \\textit{J. Myhill}'s paper in Lect. Notes Math. 337, 206-231 (1973; Zbl 0272.02039), then the obtained theory is completely existential. This fact yields (by virtue of the result of Friedman and \u0160\u010dedrov [loc. cit.]) a positive answer to the formulated question.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$C93C2026-A4A3-4720-AD10-DA9371BB7F31","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1902734$2B89F2DA-1252-4CF8-93F5-B113B5CF5511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"933c6ba8322680c85da12d59920a0a8822c2db22","datavalue":{"value":"03E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1902734$05707370-4354-4F81-843B-B8B51B0CDB07","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a418061098d89080903d195c66d8e3de3d689ef6","datavalue":{"value":"819974","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1902734$8EEA45E4-A06A-4D3D-898A-BD7BE68CD705","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e1a96ed6ffe2ea3d9e59077ea94ebf582551c14","datavalue":{"value":"independence","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$F97D087E-F388-4475-A0CC-C7DEA89FAB6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"193e9e18264a324630ab056534b18c56c3a0c0c0","datavalue":{"value":"intuitionistic set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$7CE24793-246C-43FA-AC86-DF2F57A23A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d847e8d66c5335787475c5f735a6125922fd901e","datavalue":{"value":"double complement","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$C6CBBBB0-4270-4D36-ACF5-3C9F278ED0B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0b6f552ad2fb8ffae357dc6404c3ebb617e5d87","datavalue":{"value":"collection","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$0E91FDDC-4BD1-4CA7-8255-821258D8900D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"765ab1d5379755eb3e4e5d30a0f6d93a0512b558","datavalue":{"value":"substitution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1902734$2B965329-28F1-487B-B7B5-87F94496A079","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1902734$7E5FA28B-991C-4F0D-80BB-6334E2A35807","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c955910df1e90339be147d08c85627d286bf298","datavalue":{"value":{"entity-type":"item","numeric-id":4268417,"id":"Q4268417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cba4a6fe78733b7d2cfe5768a3660fce26b1e441","datavalue":{"value":{"amount":"+0.8539028167724609","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1902734$7DAF139C-0710-46B7-A710-5D09369B83E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77651a83d13f3dd6bd7395e0e1def5d8d0d19ab3","datavalue":{"value":{"entity-type":"item","numeric-id":793723,"id":"Q793723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cba4a6fe78733b7d2cfe5768a3660fce26b1e441","datavalue":{"value":{"amount":"+0.8539028167724609","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1902734$75FFB3D9-8BFF-4F65-BE44-9CEB8A7454E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b554ef460af5f433863514f1135c1a067618d64","datavalue":{"value":{"entity-type":"item","numeric-id":722147,"id":"Q722147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88e000ad4c6b833f0077f4c06b191b12e3479145","datavalue":{"value":{"amount":"+0.8265091180801392","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1902734$EEA53B8E-CBB2-4EA0-B5E2-9F142764763A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8664d2a613545814340c2173b7516c3df588afa8","datavalue":{"value":{"entity-type":"item","numeric-id":3710522,"id":"Q3710522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c01735a562b9cebe5c72cec1ebd36ba043ba2af","datavalue":{"value":{"amount":"+0.8160863518714905","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1902734$7F1B9585-254B-423C-AE52-13E3BBD447F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ef7ea52f73b9da4b1c104d639ddbaab6352b115","datavalue":{"value":{"entity-type":"item","numeric-id":5396961,"id":"Q5396961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90d5c13298430eb642ad6611173e8ecac90543dd","datavalue":{"value":{"amount":"+0.7838154435157776","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1902734$E8D7B82A-4062-4DC8-80D9-33496E400057","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Axiom ``collection'' independence of ``DC'' principle in intuitionistic set theory","badges":[]}}}}}