{"entities":{"Q1128184":{"pageid":1138933,"ns":120,"title":"Item:Q1128184","lastrevid":46717902,"modified":"2025-12-25T11:20:47Z","type":"item","id":"Q1128184","labels":{"en":{"language":"en","value":"A characterization of the \\(\\Sigma_1\\)-definable functions of \\(\\text{KP}\\omega+(\\text{uniform AC})\\)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1187522"}},"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":"Q1128184$C0C7B769-C9E3-4499-A522-B387FAF5BC2F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f0f698ba49386ca8f31a0367d0be8edb63d8c8fd","datavalue":{"value":{"text":"A characterization of the \\(\\Sigma_1\\)-definable functions of \\(\\text{KP}\\omega+(\\text{uniform AC})\\)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1128184$386D908A-12B6-46F6-8D7C-051C73F51E39","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ff7dbe09a992f9ad15224c3746e932259723b266","datavalue":{"value":"0913.03051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$A7614338-A4DD-489D-B373-215BAF92B64F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"79f29d23fbbae73ccd3e56314eab48b3694cf512","datavalue":{"value":{"entity-type":"item","numeric-id":1128181,"id":"Q1128181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1128184$97BB4ED6-E3D5-4764-B786-43FECA87E5D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2cc3352206ac3c3088f10999365c282d6dbfc8bc","datavalue":{"value":{"entity-type":"item","numeric-id":1128182,"id":"Q1128182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1128184$3C179C2A-C455-4E5C-846C-88739217BA05","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1128184$195126D2-5F7B-4C53-BA9A-5FFE2A51A6CD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9a28ca4b86ebb8f9bf05a5bf5a9824f7507a71a8","datavalue":{"value":{"time":"+1998-10-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1128184$700FA4D8-3D95-4ADC-B079-CBCB0212DFCE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6fcca08c748ac42993d77f9957f830d63970e2cd","datavalue":{"value":"\\textit{M. Rathjen} showed [J. Symb. Log. 57, 954-969 (1992; Zbl 0761.03016)]\\ by proof-theoretic means that the set-functions primitive-recursive in \\((x\\mapsto\\omega)\\) are exactly the \\(\\Sigma_1\\)-definable set-functions of KP\\(\\omega\\) with foundation restricted to \\(\\Sigma_1\\)-formulae. The authors of the paper under review were guided by the aim to achieve an analogous result for KP\\(\\omega\\) with full foundation using a G\u00f6del-style [\\textit{K. G\u00f6del}, Dialectica 12, 280-287 (1958; Zbl 0090.01003)]\\ functional interpretation:    (1) The class of \\(\\Sigma_1\\) definable set functions of KP\\(\\omega\\) coincides with the collection of set functionals of type 1 primitive-recursive in \\((x\\mapsto\\omega)\\).    In this paper only a modification of that aim could be established, namely:   (2) The \\(\\Sigma_1\\)-definable set-functions of KP\\(\\omega\\)+(uniform AC) are exactly the set functionals of type 1 primitive recursive in \\((x\\mapsto\\omega)\\) and a fixed choice functional \\(F_C\\) of type 1.   But in the meantime the first author developed a new Diller-Nahm style [\\textit{J. Diller} and \\textit{W. Nahm}, Arch. Math. Logik Grundlagenforsch. 16, 49-66 (1974; Zbl 0277.02006)]\\ translation by which (1) can by shown. Additionally this translation allows a functional interpretation of CZF, Aczel's constructive set theory [\\textit{P. Aczel}, Logic colloquium '77, Stud. Logic Found. Math. 96, 56-66 (1978; Zbl 0481.03035)].    For the proof of (2) a variant of the Shoenfield \\(\\forall\\exists\\)-translation is defined for all formulae of \\({\\mathcal L}+\\{F_C\\}\\) which allows a G\u00f6del-style functional interpretation of KP\\(\\omega\\)+(uniform AC). For the treatment of the bounded \\(\\forall\\)-rule the choice-functional \\(F_C\\) is needed. For the remaining inclusion the computability of the used set functionals is shown by proving informally in KP\\(\\omega \\)+(uniform AC) a suitable Church-Rosser-theorem.   The article under review is carefully written. The proofs are detailed and complete.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1128184$09593C61-EC5C-4A7D-8C2F-B50AE85081C4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2ff25c2e8cc717bb47b0ce37ddc50e1d615f0b7c","datavalue":{"value":{"entity-type":"item","numeric-id":1128183,"id":"Q1128183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1128184$35F3D598-6E03-418E-AF87-F2839B88BCD8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$F1953676-3174-40BD-8EC9-02BEF7BC7ADF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$D8CBC042-E589-48E7-9E9E-0198E65EF163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$BD84574C-6191-4C2C-9FB7-848EA4FF32E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2f1459d5951e049c51abbc0d85c8bd47bc411fa9","datavalue":{"value":"03E25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$38E10A91-526F-4627-AB7D-8349835FE3D6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"59de7604a62a0112852419b445769f7ab7632c79","datavalue":{"value":"1187522","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$737156EE-3337-4626-9A9F-66087BF9BEF6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"492942e689dba58f90096ed1c12c52b0f868caa6","datavalue":{"value":"functional interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1128184$676F5D11-79FC-410F-8D72-7E5914F1B437","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f62e8e1c4d7b443eda51b480fa2916beeb866d7","datavalue":{"value":"Kripke-Platek set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1128184$B60CF47A-01F0-4E8D-AB47-836198E8ABCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c5827bc6422b1277a419f6edbfd20a5a3251b7a","datavalue":{"value":"primitive-recursive set functionals","type":"string"},"datatype":"string"},"type":"statement","id":"Q1128184$6A2BF671-B1D4-4D0A-B633-52F124892B29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dd59d671c70179e50aa218d3fbd15ae36808d8dd","datavalue":{"value":"Church-Rosser theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1128184$381B6B5C-1462-4B23-9BE3-BC8E286FCDF3","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":"Q1128184$A2125624-2145-457D-B963-B52B133C474F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"41b6e70459dbc97313b7e6fdf799cba3d9d04ce5","datavalue":{"value":"https://doi.org/10.1007/s001530050092","type":"string"},"datatype":"url"},"type":"statement","id":"Q1128184$C81E0DD8-66B6-4896-9C36-53B04883D310","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"443eb68fcfc907902ea12692e45fcd6ad1e57fea","datavalue":{"value":"W227809201","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$F31C1DE8-3278-4903-A91C-E3593B63A124","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"016fc1ae7194d25abef22723f8f7edc8beb5da84","datavalue":{"value":"10.1007/S001530050092","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1128184$289AD21A-8E93-4834-B657-0C05B3F1644A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fc7f070aa3946ccf746c1244329e4fa3a2b500a","datavalue":{"value":{"entity-type":"item","numeric-id":1590194,"id":"Q1590194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3158d952d6a141fffd4f17635eb1da567cddae13","datavalue":{"value":{"amount":"+0.8477103114128113","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":"Q1128184$E4A0BF84-5814-4E3D-9196-CED5A8792A94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43a3364d75f1def53d351db53d1753b4448aefbf","datavalue":{"value":{"entity-type":"item","numeric-id":1577478,"id":"Q1577478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb03ed738c30b94af10c9e3652913bbcbd98527a","datavalue":{"value":{"amount":"+0.801286518573761","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":"Q1128184$AED7E09A-4483-4602-88A4-EE79E9A2B283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663a6362854082b09fe2fe423549e8a7671153e5","datavalue":{"value":{"entity-type":"item","numeric-id":4981444,"id":"Q4981444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0211c7756397a77aa953c1faa8e0ffac97308710","datavalue":{"value":{"amount":"+0.793064534664154","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":"Q1128184$A82966E4-10E1-4D56-910F-7A4D1F957957","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1128184","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1128184"}}}}}