{"entities":{"Q803124":{"pageid":804972,"ns":120,"title":"Item:Q803124","lastrevid":49498369,"modified":"2026-01-07T08:16:08Z","type":"item","id":"Q803124","labels":{"en":{"language":"en","value":"Proof-theoretic analysis of KPM"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4200195"}},"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":"Q803124$6601257E-F60D-4C1A-AD16-E1100707E717","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e67173f059faf1e20aa780ecc5957ad0a6c5820","datavalue":{"value":{"text":"Proof-theoretic analysis of KPM","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q803124$13B5D61B-CEEA-4112-B188-9475034DC8CA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8387306feadeda42f32fff8bd3ec37095b0c9074","datavalue":{"value":"0727.03036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$4BFF2306-A1D5-4680-83BA-6065AC74AFF0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"503fecda8962b28fa9d36b65050d2f705f2a8249","datavalue":{"value":"10.1007/BF01621475","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$F45FC912-B734-4265-8AEF-1CF921D1FFC3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e64bf31f7adc7949599b7092674140bc267c6785","datavalue":{"value":{"entity-type":"item","numeric-id":206562,"id":"Q206562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$5BA3385F-9B89-4DDD-A646-B93A9B873F86","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$02689497-CB9A-472E-9524-2C9B42FB4708","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-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":"Q803124$D008B814-3E49-4751-BB1E-2EAD588916EC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6b1a47df7163f6dedfc5e732fbbfafe0a403a7ff","datavalue":{"value":"The aim of this paper is the ordinal analysis of the formal system KPM of a Kripke-Platek set theory which describes the properties of the collection \\(L_{\\mu}\\) of constructible sets of order \\(<\\mu\\) axiomatically, where \\(\\mu\\) is the first recursive Mahlo ordinal. Ordinal analysis of a theory T means determining the proof-theoretical ordinal \\(| T|\\) of the theory. In this case the following definition suggests \\(itself:\\)    \\(| T|:=\\inf \\{\\alpha |\\) for all \\(\\Sigma\\)-sentences of \\({\\mathcal L}(T\\vdash B^{{\\mathcal A}}\\Rightarrow L_{\\alpha}\\vDash B)\\}\\), \\({\\mathcal L}\\) being the language of set theory, \\({\\mathcal A}\\) a constant for \\(L_{\\omega_ 1^{CK}}\\), \\(\\omega_ 1^{CK}\\) the least nonrecursive ordinal, and \\(B^{{\\mathcal A}}\\) the formula which results from B by restricting all occurring unrestricted quantifiers to \\({\\mathcal A}\\). This definition of \\(| T|\\) is equivalent to the usual \\(one:\\)    \\(| T|:=\\sup \\{| \\prec |:\\) \\(T\\vdash ``\\prec\\) is a primitive recursive well-ordering of \\(\\prec ''\\}\\), where \\(| \\prec |\\) is the order type of \\(\\prec.\\)    The ordinal analysis is carried out by performing cut-elimination. Since KPM is not closed with respect to the cut-elimination operation, a system RS(M) of a ramified set theory is introduced with infinite derivations, in which KPM is embedded. For the ordinal analysis of RS(M) the method of local predicativity is applied. The ordinals used were introduced by the author in an earlier paper. He repeats the definition, thus the exposition here is self-contained.","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$FAC7A462-2E63-41E2-8096-EDC545C08296","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$7EF39CAF-CB36-481F-A734-693C6F2725FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$36E94257-6179-4E6B-88D4-541DDC3DB591","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e9bc27fca60d6d95fa18365c3cced00dd8546157","datavalue":{"value":"4200195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$47C8E7CD-0DB9-4DF3-A508-D7CA05E5A87E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"400ba340d67d1aa5d14a3323a7b62bde04670eaa","datavalue":{"value":"ordinal analysis of the formal system KPM of a Kripke-Platek set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$FE466290-4828-417C-9171-F88C07028053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b544c29ef2332a7ac7e48f9d6728288c581f4fd3","datavalue":{"value":"constructible sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$743960DC-75C4-42C2-A9DE-ACA5746E83FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c925e1c5429a73d963c80bfb54f3dce0bf0b3b66","datavalue":{"value":"first recursive Mahlo ordinal","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$A6D58B32-3E6F-42FC-9ABC-B4FFFBADB6F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"444700fc8178825c3a0820090a6d5f63820a1d11","datavalue":{"value":"proof-theoretical ordinal","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$89AA2C81-6E4F-4C42-B7B6-9301FA08E3DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$D78308F4-9DD5-4C63-925F-2DECB4EC8E54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc9634e2c4f95f0ff04acc2068cffb177a1aceca","datavalue":{"value":"ramified set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$7BB72CE2-3797-4DE2-9C4B-5F79390951D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02efba5a38516906df7b3752b37b488aaef7133","datavalue":{"value":"local predicativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q803124$5C5A8FF8-1E3C-4E5E-84E8-3C581E69E8F1","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0580dd4129e5d6439921b513d45494c072f33534","datavalue":{"value":{"entity-type":"item","numeric-id":1288968,"id":"Q1288968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$546BB84A-C112-44B1-9D64-DE9A65630DF5","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":"Q803124$5843FD1B-FCAC-4B01-A1AD-2E1155F49F1C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8973abb951181b5865d7e8e53e525f0e4b9b6f41","datavalue":{"value":{"entity-type":"item","numeric-id":4075450,"id":"Q4075450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$C0B96019-F60B-4F83-8FA3-4B7541554BA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"559d023d291e446bba13d5979c34214548a51934","datavalue":{"value":{"entity-type":"item","numeric-id":1109029,"id":"Q1109029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$019C6802-FBB8-49AF-8E57-C86447911064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4a41e51759b03d93fbc94ef3ba8acf0dd412666","datavalue":{"value":{"entity-type":"item","numeric-id":4040375,"id":"Q4040375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$13C7C8B3-A74E-44BC-BA4F-CA7A32B4CE6A","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":"Q803124$29C8032F-C5D5-418C-A3E6-70F61AADAFF1","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":"Q803124$74712FB3-6DC8-4F81-A07D-D31E79C5AE24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"126491e29fe2243aa651c260dc3c8aa88f5c48d3","datavalue":{"value":{"entity-type":"item","numeric-id":1109768,"id":"Q1109768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$1E7DD358-6EC7-4975-9D35-CC7211693300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3798ecd2352848fc7f05ce377ca3bb7ca030a458","datavalue":{"value":{"entity-type":"item","numeric-id":1801306,"id":"Q1801306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$1B2CCF6A-566A-486E-9158-717F89B0698B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3b1bb354afd2b79f7ab5c3406b5230d6055702b","datavalue":{"value":{"entity-type":"item","numeric-id":2276954,"id":"Q2276954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$4758463F-F053-4732-B083-3C0397B97DF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da7df1f230b0a1f7c4b06732c60d23fdde79f7f0","datavalue":{"value":{"entity-type":"item","numeric-id":3809793,"id":"Q3809793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$A36A26A5-FB17-4D2D-BAAD-AD20CCE949E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f8ff59a19c433a03526d2993fc18dbdfceed2bd","datavalue":{"value":{"entity-type":"item","numeric-id":920986,"id":"Q920986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q803124$ED7EFEB4-6AF5-4786-83E6-7E5481F8F41B","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":"Q803124$AF2D68F3-1CE9-4211-953A-035ABF5CDF1C","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":"Q803124$46411F08-0626-4055-BA1D-E896797B6852","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ba9f31998bfa7c5cbfffaeb105c5450affda4e77","datavalue":{"value":"https://doi.org/10.1007/bf01621475","type":"string"},"datatype":"url"},"type":"statement","id":"Q803124$68FFB0C6-8136-4706-9389-1AEF2441B3AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9165745dab13121ccd506e1e03d8b60145e277a7","datavalue":{"value":"W2064023341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q803124$C7FF3DBC-A3E6-4478-B087-C383DB915FF9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c551c20ece18e2c0d9d505fb59ec739d5c02723","datavalue":{"value":{"entity-type":"item","numeric-id":4281248,"id":"Q4281248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92e70e29b7f19592e8f45db5acdbcfaa1e3d36a8","datavalue":{"value":{"amount":"+0.8938759565353394","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":"Q803124$C0285187-3D2C-4F62-9825-3D5AAFD2FD80","rank":"normal"},{"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":"d3000e17f645711fb7062848016c06436c26e73d","datavalue":{"value":{"amount":"+0.890097975730896","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":"Q803124$98FC4EFD-0269-4F42-AD67-F8DC1A48D754","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6565e5f209a218b3fa41ed56ab5bb7691a8af717","datavalue":{"value":{"entity-type":"item","numeric-id":4882047,"id":"Q4882047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90b80dc2d0a25cf2fdac95544ec3e11aeb7fca7f","datavalue":{"value":{"amount":"+0.8764221668243408","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":"Q803124$E55B4013-FB39-495F-926E-5543A049D51E","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":"1c18ec6e5abc12a5bcbc2232789bc3978cff5d3f","datavalue":{"value":{"amount":"+0.8747339844703674","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":"Q803124$AE6C3B1F-8519-4B89-B088-E6EB6A213778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d34903a87817c2cf7368fb8f9ad046db3c04e9b","datavalue":{"value":{"entity-type":"item","numeric-id":4934564,"id":"Q4934564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b1c3b1bb68d85f12d18fea463c6696242c58fde","datavalue":{"value":{"amount":"+0.8385218977928162","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":"Q803124$7AF1AC89-A6B7-4D46-965F-A754D105A155","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:803124","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:803124"}}}}}