{"entities":{"Q2640597":{"pageid":2651340,"ns":120,"title":"Item:Q2640597","lastrevid":79437179,"modified":"2026-05-06T13:54:24Z","type":"item","id":"Q2640597","labels":{"en":{"language":"en","value":"A theorem on generalizations of proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4187800"}},"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":"Q2640597$30BCF541-B540-46AB-8AFE-A115D5EB75DA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a2befefd7f49256497099f838b2bfb8b8f65b5dc","datavalue":{"value":{"text":"A theorem on generalizations of proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2640597$8A5CC07F-67CF-4561-BDCF-AC92656FA5F7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d8c24dba91bda671b8b1230d7bbc73799d9477b4","datavalue":{"value":"0721.03038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$23FBC9F3-D85C-4295-ABA6-C3B12DBC7C7C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5876ed6480f3813cfbf954d81aace84263aaaeaf","datavalue":{"value":"10.1007/BF01621467","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$8BA22F63-4E01-46A0-9F11-1B47023098F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8b0df8cc476d314f14ae0e212e63b60a4094122d","datavalue":{"value":{"entity-type":"item","numeric-id":585197,"id":"Q585197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$E79DBEF6-DBF7-4A12-A6D2-34EBC4DB4191","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":"Q2640597$602BA076-F0D6-480B-9740-7158A7FE1240","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-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":"Q2640597$3192F89A-0181-4A9A-93BF-04FE68827053","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fc8cd1dfcd0272469404bf0202dc735f6c0e9ea5","datavalue":{"value":"A motivation for generalizing proofs is, as the author quotes, to obtain ``similar proofs'' with ``similar conclusions'' from the given one. A typical example is a Kreisel conjecture that relates a proof of \\(A(0^{(n)})\\) to that of \\(\\forall x(x\\equiv n(mod N)\\supset A(x))\\) in PA, including their lengths. In this vein, the author proves the following theorem. Assume that the given PA formula A(a), m,n\\(\\in \\omega\\), and a proof \\({\\mathfrak P}\\) of \\(A(0^{(n)})\\) satisfy the conditions: \\({\\mathcal G}(m)<n\\), the number of consecutive occurrences of ' in A(a) and the cardinality of the set \\({\\mathcal B}({\\mathfrak P})\\) are both less than m. Then there are p,q\\(\\neq 0\\), and a \\(PA^*\\) proof \\({\\mathfrak Q}\\) of \\(A(0^{(p)}+qa)\\) such that \\({\\mathfrak P}\\simeq {\\mathfrak Q}\\), \\(p\\equiv n(mod q)\\), \\(p\\leq {\\mathcal G}(m)+({\\mathcal F}(m))^ 3\\), and \\(q\\leq {\\mathcal F}(m)\\). Here, \\({\\mathcal F}(m)\\) and \\({\\mathcal G}(m)\\) are functions of order 2 to the 2 to fifth degree polynomials of m, the set \\({\\mathcal B}({\\mathfrak P})\\) gives a measure of the complexity of \\({\\mathfrak P}\\), \\(PA^*\\) allows, as beginning sequents, not only \\(A\\to A\\) but also \\(A\\to B\\) when A and B differ only by (formal) terms with the same meaning, and \\({\\mathfrak P}\\simeq {\\mathfrak Q}\\) indicates that they have the same structure as proof trees. Due to the nature of the subject, ``knitty-gritty'' analysis of formal proofs and complicated definitions are unavoidable. The author also compares similar results of his and in the literature.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2640597$91F0449C-6B23-49B7-9CE7-FFDE935520AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$C6457C36-0E90-4F13-8E6F-FD2A3F055EB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$251E7F5D-FA91-497C-9534-CAE29D05133A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$73A4CEB4-5CAA-4923-8716-2E5455B0351A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be9c119dbab884ec411b8edfa5378a8dbda58e4c","datavalue":{"value":"4187800","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2640597$662F5D17-D8CF-4A6D-83B3-D950EC1108BC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf90bd3739c9904af6ce9d5421b52c16b4645e65","datavalue":{"value":"transformation of formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2640597$76B8B42C-1E72-4E0D-8E4B-2EF4FC2EECE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2640597$1276E012-AFF9-411E-89FB-2BED4149E365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2fa957c309df6aef0870c4e466fa1de53cf5d75c","datavalue":{"value":"analysis of formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2640597$99321DDA-38B2-4196-98C2-A3E4EFB23415","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c007ae1867363f659c11dfe2e26b294ddb7e58e3","datavalue":{"value":{"entity-type":"item","numeric-id":33608,"id":"Q33608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$7B0052F3-BAD0-44D7-B508-E20A43E68B24","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":"Q2640597$5C60E8EF-4953-409C-92DE-70113B91C125","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"870c5a38858355caeeae9f446f0a3e85a9be75a4","datavalue":{"value":{"entity-type":"item","numeric-id":5517673,"id":"Q5517673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$1ED73D91-BA0F-4AB9-BA25-2D7F71B577FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba07dc7b075f512a5958344bc2487ab01c3f5b2f","datavalue":{"value":{"entity-type":"item","numeric-id":3786479,"id":"Q3786479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$A1E84EF8-D2A2-4CE5-8DBB-F6DA2FC85E8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b880d3c8511f1d53c27d1537b521daf74193b4","datavalue":{"value":{"entity-type":"item","numeric-id":1102280,"id":"Q1102280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$8DAE9A11-CA5A-4D70-9394-ADE96F4D8022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065ea4604210f6f33929664cd3c1938f56d2a34a","datavalue":{"value":{"entity-type":"item","numeric-id":4179180,"id":"Q4179180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$013C3B6C-794A-488F-B6AA-F0F8A13FCD72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e06aeba11d82d31d0908c53f7f9cab266ef5901c","datavalue":{"value":{"entity-type":"item","numeric-id":1168322,"id":"Q1168322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$532B400E-1F06-4718-87A4-ABB2BA01129D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085a1c5974566e16f17b41c7975f83d026da188f","datavalue":{"value":{"entity-type":"item","numeric-id":3794178,"id":"Q3794178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$B262EA71-B862-4EDF-BF58-5CED31A571D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f70c7f0070211df81086d4c25b73a9ca61d45c1","datavalue":{"value":{"entity-type":"item","numeric-id":5686023,"id":"Q5686023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$815CC371-61FE-4D25-ACC5-E23086B356D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07ca4424921537f8b64e05744c2b14d18371cd75","datavalue":{"value":{"entity-type":"item","numeric-id":1251655,"id":"Q1251655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$445E8670-C99E-4040-B260-5E479E2457D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2392e74c2f853e714af4751f3bd2e2895db1e3e","datavalue":{"value":{"entity-type":"item","numeric-id":1259591,"id":"Q1259591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$3DB95615-CB6B-4AC9-98E0-53DACEE77E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66a70d6da0d08ebdcb42845dcbd6c303c09f3d9d","datavalue":{"value":{"entity-type":"item","numeric-id":3788004,"id":"Q3788004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2640597$569C7A99-F805-473E-AB5A-85AD7454BF5A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc968fc081bfd42f16362de6125da6f02619ffa6","datavalue":{"value":{"entity-type":"item","numeric-id":930260,"id":"Q930260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b611dde328408293ee266349fb6d0427f756fbc0","datavalue":{"value":{"amount":"+0.8381279706954956","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":"Q2640597$C07F32FF-812B-4E50-99A7-3DEB46E13FB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d40d92fa97093c76018459af70da45c4cb1a659a","datavalue":{"value":{"entity-type":"item","numeric-id":3469102,"id":"Q3469102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91e0d2d7a3ce2b1afc3b9537fb1cff1b6c7f8fda","datavalue":{"value":{"amount":"+0.7871231436729431","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":"Q2640597$DEA7EF4D-AA75-4ADB-A7C5-8B028D857D14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e250c9950b9fbb4fb32f1056f995f17bc1e86f4","datavalue":{"value":{"entity-type":"item","numeric-id":3788004,"id":"Q3788004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7998a3f4fe858d21bc17f6a3acc8c3a5447c5e7","datavalue":{"value":{"amount":"+0.7849476933479309","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":"Q2640597$F6B9BA9B-8FAC-4ACD-A5BA-6FD060654549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de9069c6dfe841bb296f1a96559236500d84d14b","datavalue":{"value":{"entity-type":"item","numeric-id":3786479,"id":"Q3786479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0466b318ec3b99578f300a1ef6321bd9ed91a73d","datavalue":{"value":{"amount":"+0.7803441286087036","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":"Q2640597$8EB8EC3B-98AD-4E46-8824-E7C4568D4290","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21473e318044af4735c8f559ea4a6ecae3509f4b","datavalue":{"value":{"entity-type":"item","numeric-id":3773879,"id":"Q3773879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67a60ded9abe6b84411e3a52315da4131c00e1c9","datavalue":{"value":{"amount":"+0.7705831527709961","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":"Q2640597$652BFFC3-A572-408B-9255-F5B15AF2A615","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A theorem on generalizations of proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_theorem_on_generalizations_of_proofs"}}}}}