{"entities":{"Q1820780":{"pageid":1831522,"ns":120,"title":"Item:Q1820780","lastrevid":70909137,"modified":"2026-04-13T18:10:44Z","type":"item","id":"Q1820780","labels":{"en":{"language":"en","value":"Intuitionistically provable recursive well-orderings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3995670"}},"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":"Q1820780$2F9C04AC-E3A5-468D-9958-787A72563978","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5a5b119092d40ec2666e02099e7a681767b4f2bd","datavalue":{"value":{"text":"Intuitionistically provable recursive well-orderings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1820780$D0D09EDC-A2BD-4BF9-92CF-2CBA1B2AEF30","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"204e0efe114784957869a799b542ca5d4683469c","datavalue":{"value":"0615.03046","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$FD3783A5-EF50-48DC-920E-D631ED63FD67","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3eddf205c32851ceac4b68e85a2a991639bc2931","datavalue":{"value":"10.1016/0168-0072(86)90004-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$263E27E2-E9DC-47E6-86F1-1F0CF90679DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4db7d460ffc6b3e0069ff40b20b2755df97aa354","datavalue":{"value":{"entity-type":"item","numeric-id":196044,"id":"Q196044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$4D201430-8304-4692-8478-308B21D598F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"183df695ae89db8e2a7647ddbe2de62ff0deb022","datavalue":{"value":{"entity-type":"item","numeric-id":1052316,"id":"Q1052316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$218461D0-45C3-40A1-BAD8-5E3C25F35CCB","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":"Q1820780$3F163511-3725-457A-9802-988E0E1C3722","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-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":"Q1820780$7EA47EB8-A6EC-41BC-9BB0-032A8591725D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0cb4094b476b9e7ea0b46fde448d5444fb83319a","datavalue":{"value":"The authors extend their result in Adv. Math. 56, 283-294 (1985; Zbl 0585.03031) to a wider class of (formally) intuitionistic systems by means of a different proof. Let TI(P,R), for demonstrably primitive recursive R and a free predicate variable P, express transfinite induction on R applied to P. Then there is a specific arithmetic A independent of R s.t., if TI[P/A] is derivable in any of the systems considered, so is TI itself; thus R is in fact well-founded. The authors stress the striking contrast to the case of classical systems, which was topical 35 years ago. To the reviewer their result suggests so to speak new ''programs'' for (intuitionistic) logic, which has proved unrewarding for its own (foundational) aims, as follows. The formula A above is viewed as a kind of analogue to transcendental numbers \\(\\alpha\\) in algebra, with the - class of - formulae TI(P,R) corresponding to equations, say, E, with variable x (and derivability to validity). Here E holds generally, if E[x/\\(\\alpha\\) ] holds. The ''program'' looks for classes C of formulae F other than TI and some specific \\(A_ c\\) s.t., for F in C, F is derivable provided only \\(F[P/A_ c]\\) is; in the first place for intuitionistic logic, but perhaps also for classical logic (for suitable C). In their opening paragraph the authors say, perhaps fairly, that the (broad) issues of TI in classical arithmetic were discussed (adequately) in the old literature. But the particular results that they state were found by H. Friedman in the late sixties after he had been informed of those issues, and circulated (privately), but apparently not published.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820780$96C0E28C-5F4E-45BC-BEC6-B0DDA6DE5334","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$10B507F8-A45A-459B-AF9E-1536C346CAF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$B0DDA8A3-B88E-4DF1-9BDE-4171B0D7DC82","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7324fd58549abcf0fb54355ba72cf5e8085f9a13","datavalue":{"value":"3995670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$E72608D5-A0CD-4224-865D-2DFE5B83FB9E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b64e6ced348a10e3ce9b1194543991e5a94f6db","datavalue":{"value":"intuitionistic number theory with recursive infinitary rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820780$CAB08850-D5A6-49DC-A317-0C1A7CC6EE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6951b1eb2161cddf940a9d4dff7949bcae6352f","datavalue":{"value":"\\(HA^ *\\)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820780$1D88D984-CFFB-4E4F-8F01-53383CD81D09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8cc87407ab9572d85505f2cace7811c9ecc29db","datavalue":{"value":"transfinite induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820780$E499AE68-D58E-43A0-899E-686D0AEADB57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"029259a2377b5daa81be3f3c51f900ae1ab3ba67","datavalue":{"value":"well-founded","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820780$C5ABC8A5-29E8-4436-AC5B-F814EC654448","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"34c3a346e5e5e392396f93c6af311795a4a09543","datavalue":{"value":{"entity-type":"item","numeric-id":1238802,"id":"Q1238802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$C5D02B90-0B7C-4565-943C-D95307426354","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":"Q1820780$6B27B1D7-B829-442A-860B-9958A27A9B50","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4ce71bf60995f8f1275d9b669e4fd1f560ae1fdb","datavalue":{"value":"https://doi.org/10.1016/0168-0072(86)90004-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1820780$94925FFB-8B58-416A-913B-750EE46FA0D2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"00a89087a0e9211eff5b5a48ee5f1949ce71070e","datavalue":{"value":"W2068211235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820780$B54AA2E5-E7AD-4795-8501-B0DE850B76E6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"20078d69304e2df97ca3f40332c8d92086a6b541","datavalue":{"value":{"entity-type":"item","numeric-id":4179016,"id":"Q4179016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$213DA238-5958-40E6-89A4-8BCC61EB792E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"737af7fd7604b6559f5e67fbb4992a43c64a5893","datavalue":{"value":{"entity-type":"item","numeric-id":1071019,"id":"Q1071019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$EBBB8794-CE32-4D12-9D6A-795E3BB369BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e7e03735b909b53820c703a9da6432b741484a5","datavalue":{"value":{"entity-type":"item","numeric-id":3659778,"id":"Q3659778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$0A4BD8E4-7E1D-4755-9343-8648BD669A30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dec668d27b17236d20c4d0c731e94df29b5e12e","datavalue":{"value":{"entity-type":"item","numeric-id":5519129,"id":"Q5519129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$1CEE5359-2D98-4230-91E7-FB9B3AF086C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"160a2374c05e466369d09ccede54688eb30beecb","datavalue":{"value":{"entity-type":"item","numeric-id":5183475,"id":"Q5183475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820780$A6BFC160-BBEC-4ADC-9E04-0AE8F0E06E2C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8308608f5c03ddfbe324dbce555fb603dd66696","datavalue":{"value":{"entity-type":"item","numeric-id":3801546,"id":"Q3801546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aaab9feca9831941f76f49bc02414a64882db1f4","datavalue":{"value":{"amount":"+0.9072348","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$55A177C2-7053-4101-9E9A-7F26B09BE808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"259b5fd7a0f989fc0d40f257fa5f1477fdb4f3f7","datavalue":{"value":{"entity-type":"item","numeric-id":5055281,"id":"Q5055281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"901f3dc0d0360db5d9b008e588430309a378d8c4","datavalue":{"value":{"amount":"+0.90692747","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$D6D8D2D1-A008-4774-ABC5-9BC2513A9D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9ac4b064bdeaebfca62bec9d5edc1a02ec51329","datavalue":{"value":{"entity-type":"item","numeric-id":2309489,"id":"Q2309489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"286e43ad0a945eb85e73e42c5f9fc66f9b870e0a","datavalue":{"value":{"amount":"+0.9032007","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$98BB1E42-D959-4212-84BC-0D0C0CAA81C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eed61c411ec4b693d6d36608c97770795414f4f1","datavalue":{"value":{"entity-type":"item","numeric-id":1071019,"id":"Q1071019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05fca813088664194e63300bb13ef08079dcf282","datavalue":{"value":{"amount":"+0.90264994","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$73847DDD-4ECD-4082-8225-264FC1BB3082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b7afeb5e6e6cc8d88de254a6cef99665bf629aa","datavalue":{"value":{"entity-type":"item","numeric-id":5403201,"id":"Q5403201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c58764a9c942d465b67d564cbc90477387e5a6a","datavalue":{"value":{"amount":"+0.9013603","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$533312CA-7ABF-45D3-A525-534133290536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de0e85d61448856d340e81ebe43ecf930f018474","datavalue":{"value":{"entity-type":"item","numeric-id":4844236,"id":"Q4844236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f5e6925e09a469a9c816a327e829fb44dbf7656","datavalue":{"value":{"amount":"+0.8956684","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$ECC273BA-3E8E-475F-A8B9-225730F8CED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e39169da5fdef24d5c6efb3a36af7e2cd02ba8d1","datavalue":{"value":{"entity-type":"item","numeric-id":3094183,"id":"Q3094183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"731c9f9707c10ead2eabadcb2147fcb7d40e7c9e","datavalue":{"value":{"amount":"+0.8937579","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$581D1761-DCCF-4352-9DF4-EB281AB8218B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d833b0578279e3cc7f848e4881c7ebadfe22b62","datavalue":{"value":{"entity-type":"item","numeric-id":6080077,"id":"Q6080077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a54453c125863ec8509be54b32ce1ba4b1f6b67","datavalue":{"value":{"amount":"+0.8921126","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$B29CB8BF-6B90-4A28-930C-DBC309C5CD42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51317d764d5d3e054bce179d6a4ce248d0865c8b","datavalue":{"value":{"entity-type":"item","numeric-id":5013902,"id":"Q5013902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9630e4fb02bf48f22fe7d35f72f8c10444a6886d","datavalue":{"value":{"amount":"+0.8899852","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$FA97CC21-F0C1-4818-920F-114C1A2FDFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a749c88e916ba664a0472496251827c9cd968ba2","datavalue":{"value":{"entity-type":"item","numeric-id":5084572,"id":"Q5084572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de9e01d71ecc895098286216e272cbe725b7264a","datavalue":{"value":{"amount":"+0.889232","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1820780$E56D1BC3-5418-48C2-BF91-A6AA2B0B4637","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Intuitionistically provable recursive well-orderings","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Intuitionistically_provable_recursive_well-orderings"}}}}}