{"entities":{"Q1109029":{"pageid":1119778,"ns":120,"title":"Item:Q1109029","lastrevid":66687381,"modified":"2026-04-12T11:58:55Z","type":"item","id":"Q1109029","labels":{"en":{"language":"en","value":"A new system of proof-theoretic ordinal functions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4068862"}},"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":"Q1109029$3AE32D2E-6D0A-4B15-BC3A-23A1EB8D5FAF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"152e70c36ebf7cad984e38149d2f49ae2f87a6e4","datavalue":{"value":{"text":"A new system of proof-theoretic ordinal functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1109029$F4CBE95C-A7F8-47C4-9CF5-DBE0392CE173","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7517d9da70b8eac94e4fac214ecf9226f03bb70a","datavalue":{"value":"0655.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$E2EB7629-EA71-4B33-9113-E5A12EBDB88A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"322613cfb8eb4e867aa7e15859d48a854badb584","datavalue":{"value":"10.1016/0168-0072(86)90052-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$90F48CF8-F18D-45C6-9624-F2A60B1E2787","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":"Q1109029$95EEBD32-2438-418C-8D16-ACBE01953DB7","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":"Q1109029$0569156F-AFEB-4FE4-92F6-BF169CF7A4FA","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":"Q1109029$AA9492DE-076F-4565-9750-2D08BA1206B6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f8a852731d3ef147ece4465c21eaa28cf0a84d3","datavalue":{"value":"https://epub.ub.uni-muenchen.de/3841/1/3841.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1109029$368C7BA7-0FDF-487A-B444-235BC9639ACB","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5a59c43a15bbde60a7fd8d2768fa6bc8c939bddf","datavalue":{"value":"In this paper we present a family of ordinal functions \\(\\psi_ v(v\\leq \\omega)\\), which seems to provide the so far simplest method for denoting large constructive ordinals. These functions are a simplified version of the \\(\\theta\\)-functions, but nevertheless have the same strength as those. In Section 1 we define the functions \\(\\psi_ v\\) and prove their main properties. In Section 2 we define a primitive recursive notation system (OT,\\(\\prec)\\) based on the functions \\(\\psi_ v\\). This system has the great advantage that its ordering relation \\(\\prec\\) is very simple and can be defined without reference to sets of coefficients or any similar concept. OT is introduced as a subset of a larger set T of terms, which plays an important role in Section 3. There we show that the statement \\(PRWO(\\psi_ 0\\Omega_{\\omega})\\), which says that there exist no primitive recursive infinite descending sequences in (\\(\\{\\) \\(x\\in OT:\\) \\(x\\prec \\psi_ 0\\Omega_{\\omega}\\},\\prec)\\), is not provable in \\(\\Pi^ 1_ 1-CA_ 0\\). The proof of \\(\\Pi^ 1_ 1-CA_ 0\\nvdash PRWO(\\psi_ 0\\Omega_{\\omega})\\) is based on the following results of \\textit{W. Buchholz} [ibid. 33, 131-155 (1987; Zbl 0636.03052)]: \\(ID_{\\nu}\\nvdash \\forall n \\exists k c^ n_{\\nu}(k)=0\\) (\\(\\nu\\leq \\omega)\\), where \\(c^ n_{\\nu}(k)\\in T\\), for all \\(n,k\\in {\\mathbb{N}}\\); and every sequence \\((c^ n_{\\nu}(k))_{k\\in {\\mathbb{N}}}\\) is primitive recursive. In Section 3 we prove \\(c^ n_{\\nu}(k)\\in OT\\) and \\((c^ n_{\\nu}(k)\\neq 0\\Rightarrow c^ n_{\\nu}(k+1)\\prec c^ n_{\\nu}(k)).\\) Since for all \\(\\nu <\\omega\\) we have \\(c^ n_{\\nu}(k)\\prec \\psi_ 0\\Omega_{\\omega}\\), it follows that PRWO \\((\\psi_ 0\\Omega_{\\omega})\\) implies \\(\\forall \\nu <\\omega \\forall n \\exists k c^ n_{\\nu}(k)=0\\). Since this can be proved in Peano Arithmetic and since \\(\\Pi^ 1_ 1-CA_ 0\\) is conservative over \\(\\cup_{\\nu <\\omega}ID_{\\nu}\\) with respect to arithmetic sentences, we obtain now \\(\\Pi^ 1_ 1-CA_ 0\\nvdash PRWO(\\psi_ 0\\Omega_{\\omega})\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109029$DEA1143C-F440-459A-A3B7-01AA924247C9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$DBB229A8-46BA-469F-8A5A-77084EB2A664","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"408009683996a136f252afa79a2f3e141008d088","datavalue":{"value":"4068862","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$AAD0DC74-FC45-4BB2-9079-CCF045D90A92","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"503f76f16f1674758a96c15192462f8da2b23952","datavalue":{"value":"ordinal functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109029$60309CAC-2D75-4136-B89E-5A301923C7DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0433f4da0949a1d07642794d006c784d9ab06996","datavalue":{"value":"large constructive ordinals","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109029$BB50B0CC-66D7-4F5A-A7DA-E86D5593EB6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0cff0f943e93ddc8ceae34e6296639abddff679","datavalue":{"value":"primitive recursive notation system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1109029$E6C3C3C6-F476-4465-AD10-CF4D56CB5AC8","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"28d0983eb81c3b863359d2924e4c14604e66f4bd","datavalue":{"value":"Q29396669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$2C296D9D-4017-4034-87FE-30C17D183174","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":"Q1109029$A3A51282-4298-4EEC-A786-373A30DE5BA3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d83cdf82ee18cde81c63ab05b6485ae35c07490e","datavalue":{"value":"W2077219408","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$1E6423C7-6DD1-4AB0-B3EA-648EC474CCD7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"17fc2e7459eaf322f6bdf4106f28738c73144017","datavalue":{"value":{"entity-type":"item","numeric-id":4198748,"id":"Q4198748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109029$CCEF4EB0-D9AC-4E14-B783-3979BA7E7820","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c51450d884b7db77c14a0ec5b7db228e4f4a3b8","datavalue":{"value":{"entity-type":"item","numeric-id":3335775,"id":"Q3335775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109029$BA1C1785-ED43-4977-ACC7-DEF65102E4EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cc2143eb9934bad347b67d1052a1c677ec1b276","datavalue":{"value":{"entity-type":"item","numeric-id":4175275,"id":"Q4175275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109029$0DC785EB-37FA-410E-A98C-150593403416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d64bbc8c36466cd75ac5f7c3e1e13abe00124c","datavalue":{"value":{"entity-type":"item","numeric-id":3731598,"id":"Q3731598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1109029$CAD75E9D-8DFD-44CA-9698-51C1FE961A37","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"287c56021601a56abd44136c95f0dad977e5e717","datavalue":{"value":"journals/apal/Buchholz86","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1109029$4B750F91-09DA-462D-8FEE-397B5FFFD518","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b893d0fe6537bdf6de922ff97b37331fdb5c75b2","datavalue":{"value":{"entity-type":"item","numeric-id":4934566,"id":"Q4934566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45709b6fbff6c81c0114d56eac9a69bdd327055b","datavalue":{"value":{"amount":"+0.8255029916763306","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":"Q1109029$02BE10BB-5343-4DCC-B355-A0E59AD012BD","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":"6d0027c6df232da239a4e6d86f3ead862705a04a","datavalue":{"value":{"amount":"+0.8232646584510803","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":"Q1109029$7CFD351A-A93A-49D2-975E-259CBC949D71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d95f1cde2766d35c13522885aebafc4ae650245","datavalue":{"value":{"entity-type":"item","numeric-id":1102279,"id":"Q1102279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f947e22f9ecd602c7fdc10f70124ff4318928668","datavalue":{"value":{"amount":"+0.8112508654594421","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":"Q1109029$7A3FAB04-1810-4112-8AE4-AC56D58510A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a709d771b80aef449fc8091fe5b3d4c6a745323","datavalue":{"value":{"entity-type":"item","numeric-id":3775552,"id":"Q3775552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b5bc5daa402258e1f0d01b3ebeb175b008dec4d","datavalue":{"value":{"amount":"+0.8112273812294006","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":"Q1109029$7C8C3B82-5433-45F6-BC97-7338D550B396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cd86ac1794ec10387752f75b51cb3b896ca66c2","datavalue":{"value":{"entity-type":"item","numeric-id":582289,"id":"Q582289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecf3bfb8a80e74742986a3926c9f12e0190b18a1","datavalue":{"value":{"amount":"+0.8038491606712341","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":"Q1109029$16DD7495-3480-4497-99D2-DBD4FBD28E88","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A new system of proof-theoretic ordinal functions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_new_system_of_proof-theoretic_ordinal_functions"}}}}}