{"entities":{"Q2743649":{"pageid":2754388,"ns":120,"title":"Item:Q2743649","lastrevid":83064134,"modified":"2026-05-07T05:50:53Z","type":"item","id":"Q2743649","labels":{"en":{"language":"en","value":"Finitary treatment of operator controlled derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1652347"}},"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":"Q2743649$BD91F0A2-2428-410A-BAD6-7D0077867B44","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fe93ae375852ed39f9935eae520b5479f7d4a16b","datavalue":{"value":"0986.03044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$6267664D-F125-4972-9512-995BD7CDAA1E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca3d0fdc4dfe73f15e4cc6198de2fda062014c98","datavalue":{"value":{"entity-type":"item","numeric-id":204229,"id":"Q204229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2743649$2B6599EE-8A3A-4F9E-9915-63028CBE4845","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"89979698039692d8b30dd476805176a82a96347c","datavalue":{"value":{"time":"+2002-06-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2743649$CC086D2D-BB09-4383-B558-69254CD9E2C7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$112D30E0-CAF3-41B8-9C72-454C2125E805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$FE1EF975-C93E-411C-8BBE-F93235075881","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a27e74511e75c8b42da27a94602b73c8283618f9","datavalue":{"value":"1652347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$46B0B2CA-D1DE-4E8F-B933-15D7DCFE7E5D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$D4E59573-3045-4CD0-AAA7-D58BB54B8473","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"664c217a1a00d62effaec670f5656be452525922","datavalue":{"value":"ordinal analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$D6C5D2FE-B2EA-4609-8368-8FAA343E21E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$118DC584-98A6-420A-B5B9-5365A9B0C494","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"425e268df6c5cb5624c84c71ce4739194b7f0d90","datavalue":{"value":"provably recursive functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$08A88D26-BE3F-49EF-BFD9-D27DAF4A63DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d627bb0d41eeb50845a4444ff6f27448eb2d0821","datavalue":{"value":"proof-theoretic analysis of impredicative systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$3FBEB304-836D-46BF-8BC2-373DC73A0E47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0158683270834b0a1ac3fc6a995c32051e4040fa","datavalue":{"value":"admissible set theory with inaccessible universe","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$41163473-440F-4058-9FFD-1117FC358B20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc12d81b4399618115f25f707be934c54c466482","datavalue":{"value":"bounded multifunctions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$E2F6A560-B3D9-4258-A85B-0D76B1723041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6805cd779fb0b2cacd6147aa42cec0eee9b2950","datavalue":{"value":"infinitary proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$7BD7D62C-5274-489E-90AB-4408A4AFBB4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc9634e2c4f95f0ff04acc2068cffb177a1aceca","datavalue":{"value":"ramified set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$B9447CEE-49D4-457F-854E-9033D7C647E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"875f4722c488b3dd9924712f6ea14fa985bcb55b","datavalue":{"value":"ordinal notation system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$2B8AA858-6F1D-42CC-A8DF-3F7D0EF95C2A","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":"Q2743649$44A66ADA-07FB-4D04-BAC8-2F6ECF46E5B7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"677aab2dbfa3698c3fb9c167819320d85efd440a","datavalue":{"value":"W2010485236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$0E134EB3-8B1F-45BA-8896-979202405192","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8a0a30ea237ed752549192ab76f9769b5467c189","datavalue":{"value":"10.1002/1521-3870(200108)47:3%3C363::AID-MALQ363%3E3.0.CO;2-P","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2743649$A285A759-52A6-47E8-94F4-826C60DB2B76","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"86a0c198898ec23b530384ed04d73e4ad27cf2d2","datavalue":{"value":"https://doi.org/10.1002/1521-3870(200108)47:3%3C363::aid-malq363%3E3.0.co;2-p","type":"string"},"datatype":"url"},"type":"statement","id":"Q2743649$2DFAB337-38A5-49ED-94CE-EB09AE5A2579","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"16e7b06eae6f2ced0e9f85423c41d56e13844792","datavalue":{"value":{"text":"Finitary treatment of operator controlled derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2743649$CEE2D83F-E68B-4F2B-ABA9-D2C467905F1C","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":"Q2743649$0193F3C0-10B9-460C-9D52-29CFAC9AAC27","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3618adbcd92afb7bd0e7711a3da717b3f0233e58","datavalue":{"value":"The present paper provides a kind of semantics for the proof-theoretic analysis of impredicative systems, based upon finitary combinatorial techniques. It is part of a research program which started by systematically interpreting Gentzen's finitary reduction steps for first-order arithmetic in terms of \\(\\omega\\)-logic, and it is now applied to the system \\textbf{KPi} of admissible set theory with inaccessible universe (for related works, see the papers by the same author reviewed in Zbl 0887.03043 and Zbl 0795.03078).NEWLINENEWLINENEWLINEThe main result is a theorem classifying the bounded multifunctions from the collection HF of hereditary finite sets with values in HF. It is shown that if \\(z\\) is the set HF, \\(\\phi\\) is a bounded set-theoretic formula and \\textbf{KPi} proves \\(\\forall x \\in z \\exists y \\in z \\phi(x,y)\\), then there exists a function \\(F\\) satisfying the following conditions: (i) \\(F\\) is \\(\\alpha\\)-primitive recursive, for some \\(\\alpha\\) less than the proof-theoretic ordinal \\(\\psi_\\Omega(\\epsilon_{I+1})\\) of \\textbf{KPi} (which is a constructive collapse of the first inaccessible ordinal \\(I\\)); (ii) \\(F\\) is a bounding function for \\(\\phi\\), i.e \\( \\forall n \\in \\omega \\forall x\\in L_n \\exists y \\in L_{F(n)}\\phi(x,y) \\) is true (in the standard interpretation, \\(L_k\\) being the constructible hierarchy up to \\(k\\)). NEWLINENEWLINENEWLINEAfter presenting an infinitary proof system RS\\(^\\infty\\) for ramified set theory, the author introduces the crucial notion of notation system for RS\\(^\\infty\\)-derivations and shows how to build up a family of notation systems (H)\\(_\\delta\\) for RS\\(^\\infty\\)-derivations which are suitably controlled by corresponding ordinal operators H\\(_\\delta\\). In particular, the notation systems are strong enough to represent derivations arising from the embedding of \\textbf{KPi} into ramified set theory and from cut-elimination and collapsing procedures. The constructive treatment of ordinals is based on the so-called \\(\\psi\\)-functions and an associated ordinal notation system OT is laid down. In the final step the bounding functions are effectively read off from notations of cut-free derivations of the required \\(\\Pi^0_2\\)-statements. The paper is technically quite complex and yet carefully and neatly written.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2743649$C44CC75C-A114-430E-A0CF-3026FFCCEA01","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"5634ed46a52c7680a2cf61c8cfb118a9c5e1d936","datavalue":{"value":{"entity-type":"item","numeric-id":588330,"id":"Q588330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2743649$94B15529-B119-4767-9CE2-BB0E23391DF0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57c6e74f0dc692143d060bf08d947a0a68fceff2","datavalue":{"value":{"entity-type":"item","numeric-id":4325775,"id":"Q4325775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d782795da25b46cff776be2e4c78714b725ea45e","datavalue":{"value":{"amount":"+0.7927099466323853","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":"Q2743649$0D14C80D-2CE0-43EA-B2BA-6C3C7A7B51AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cf20a72c87c85cf6f836cdd293a539c83e95161","datavalue":{"value":{"entity-type":"item","numeric-id":1332853,"id":"Q1332853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67d25005512e22a9bd70f4d896800124fb8a79b7","datavalue":{"value":{"amount":"+0.7874252200126648","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":"Q2743649$CC1DE37D-BFE0-44A2-803A-3E425925BC76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b27448d4f8c467ed365162749d9f337a8916ee07","datavalue":{"value":{"entity-type":"item","numeric-id":3416113,"id":"Q3416113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0c5477d24b025a72a793bace0b8bd1852be8734","datavalue":{"value":{"amount":"+0.7868503928184509","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":"Q2743649$92810C7A-F98B-41C0-9D2F-F90645CCEBF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ed3a6a12710792cf3fc040f80ce51b3d8ec4caa","datavalue":{"value":{"entity-type":"item","numeric-id":2277451,"id":"Q2277451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad884502aac56b48f7bdf99a4193bbf178d1c92a","datavalue":{"value":{"amount":"+0.7732211351394653","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":"Q2743649$79E7AF85-07E9-43CB-80CC-D4F1914A7297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62c1f05387d305becbd6de9ac3e40ebdd21dfa5a","datavalue":{"value":{"entity-type":"item","numeric-id":1300010,"id":"Q1300010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7985166c8c964834b4b2b8298b9e69e2d9988180","datavalue":{"value":{"amount":"+0.7724560499191284","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":"Q2743649$B9762B52-B66C-4C86-812F-E5993EC932D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Finitary treatment of operator controlled derivations","badges":[]}}}}}