{"entities":{"Q1590194":{"pageid":1600934,"ns":120,"title":"Item:Q1590194","lastrevid":47549794,"modified":"2026-01-02T01:28:41Z","type":"item","id":"Q1590194","labels":{"en":{"language":"en","value":"A Diller-Nahm-style functional interpretation of \\(\\text{KP}\\omega\\)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1545484"}},"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":"Q1590194$20472D43-FB7C-47FD-8F03-99F909D86A04","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c67cdde2b4166f6a57b50d88ea6c2a1e59fc1d16","datavalue":{"value":{"text":"A Diller-Nahm-style functional interpretation of \\(\\text{KP}\\omega\\)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1590194$297DBE88-A98F-4D61-8FE0-B2FE297F9ACC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5afadeea4f054e2e5269e5f86d7adb33b2cffec7","datavalue":{"value":"0968.03066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$79F08489-1B24-47E1-BD1E-1644FB9C0324","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":"Q1590194$FFB331FB-641D-4332-BDBE-FD9A6A320434","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":"Q1590194$4AF8B352-61F7-4C3C-9455-CC8A905A2279","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f06e3965919c6d8e09cf93fa6be5852ecd89988e","datavalue":{"value":{"time":"+2001-03-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1590194$1792137E-9E7B-4990-81F9-0ED7C673E75E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"55ca6dcf869473f0a3d4325ce7f7406efc659c1c","datavalue":{"value":"\\(\\text{KP} \\omega\\) stands for Kripke-Platek set theory with infinity. In a previous paper [ibid. 37, No. 3, 199-214 (1998; Zbl 0913.03051)], the author, with \\textit{V. Hartung}, presented a Dialectica functional interpretation of it. But they needed a choice functional, and so the theory interpreted is not \\(\\text{KP} \\omega\\) but \\(\\text{KP} \\omega+\\)(uniform AC). The difficulty lies in set theory itself. For instance, to interprete a simple formula \\(a\\neq\\emptyset \\to\\exists y\\) \\(y\\in a\\), one must produce a term \\(t(a)\\) that verifies \\(t(a)\\in a\\). And so, a choice functional was necessary. In this paper, the author takes a little different route, and gives a ``set'' of terms containing some that verify the formula (rather than a specific term), using bounded quantification as the Diller-Nahm variant did. An object of the lowest type, i.e. type \\(o\\), is a set. To handle a set of higher type \\(\\tau\\), the author uses a pair of functionals, \\(w\\) and \\(X\\), of types \\(o\\to\\tau\\) and \\(o\\), and lets \\(\\{wx/x\\in X\\}\\) be the set. Since the author uses the Shoenfield style interpretation, the translation of \\(\\varphi\\) takes the form \\(\\forall v\\exists wX \\exists x\\in X\\) \\(\\overline \\varphi(v,wx)\\). The main result states: if \\(\\text{KP} \\omega\\vdash \\varphi\\), then there are functional terms \\(w\\) and \\(X[v]\\) such that \\(\\exists x\\in X\\) \\(\\overline\\varphi (v,wx)\\) is valid in the type structure over \\(V\\). The proof is long and complicated, but straightforward. A characterization of \\(\\Sigma\\)-definable set functions of \\(\\text{KP}\\omega\\) is given as a corollary: they are exactly those type 1 functionals that are primitive recursive in \\(x\\mapsto \\omega\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1590194$E0359111-AD42-430D-8DDC-9120834C7ED4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$4C34A06F-5B6E-40EC-B3E3-98D6D62E2DD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$A90851AF-14F7-4713-A6A1-02F9780B3600","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74414636891754d120bf3eb3ae4b2d6570aa26ea","datavalue":{"value":"1545484","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$D45859B3-635F-4A65-841C-2E2F7C0BDDF7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9904bae370afc3918c73be3d23e76d4658c04b11","datavalue":{"value":"Diller-Nahm and Shoenfield style Dialectica interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1590194$15F9F808-F5C7-4A94-9F0A-A29494D69953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f62e8e1c4d7b443eda51b480fa2916beeb866d7","datavalue":{"value":"Kripke-Platek set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1590194$E69E6A10-1A69-443B-8FE3-DE25F87E19DD","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":"Q1590194$B2A1BB28-0278-4F29-9568-74DDC6C6C85B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f0b709604c2b18ce31cbcfe66f95909842cdfb4","datavalue":{"value":"https://doi.org/10.1007/s001530050167","type":"string"},"datatype":"url"},"type":"statement","id":"Q1590194$15DB2D83-68E8-4CB6-9317-A44918795B5D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"add9d0f410b15bc5f34f87f4801c40fdda80c189","datavalue":{"value":"W2079521728","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$97A01ACE-8AB3-4AC2-AF7F-238192870E69","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7c5d3c14d8b3f7108c5974e05719d4ffe1a13029","datavalue":{"value":"10.1007/S001530050167","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1590194$595EE74E-222F-43AA-8754-8F928D5BB427","rank":"normal"}],"P1643":[{"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":"9393e4d06f3f282ad79f1494e3c70276b969ada7","datavalue":{"value":{"amount":"+0.8751106858253479","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":"Q1590194$2F2383B8-B1B6-42F4-9987-42222B41CCDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0be31638e28fc785f354798c17524dc1ea18b75c","datavalue":{"value":{"entity-type":"item","numeric-id":1128184,"id":"Q1128184"},"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":"Q1590194$F10CA71B-EEB2-412C-8974-ED8EC06C4FC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e835cf8f8055c9f07f170d70eba8a448d71316b1","datavalue":{"value":{"entity-type":"item","numeric-id":2836179,"id":"Q2836179"},"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":"Q1590194$98EBCA14-5744-4D93-BD87-A2DCB7E7F248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e0c2655456339de4599b5367a3a8b9920d862a2","datavalue":{"value":{"entity-type":"item","numeric-id":3081643,"id":"Q3081643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17e897b7bc96c0695eac6bd4af2c30120c0b9211","datavalue":{"value":{"amount":"+0.8073143362998962","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":"Q1590194$26437B3E-DE3B-462B-A0EA-31EDADEAC719","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":"b64f198c1bde3804dd3e067630df6fa7c17f6dae","datavalue":{"value":{"amount":"+0.8057724237442017","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":"Q1590194$801F6116-31D3-4F4F-B079-EF82C4AB8C82","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1590194","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1590194"}}}}}