{"entities":{"Q1400604":{"pageid":1411344,"ns":120,"title":"Item:Q1400604","lastrevid":48152206,"modified":"2026-01-03T19:28:23Z","type":"item","id":"Q1400604","labels":{"en":{"language":"en","value":"The proof-theoretic analysis of \\(\\Sigma_{1}^{1}\\) transfinite dependent choice"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1963867"}},"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":"Q1400604$C93B4B0C-0F01-401B-B04C-2353D7B81CC3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd476c95f56a543cf3ddc632b1ae87fbfe85ca35","datavalue":{"value":{"text":"The proof-theoretic analysis of \\(\\Sigma_{1}^{1}\\) transfinite dependent choice","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1400604$214C5E26-38AE-475C-960F-394CFE6E3CF6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f1ba7630415dbb73fe0b8e2fcad1851ae6738151","datavalue":{"value":"1032.03051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$867FCC42-AE2D-4388-A613-702F97DD4EC3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ef64e40bf17898194b01e4a996e7d243055811f2","datavalue":{"value":"10.1016/S0168-0072(03)00006-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$A5992932-7283-498D-B304-46C52105416D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bae13f3938eac1cb218455b44b8a722b6832f12c","datavalue":{"value":{"entity-type":"item","numeric-id":1400603,"id":"Q1400603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$00166208-24CD-4E4F-83AF-E251E01CD4E4","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":"Q1400604$6B11DC55-1E0E-4304-A636-0BE5336D614A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a8cb865adec83a83fbad4bf48440b81dd66fe0c6","datavalue":{"value":{"time":"+2003-08-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1400604$BC64B8B2-9A20-4626-9084-A59002E2723F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"336dc2e499589d2a3787324844d9a21e0e8fec47","datavalue":{"value":"The theory \\((\\Sigma^1_1\\text{-TDC})_0\\) of \\(\\Sigma^1_1\\) transfinite dependent choice is a strengthening of \\(\\Sigma^1_1\\) dependent choice \\((\\Sigma^1_1\\text{-DC})_0\\) [cf. \\textit{A. Cantini}, J. Symb. Log. 51, 360-373 (1986; Zbl 0632.03046)], which states the existence of implicitly \\(\\Sigma^1_1\\) definable sequences along an arbitrary well-ordering. The author gives a proof-theoretic analysis of this subsystem of analysis. For the lower bound a well-ordering proof is given (following \\textit{T. Strahm}'s work [in: S. B. Cooper et al. (eds.), Sets and proofs. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 258, 383-402 (1999; Zbl 0961.03057); J. Symb. Log. 67, 260-278 (2002; Zbl 1032.03050), reviewed above]). The proof of the upper bound shows the standard methods of infinitary proof theory at work. As proof-theoretic strength of the theory one gets \\(\\varphi\\), \\(\\omega\\), \\(0\\), \\(0\\) (in terms of the ternary Veblen function \\(\\varphi\\) [cf., e.g., \\textit{G. J\u00e4ger}, \\textit{R. Kahle, A. Setzer} and \\textit{T. Strahm}, J. Symb. Log. 64, 53-67 (1999; Zbl 0937.03065)]). Therefore, \\((\\Sigma^1_1\\text{-TDC})_0\\) is an example of a subsystem of analysis belonging to the new area of {metapredicative proof theory}.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1400604$AF314F09-859E-474F-98B3-182AAA537045","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"698ef69cf2501558685cb66472f90d21aa909f07","datavalue":{"value":{"entity-type":"item","numeric-id":194998,"id":"Q194998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$FBC01E93-1555-41A7-BBF4-4598DBAA015E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$EBC2D8E3-0F20-47F3-9C90-24E9133F979D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$A2ADD967-4C9E-444D-9916-7F59120E6CBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$5BD4937D-F909-4AD8-B1DF-E649CCC252B1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bbd672533ba37584a71b6bd621e3f676c661fc37","datavalue":{"value":"1963867","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1400604$657E10E6-8480-4E34-AFFC-37E476DF4172","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"80185ab498b19040bb4c8ec9a598ccdcba1335b3","datavalue":{"value":"\\(\\Sigma_1^1\\) transfinite dependent choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q1400604$ECBC6198-24B3-4722-8BF8-FE67DFA9AC6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"526657a0ca390f11b64c630e88c4b1bc5e436575","datavalue":{"value":"Metapredicativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1400604$879BF9EE-A8C6-417C-869C-4C68875BD3F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f763be8f9480641fc901542d7275479ffb03b5c0","datavalue":{"value":"Ordinal analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1400604$2CBD772C-6793-4707-B1BD-0844CEFE73BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"415190ea48895d5e2d89992da82928e762b3d65a","datavalue":{"value":"Subsystems of analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1400604$9E650591-19AE-4A75-BCA2-5180791D775F","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":"Q1400604$CF406BE7-81B3-494E-8895-D4E4D680FADF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e299cd24790cf833246b68534501b445b379b03","datavalue":{"value":{"entity-type":"item","numeric-id":5687314,"id":"Q5687314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$F0FF5092-AD70-449A-ACA2-16B45BC638FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53896d5eb3675aae4ccf944284341c082a1794fc","datavalue":{"value":{"entity-type":"item","numeric-id":3768896,"id":"Q3768896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$6D139F17-0351-49FB-86B5-58B241FAFFC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39fc44a12c6438cb90522e8e2687faea7c2e4f4f","datavalue":{"value":{"entity-type":"item","numeric-id":3981446,"id":"Q3981446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$2ED560C5-5E0B-41F4-ABD5-738BE439FC21","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":"Q1400604$9C38DC0E-DBC3-4726-913A-2B866B52F06C","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":"Q1400604$3AFE85FA-EAB5-40D8-AA4E-42DEC4FC35EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4e3a045fb18057576e3a052695370f915c6320","datavalue":{"value":{"entity-type":"item","numeric-id":4254619,"id":"Q4254619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$CD9EA3C9-E743-4E6D-8788-01A5A5435976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ae10646c4541c33d72edf12c66f71b78185b320","datavalue":{"value":{"entity-type":"item","numeric-id":1590660,"id":"Q1590660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$D65133AC-5049-41BF-AD6E-4C5C9DB75901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42bb7bb61202307db43d4802956efbc479572508","datavalue":{"value":{"entity-type":"item","numeric-id":2747729,"id":"Q2747729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$786B4BAC-B99B-479E-9353-FE9C46546166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b24b5b561cde7a5eef6f6e87df461bfda495bb00","datavalue":{"value":{"entity-type":"item","numeric-id":3773877,"id":"Q3773877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$F8DB59D9-5C4C-49C0-91F8-411C5D049C06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"509f914c9bb02a5a157b793e56d4da4ee0369382","datavalue":{"value":{"entity-type":"item","numeric-id":1976875,"id":"Q1976875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$67E1809A-B51E-4BE2-A53E-37CDED35684C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7049f5223f308cd57c9ac20d4efb3aafce66ff1d","datavalue":{"value":{"entity-type":"item","numeric-id":4779657,"id":"Q4779657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$52521546-E252-499C-BD1F-6C32B1C4F912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29ffdb5f609972b5e61b742f9aacd4fe427f5eb7","datavalue":{"value":{"entity-type":"item","numeric-id":2651619,"id":"Q2651619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$C0330695-73F8-4F51-8905-5F7506210019","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":"Q1400604$0841976C-F02C-427A-AAEC-C6EBE8CA45F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ab695f6ca892767fcc28ad56cbfb6e401ee2f69","datavalue":{"value":{"entity-type":"item","numeric-id":4934569,"id":"Q4934569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$DC366E5E-8994-4CB6-8059-EDCCB829F410","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"924ac7dda420fe7f2b11191b37cb4d0940598f19","datavalue":{"value":{"entity-type":"item","numeric-id":4944925,"id":"Q4944925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$245B54A0-9FE8-4087-A4D3-C375CAD2FD38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da21334ee638fdfaa9f205c067a244ea7b96c11f","datavalue":{"value":{"entity-type":"item","numeric-id":4532614,"id":"Q4532614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1400604$5B8086C9-3B6F-4001-B10E-298AE7312F2F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c17330142912040dd4e0b802b9cbdd1e53e10e47","datavalue":{"value":{"entity-type":"item","numeric-id":4779657,"id":"Q4779657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aab2d027d70daee5bc3e76244db0cab0ed9ee1c5","datavalue":{"value":{"amount":"+0.8253002166748047","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":"Q1400604$7BBFB27F-DE53-4DBF-8EE5-AF966D567A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b89f3753e44e204fd1b35b530c585acef21f74f","datavalue":{"value":{"entity-type":"item","numeric-id":4040375,"id":"Q4040375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0171b039c1ae4003be8a8887227306437d45e5a0","datavalue":{"value":{"amount":"+0.743858277797699","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":"Q1400604$5E29562D-3610-4996-80E4-5375BD4A8E6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce26ed2180efea7b2de854b2112726dec0507f39","datavalue":{"value":{"entity-type":"item","numeric-id":4254619,"id":"Q4254619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e7469e638e404d7ee58486f2efb003dd4579545","datavalue":{"value":{"amount":"+0.7430625557899475","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":"Q1400604$8F902996-5CCE-4B35-82C4-AAFB301A4552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4893a7f4c88675eebffad26a0ef7722a9c22f92d","datavalue":{"value":{"entity-type":"item","numeric-id":1590660,"id":"Q1590660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"121eef0cf9666e0a1fb42234e702c981dc306cbf","datavalue":{"value":{"amount":"+0.7423514723777771","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":"Q1400604$940D5F14-0A23-4F7B-8699-984C4DD7E0B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d7b1dc6e396f4d398e8d9631206e9766f4ebbc85","datavalue":{"value":{"entity-type":"item","numeric-id":2276954,"id":"Q2276954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7b32cc39584b5873658ec81cec37001cb11d8b9","datavalue":{"value":{"amount":"+0.7279777526855469","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":"Q1400604$1B9C197B-3862-4321-9581-35F32A3B0FE3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1400604","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1400604"}}}}}