{"entities":{"Q1121882":{"pageid":1132631,"ns":120,"title":"Item:Q1121882","lastrevid":66814524,"modified":"2026-04-12T13:02:42Z","type":"item","id":"Q1121882","labels":{"en":{"language":"en","value":"An interpretation of intuitionistic analysis with restricted transfinite inductive definitions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4104950"}},"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":"Q1121882$AA6B8CA4-8CE6-4D8C-991B-99D20EDB583C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3ae2a0bc8da971c36b24b05c34e0b1b641f7933c","datavalue":{"value":{"text":"An interpretation of intuitionistic analysis with restricted transfinite inductive definitions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1121882$F541A836-ECD8-429C-B058-B4133FB73C31","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ba04d66b8fdbe49c3a662d79ecca556ceed0c64d","datavalue":{"value":"0675.03037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1121882$51348674-928A-4918-83AA-69CBC7581720","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e3301a6b980c5e366145dcc00594aa89b08fc93","datavalue":{"value":{"entity-type":"item","numeric-id":1058512,"id":"Q1058512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1121882$84A4FD3C-5B62-473E-9485-442B5AF21E10","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4644ee9c6c93e22a4aa2641411a372d7ea43bad8","datavalue":{"value":{"entity-type":"item","numeric-id":180651,"id":"Q180651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1121882$0C194A34-B7E2-445C-BBC7-8D46A178D62E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1121882$05B7259B-91F8-4118-A90D-70158FA1CD87","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9b7a441935668f5550e697f2afcc311adeab2f15","datavalue":{"value":"The article considers a system of intuitionistic analysis S(I), which is characterized by bar induction as well as successive inductive definitions along some accessible orderings. The `admissible' formulas of S(I) are restricted so that the modified realizability (mr-) translation can be consistently applied. The mr-translation of S(I) is then realized in the `two-storied universe of transfinite mechanisms', which is defined in the author's preceding work reviewed above (see Zbl 0675.03036). The universe of such mechanisms is a computational system which constructively interpretes some systems of intuitionistic analysis. The reason why the author investigates systems such as S(I) and the mr- translation is metamathematical interest. That is, S(I) is an (a modest) extension of ASOD, a system in which proof-theory to a certain extent can be formalized, and the mr-translation of the implication matches its proof-theoretical interpretation. A counter-example to the mr-translation of `non-admissible' formulas is given in the end.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1121882$1C17F612-80DE-4A02-87BE-70C97D8E40FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1121882$D7E020F3-B415-41A6-854A-0E9167DF9D5E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cf93b5d43710cadc7e5546cb77f1584aa20870d0","datavalue":{"value":"4104950","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1121882$213EA61A-3E82-4CA9-ACDD-0DE90826EBB1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0762595aba73aeeee9b7820b2b282493be06f1b9","datavalue":{"value":"intuitionistic analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1121882$C57E2C83-38EF-4D85-8155-5B58D8333914","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ecd18eca3fc9713df6a82ddda202d74f024f012","datavalue":{"value":"bar induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1121882$981E5487-CCDA-4BFD-9FE2-4C0A7E954D52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f7236c44e5f2863c81afe436f459f4143006643","datavalue":{"value":"successive inductive definitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1121882$AF876A72-B86C-4BC3-8141-D522DC68279D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dec970d83d5a96d3dc380a53aa87d56ce3bb61b6","datavalue":{"value":"mr-translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1121882$9B255403-6C2A-48A3-BC01-2C8B1D57C66D","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":"Q1121882$C952D710-ED95-4771-B6FE-450EB6BE6039","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d00500923b5214a4d90786420005152cf14b18ad","datavalue":{"value":"https://doi.org/10.21099/tkbjm/1496160832","type":"string"},"datatype":"url"},"type":"statement","id":"Q1121882$94864F86-8C67-40D5-9D12-5FDC4BEABBB9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a39d87bb789a9bcd530f46f6e4af3ec94227d547","datavalue":{"value":"W1691232567","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1121882$BD614427-2681-4B8F-8F25-540C109F48C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f9f56a383e2dfe3a59f0a443e0f3f6064be6fd84","datavalue":{"value":"10.21099/TKBJM/1496160832","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1121882$F5886683-CBE6-4143-8581-FAB77BA75FD1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54c78480b647da916ec4a81a367238985aec48ae","datavalue":{"value":{"entity-type":"item","numeric-id":3312223,"id":"Q3312223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7a22b9fbed8d7dcdbf6749752d1d01e443b6a95","datavalue":{"value":{"amount":"+0.7425152063369751","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":"Q1121882$8BE62522-4D12-4973-81F1-42CC563BFA8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4fe2a6eabce97e0321edb38acf5496eec5606879","datavalue":{"value":{"entity-type":"item","numeric-id":3552398,"id":"Q3552398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd61bc7834df31a255d613b01efad0b82c04d913","datavalue":{"value":{"amount":"+0.7352064847946167","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":"Q1121882$EFD0B03B-8288-4E19-AA5C-A00D6502A095","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e60f00e2433adf6505e02648c246af89ebd9e71f","datavalue":{"value":{"entity-type":"item","numeric-id":4602433,"id":"Q4602433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93ffb362a1462f3ea895ac08b160b5a6a6c188ed","datavalue":{"value":{"amount":"+0.7333974838256836","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":"Q1121882$EA9805E4-11C1-49C6-860A-AB753BA238CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bebb7b78ec98a09784f4ed322a7578ba0e41aabf","datavalue":{"value":{"entity-type":"item","numeric-id":4304621,"id":"Q4304621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60b31b05845347ef4a492f29dae0769daed64bf4","datavalue":{"value":{"amount":"+0.720592737197876","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":"Q1121882$11AD51DF-5320-49E5-BAC8-A7C739435CAE","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":"6443925b4582487ad67bd79cc43ef0c98d68b2ed","datavalue":{"value":{"amount":"+0.7171975374221802","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":"Q1121882$1B6B6D12-E09C-4EAD-9DF0-33FA59AE9E1F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An interpretation of intuitionistic analysis with restricted transfinite inductive definitions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_interpretation_of_intuitionistic_analysis_with_restricted_transfinite_inductive_definitions"}}}}}