{"entities":{"Q946579":{"pageid":948427,"ns":120,"title":"Item:Q946579","lastrevid":42779130,"modified":"2025-07-11T10:02:39Z","type":"item","id":"Q946579","labels":{"en":{"language":"en","value":"Hybrids of the \\({}^ \\times \\)-translation for \\(\\mathsf{CZF}^{\\omega}\\)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5346261"}},"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":"Q946579$27D4F0B7-C7DC-435F-B48B-81954D18B6FF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"adcbfad1bb11094106f88aac669a24499b772557","datavalue":{"value":{"text":"Hybrids of the \\({}^ \\times \\)-translation for \\(\\mathsf{CZF}^{\\omega}\\)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q946579$7257DB62-0804-4DE8-B843-89B6C3D91756","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"92e39d78a81d04ff06f819be0336734c5bf32d21","datavalue":{"value":"1156.03052","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$7E9ED204-17BA-4DE9-9B2A-03DF06F56015","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3721cd985b37e53faf62cde628ee8c7cffc62636","datavalue":{"value":{"entity-type":"item","numeric-id":946578,"id":"Q946578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q946579$01352FB3-3E9D-41B6-8EE7-A58FCAF13CAE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fd9c858b64e538228c66f00c768fd1506ee71010","datavalue":{"value":{"entity-type":"item","numeric-id":124852,"id":"Q124852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q946579$C36D385C-2472-4F80-A2D1-7D58C7A2108A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5974dd87aa4f0aaee17beaa07c015c32b4db7f85","datavalue":{"value":{"time":"+2008-09-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q946579$840559D0-87AE-47F6-B609-61A8DD9AF0EB","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9f0fd26e5b51da3c3c14bf9e0d7726730751ad03","datavalue":{"value":"By means of translation technique, the author investigates admissibility of various rules in \\(\\text{CZF}^\\omega\\) -- constructive ZF in all finite types. All five translations used are in the spirit of G\u00f6del's Dialectica translation. Three are based on realizability. The author's \\({}^ \\times\\)-translation is a modification of \\textit{W. Burr}'s one [cf. Ann. Pure Appl. Logic 104, No.~1--3, 31--73 (2000; Zbl 0959.03043); also, the details of \\(\\text{CZF}^\\omega\\) can be found here], and his \\({}^ {\\times q}\\)-translation is a further variation \u00e0 la \\textit{J. Diller} and \\textit{W. Nahm} [Arch. Math. Logik Grundlagenforsch. 16, 49--66 (1974; Zbl 0277.02006)]. The author investigates five rules: weak axiom of choice, independence of Harrop premises, Markov principle for \\(\\Delta_0\\) formulas, the existence property (EP), and the existence definability (ED). Here, ED claims: if \\(\\vdash\\exists x F(x)\\) then there is a term \\(t\\) (of the same type as \\(x\\)) such that \\(\\vdash F(t)\\). EP is a weaker rule, just saying that there are \\(S\\) and \\(V\\) such that \\(\\vdash S\\neq\\emptyset\\wedge\\forall y\\in S\\,F(Vy)\\). The first four rules are shown to be admissible. Needless to say, one translation can show the admissibility of more than one rule, and one rule can be handled by different translations. The admissibility of (ED) is still unsettled, but the author reduces it to the special case where \\(F\\) is a \\(\\Delta_0\\) formula and \\(x\\), \\(t\\) are of type \\(o\\). He also gives a detailed proof of the interpretation theorem for the \\({}^ {\\times q}\\)-translation: if a formula \\(A\\) is provable, so is \\(A^ {\\times q}\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$9042D8CA-2A6E-4DE9-A30F-D0514597227D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$926AEF60-FE19-4113-95BA-5BB9F65FDE8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$BFF58986-7DD6-41EF-A84E-C5E5E43EC91C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$DEC5A974-29D9-43B3-9985-412A174800F1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4ae37cd0fedce4cca8433ed322a834478d60e3b6","datavalue":{"value":"5346261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$B2DCAD3B-7F70-4D70-9656-362284B90D57","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"492942e689dba58f90096ed1c12c52b0f868caa6","datavalue":{"value":"functional interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$C25F8997-67CE-4444-96CA-37BC2FF01409","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"901914fe530e7ce0a6006efd574fec9ce0f5e885","datavalue":{"value":"admissibility of rules in \\(\\text{CZF}^\\omega\\)","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$0E810180-7790-47D9-9CA0-56A5E274B5F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ba8d809a967de4f70931881b6ceb82308135934","datavalue":{"value":"constructive set theory in all finite types","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$1FC2A1D2-50C1-494F-887C-F29DADF1D6D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c126a6a0aa8a99dd8c3523950bf1c5cd64c53183","datavalue":{"value":"q-hybrids of translations","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$62D5BEE7-BBD1-4BB7-A79D-E345176F86EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"38b650e328394bcd4c620109452554c04d510d51","datavalue":{"value":"modified realisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q946579$456098E8-B6FB-4813-B9A9-A367A78767AB","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":"Q946579$5A5CC86B-7644-4DAB-87F3-0427B2CEFD91","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c18563b2be55e5b7368d788ad5d8812f01db9175","datavalue":{"value":"https://doi.org/10.1016/j.jal.2005.09.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q946579$F27C25FF-20EB-4CE1-AE24-FA94131D8F33","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fed84ce7bafefb4a436ac225fd6357289c7797b7","datavalue":{"value":"W2028764919","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$6C6DA407-A604-4BBE-B434-09A16BF29C1D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"51d3dac9adb980e5335d28029f3d6248bc26dad2","datavalue":{"value":{"entity-type":"item","numeric-id":1577478,"id":"Q1577478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q946579$04F52F0A-7994-4090-A502-E32DD2422D96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"117810964db980ad00f39ab39d43879214724e8d","datavalue":{"value":{"entity-type":"item","numeric-id":4401924,"id":"Q4401924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q946579$3C3E5B91-78F8-4748-8B6B-07186E59AF23","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":"Q946579$E7690F82-ACE5-4928-BE5C-67F955F49CD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"889750e6b63c62516f108fd0d35f770cecc8f256","datavalue":{"value":{"entity-type":"item","numeric-id":1264579,"id":"Q1264579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q946579$761A8629-A56F-4A54-8BDE-E8AE3624004B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"497f4f7d8dcbde989df601e2a2ff5e3e52b9baba","datavalue":{"value":"10.1016/J.JAL.2005.09.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q946579$854D36B6-C6A7-4E49-85CB-0844FA27C46A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae054e847da0e7451a9fb7f00acf415d1c3b68ee","datavalue":{"value":{"entity-type":"item","numeric-id":3367516,"id":"Q3367516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c6782af66854bfcd8bb6fb6053c10f21eabe016","datavalue":{"value":{"amount":"+0.72137845","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$AD55D25B-4F3E-43E3-8110-681F9A4E0A8B","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":"75b964d2e6af173ad7425e36c7ac803995cb6a00","datavalue":{"value":{"amount":"+0.71185154","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$F17897BB-50BE-405B-9A9E-A25CE83ED9ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ec70ff52fc796e00caacfc9a4c85f6c74c9f07a","datavalue":{"value":{"entity-type":"item","numeric-id":5477363,"id":"Q5477363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0ee343225ccc5db855e05048eb68a123aa59433","datavalue":{"value":{"amount":"+0.71146715","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$A40AB72A-BAC0-460F-B563-518D862C7995","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":"f013046e209b8fafac6a69a02371d528fb3a0f1d","datavalue":{"value":{"amount":"+0.70502454","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$B6395BFE-EE44-4B9F-94A6-CCA32520C0E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6e3531ca5baa0e71d970e1f7742f2d4f1bea84d","datavalue":{"value":{"entity-type":"item","numeric-id":2500469,"id":"Q2500469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ecf1a221c5a91cc4b5381f510c9385799020dee","datavalue":{"value":{"amount":"+0.70327055","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$4B58AC61-7BDF-448D-8701-F80E7AEC0020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad14a45e62d2df7c44ea6e92554e954392cabbde","datavalue":{"value":{"entity-type":"item","numeric-id":1372877,"id":"Q1372877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4bcf96d8fdfe0f235ff5675e99111d242df46e6","datavalue":{"value":{"amount":"+0.69270825","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$E8C13BAC-626A-4611-A258-BE06F105E51A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cee89132d7b998afbc83c8c4afa220269b3a2065","datavalue":{"value":{"entity-type":"item","numeric-id":5486250,"id":"Q5486250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2c6b11e5547e0715068164afb0df39f3d48d247","datavalue":{"value":{"amount":"+0.69233817","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$63208A09-E027-4BE2-B5D3-D462DDE959C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc6f16e5d3efa5a65e251568c9079f176d261c98","datavalue":{"value":{"entity-type":"item","numeric-id":6109095,"id":"Q6109095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a464b03ca6c0986f2803722d6566d09dc5d8a66d","datavalue":{"value":{"amount":"+0.69058186","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$14795043-28A2-46D3-A3FA-E06282D98112","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":"7ddf599f58d7b79f0ec0aebcabbdc69e7f615b18","datavalue":{"value":{"amount":"+0.6851465","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$EB9B46EC-55A8-463F-B37A-F28D31E9FE66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f908016c8de4c7ab1dffa9c501c98537f2530e2","datavalue":{"value":{"entity-type":"item","numeric-id":4981438,"id":"Q4981438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"440a258779756c52b3485a32a78ac69ec4d496c3","datavalue":{"value":{"amount":"+0.67871094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q946579$4F2179F3-F831-456A-8B46-A1F744EDF58F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:946579","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:946579"}}}}}