{"entities":{"Q1098849":{"pageid":1109601,"ns":120,"title":"Item:Q1098849","lastrevid":66294993,"modified":"2026-04-12T08:53:24Z","type":"item","id":"Q1098849","labels":{"en":{"language":"en","value":"Subcountability under realizability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4037862"}},"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":"Q1098849$ADCD1DB3-5A80-4169-A1FF-8AE0F49636B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"83e015cc7971adeded29ae195b928a66e70ab999","datavalue":{"value":{"text":"Subcountability under realizability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1098849$F4BDDEF2-56B4-46DD-9F7A-451A8F66AB03","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5369e563348c926cf72a9b905e4ec81c7fc48d7c","datavalue":{"value":"0637.03060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$EBDF4B3E-256C-4BD0-B899-D987287DFA93","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32d6e27545f5ff87bd8e85f58155ee9385c69934","datavalue":{"value":{"entity-type":"item","numeric-id":595650,"id":"Q595650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098849$E89D42D3-BA88-4DE0-9A0F-D414AFF9D2D5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1098849$317340EA-B875-4984-A10C-FACD8A66E399","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1098849$9D06006D-8669-4888-B252-DE87FA51FB52","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"05b0cc6b5f59b8fac2873e168b2b0841bcb6240a","datavalue":{"value":"In constructive mathematics, a set a is discrete if it satisfies \\(x,y\\in a\\to x=y\\vee x\\neq y.\\) A set is countable if it is the range of a function on the integers, and subcountable if it is a subset of a countable set. Unlike in classical mathematics, subcountable sets need not be countable; even Baire space might be subcountable (e.g. if Church's thesis CT is true). All known discrete sets are subcountable, and if CT holds so are separable metric spaces. So the problem was raised whether it is consistent to assume (SCDS) all discrete sets are subcountable, or perhaps even the stronger (SCMS) all metric spaces are subcountable. (It is stronger because a discrete set can be given the discrete metric.) The paper shows the consistency of both these principles with intuitionistic ZF set theory IZF. The method is straightforward: the principles turn out to be recursively realized. The proof itself is not quite straightforward, requiring a clever ``reflection'' in which the realizer of \\(x,y\\in a\\to x=y\\vee x\\neq y\\) is shown to contain an object realized to be a ``subcounting function'' of a. (Lemma 2).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$C1226C11-C05F-48C7-9835-5D6D40227A31","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$822B2520-EABA-4E97-A77D-8C40767B01D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$01DD88DE-6978-4B80-9FC4-A614F18E9C59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$A998B89F-2AC0-4168-BAA1-B6571E039A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"933c6ba8322680c85da12d59920a0a8822c2db22","datavalue":{"value":"03E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$DC32F295-935F-4204-A97B-749FB8577A3A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"338604037f585e41da25653a89194cdc3e832515","datavalue":{"value":"4037862","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$C8D9D203-59A4-424D-B347-FBC0EAF704FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5071adeaef862820b8faa822168b8d4b7290b98f","datavalue":{"value":"subcountable sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$204876E3-ABA2-4FE7-A997-CD20DC41D9C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6b86423b5686667f7394bb6da25ec5323abb4a73","datavalue":{"value":"Church's thesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$E9A90004-80F2-4A7D-B959-AA4A33733325","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"23e41453da5646667e60c0340684b001c287b2a5","datavalue":{"value":"discrete sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$A56113D3-52C4-4633-AA44-0C984917DFB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"880958f8426d35e1b206252f9c79a8da7b632921","datavalue":{"value":"metric spaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$26A6ED55-C2F9-495C-96E6-822ABB613C3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f395fea1231e08b3cf6df7859babcb0988b6b22","datavalue":{"value":"intuitionistic ZF set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1098849$EB7FC1FD-7C6C-4887-ABAC-C751E85F8A33","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":"Q1098849$17A2FC87-27D2-4524-B0C0-3BD4E12FDD32","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"03498780b0a5f680d418434c8cfb3a080bb83a91","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1093636613","type":"string"},"datatype":"url"},"type":"statement","id":"Q1098849$F205DD31-BF97-4580-A348-101D2DD8B251","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e9a73abe8544e0d2bcbd0d15ddb4771c63d1de58","datavalue":{"value":"W2025502180","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$346B93B4-CB3E-4C01-9CAF-CC83CA8FD4E0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2273060bf8b312ef05d68ad76008a933220e6d97","datavalue":{"value":"10.1305/NDJFL/1093636613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1098849$84D37D0F-4C68-4A45-B0AD-C526BE3BF5B4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb3c0ceb5b2434d82c104b06e03441dd141e6f60","datavalue":{"value":{"entity-type":"item","numeric-id":3150911,"id":"Q3150911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"009cafc74bad9b6ebdbc1eff4448e87befabc39e","datavalue":{"value":{"amount":"+0.870773","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$595E1CE4-DD72-447D-8246-3B7B9B4AFF9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87e5707dfdbc8e7a539919ae38b2c2a8584151d8","datavalue":{"value":{"entity-type":"item","numeric-id":649820,"id":"Q649820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"361da79b240f6e5d628dd331340a38176649185d","datavalue":{"value":{"amount":"+0.8654038","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$3A6E114E-D98D-4D02-829E-7AEFE0738B64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45b6fa8692ad937f1d8a846cdefafddb6b64995b","datavalue":{"value":{"entity-type":"item","numeric-id":456878,"id":"Q456878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"01d4c5722f0a64f49acb94c7102853bef512d3d6","datavalue":{"value":{"amount":"+0.8642508","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$D8246ABA-FC89-4F65-9BF2-4718A2AC2B87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ca8f59e15862a5666cfce84c1e704311eb47f81","datavalue":{"value":{"entity-type":"item","numeric-id":2040533,"id":"Q2040533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d9093ad1fc8737af73f49227b5422dd0941d0ff","datavalue":{"value":{"amount":"+0.86188924","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$386A3B1D-B7CC-4F39-8D15-6AE27B054711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0664e71bd49a431bedb92c8908580a5051c14f94","datavalue":{"value":{"entity-type":"item","numeric-id":4787498,"id":"Q4787498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e2dba7fef04230ad8967633f7c846ff5faea3a7d","datavalue":{"value":{"amount":"+0.856687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$36AAEADE-4519-4908-9AE0-4FF705968A07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cee338357dc9e1c64d263b2312d47423ef7a7762","datavalue":{"value":{"entity-type":"item","numeric-id":3137318,"id":"Q3137318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3c72183fe87782b1d691f8e8e2d4d2240340ac1","datavalue":{"value":{"amount":"+0.8564196","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$2C6E5781-A9C0-44F1-B6A3-EF7FE4C0B6B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73cc4b94c0832cdced10e25bad1184198ef1788f","datavalue":{"value":{"entity-type":"item","numeric-id":4819425,"id":"Q4819425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed4d789c04fcddb55bd2c42c61a7f4e8fae38638","datavalue":{"value":{"amount":"+0.8539988","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$7961831B-BB1A-4ABC-B14C-2DF8037B35D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f40c7278bfe50cba94c119e945b5bb3a359f5831","datavalue":{"value":{"entity-type":"item","numeric-id":1094418,"id":"Q1094418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ea6b40cb1efbc9222673384b14f905c6c222729","datavalue":{"value":{"amount":"+0.85344696","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$234630B1-ECF3-4796-938E-B00FC9D8521F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"869981114fea373556666cbbff6b8922437c5436","datavalue":{"value":{"entity-type":"item","numeric-id":5614902,"id":"Q5614902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0eed0eb3b3e0b335abcf4ed12efb2360c4c10604","datavalue":{"value":{"amount":"+0.8519224","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$4BF0EA01-8B4D-4C7B-959B-7266FBF279D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db3b92f986eba7cf38477514b9ce0c7fad97c18f","datavalue":{"value":{"entity-type":"item","numeric-id":5185689,"id":"Q5185689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8da1c6bbe6967e0eae31e79f3d7750d9c8640ec6","datavalue":{"value":{"amount":"+0.8509239","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1098849$21E0B99D-F62B-4FAD-9C17-1928CDFD0EEE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Subcountability under realizability","badges":[]}}}}}