{"entities":{"Q1706266":{"pageid":1717007,"ns":120,"title":"Item:Q1706266","lastrevid":57489294,"modified":"2026-03-31T03:40:39Z","type":"item","id":"Q1706266","labels":{"en":{"language":"en","value":"Intuitionistic nonstandard bounded modified realisability and functional interpretation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6851799"}},"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":"Q1706266$EE16081D-4484-43E6-88EE-0D4B0EAE59D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c904a0b9566a53b65ba7d8ba2ac91103fc06b020","datavalue":{"value":{"text":"Intuitionistic nonstandard bounded modified realisability and functional interpretation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1706266$359481AD-BF7D-4AEA-9C47-DF346124C39B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"317a4d9768f152210a23ed4d4f93af259d8ad437","datavalue":{"value":"1426.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$DFB1D143-951E-46FD-BBA5-FB8F0CFAFCF0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38d6bea29efcdcc9bcc6fc4eb5432297bea74e4f","datavalue":{"value":{"entity-type":"item","numeric-id":1705750,"id":"Q1705750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$5698E582-8444-437D-BBC2-897300F030CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e86e1216a92c4550f95799f0e9e6b17064108fc7","datavalue":{"value":{"entity-type":"item","numeric-id":361871,"id":"Q361871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$F56BF545-8789-4B37-B992-9DD50ECAAAC3","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":"Q1706266$CB25F64F-B377-4279-9BA4-52D4EEA7CA21","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7b370aaa83f4efe6143e52606b64b18fd663e7c7","datavalue":{"value":{"time":"+2018-03-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1706266$0AAA4616-73FA-412F-B043-6DDFCAD0E3E2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dca2fe24231590fe751d495d42a7a039fb6e392a","datavalue":{"value":"https://arxiv.org/abs/1512.07113","type":"string"},"datatype":"url"},"type":"statement","id":"Q1706266$C523525C-0075-4D37-A852-8214C5A958DE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0fa8995d5e6487822ced9725d727b3b5258823da","datavalue":{"value":"\\textit{F. Ferreira} and \\textit{P. Oliva} [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)] introduced bounded functional interpretation for formulae of arithmetic in all finite types with equality only for the objects of type 0 with special treatment of existential statements: it does not provide precise witnesses but only bounds for the witnesses in the sense of Howard-Bezem strong majorizability. The same idea is used in bounded realizability introduced by \\textit{F. Ferreira} and \\textit{A. Nunes} [J. Symb. Log. 71, No. 1, 329--346 (2006; Zbl 1100.03050)]. Intuitionistic nonstandard arithmetic $\\mathsf{E}\\text{-}\\mathsf{HA}^\\omega_{\\text{st}}$ was introduced by \\textit{B. van den Berg} et al. [Ann. Pure Appl. Logic 163, No. 12, 1962--1994 (2012; Zbl 1270.03121)]. It is an extension of intuitionistic arithmetic in all finite types by adding the predicate $\\mathrm{st}$ and appropriate standardness axioms. The same authors defined variants of realizability and functional intepretation similar to the bounded ones, where a bound is replaced by a finite set containing a witness. In the paper under review, bounded functional interpretation and bounded realizability are transferred to $\\mathsf{E}\\text{-}\\mathsf{HA}^\\omega_{\\mathrm{st}}$ formulae and are used for proving various equiconsistency, conservativity, and independence results.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$A257F1C2-96DD-4520-A5ED-7A1ED0684C6A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b1f73afd33192153e94113807fdc62b87cbaa1ee","datavalue":{"value":{"entity-type":"item","numeric-id":234728,"id":"Q234728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$3B65EA41-FFEF-4A62-9B04-1C1F92A9A6C5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$367501D3-755B-48A2-8318-1428AEA9C1EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$B35AE447-6F03-4AC0-BCC3-371B849AA8B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$51C82836-5019-4A7D-BDDF-32558FA7CD41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0863e8f77401912a1f46a81052ba05901a6c171","datavalue":{"value":"11U10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$9702DB4C-E049-44CC-881A-910378E529E6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"187b2b5cb4ab496acc65ecfc1ad75dd7f13a7d94","datavalue":{"value":"6851799","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$DC7ADAB2-5DFA-416B-ABED-5699097B7EB4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7a416e0b794520b49bf582a85e2ef29f146f045","datavalue":{"value":"intuitionism","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$6EDE7AED-740B-425C-8404-A8256F4B75E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9dcaf5a139b06781aa7ffdacc1a94196c808bb8","datavalue":{"value":"bounded functional interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$2F64A32F-5A3C-4452-8F6D-FE9430ED1004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"766db15f08c08092d28e6c4636643f09ef1af30c","datavalue":{"value":"bounded modified realisability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$CE5863AB-CA87-4F94-8EFD-9B4521B2DC53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b4c94a72fc131d3e634b550c3679a1c2997c8772","datavalue":{"value":"majorisability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$A52EEBB0-FA04-47F6-8E2B-8A5C8C196962","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc0ae92f85a2c0624148c2c26d6bdacf11df2351","datavalue":{"value":"nonstandard arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$2DE2B97C-57F1-4252-8A3D-546D58626237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6c681a96dcccad8e4786bf58b5a108b5b3689fc","datavalue":{"value":"transfer principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1706266$83FC4450-45DD-4FC7-A0C2-11EA51E3AEF9","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":"Q1706266$BF75741C-845C-47E6-935B-51BA37D3E700","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"22c6ae12911d4f2c8d8382741a8eb7b438e0bb28","datavalue":{"value":"W2775216664","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$BB6D9CD3-F971-4BE8-8FA4-06B0FB3A705F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d248cbfc7feae2d5c5e1983acca757ec689a41c2","datavalue":{"value":{"entity-type":"item","numeric-id":1407559,"id":"Q1407559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$C0F49C46-B69E-4719-AC48-BB46E36F0372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aba82a794e7b50f883ca25aef5af8219c4085648","datavalue":{"value":{"entity-type":"item","numeric-id":714729,"id":"Q714729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$0879AC63-5B99-44BB-8F5A-F1489A58AE54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"255ee49ffb6e409a3ee7cd255cf0ba0ce9b8a9ab","datavalue":{"value":{"entity-type":"item","numeric-id":3699687,"id":"Q3699687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$E6B0F102-C8F3-4F1A-BFD9-B0A1D3869B8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3c43ad45aa5b3a97181ec14ca3061a69c8be3de","datavalue":{"value":{"entity-type":"item","numeric-id":1905745,"id":"Q1905745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$34540114-CBA2-4176-B6A3-69B406BAC1C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b802fb943f5e74a55181e7600f8966a96e6cbec4","datavalue":{"value":{"entity-type":"item","numeric-id":5108095,"id":"Q5108095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$8B9F3DC1-AF8A-4BCF-81CF-5D6B3310BE95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4efcd400b3216ec62e853977f51a54bd5d5d9f37","datavalue":{"value":{"entity-type":"item","numeric-id":2344622,"id":"Q2344622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$B9AE25C4-896B-46BA-8F05-69E0DBA82C7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d26e7e48781a52e6dc033fbfd496250fb6f1e60e","datavalue":{"value":{"entity-type":"item","numeric-id":5477639,"id":"Q5477639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$4582DA91-D558-4ECF-AF2F-1D92C4A2D5DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d26b1ef00bc67d2868d77b06ad6b8d2cf11afcb4","datavalue":{"value":{"entity-type":"item","numeric-id":2488269,"id":"Q2488269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$8EF1195B-49C9-47FB-A919-429AF8B7C488","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":"Q1706266$0C1D5D11-90BB-4257-BB02-62E148B70DAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ecd81987eb2b3620646f2d151ff26bdb537b884","datavalue":{"value":{"entity-type":"item","numeric-id":4001935,"id":"Q4001935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$B8065388-7D49-4182-B9D9-AA0B9F93352D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8b13c272f7e0efff584d99603822371efbd61ab","datavalue":{"value":{"entity-type":"item","numeric-id":1891250,"id":"Q1891250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$83BA3DE6-DB2C-4477-ADD6-B23D3AB1AD29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bec2770e1b1bced5acaf1a085e30e72a51ee32bf","datavalue":{"value":{"entity-type":"item","numeric-id":4149449,"id":"Q4149449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$6A8C4345-A2EC-4281-866E-D8C3269E9EB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db2bd7a95e48b5516737702decb40381174ad6e7","datavalue":{"value":{"entity-type":"item","numeric-id":1101109,"id":"Q1101109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1706266$D5E0673E-19F7-4E4D-83F1-BEA89DD57144","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"94caeb804bf15023498ac45bd88f900abdb8156c","datavalue":{"value":"10.1016/J.APAL.2017.12.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1706266$EE4D3A9C-7089-4BBB-82AA-A9DF18905424","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b0971ae14a0042af53c3be105ed8834bdf08b2f","datavalue":{"value":{"entity-type":"item","numeric-id":2344622,"id":"Q2344622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbbf37e5b36d5e5ceecf09e2874552d5df7bbc8d","datavalue":{"value":{"amount":"+0.8580974340438843","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":"Q1706266$534070B2-8F3E-44C5-964B-174544F62EAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c1eca4444bb99a64ff5e45d5c3692d1f030ef28","datavalue":{"value":{"entity-type":"item","numeric-id":424545,"id":"Q424545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4e04306f4210c1925b5d32b94a4d02dee37c97f","datavalue":{"value":{"amount":"+0.8050216436386108","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":"Q1706266$C582CF49-3FD2-403A-988F-03B597D79B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35e68142a32a3a5b269b426f5571e03bcec68080","datavalue":{"value":{"entity-type":"item","numeric-id":714729,"id":"Q714729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58d91be81b3c3f6bc4a2a65db0aec2ec81f8a491","datavalue":{"value":{"amount":"+0.7974210977554321","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":"Q1706266$4DBC57BE-4585-4F1B-B041-07E859E3F5D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f2ca2f7785c5c758f37d5bc6832da68a2049b37","datavalue":{"value":{"entity-type":"item","numeric-id":2488269,"id":"Q2488269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3b46a3143320bbcb7d3d75b87f3bbc09e5c9ff5","datavalue":{"value":{"amount":"+0.793242335319519","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":"Q1706266$1EED13E2-0547-42DB-A3A4-A5CC7176681D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05c0c76694c34ed2d1ebf0a526d75ad1d02f420f","datavalue":{"value":{"entity-type":"item","numeric-id":5477639,"id":"Q5477639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6d8255597c810333ebdf3fb275398124ed844cb","datavalue":{"value":{"amount":"+0.7742159366607666","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":"Q1706266$29AB06D0-DDF1-4A63-B010-F3D40519058A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1706266","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1706266"}}}}}