{"entities":{"Q793723":{"pageid":795571,"ns":120,"title":"Item:Q793723","lastrevid":48707698,"modified":"2026-01-05T16:31:11Z","type":"item","id":"Q793723","labels":{"en":{"language":"en","value":"Set existence property for intuitionistic theories with dependent choice"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3857099"}},"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":"Q793723$E9B16651-21F9-41C8-A751-4FEC99FD6BDC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"048c24315b54b05a839da4803fe890c345e138cf","datavalue":{"value":{"text":"Set existence property for intuitionistic theories with dependent choice","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q793723$1B49CFAE-A32A-47D9-B02E-537B702BFEEA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2fee70f6e59f26b73242cd23a3fccccea462a7dc","datavalue":{"value":"0539.03039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793723$8D2EE238-4C14-45D9-8561-5020FA1AA5CE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5ea9806dc0c6c0d51ae5212427b12fb048ffb288","datavalue":{"value":"10.1016/0168-0072(83)90011-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793723$BEB51AC8-A7E8-4563-B401-3C197A933177","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4db7d460ffc6b3e0069ff40b20b2755df97aa354","datavalue":{"value":{"entity-type":"item","numeric-id":196044,"id":"Q196044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$338F7DB7-45B0-4C7A-9881-681A872D7EFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"183df695ae89db8e2a7647ddbe2de62ff0deb022","datavalue":{"value":{"entity-type":"item","numeric-id":1052316,"id":"Q1052316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$367C5E15-5814-46C8-AC7B-A4DC0AC1B0FD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$2E1496A7-76BB-46CE-9918-3E5000CE79BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0136733d5dd7d9f4d36f24c87a0b8375ae1cb2fd","datavalue":{"value":{"time":"+1983-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":"Q793723$3CBA4B0D-EE69-4171-ACE5-9048CF23DA32","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3035ff8a9696cb63677c985be862fb392a0dc546","datavalue":{"value":"It is known that many intuitionistic theories have the existence property (EP): if a sentence \\(\\exists x.A(x)\\) is provable, then so is A(t) for some closed term t. In the presence of countable choice (CAC) or relativized dependent choice (RDC), however, only fragment of EP regarding the existence of natural numbers (numerical EP) was established [\\textit{J. Myhill}, J. Symb. Logic 40, 347-382 (1975; Zbl 0314.02045)].    The authors first show EP for second order intuitionistic arithmetic with CAC. The proof involves Friedman's extension of the Kleene slash, not in the classical metatheory, but in the 1945-realizability model. Numerical EP is then used. The method readily extends to intuitionistic type theory (resp. intuitionistic Zermelo set theory) with RDC. A modification of the argument establishes the following for intuitionistic ZF set theory formulated with replacement, and with RDC \\((ZFI_ R\\)+RDC). Let TI be the schema of transfinite induction over all (true) primitive recursive well founded binary relations on natural numbers. Let T\\(I^-\\) be the fragment of TI referring to such relations provably well founded in intuitionistic ZF with collection and RDC. Let a sentence \\(\\exists x.A(x)\\) be provable in ZF\\(I_ R\\)+RDC (in ZF\\(I_ R\\)+RDC+TI, resp.). Then there is a formula \\(B(y)\\) with exactly y free, such that \\(\\exists x(A(x)\\wedge \\forall y(y\\in x\\leftrightarrow B(y)))\\) is provable in ZF\\(I_ R\\)+RDC+T\\(I^-\\) (in ZF\\(I_ R\\)+RDC+TI, resp.).","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$B9D775F0-B90D-4BDC-BFD4-C2C18412F56D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793723$9AE6777D-D970-4FCD-B5FE-64E1B93AB455","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"960038531306b6850f13586fdbf5093241061485","datavalue":{"value":"3857099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793723$FA45FBFC-E839-4036-B3AD-2F1EB3E6348C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dbb5e6b6fd60a12de84cd884b1ebcd27eb26a87","datavalue":{"value":"Friedman slash","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$7DB18E97-B02E-4644-8404-F88AA1574BC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"59dc69d0521f0be6c639e519b48339bd7290ba7b","datavalue":{"value":"recursive realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$7F29679A-ABD8-4B8E-A2D6-DD2C4FE99181","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20d362ffe83d0c9cef8194f5c98afe3fe5803803","datavalue":{"value":"intuitionistic theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$70F0D960-1B5B-4F5E-9B3E-CD79E79B3255","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"46e827a2f1d9e2ec3bdc3a7ec6d04e64033483bb","datavalue":{"value":"existence property","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$8937EA09-D438-4002-8E2F-62F41B0802AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"10ab4ac6221d10db0f61cf610dd5def513f40201","datavalue":{"value":"countable choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$1A8DEEE5-D5FC-4F45-84EF-800C51E51C2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87c9f2004de3fc2a8c1751b46e78d7822080c356","datavalue":{"value":"relativized dependent choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$CB17D359-D857-4E3B-B1DA-D5759ABF9C74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82ae87d0eae6a4167b32046b42f421f4cab8596c","datavalue":{"value":"second order intuitionistic arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$26291E7F-A28B-4D7A-A21D-B90674D4657E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"486173fdea484958e371bcc478b16d274811d71a","datavalue":{"value":"intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$F7D8283E-804A-401D-BEEC-BBFE5AE50A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"32bfb68e90ec7291903ac81047350550ba78e857","datavalue":{"value":"intuitionistic Zermelo set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$D59077C6-EEFB-4941-B84F-4506376695E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"57e7221db39bf9b3993ac689b6d1bd5044870197","datavalue":{"value":"intuitionistic ZF","type":"string"},"datatype":"string"},"type":"statement","id":"Q793723$CA60CACF-A76D-4E6F-8600-3AFE246755B3","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":"Q793723$1EAB6FCA-C7CE-485B-8A33-D6231015273A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"42f1fd99e239537bc6eacacd795dc2dee20bcd88","datavalue":{"value":"https://doi.org/10.1016/0168-0072(83)90011-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q793723$B9EFA7C4-3E4E-4323-858A-A1E02425DEB6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8724157e5a08e8628628831316d3e2af93723567","datavalue":{"value":"W2074713441","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q793723$F8A1064D-4E45-4E4F-9294-6A1E4B5F0C0D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"889c98b06b71353ead9711d9cef7ccbd6f932035","datavalue":{"value":{"entity-type":"item","numeric-id":3214890,"id":"Q3214890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$E5EC4070-59DE-4193-AB99-483641B1271F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bd72dbbdbb28e49bc58fdcc6d69fc1738d5bbb0","datavalue":{"value":{"entity-type":"item","numeric-id":5552747,"id":"Q5552747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$4B766BCA-04D9-4768-B6B6-EEE21E03C18F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e13325bae56272b4ba305483ee09cc3ad5047e8","datavalue":{"value":{"entity-type":"item","numeric-id":3214891,"id":"Q3214891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$8644F15B-D097-4B13-9F6E-16C2F408DC80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74605135c388db78d4d0ca86dc0cd54881585bea","datavalue":{"value":{"entity-type":"item","numeric-id":4073362,"id":"Q4073362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$5160B3B5-7126-408F-8FF2-30201FAEC84F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q793723$28DDD17C-55FA-44BA-81F5-FFFA546D5D57","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84069e5424d58b66e2c1cc277fb7153e26b1edea","datavalue":{"value":{"entity-type":"item","numeric-id":448335,"id":"Q448335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"796dd1640e9378c06fdef8e57bf43257bd9d8daf","datavalue":{"value":{"amount":"+0.8352411985397339","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":"Q793723$4A22042A-4C2B-409D-B569-0C46E80D08C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd32bf7ba0e3c2dc900409072052fcfc16181055","datavalue":{"value":{"entity-type":"item","numeric-id":5384979,"id":"Q5384979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95f637c80c3ebf90111002a1d525f1384ce2e3ca","datavalue":{"value":{"amount":"+0.7934800982475281","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":"Q793723$B211C383-BD4F-49F5-90E9-09365078B020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"011316d428c9e4011f8c77d6d4d528a075be43f4","datavalue":{"value":{"entity-type":"item","numeric-id":2637709,"id":"Q2637709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e684648787d1aa74ecd6e755bb7296bcb32428a","datavalue":{"value":{"amount":"+0.7835105657577515","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":"Q793723$10D45A65-F4BA-4014-9FC4-568E5095DDAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37761375316c6429f71112a85b1df03507efa51b","datavalue":{"value":{"entity-type":"item","numeric-id":1071017,"id":"Q1071017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8913de8ab5e35945d3d00f3532b43167f53fea9","datavalue":{"value":{"amount":"+0.7834631204605103","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":"Q793723$153130DC-FE55-4918-9D17-7CBBB8EE0BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0ba7bbd700a778f4a57a32b650b5f91617932e9","datavalue":{"value":{"entity-type":"item","numeric-id":4764119,"id":"Q4764119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f59d0c302b29f267c7ba776d200653f49917a0a5","datavalue":{"value":{"amount":"+0.7711775302886963","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":"Q793723$CF657D78-C074-4B79-AFCE-84533437CC2E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:793723","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:793723"}}}}}