{"entities":{"Q2277451":{"pageid":2288194,"ns":120,"title":"Item:Q2277451","lastrevid":49490458,"modified":"2026-01-07T07:17:03Z","type":"item","id":"Q2277451","labels":{"en":{"language":"en","value":"Notation systems for infinitary derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4197981"}},"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":"Q2277451$2C5CBAD6-6764-42DA-B9E8-0E2FC2983505","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c1316f8ab410a4ea2bb464f201bf671b12fcb363","datavalue":{"value":{"text":"Notation systems for infinitary derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2277451$2DCDFD47-606E-4BC8-BBBB-F8D3EE05DB92","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a79af88ba95a0805c7d87e10acecf7f50bd495ec","datavalue":{"value":"0726.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$596B01A7-2653-4AAF-B190-12A9F654679B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"07293858cb632fac0f8821890d894977f1390e20","datavalue":{"value":"10.1007/BF01621472","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$E62188B4-79F0-4877-A822-79837E66A764","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":"Q2277451$D16FEC9B-CD42-4A4C-B85F-DE4F2C833BFE","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":"Q2277451$8DF05A5E-EEF9-4734-B8B9-79D509EE21C0","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":"Q2277451$6490B8D9-BBF7-4749-A513-E9AAEB851625","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"66d9a66406533dc70f6d08f8a88c8d0b0e9de804","datavalue":{"value":"The author calls his paper modestly a supplement to presentations of \\textit{J.-Y. Girard} [Proof theory and logical complexity. Vol. I (1987; Zbl 0635.03052)], \\textit{G. E. Mints} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 49, 67-122 (1975; Zbl 0341.02020)], and \\textit{H. Schwichtenberg} [``Proof theory: some applications of cut-elemination'', Handbook of mathematical logic, 867-895 (1977; Zbl 0443.03001)]. Actually he provides an elegant method of finitarily describing infinite derivations of \\(\\omega\\)-arithmetic \\({\\mathbb{Z}}^{\\infty}\\) without numerical coding. Instead he uses finite terms as notations for infinite derivations. The system of these terms is generated starting from constants for finite derivations by function symbols \\(I_{k,A}\\), \\(R_ C\\), and E, which correspond to the operations \\({\\mathcal I}_{k,A}\\), \\({\\mathcal R}_ C\\), and \\({\\mathcal E}\\) on \\({\\mathbb{Z}}^{\\infty}\\), the set of well-founded infinite derivations of \\(\\omega\\)-arithmetic. \\({\\mathcal E}: {\\mathbb{Z}}^{\\infty}\\to {\\mathbb{Z}}^{\\infty}\\) is to be the cut-elimination operator, \\({\\mathcal R}_ C: {\\mathbb{Z}}^{\\infty}\\times {\\mathbb{Z}}^{\\infty}\\to {\\mathbb{Z}}^{\\infty}\\) the reduction operator, which associates to each derivation containing a cut with cut formula C a derivation with a simpler cut formula in the corresponding cut. \\({\\mathcal I}_{k,A}\\) is the inversion operator, which substitutes each occurrence of A in the derivations by some A[k], which is simpler than A.    The method is applied to gain two known results of proof theory: Let \\({\\mathbb{Z}}+TI_{\\prec \\upharpoonright}\\) be the system of Peano arithmetic together with the schema of transfinite induction up to any proper segment of the given primitive recursive well-ordering \\(\\prec\\). Then it is shown:    (I) If \\(R\\in \\Sigma^ 0_ 1\\) and \\({\\mathbb{Z}}+TI_{\\prec \\upharpoonright}\\vdash \\forall x\\exists yR(x,y)\\), then there are primitive recursive functions g and o from \\({\\mathbb{N}}^ 2\\) to \\({\\mathbb{N}}\\) such that  \\[  \\min \\{m| \\quad R(n,m)\\}=g(n,\\quad \\min \\{k| \\quad o(n,k+1)\\nless o(n,k)\\})\\text{ for all } n\\in {\\mathbb{N}}.  \\]  (II) PRA\\(\\vdash PRW O(\\prec)\\Rightarrow\\Pi^ 0_ 2\\)-Reflection (\\({\\mathbb{Z}}+TI_{\\prec \\upharpoonright}).\\)    At the end of the paper the notation system for well-founded derivations is extended to a concept of derivations which have not necessarily well- founded tree structure. The cut-elimination operator \\({\\mathcal E}\\) is extended to an operator \\({\\mathcal E}'\\) which operates on generalized derivations such that local correctness with respect to the derivation rules is preserved and \\({\\mathcal E}'\\) is continuous. Thus an alternative description of the continuous cut-elimination operator of Mints [loc. cit.] is provided.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$23D1C2DE-2360-4246-99CF-6694331F06F8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$E9A488A3-E9BF-4273-8892-EF7433F5F3A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$B4F26386-DB76-425B-A622-DE40C9EBC404","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$F6D3F030-5B42-4A4E-A768-2A2CF2C70304","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c5ba243d9fa409db7724c8472d8c000ed46101a7","datavalue":{"value":"4197981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$22AB2FCB-B60F-43EA-9C36-65976D72F924","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93f6513da07f955593a72683f0b4cf7e6a48be35","datavalue":{"value":"infinite derivations","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$F425C4CA-0078-46AB-A51B-66451F9FB69C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c71109c92baf9c9272ee5565434c69c16edc1870","datavalue":{"value":"\\(\\omega \\) -arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$71051AA9-E7AB-457F-A693-008F36D7E022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ff0a8c781720ff45533729f87a4db97d1554120","datavalue":{"value":"cut-elimination operator","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$26767F29-10F9-4C3A-AC2A-3E9FF07078D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"28962c773ed56dc9d49f62eb7621becf63a08850","datavalue":{"value":"reduction operator","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$B69FC054-FA55-46F6-9FC7-26C880D3C620","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4d0591c7fbeb97996f1c96f89d90802791072a8f","datavalue":{"value":"inversion operator","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$2AFB1198-18A0-41F7-9D77-D0607A64E814","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$C1449696-0AC8-4009-B992-5E454604B8B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8cc87407ab9572d85505f2cace7811c9ecc29db","datavalue":{"value":"transfinite induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$EBE68AAD-ED28-4C6D-9558-2C61FBE323C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75215c80968178951612818bc08b3e62e2862f51","datavalue":{"value":"notation system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2277451$113D6A0F-67B8-4E1F-90B7-800DE76ADCA3","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":"Q2277451$CA257424-00F0-4071-AB40-FC0A85806FF2","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":"Q2277451$937D6F22-21FF-4E86-925F-891FA2DD3F60","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a454ef6b42682012c40ff7e7cb072f359af068d","datavalue":{"value":{"entity-type":"item","numeric-id":3773880,"id":"Q3773880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$76796FEF-0024-4BC1-ACBF-A55E6898C045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25eaa6c3e9bb9d8953ff182f9af4a923fe4aa505","datavalue":{"value":{"entity-type":"item","numeric-id":5925300,"id":"Q5925300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$BA6D6B91-A635-4421-BFD0-AE23DEB64349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b97dc288c0e9f823be86d021de4ec9cff71dce18","datavalue":{"value":{"entity-type":"item","numeric-id":2647392,"id":"Q2647392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$5B51DBC9-F62E-4C67-B7F4-1056133DAEA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$7075CFD7-8461-4E96-AE81-7AF5F6E21187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"967caee0f4b629b2770249b58352d882fa57e30d","datavalue":{"value":{"entity-type":"item","numeric-id":911585,"id":"Q911585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$228748F5-BF38-4485-BEB8-301D686DF0E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd563c8e7e782ee36eec340808cf341dbeeb62bd","datavalue":{"value":{"entity-type":"item","numeric-id":5569099,"id":"Q5569099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$250C112A-90EA-4C46-8D6E-86DE2EFBE4F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fc20c39e0b33b874af0982ebf6bc1d64db55ff3","datavalue":{"value":{"entity-type":"item","numeric-id":4079564,"id":"Q4079564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$E25EFE4F-0F6A-4619-89DE-C5136AD26B51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e8f21ae813780ffb1b14b622d2c99e2bf7de1d2","datavalue":{"value":{"entity-type":"item","numeric-id":1254248,"id":"Q1254248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$65837B2F-F8C6-4236-84BC-234C8A5912A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b34a3bbe6833c1249dbe3ebbfcdb81d97201d76","datavalue":{"value":{"entity-type":"item","numeric-id":2649136,"id":"Q2649136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$3AEA2630-354E-4C4B-8AD3-F4BD6CBE925B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21aa2c8417444bb3098b83ec743e607734c3bfb","datavalue":{"value":{"entity-type":"item","numeric-id":3285631,"id":"Q3285631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$CB8F3E73-C0A1-488D-A070-088DD498E995","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":"Q2277451$A4B8BAE0-C462-4170-A2A1-25CCC3F56C8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa5a4f2837dd5c65f7591e5307e1bfb3bd015425","datavalue":{"value":{"entity-type":"item","numeric-id":3801545,"id":"Q3801545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$C45FA734-6C05-4925-A8C8-2219DF21EA06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2277451$1A2C261F-0648-441F-96FC-F35D4B56869F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0612e4842628492bf9bf119674925dfcd034a956","datavalue":{"value":"https://doi.org/10.1007/bf01621472","type":"string"},"datatype":"url"},"type":"statement","id":"Q2277451$E7D84803-C29C-4724-ABD5-504BA1583D3C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d6f8b7feb30a7631ddebeaf810a5f012f118241d","datavalue":{"value":"W2068743712","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2277451$5E48A858-F47B-4C47-A617-ADDA338B9323","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad671a5cdca8ff0bcc6d5067de9976bfbe6ba45c","datavalue":{"value":{"entity-type":"item","numeric-id":1295405,"id":"Q1295405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07a6b11b5ff5da000a03e4169d527f424a9317e1","datavalue":{"value":{"amount":"+0.8533158302307129","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":"Q2277451$336BC452-426E-41A9-BEDD-ADD5DF8310E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f577a555e5a17c3fd40e19c0409b8141c311a7c","datavalue":{"value":{"entity-type":"item","numeric-id":5944050,"id":"Q5944050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07a6b11b5ff5da000a03e4169d527f424a9317e1","datavalue":{"value":{"amount":"+0.8533158302307129","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":"Q2277451$051314EB-9D3A-4DCA-88E6-8A9F1489C09E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1e25f8bb5ff79748934d4b0654073078b908c4e","datavalue":{"value":{"entity-type":"item","numeric-id":1577482,"id":"Q1577482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6755e0d68edfd4f52b281f3d955f06f98a122f9","datavalue":{"value":{"amount":"+0.7971805334091187","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":"Q2277451$0BA9B980-D1B0-4D06-AE9D-38F88CCF4E1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66b06a363e99233f409cb556c258e79cd75b17df","datavalue":{"value":{"entity-type":"item","numeric-id":1295413,"id":"Q1295413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6755e0d68edfd4f52b281f3d955f06f98a122f9","datavalue":{"value":{"amount":"+0.7971805334091187","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":"Q2277451$455AA70C-62CE-4F43-AD53-2708552EEE97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89b83846e77848704234acd12a129f1bca7015c5","datavalue":{"value":{"entity-type":"item","numeric-id":2743649,"id":"Q2743649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad884502aac56b48f7bdf99a4193bbf178d1c92a","datavalue":{"value":{"amount":"+0.7732211351394653","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":"Q2277451$DEA1C496-7B0D-45F2-9506-1A020A8A3C2E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2277451","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2277451"}}}}}