{"entities":{"Q1577482":{"pageid":1588222,"ns":120,"title":"Item:Q1577482","lastrevid":47015499,"modified":"2025-12-26T01:29:50Z","type":"item","id":"Q1577482","labels":{"en":{"language":"en","value":"Reduction of finite and infinite derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1501505"}},"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":"Q1577482$148EC5E3-4D39-48CF-A64E-291AF951A27C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"faf3d179109e48c4f4cfa0c5b16ae564fedad59c","datavalue":{"value":{"text":"Reduction of finite and infinite derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1577482$8AABF2C7-88F5-4991-89F8-9C1E113CC9C9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f4778af7ca430ed41a389a3ff608727995f357e4","datavalue":{"value":"0964.03057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$B2A2FCD3-1E4F-498D-81BC-14B47933FF21","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5a9f045dd2a3eb15324dab5e948475acb4266511","datavalue":{"value":"10.1016/S0168-0072(00)00011-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$7E96528E-DBEA-409F-A695-0E8BA9BA09C3","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":"Q1577482$3A1AE18D-F0FD-439C-9723-51B857480077","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"93a856ec74c83d630bb9a006b922edf955f6e7da","datavalue":{"value":{"time":"+2001-07-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1577482$6F6EB71B-8949-4B71-B9F3-F6428BBD4C77","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cea6c075a471c68c8834d7fb511e8b0315cfa372","datavalue":{"value":"The author presents a general schema of easy normalizations proofs for finite systems \\(S\\) like first-order arithmetic or subsystems of analysis having good infinitary counterparts \\(S_\\infty\\) and promotes a view of a derivation in a standard finite system with induction as a finite encoding of some infinitary derivations. The paper is essentially based on some of the author's previous works [see \\textit{G. E. Mints}, J. Soviet Math. 10, 548-596 (1978; Zbl 0399.03044), translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 49, 67-122 (1975; Zbl 0341.02020), reprinted in \\textit{G. E. Mints}, Selected papers in proof theory, North-Holland and Bibliopolis, Amsterdam and Naples, 17-72 (1992; Zbl 0773.03038), and \\textit{G. E. Mints}, J. Soviet Math. 20, 2322-2333 (1982; Zbl 0492.03021), translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 88, 106-130 (1979; Zbl 0439.03042), reprinted in \\textit{G. E. Mints}, Selected papers in proof theory, North-Holland and Bibliopolis, Amsterdam and Naples, 77-96 (1992; Zbl 0773.03038)]. The author considers a new system \\(S_\\infty^+\\), with the same rules as \\(S_\\infty\\), but different derivable objects: a derivation \\(d\\in S_\\infty^+\\) of a sequent \\(\\Gamma\\) contains a finite derivation \\(\\Phi(d)\\in S\\) of \\(\\Gamma\\). Sufficient conditions for \\(S_\\infty^+\\) implying a weak normalization theorem for \\(S\\) are obtained, followed by three examples of application including variations on Peano arithmetic and subsystems of analysis.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577482$5D850B6A-37CC-4AEA-A0AF-7A841D4C1F00","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$2A76EA1E-B7A6-4551-8F3F-8B98625EC7B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$760F4007-0C0B-44AF-9FF9-6AFC1EF91DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$03FE65E7-624E-449A-BE70-78D688B338D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$75C44B60-9472-43D2-A25B-3DA58DFA99AF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0e191cfabe5dbb4ad63fec2ac041523ed5a4237b","datavalue":{"value":"1501505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$BD49F421-8DE2-4342-87F5-FA1B9A7C1AC6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4296281254337308ad2c5f734043898466afdb58","datavalue":{"value":"normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577482$69E7F006-0CBE-40A8-824B-8E26E633C825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577482$29D39671-E34B-4DB5-8AFE-901447B42205","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"29e85a61e7939ee6f14f83214f0f77882dcad4fc","datavalue":{"value":"first-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577482$2EC45DF1-AEC6-4021-B885-DF9B8E4CF68E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e794ff676dbb33d99c44e2174579ff38cb07c71","datavalue":{"value":"analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577482$F4AE3769-EFF7-45A2-A3AA-C1B869E0068C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$E1383C5D-67B9-44CD-BDD4-7E494D572DB8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$3980BE22-35C0-4DF1-8E03-85579C89B20F","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":"Q1577482$6E97124F-58A3-427D-93BC-69A4FFF5C73D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"956c663a8c65ca7a493106b21f9b04a9a741383f","datavalue":{"value":{"entity-type":"item","numeric-id":1155602,"id":"Q1155602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$73C9E14F-E8E2-48FC-BC37-C217E802664B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc23233d37a7b707fdf4001c24c05adf785fcdc7","datavalue":{"value":{"entity-type":"item","numeric-id":2277451,"id":"Q2277451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$39F5AC0D-140B-4675-87AA-B564D229E6A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2973547328e6dae9da9b71e994c43f18327ab1f0","datavalue":{"value":{"entity-type":"item","numeric-id":4364500,"id":"Q4364500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$4461CA5D-DDBD-45E0-B8C8-A9355EF14D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ed33d75210f4b470fc995229f8d6e408696f04","datavalue":{"value":{"entity-type":"item","numeric-id":3922646,"id":"Q3922646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$BC34D869-789E-4B6E-8E70-616C526C5DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$A72789AC-66FF-4E0A-AB6F-8C285E728B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$61C9D277-AE7F-419F-A428-DF5ABBB6A618","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":"Q1577482$8243D59A-BD81-4425-9665-B4AA93FFDF23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"821ba052327064437d4dc5b12ef56d677e2220c5","datavalue":{"value":{"entity-type":"item","numeric-id":5633976,"id":"Q5633976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$662DC6C4-E015-424D-8772-7C6840193386","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":"Q1577482$DCDA1251-2224-410C-A1EC-6466EB982D77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f5db3554df72b639abe6b8020040bb56cb5e9e9","datavalue":{"value":{"entity-type":"item","numeric-id":1167719,"id":"Q1167719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$E5EFE58B-BDC3-4662-B192-C99801A394D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d9a69fdba20de6f6ac42d9e2851538bf1de7dff","datavalue":{"value":{"entity-type":"item","numeric-id":2367413,"id":"Q2367413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$3FA28372-F159-4D42-BF2C-8F403DC0F4EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28711599010bca9ffbebf4fe0012f8e3f98c05ed","datavalue":{"value":{"entity-type":"item","numeric-id":3999386,"id":"Q3999386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$A0BF289E-891E-49B4-9D9C-E62D38557C18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ec6af83f9a6c90ef054757ef63aea9bbf0884e2","datavalue":{"value":{"entity-type":"item","numeric-id":803124,"id":"Q803124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$1591CAC1-2D43-43E8-8869-5CCF258E30F9","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":"Q1577482$37C1E4B1-1227-434F-B245-E8D028E6AA31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$BC952202-44F0-46D5-9BEE-50413E06872A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$8EB3A1A3-D7EE-465A-8CB2-801F684641FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e1886c56990caf7504c5ed21ae2f5bef0a0586e","datavalue":{"value":{"entity-type":"item","numeric-id":4944926,"id":"Q4944926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577482$BC2BAC84-20A1-4FC0-8BF3-7707D8B25DFD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d7b50a84ca24d3528986a00071b16ec4ff961ab6","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(00)00011-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1577482$88F2C7A3-052C-4DCA-B55D-F377452B5874","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"573e6b946dd0fc929e242bc03dc4bf556ddc1f2c","datavalue":{"value":"W1969898883","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577482$6A56E606-8F35-460A-8FE5-A19B0DAB9D95","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ed3a6a12710792cf3fc040f80ce51b3d8ec4caa","datavalue":{"value":{"entity-type":"item","numeric-id":2277451,"id":"Q2277451"},"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":"Q1577482$7A597528-B138-4B05-860A-C258EC22298D","rank":"normal"},{"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":"a217680de3dcad6aea4b35bf1c0475afba91ff88","datavalue":{"value":{"amount":"+0.775239109992981","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":"Q1577482$7C044D91-D7AA-4AD3-B138-83A070AE35FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d348a38c7a1069e80a95427043d7d77b16e16eb5","datavalue":{"value":{"entity-type":"item","numeric-id":2367413,"id":"Q2367413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c61cc160a3b0277dc04103ac0fb5b51d900e41c","datavalue":{"value":{"amount":"+0.7603188157081604","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":"Q1577482$B720B407-1576-40C8-9263-CF3B98587398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3310318f87dcc5347990533329007727d8ae87d","datavalue":{"value":{"entity-type":"item","numeric-id":3801545,"id":"Q3801545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4fe7219fcd8c0ba56a5d4cd1f30f7383d5711215","datavalue":{"value":{"amount":"+0.7405117154121399","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":"Q1577482$C421B4F1-A2F4-41CE-86FC-5D01C621FA76","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1577482","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1577482"}}}}}