{"entities":{"Q1375747":{"pageid":1386487,"ns":120,"title":"Item:Q1375747","lastrevid":71009811,"modified":"2026-04-13T18:53:02Z","type":"item","id":"Q1375747","labels":{"en":{"language":"en","value":"A normal form for arithmetical derivations implying the \\(\\omega\\)-consistency of arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1102891"}},"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":"Q1375747$3AA5F920-0DBE-4DA9-9D6A-93CE7BB2438F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"07e283d1077c1371e38f97b5d0c2286f7cfb69c4","datavalue":{"value":{"text":"A normal form for arithmetical derivations implying the \\(\\omega\\)-consistency of arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1375747$9EC6D27D-2165-44BA-A8D1-3692EB9444BB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"093036cd514721fe1fe7ba3e588a11418fe03bab","datavalue":{"value":"0895.03024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$DE02C0DA-14A4-45BF-98B9-7C3113565777","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"67f276609d1b22783c31e8de118a086aea2965b9","datavalue":{"value":{"entity-type":"item","numeric-id":1277149,"id":"Q1277149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1375747$8432B989-47B6-4338-BEE4-DA3D2DF43671","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4644ee9c6c93e22a4aa2641411a372d7ea43bad8","datavalue":{"value":{"entity-type":"item","numeric-id":180651,"id":"Q180651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1375747$6D072FDB-00E9-4FD3-9515-E86B294C6820","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1f4edbc315b46accf8681ddd2933c397936bf8c2","datavalue":{"value":{"time":"+1998-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1375747$5FB463B0-4190-4BBE-BD9D-4A3239756C75","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f1b7da442569fd3abdb387987bb3a88d50575803","datavalue":{"value":"A derivation in Peano Arithmetic PA is strongly irreducible (s.i.) if it does not contain redundant free variables, redundant inductions (induction term is closed), redundant cuts (no cut formula is obtained by induction) or \\(\\forall\\)-antecedent with side formula derivable in PA. If an s.i. derivation of a sentence \\(\\neg \\forall xA(x)\\) is given, the lowermost \\(\\forall\\)-antecedent inference has side formula \\(A(n)\\) underivable in PA. Hence the proposition SI stating that every derivable formula has an s.i. derivation implies \\(\\omega\\)-consistency of PA. The author proves this proposition using induction up to \\(\\varepsilon_1\\) by the method of Gentzen's second consistency proof. The proposition SI extends the reviewer's normal form theorem from Ann. Pure Appl. Log. 62, 65-79 (1993; Zbl 0786.03040). T. Arai noticed that SI can be extended from PA to any theory and even to any finite sequence of increasing theories. This extension has an easy model-theoretic proof using ideas of the reviewer's paper [loc. cit.].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1375747$5E3CCCEE-31C2-4C43-9DCC-69AE257C391F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$8E0ECA0F-7D46-4B5A-9141-828E269A8D21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$2BE25705-9E03-4C6D-A8D4-1C6819615C2C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"742476ebe7318a8271fbf8790856083ff2d45f0a","datavalue":{"value":"1102891","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$C6803476-C23C-40A4-85A0-1E4A158FBB9B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"29ce1fefb40819e807bb1256377328519e155666","datavalue":{"value":"strongly irreducible derivations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1375747$AE0DFD81-B3E8-4F4A-BAB9-2AF62442D5D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1375747$8EE0941F-B059-4311-9517-846CC9D74AA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9da5cc793147a473f75d83c548f4d52dcf2e1560","datavalue":{"value":"\\(\\omega\\)-consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1375747$DA4E5583-45E9-4F8D-A6B5-819C9DD33CEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9d8bc31c314d5d0bc758d21c21c5ec1118a6bc6","datavalue":{"value":"normal form theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1375747$482B4DFF-4F53-4EA0-8262-E91B6CF888AF","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1375747$378B4880-6D61-43EE-9DDA-5BE5CF3A2EDB","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":"Q1375747$AC63CCD9-0443-427C-B7EE-026E0C91A18F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"75baa2517b9bfa5a48d20ac71ec44260e2ec6841","datavalue":{"value":"https://doi.org/10.21099/tkbjm/1496163242","type":"string"},"datatype":"url"},"type":"statement","id":"Q1375747$0458FEFB-0A10-4B2A-A478-D72CFC768EC7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c4bc491ff048cdced43b54516cd7e7b0e3f6330","datavalue":{"value":"W377128222","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$0CE789D7-D16B-4B94-BE48-225C8A7490F5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d878f782365ce45046340fdabf3978d4af785c04","datavalue":{"value":"10.21099/TKBJM/1496163242","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1375747$9B3AE515-74FF-45A7-A0F5-46FEFEBF97A8","rank":"normal"}],"P1643":[{"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":"2c0b1f406219fa6276c0ebcdb7a9934452870c09","datavalue":{"value":{"amount":"+0.93471247","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$A44B224E-5BEE-4B3F-967D-445F4987BE6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba0e8bd64e7c43c2c3853d7a87188d980ea52e44","datavalue":{"value":{"entity-type":"item","numeric-id":1277150,"id":"Q1277150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1808640fa5d0cf6728147415bef44aa361b7fdae","datavalue":{"value":{"amount":"+0.8801909","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$09508D50-FE05-4B54-8A33-BFDB7DD630CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0285b1c03c9b3972ae14ca8db863da41233c811a","datavalue":{"value":{"entity-type":"item","numeric-id":3593501,"id":"Q3593501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10e3f1dee64e2908b45ddd82fc71c30d07984b29","datavalue":{"value":{"amount":"+0.8710958","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$B8E930D3-B4D7-48A7-9CB3-92DA24C2E8AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d41218928b8e812851ddfaaa5e2bdc5d7db555a0","datavalue":{"value":{"entity-type":"item","numeric-id":5704007,"id":"Q5704007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d9ae3c05cb4ab2ad255f6b2e80003841fda2c96","datavalue":{"value":{"amount":"+0.8669102","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$F6C6A5C8-1051-4075-8A5F-6779473554B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea5f5bb423a10705dd76c66bf44abada43e76174","datavalue":{"value":{"entity-type":"item","numeric-id":5361247,"id":"Q5361247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e85eb6a9b15266a76b33776c11213846ceee52e","datavalue":{"value":{"amount":"+0.8666131","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$328EAF29-44E4-4375-AE93-1D9CC1721CAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46837bc29d87c3d7145f5a48f5ff17d766dc2ebe","datavalue":{"value":{"entity-type":"item","numeric-id":4397029,"id":"Q4397029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"863546832a0ce3ffd93cd27e39a293e500aed224","datavalue":{"value":{"amount":"+0.8647427","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$4DB3464B-0407-4D79-8260-844919FEE612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d379272fd586084fcc0dfe56e611e00c99324d56","datavalue":{"value":{"entity-type":"item","numeric-id":5895465,"id":"Q5895465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8ba7cb8b278f9a483efa45af4b7a36689a18073","datavalue":{"value":{"amount":"+0.8604909","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$4B7F473D-2E9D-4995-9883-DBF9F64A562E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff978e7d78e7110203870fe27b9716653d963cb2","datavalue":{"value":{"entity-type":"item","numeric-id":3366964,"id":"Q3366964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a66e09b1f37f78cc48023118877ee810dceeb718","datavalue":{"value":{"amount":"+0.8597154","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$F4042597-8515-4429-8672-7A90B6DB409E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d62968ef23715f8b586506f65ed13ddb83c3586a","datavalue":{"value":{"entity-type":"item","numeric-id":1064076,"id":"Q1064076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"385b36ae66d53ab0a50841df29230dde3f154e2d","datavalue":{"value":{"amount":"+0.8579506","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$956DCBBC-E9A9-4E61-9387-76DD3B05312B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aecdd27b198190ff3ad89c3388c78e942d0fe973","datavalue":{"value":{"entity-type":"item","numeric-id":3714071,"id":"Q3714071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2944cd6f7c9e31099d0ef1d2f4a9746c6868af61","datavalue":{"value":{"amount":"+0.8568734","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1375747$A1F01004-E8F6-416E-B133-AC7F52FE4D44","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A normal form for arithmetical derivations implying the \\(\\omega\\)-consistency of arithmetic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_normal_form_for_arithmetical_derivations_implying_the_%5C(%5Comega%5C)-consistency_of_arithmetic"}}}}}