{"entities":{"Q1577487":{"pageid":1588227,"ns":120,"title":"Item:Q1577487","lastrevid":72234627,"modified":"2026-04-14T03:31:29Z","type":"item","id":"Q1577487","labels":{"en":{"language":"en","value":"The non-constructive \\(\\mu\\) operator, fixed point theories with ordinals, and the bar rule"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1501510"}},"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":"Q1577487$40FFD1CA-9D92-4F2C-9B46-3EDA556C53BC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f8bcf9b6bafe35102799ffe3136a32785e809bc2","datavalue":{"value":{"text":"The non-constructive \\(\\mu\\) operator, fixed point theories with ordinals, and the bar rule","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1577487$BEA34A23-6FAB-41B4-8AF2-505AAF7FB6AC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6a163f409465b10e901855b72a50bbec4f673069","datavalue":{"value":"0964.03061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$DF2554AB-A671-4991-8F86-9CCAABD590F3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"483976ee9c15c16215fc49c7d87ce6803bb2b5ee","datavalue":{"value":"10.1016/S0168-0072(00)00016-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$960904A3-C16A-42AF-98C7-6881D9A41783","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"703e8b987ff5a02d9a59e4ce9f4b68bdce3e6ac3","datavalue":{"value":{"entity-type":"item","numeric-id":588960,"id":"Q588960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$89E3F263-920E-4943-A4BF-34F8C305A716","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":"Q1577487$E99749A6-395A-46FF-93C1-EE9D09A61344","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0c1d27f90c5efc0baf8dad41a96c8a8197323785","datavalue":{"value":{"time":"+2001-07-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1577487$CB05E5A5-027F-4BAF-809A-25D1388BA3E6","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"dfc199b6469877dfc970c9e0ac00b21a573db590","datavalue":{"value":"The author considers a first-order applicative theory \\(\\text{AutBON}(\\mu)\\), and shows that it is proof-theoretically equivalent to predicative analysis, hence its proof-theoretical ordinal is Sch\u00fctte-Feferman's \\(\\Gamma_0\\). Here, BON stands for the basic theory of operations and numbers (Feferman et al.), and \\(\\mu\\) is the unbounded (hence non-constructive) minimum operator. Further, this theory has the inductiion scheme, and the bar rule: infer \\(\\text{TI}(\\prec,A)\\) from \\(\\text{TI}(\\prec, U)\\), where \\(U\\) is a unary predicate variable, \\(A\\) is any formula, \\(\\prec\\) is a recursive binary relation, and TI expresses transfinite induction. The method of proof is standard: \\(\\Aut(\\Pi^1_0)\\) is interpreted in the theory in question to give the lower bound, and the theory is, in turn, interpreted in \\(\\text{PA}^w_\\Omega+ (\\text{Subst})\\) for the upper bound. Here, \\(\\Aut(\\Pi^1_0)\\) is second-order arithmetic with autonomously iterated \\(\\Pi^1_0\\) jumps, and \\(\\text{PA}^w_\\Omega\\) is the fixed-point theory (so, with inductive operator axioms) over PA with ordinals \\(\\Omega\\), and \\(\\Delta_0\\)-inductions \\(w\\). To determine the strength of the last theory, the author uses systems with infinitary rules, cut-elimination, asymmetric interpretation, and so forth. In the form of an appendix, the author gives similar consideration to the theory whose underlying applicative system is recursive, and shows that it is equivalent to ramified analysis in all finite levels and hence its ordinal is \\(\\varphi 20\\) in the Veblen hierarchy.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$232B70ED-3A22-473E-9C43-24EA52FF8973","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$947BB033-380D-460C-8211-E2F639C1A2DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$70F54091-4BDA-43A2-9B1E-58B07BC49C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$88E1F2E8-AEDB-409A-951D-470CF73638BE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c408082a45015c6245ede8f65f9cbd51ca7064a","datavalue":{"value":"1501510","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577487$A906930D-8672-4CFB-9E6F-C8267E0F3F5B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"510424bd5d3a9753d8b9e3a9ba02bde51d79a894","datavalue":{"value":"first-order applicative theory \\(\\text{AutBON}(\\mu)\\)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$AB8C4B93-5EB0-488B-AB9F-0A813CBF5B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"134c05a5074e79203aa4274a5666221d6d469de9","datavalue":{"value":"predicative analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$F0076968-0D7A-4632-81B4-0298EB5F5340","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"444700fc8178825c3a0820090a6d5f63820a1d11","datavalue":{"value":"proof-theoretical ordinal","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$326F4C38-8E25-42AC-9DE8-88EF5072F528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b0d18202daf525538448ca1262425d196033741","datavalue":{"value":"bar rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$DB573416-A094-4620-B853-01FFA6129A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8cc87407ab9572d85505f2cace7811c9ecc29db","datavalue":{"value":"transfinite induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$BEF8560B-2ED4-4E7C-A6ED-A82430A4E338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e928ef71c0e7c501fd4e474de74400a15fc3e89d","datavalue":{"value":"second-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$9B50FCE2-DB00-4C3B-83C6-97A8DEDB99D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7cbe99b06a56a772e67531db7b5d75f216e8188a","datavalue":{"value":"fixed-point theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$14A62107-BA2E-4D12-BFEF-274233F4EBC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"65284cd5d923b12247f8ce35e25ffb7243aa5ba6","datavalue":{"value":"systems with infinitary rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$90C41875-518B-4435-A9B8-16518947214C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"552adda245d674b0f3c5b8f3c692eb6182373276","datavalue":{"value":"ramified analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577487$481536B4-FA73-4B14-972E-09540DED2814","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":"Q1577487$E71E0E63-C77F-4D16-8989-C3C57529A956","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2e1ab8d6c4a6ea4362f203e5137d4541ef80eb","datavalue":{"value":{"entity-type":"item","numeric-id":3679172,"id":"Q3679172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$E6E09B30-BCAF-4858-A2DA-1D7B2F7EC2C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"657968a87a1849cc9d0a2c04676a0be49fdb6449","datavalue":{"value":{"entity-type":"item","numeric-id":3705449,"id":"Q3705449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$24C44893-C87C-4DDA-B840-DA01E76103BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3af6d79cb7627680af279f9390de4528d7005030","datavalue":{"value":{"entity-type":"item","numeric-id":5344166,"id":"Q5344166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$4D8314A9-514B-474D-91F2-E0106F2762F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e4d4fc8f3a9eaeb100853b2c4bc95517741895a","datavalue":{"value":{"entity-type":"item","numeric-id":5595153,"id":"Q5595153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$E6CB424B-57B0-48DD-BE3E-22C88C725C6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"795988a055edb64e2872e1fd206565bb5c7a4af7","datavalue":{"value":{"entity-type":"item","numeric-id":5622162,"id":"Q5622162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$47F7F2E5-58DF-4EE7-B52C-6E31ED6D6CF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51fdc6e6c91c016e9985f506925ea38ed52ac667","datavalue":{"value":{"entity-type":"item","numeric-id":4128540,"id":"Q4128540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$4A28E864-27FA-41E5-BD8C-4D0B0EFBB8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a105535a0b4cf840366405592d4900ef990604f","datavalue":{"value":{"entity-type":"item","numeric-id":3882452,"id":"Q3882452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$50706462-8601-473D-8306-59EE3F6F396F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a867c6508cff28341ab32c6df4351fa77ca0b89c","datavalue":{"value":{"entity-type":"item","numeric-id":3039341,"id":"Q3039341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$9F136DD9-8079-40B5-8EF7-BCEEF3186239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb7de10908c6a54ef57b4383c3a54c934a390ea7","datavalue":{"value":{"entity-type":"item","numeric-id":1314542,"id":"Q1314542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$C9589CD9-2F5B-4ACE-99A3-0CBF3A4C081B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb73f10ef06d2f95cf34fa3f9d1b79e97709c0d1","datavalue":{"value":{"entity-type":"item","numeric-id":1919537,"id":"Q1919537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$B7218741-A33E-4B0D-8E5E-BAD243DA62A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e8ebd0adc06fe7c4575ee72369b3335638736e0","datavalue":{"value":{"entity-type":"item","numeric-id":1577479,"id":"Q1577479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$93C24E8A-24F6-45C7-A805-1A2DEFF99642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18833ee5d6be366acf0e86e4da70da9a3f2df977","datavalue":{"value":{"entity-type":"item","numeric-id":5619071,"id":"Q5619071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$698502CE-9599-46AF-B352-D803AF77F354","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52d8827d3a0ae8539d3c5d2339422865705a7449","datavalue":{"value":{"entity-type":"item","numeric-id":2563984,"id":"Q2563984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$4A0DC2F2-9BB9-4731-BA91-D2BEDE600B0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c26764e82c9ce1a5fcfcc1bf552b3a6da2b17f4c","datavalue":{"value":{"entity-type":"item","numeric-id":3778746,"id":"Q3778746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$34DA36CB-A288-417E-8408-5C42791B0C0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd228306c03acaf84fd1c55f443623cadcf212a2","datavalue":{"value":{"entity-type":"item","numeric-id":1210139,"id":"Q1210139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$BD41F56B-8902-49DD-827B-B8E12C3BC833","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07938c6dc0cbfdc3ba8a7f8b528364b3b071d379","datavalue":{"value":{"entity-type":"item","numeric-id":1908814,"id":"Q1908814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$F4F247B7-31C7-4828-9212-183D90FC9949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b209eb909f7b2405120231556d3122ec858afb37","datavalue":{"value":{"entity-type":"item","numeric-id":1896484,"id":"Q1896484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$5B614BEA-DFD8-43ED-A04D-A0EFAAD80DAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"344d2929ee1482cc0700fb8902daf5fde5955e19","datavalue":{"value":{"entity-type":"item","numeric-id":5687318,"id":"Q5687318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$9469939E-BF03-412D-A4B3-A4068A829DF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1dceb578b78d6e9bede36222164db87e36a5ed7","datavalue":{"value":{"entity-type":"item","numeric-id":1267848,"id":"Q1267848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$5F2E46A4-F000-49DB-BEEF-A7197DA0AA6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1b724e30ff53b009563e4451246f8778dce7a59","datavalue":{"value":{"entity-type":"item","numeric-id":1805407,"id":"Q1805407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$EEFC35A2-0AFA-4DF7-A159-B7EFDAFA1F04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$DB7A4E02-0C1A-448E-94E5-D2E17A6529D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577487$EA993E8E-3221-4410-BEB1-5E6EB7A46AA5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b6c7721c70860bbb05a7223c6c91e3f9f9b7769","datavalue":{"value":{"entity-type":"item","numeric-id":1314542,"id":"Q1314542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fced455e39af2262daf94dc3d82a0203d7a30931","datavalue":{"value":{"amount":"+0.821924090385437","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":"Q1577487$373E45D0-02E0-4DE2-88DA-3789163A803F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"668bcb1c1a942ce16e0bd7468ad79496ad2fa844","datavalue":{"value":{"entity-type":"item","numeric-id":1919537,"id":"Q1919537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"835c97390fdef3e55457cfed265953b9480b17ef","datavalue":{"value":{"amount":"+0.7838186621665955","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":"Q1577487$3545427D-B991-481C-B095-4C4F59CFBF66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14a92b24d89c12e4743a7835410c4dc4906b44ee","datavalue":{"value":{"entity-type":"item","numeric-id":1267848,"id":"Q1267848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d4a0acc9981b950d597f56988ecdafc65a1e77b","datavalue":{"value":{"amount":"+0.7790448665618896","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":"Q1577487$E2E8A8FC-D5EF-4B1A-AF4E-34831B19B37C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The non-constructive \\(\\mu\\) operator, fixed point theories with ordinals, and the bar rule","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_non-constructive_%5C(%5Cmu%5C)_operator,_fixed_point_theories_with_ordinals,_and_the_bar_rule"}}}}}