{"entities":{"Q2910991":{"pageid":2921716,"ns":120,"title":"Item:Q2910991","lastrevid":84974063,"modified":"2026-06-03T05:23:43Z","type":"item","id":"Q2910991","labels":{"en":{"language":"en","value":"On Spector's bar recursion"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6081355"}},"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":"Q2910991$A5BC2EAE-1F93-44AB-8DD9-1C20116CCC71","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b0f5e2ad7cbac18a42d25ae4a369ba6f0037ba66","datavalue":{"value":{"text":"On Spector's bar recursion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2910991$58AC3C9B-7B11-4862-A1DD-3FAE263BE502","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c2f11a57c1684605835e25b127197227f90367f","datavalue":{"value":"1251.03066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$D3983769-FB55-43FE-B499-75C945ABBCA5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"392bef464532f1fb6c9d97acd60a5df3e0795638","datavalue":{"value":{"time":"+2012-09-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2910991$57812AE1-C9D6-4DF3-8343-BE7096A1283F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$CCBC5DF8-1B9F-4042-A1B2-A5AF1E5C7EB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$F6370038-0694-4DBA-B874-E04C251E8C4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$222ABB51-D017-440E-A894-945A0A773DEF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4ccccee8c3915e0a560739430cbf030c28d2ba9c","datavalue":{"value":"6081355","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$B8D96952-210C-462A-8F48-B05888371ADC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9afc28f285882597daf0d20a75393d45884ee988","datavalue":{"value":"Spector's bar recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q2910991$98DB381D-0995-4A4B-9A91-FA2ADFC069EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b7331feef51f3c076fa12088fad6aa1615da1ee","datavalue":{"value":"selection functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2910991$A5EBBCE2-EF24-49F5-B9A2-5B13104D110B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2fd2c0b58e8812a21e86c41ee51775c8f0b09501","datavalue":{"value":"T-definability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2910991$73F67AF7-7BA7-4327-8119-75EA4A8C6E94","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":"Q2910991$5FF13D91-7CA9-420A-B88C-C214680F90EF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b1384b381ca6229c70a0ff61a7d604b1fd200f64","datavalue":{"value":"https://doi.org/10.1002/malq.201100106","type":"string"},"datatype":"url"},"type":"statement","id":"Q2910991$6D7BC72D-C12C-4970-9236-5AA64EA62C84","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"30a193b5bf40e892846a28c056f6df35e33b3765","datavalue":{"value":"W1965352021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$67E34001-EC89-441A-863B-D46B62A1EA6F","rank":"normal"}],"P223":[{"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":"Q2910991$358F2D9F-15E3-4E65-B884-104168DF69DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d2d5cf70957811b3c1a72086f7c66b724e20b4a","datavalue":{"value":{"entity-type":"item","numeric-id":3559969,"id":"Q3559969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$4506971E-983E-43C5-94C7-C7382E99DBE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70de28c5744e3d74f5cb50c3c7187b1579dc8426","datavalue":{"value":{"entity-type":"item","numeric-id":3104817,"id":"Q3104817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$6963F151-DEE0-458C-8495-D2C49F572097","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d357a47c04e8c031646a6927518ecdcc37982e0","datavalue":{"value":{"entity-type":"item","numeric-id":3262780,"id":"Q3262780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$588356BF-3690-4CCF-BD32-7E51C671721F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed487916d3cdc9c48e6c95427874ba546cc872ae","datavalue":{"value":{"entity-type":"item","numeric-id":5545953,"id":"Q5545953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$137F34EE-8D7E-4304-B1FA-CE1CB646EC94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52ade55e2c6c484c833d7e5a2d3940069198c8b4","datavalue":{"value":{"entity-type":"item","numeric-id":3912574,"id":"Q3912574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$48759235-D2F7-4DF4-B31F-6C9B6A29A92D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77765a4477c55f314baec87f180c178599579624","datavalue":{"value":{"entity-type":"item","numeric-id":4948521,"id":"Q4948521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$515CD943-E6F1-4FB8-9E74-638ADB31D6C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e73cbdc4f532ed72bacdc9e85f4929b162897095","datavalue":{"value":{"entity-type":"item","numeric-id":5450521,"id":"Q5450521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$86C0DCE9-1A98-4900-AE78-D37F6337D5A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e173e3f88a53b33fbc52906169cfc40c731fbc22","datavalue":{"value":{"entity-type":"item","numeric-id":2560813,"id":"Q2560813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$1E3E3B36-A64A-43D4-8607-3FBBF90AEDC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9969e44e74a4ddcb9248ec285f5a1c9f4cf96634","datavalue":{"value":{"entity-type":"item","numeric-id":5613181,"id":"Q5613181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$BD835794-15F6-49C9-94D8-7473F7A10082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5684a36bec92b21620fadc7675826463b2988db","datavalue":{"value":{"entity-type":"item","numeric-id":3870893,"id":"Q3870893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$176305A5-D298-4109-B477-97D15893260D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dac56f2072a3893c756d692707c0c07bfe6e585","datavalue":{"value":{"entity-type":"item","numeric-id":5519134,"id":"Q5519134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$77BDCF0F-9E1A-421A-8DC2-203D4E994106","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":"Q2910991$63AF0FB9-3F96-4554-86BA-7EEE4A75CF05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"59b449850b5b692906ab23c3bed750a6e64235a0","datavalue":{"value":"10.1002/MALQ.201100106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2910991$FA488AEA-219A-471F-8263-2F7C45C20F4B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"68cefe03c91c7bc1481d1ede29225e2a54af1e4c","datavalue":{"value":{"entity-type":"item","numeric-id":6561648,"id":"Q6561648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$264E5A02-CE7E-4A7D-8B1F-E205F0A79373","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"62de1bd65cd36d521902ae54b685bc4b017ceeca","datavalue":{"value":{"entity-type":"item","numeric-id":408161,"id":"Q408161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$473F18C4-9E8C-446F-A8FA-3DCEE254B76D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"84e68459ec5091ff99e984b785341f0769afc672","datavalue":{"value":{"entity-type":"item","numeric-id":2730251,"id":"Q2730251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$1A6F6452-44FF-4D16-A129-C515C77929A2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b2ea070e416ee0ccef28904c4c5d15ce27d07d35","datavalue":{"value":"Bar recursion, introduced by \\textit{C. Spector} [Proc. Sympos. Pure Math. 5, 1--27 (1962; Zbl 0143.25502)], is a generalized form of recursion. It is the computational analogue of the well-known principle of bar induction, in the same sense as primitive recursion is related with the logical principle of induction.NEWLINENEWLINEIn fact, Spector describes in [loc. cit.] two forms of bar recursion: general bar recursion (inspired in the above analogy with bar induction) and restricted bar recursion (enough to construct a Dialectica realizer for the double negation shift).NEWLINENEWLINEOne may be led to think that restricted bar recursion (rBR) is strictly weaker than general bar recursion (gBR). In the present paper, the authors show that this is not the case. They prove that the restricted and the general forms of bar recursion are inter-definable over system T.NEWLINENEWLINEIt is easy to see that rBR follows from gBR over G\u00f6del's T (see also [\\textit{U. Kohlenbach}, Applied proof theory. Proof interpretations and their use in mathematics. Berlin: Springer (2008; Zbl 1158.03002); \\textit{H. Luckhardt}, Extensional G\u00f6del functional interpretation. A consistency proof of classical analysis. Lect. Notes Math. 306. Berlin-Heidelberg-NewYork: Springer-Verlag (1973; Zbl 0262.02031)]). The main contribution of the paper lies in proving that rBR is in fact as general as gBR. It is accomplished by constructing a term in T + rBR which satisfies (provably in T + rBR) the equation for gBR.NEWLINENEWLINESince these two forms of bar recursion correspond (see [\\textit{M. Escard\u00f3} and \\textit{P. Oliva}, Lect. Notes Comput. Sci. 6158, 141--150 (2010; Zbl 1251.03073)]) to the (explicitly controlled) iterated products of selection functions and quantifiers, we can conclude that this iterated product of selection functions is T-equivalent to the corresponding iterated product of quantifiers.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2910991$7A28486A-170B-40F6-BD04-52F6369D74A9","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"15a5be954de63b9a09120e92802adc210813c3df","datavalue":{"value":{"entity-type":"item","numeric-id":424544,"id":"Q424544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2910991$AC94C148-FB6C-4701-A539-B8760A84A0BD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b6b28e81522e997b721e65f3f0bfdbea783f7f9","datavalue":{"value":{"entity-type":"item","numeric-id":5251356,"id":"Q5251356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18fc628c79e51328470ea644effc518172a32057","datavalue":{"value":{"amount":"+0.8302168846130371","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":"Q2910991$67DC9EF7-A5C3-4A71-9141-A3690891B8D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b792d1ab353f6d7574557eba90ec430d3792b90","datavalue":{"value":{"entity-type":"item","numeric-id":5898840,"id":"Q5898840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ba8f7cc611f3fb792c526d6516fe304aea84545","datavalue":{"value":{"amount":"+0.809991717338562","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":"Q2910991$73F2A588-1174-42F8-BB4C-3F185BE9A2C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37b47cf82ef6f4afa58ebc91b7702bdba05b8837","datavalue":{"value":{"entity-type":"item","numeric-id":515562,"id":"Q515562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4abb5fc6f388c8cfbc6548cc9296b1180eaa44a5","datavalue":{"value":{"amount":"+0.8028551340103149","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":"Q2910991$26CBAE22-09E2-499D-9F6E-77F8B86AF4CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ced790569a69b64d50e7536f6e53d0921d97af0","datavalue":{"value":{"entity-type":"item","numeric-id":5211057,"id":"Q5211057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9781d99f4097a4832a762cd8e9818fdd3025d7ba","datavalue":{"value":{"amount":"+0.7971306443214417","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":"Q2910991$155A3371-EA95-4B26-AFB3-C7B1F79C7D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af5955716d3e538dd02f0b7403e1b04485cacb55","datavalue":{"value":{"entity-type":"item","numeric-id":1115867,"id":"Q1115867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96f39372945e94bc0c00a4c84adb485364507e7e","datavalue":{"value":{"amount":"+0.7890745997428894","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":"Q2910991$A8332EDF-0480-4286-8B19-FC1CA400B98E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On Spector's bar recursion","badges":[]}}}}}