{"entities":{"Q1920237":{"pageid":1930979,"ns":120,"title":"Item:Q1920237","lastrevid":47408221,"modified":"2026-01-01T16:11:01Z","type":"item","id":"Q1920237","labels":{"en":{"language":"en","value":"Fragments of HA based on \\(\\Sigma_ 1\\)-induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 918721"}},"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":"Q1920237$DEF147F6-F693-4C60-8A26-244D581AD234","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fd69953e2f3dab8883c3c1ba58103697c3fa5add","datavalue":{"value":{"text":"Fragments of HA based on \\(\\Sigma_ 1\\)-induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1920237$EC81CCD0-3E80-4E88-AFD3-518C6968AF9A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b078c2b552e6ee52cc867714ee899ab35ee75dd4","datavalue":{"value":"0886.03040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$01432162-8897-49F6-A433-7E247974D57C","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":"Q1920237$C17EEED7-3561-467C-8325-BBF117EBFA73","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c52e4811fffdb8f318da6437d640586a60136db4","datavalue":{"value":{"time":"+1996-09-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":"Q1920237$64BD61E2-C859-4BED-AEF3-300F4E798FE1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a0d0329659ec07d172507d55a0cd9a4b8e5a8ccd","datavalue":{"value":"In the first part of this paper we investigate the intuitionistic version \\(iI\\Sigma_1\\) of \\(I\\Sigma_1\\) (in the language of PRA), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for HA and establishes a number of nice properties for \\(iI\\Sigma_1\\), e.g. existence of primitive recursive choice functions. We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is much less powerful intuitionistically than classically: \\(iI \\Sigma_1\\) together with induction over arbitrary prenex formulas is \\(\\Pi_2\\)-conservative over \\(iI \\Pi_2\\). In the second part of the article we study the relation of \\(iI \\Sigma_1\\) to \\(iI \\Pi_1\\) (in the usual arithmetic language). The situation here is markedly different from the classical case in that \\(iI \\Pi_1\\) and \\(iI \\Sigma_1\\) are mutually incomparable, while \\(iI \\Sigma_1\\) is significantly stronger than \\(iI \\Pi_1\\) as far as provably recursive functions are considered: All primitive recursive functions can be proved total in \\(iI \\Sigma_1\\) whereas the provably recursive functions of \\(iI \\Pi_1\\) are all majorized by polynomials over \\(\\mathbb{N}\\). \\(iI \\Pi_1\\) is unusual also in that it lacks closure under Markov's Rule \\(\\text{MR}_{PR}\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$527D5032-7616-4746-BB27-6CCEBBCF72A7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$CB08D567-1507-40FE-94F3-244682F3EBF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6ee9f5484d11a01fb95552e5bea2154ebac0877","datavalue":{"value":"03D20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$97CE9837-A7D9-4CB5-BA33-3C7ABFB8198E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb376507bef486d80cb02bb3cdef5b5fe01bc55f","datavalue":{"value":"918721","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$A5A5EA98-A63F-4DEC-A2B3-6F7006EBD922","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8237e8df99162e5083252faafeaccb5723d90d5","datavalue":{"value":"Kleene's recursive realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$ABA8CCE4-8E79-42C0-BECA-A6329DB0148B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c9f8ee48cf035ffdd93e913368c34fcb9138998","datavalue":{"value":"primitive recursive choice functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$41E3DC08-3212-4888-8934-FEFA9E748467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e138a1670dd04bbc9b0b004a6a70f93eb7587498","datavalue":{"value":"quantifier alternation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$3F8A4D7B-3424-46DA-9E76-1852E898D403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"beb8e031f2b28fbaa8c262e3b135d8604858dd9a","datavalue":{"value":"prenex formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$8FBAD32E-C859-4FFF-ADCE-D2233A3ADBD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"425e268df6c5cb5624c84c71ce4739194b7f0d90","datavalue":{"value":"provably recursive functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$29EAEB29-9373-4279-9128-708F34FAD970","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfa40d769f07cdfbcfc8196efb73c1253dbfc567","datavalue":{"value":"primitive recursive functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920237$8AE5E353-50A3-46B8-8AD0-B1C15D5187BD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6874d9554109ddfa631a3bcceed3f011aa3addc3","datavalue":{"value":{"entity-type":"item","numeric-id":704040,"id":"Q704040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1920237$075FE3ED-BB1C-4D92-B78D-6EE982BB7E09","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":"Q1920237$B5D06F66-7664-4F0E-9005-5A85523D1C05","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"26048cd615acfe068c7b4243322122338471c0ee","datavalue":{"value":"https://doi.org/10.1007/s001530050081","type":"string"},"datatype":"url"},"type":"statement","id":"Q1920237$B623D87A-B013-4DA9-BAF3-561BECC56E40","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc44486f40468aa8e5a91546b0056605effc4f78","datavalue":{"value":"W2050152670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$924EB3FC-C822-4D39-BC03-F66510871075","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a8011dce6d24a3265b18a486620bce93afd4c079","datavalue":{"value":"10.1007/S001530050081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920237$6A78C41A-06FF-433C-9737-1B4A6F181F0E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe0d34b6b41f86704ba74a39eccb5da6b0970ce2","datavalue":{"value":{"entity-type":"item","numeric-id":964451,"id":"Q964451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d463b9e1ddeff6ce1ce8f972eea94461577a289","datavalue":{"value":{"amount":"+0.817447304725647","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":"Q1920237$01797364-B35E-4EBD-8D87-E3978970051F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69f15e5c9ab71465b79d2ec17ced4eba42d5469f","datavalue":{"value":{"entity-type":"item","numeric-id":5486242,"id":"Q5486242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82c257e6fd43bf47f86ccdbca159123bd045c20b","datavalue":{"value":{"amount":"+0.7884852290153503","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":"Q1920237$669BFEC9-124B-4571-AD96-2EF6B420F22C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7661eec4135d4db476187d80408f2e3ee2b19821","datavalue":{"value":{"entity-type":"item","numeric-id":4527922,"id":"Q4527922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae914ba6737389de56cf063bbeade4aec6e2902f","datavalue":{"value":{"amount":"+0.7866871356964111","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":"Q1920237$70C48EC3-AAE9-4AFD-9D83-B09F84EDB473","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"128e0e096ad44d4b1aae609bffaae7b436943236","datavalue":{"value":{"entity-type":"item","numeric-id":720757,"id":"Q720757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"551315e6425cdba9b8b2abd536efe60e04e99ca0","datavalue":{"value":{"amount":"+0.7642155289649963","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":"Q1920237$6175AF1C-7FF5-47D5-B626-B509377BB938","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1920237","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1920237"}}}}}