{"entities":{"Q1057857":{"pageid":1059705,"ns":120,"title":"Item:Q1057857","lastrevid":66156516,"modified":"2026-04-12T07:55:21Z","type":"item","id":"Q1057857","labels":{"en":{"language":"en","value":"An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3898879"}},"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":"Q1057857$26AFD495-B08D-4416-995B-48A9F0D82A3C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a37c38282e9ec27f7fa226000d880769b8e366e1","datavalue":{"value":{"text":"An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1057857$CB96C7E9-7709-42B2-B900-A57643402675","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"77628278c320621a58559850455272873132637a","datavalue":{"value":"0564.03041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057857$862C4EB4-0F4C-45CD-AE60-5D07C0485D50","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"98156e494398a35b2d843b98a737abd4eb3af2cb","datavalue":{"value":{"entity-type":"item","numeric-id":494641,"id":"Q494641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057857$4C11F534-5A02-4A48-9CD0-ADFEAA5FBDC9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4644ee9c6c93e22a4aa2641411a372d7ea43bad8","datavalue":{"value":{"entity-type":"item","numeric-id":180651,"id":"Q180651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057857$144687D4-D00D-4910-AE35-726FC9A43FB1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-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":"Q1057857$4A5D0234-616D-4798-8224-CAAC99FB5AAA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"aada6d1825fcbf4fbab0a42621e6a16b41768824","datavalue":{"value":"Let \\(ID^ i_{\\xi}\\) and \\(ID_{\\xi}\\) be the intuitionistic and classical theories, respectively, of \\(\\xi\\)-iterated positive inductive definitions (which are known to be proof-theoretically equivalent). Let \\(| O(\\xi +1,1)|\\) be the order type of \\(O(\\xi +1,1)\\), the system of ordinal diagrams ordered by \\(<_ 0\\). It is shown that each diagram in \\(O(\\omega +1,1)\\) is provably accessible in \\(ID^ i_{\\omega}\\). Thus \\(| O(\\omega +1,1)|\\) does not exceed the supremum \\(| ID_{\\omega}|\\) of the decidable well-orderings provably accessible in \\(ID_{\\omega}\\). In a forthcoming paper the author will use the accessibility of the diagrams in \\(O(\\omega +1,1)\\) to prove the consistency of the theory \\((\\Pi^ 1_ 1-CA)+BI\\) of second order arithmetic with \\(\\Pi^ 1_ 1\\)-comprehension and bar induction on decidable trees. Since Buchholz, Pohlers, and Sieg have shown that this theory is proof-theoretically equivalent to \\(ID_{\\omega}\\), the author concludes \\(| O(\\omega +1,1)| =| ID_{\\omega}|\\), which is the main conclusion of the paper. The author conjectures that \\(| O(\\xi +1,1)| =| ID_{\\xi}|\\) holds for all ordinals \\(\\xi\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057857$7E10D014-FDF4-4AF6-9381-72A8D8A9240A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057857$6F389E87-977A-466D-B5B8-401837F43258","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"203f48c2fba339d8e2560e1704a634a41cd7265b","datavalue":{"value":"3898879","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057857$7116877B-05E7-463A-BE07-D20E5BBEB945","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f3c8eeae433899a8000a2cf9147f2ec8bd59935","datavalue":{"value":"Bachmann notations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057857$8217E577-EA2D-4BA9-84AC-52ADE1E5865F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f11b15c92d415a607a87aa12dff6007cac8b313c","datavalue":{"value":"intuitionistic inductive definitions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057857$DF0A00BF-191B-49EE-8228-52961E2EC377","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057857$442FCDFA-E55A-4B88-A308-FF8BF8EAA700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d851dc6dad0c21e96d2633170c6d7b269b86574","datavalue":{"value":"ordinal diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057857$B9F89EE3-33E9-4485-8042-840C154D42FA","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e5e2a5720a49af3f774a10463c80dd488df8d858","datavalue":{"value":{"entity-type":"item","numeric-id":1161721,"id":"Q1161721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057857$1C3C1B59-8C66-410B-B7CB-86C9F0B80C33","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":"Q1057857$1AF4ECF3-BE81-4BC1-A783-F85ED42C116B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"430837931bf84686b55746a0f860fafb0961c29c","datavalue":{"value":"https://doi.org/10.21099/tkbjm/1496160038","type":"string"},"datatype":"url"},"type":"statement","id":"Q1057857$4B448464-CFE0-4C8B-9057-D75FBEE7BEB7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3e1f9e9b61834797d29dcb81a31e05c6ae4210f6","datavalue":{"value":"W790861174","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057857$AB0BBE98-1977-4CC2-80F5-A05906EC5648","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"212b61a6eb70cd2451e9c86a3f5ad4be797b8b0d","datavalue":{"value":"10.21099/TKBJM/1496160038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057857$240CEC6E-26B0-48AD-A8E8-B714542200DF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9c95017633b9bade18bfd563c1f89925bb662ea","datavalue":{"value":{"entity-type":"item","numeric-id":4722071,"id":"Q4722071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45e26e82bd72cbd95df94c7ca4e52cb4c9430905","datavalue":{"value":{"amount":"+0.8199480772018433","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":"Q1057857$97DE92EF-A9E5-48D9-A77A-8566329A6AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99e97fc611077d659d61a70cdfb98f0ddbce6c56","datavalue":{"value":{"entity-type":"item","numeric-id":3338234,"id":"Q3338234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da4fdc16209b00a11772ac8b1403c9f8bbafd800","datavalue":{"value":{"amount":"+0.8142181634902954","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":"Q1057857$6978698B-6CA1-4AE4-A180-99081F28A17A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"535c52bc0cd5800b5f2a94491f7536b290614fac","datavalue":{"value":{"entity-type":"item","numeric-id":3770526,"id":"Q3770526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d49308b990a25ecaf7ce4d7be2fe077d93ad5b1f","datavalue":{"value":{"amount":"+0.791803777217865","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":"Q1057857$878F7876-57F3-4A6C-B42A-A6FA4D0F1D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1ba86183230335eb5090bd9590001d18c146028","datavalue":{"value":{"entity-type":"item","numeric-id":1100461,"id":"Q1100461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a40b1093d728512ef63db8c2966394c74f7becfe","datavalue":{"value":{"amount":"+0.7661084532737732","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":"Q1057857$9B781B49-871A-478E-B96B-17290361CA9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2cec389dbec5380b2d49d516875028782328c4b","datavalue":{"value":{"entity-type":"item","numeric-id":5687318,"id":"Q5687318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f768e20874c10c7950a9946e962680c528ef3b1","datavalue":{"value":{"amount":"+0.7578520178794861","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":"Q1057857$061F17EB-9C5F-4E78-B3F1-59BBC6C66854","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_accessibility_proof_of_ordinal_diagrams_in_intuitionistic_theories_for_iterated_inductive_definitions"}}}}}