{"entities":{"Q2367413":{"pageid":2378156,"ns":120,"title":"Item:Q2367413","lastrevid":43953912,"modified":"2025-11-18T12:02:04Z","type":"item","id":"Q2367413","labels":{"en":{"language":"en","value":"A normal form for logical derivations implying one for arithmetic derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 243577"}},"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":"Q2367413$54979554-620A-43F5-BCE8-BD8BA9525914","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1803bf63017e3f9b8d79702693bb99676b848fe9","datavalue":{"value":{"text":"A normal form for logical derivations implying one for arithmetic derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2367413$4F5ED085-80A8-4B4A-AC35-134159F9CCB8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b61425985bc146e5e1614ab47ad289886c15cec2","datavalue":{"value":"0786.03040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$6C3A1DBB-D413-4F2C-8037-D8D53349714F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"be49226047b71cbcff613ad756387383a72f5d6f","datavalue":{"value":"10.1016/0168-0072(93)90188-J","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$A4584ECA-2D86-4B26-9ABA-1B84D8B0F36A","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":"Q2367413$6B2DAF1E-5460-4E97-AE42-5A1675261D2E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2a03d7e72c2f27d8f30f9a3e566010dcf9193975","datavalue":{"value":{"time":"+1993-08-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":"Q2367413$3E46CCF7-C5F1-4A7B-BD2A-82F59FAC7B67","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fcaf12900fdd9601a890b15b280a218221e1a662","datavalue":{"value":"The main result of this paper is a refined normal form theorem: a provable sequent has a cut-free derivation with the proper variable condition (i.e. a variable in the derivation is either an eigenvariable or occurs in the last sequent) and with the main formula restriction (i.e., no main formula of the antecedent is derivable). The author first proves the existence of such a derivation model-theoretically, and then the normalization theorem (that giving a procedure for converting a given derivation into a normal one) via an infinitary calculus. The results and methods are applied to systems of arithmetic. One result is that a derivation in arithmetic can be replaced by one that satisfies the proper variable and the constant normal condition (i.e., in each induction rule the induction term contains a variable). As a consequence, an existential statement is provable without induction, if it is provable at all. A normal form theorem of a more elaborate kind is proved; and the extendability of these results to the intuitionistic and the higher-order system is explained.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$575AADC5-2103-41FF-96C9-CA3B4A476478","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$737E6940-1D76-487A-8DA9-DFE27F93D3E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$272CE555-CA70-4C44-9EF9-91207120608D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"99540c484cd75e8fee931f882e9d98c9501a545b","datavalue":{"value":"243577","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$93944248-6773-4CED-8CEB-400C47ABDB1D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$071FA445-FDA0-4519-92F3-AA805EC7221F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fa6661322f0d303a91284f2db4c6cf4667ee15","datavalue":{"value":"constant normal condition","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$145C248F-362C-4EF3-84C2-F26BE252F29C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9d8bc31c314d5d0bc758d21c21c5ec1118a6bc6","datavalue":{"value":"normal form theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$056506DF-110C-4B17-87A4-A052046D1512","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"964bdf5f3eca7c6c742933186138f32c66f4456c","datavalue":{"value":"proper variable condition","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$2CB8854E-AB8D-4360-96AF-017D9C91813E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e06942484a31af91a065f33ec09e7146676d4517","datavalue":{"value":"main formula restriction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$C9C1F7CF-9D1C-44EA-A300-253CCB520FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a0e0509b775158dc74b6a66af9b55040c03cc06","datavalue":{"value":"systems of arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2367413$BEA75B2E-5394-4B9E-BC1E-A32F2B5FBC10","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":"Q2367413$EFDF4658-FECE-4831-B227-FC34FF77FC13","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":"Q2367413$925671B9-3AA7-4985-9DC3-D2ECF3EDBB60","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c89e08f8e981b15d9e994bd9b66679f47871eb79","datavalue":{"value":{"entity-type":"item","numeric-id":5528627,"id":"Q5528627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367413$1CF28824-CB8E-4601-9EEE-9BB5C95F204A","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":"Q2367413$73BF8B92-7D01-4D76-90A6-3944CDD6D4F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d71305c8d9d041668e564bf7f2f69f04f88a1b7","datavalue":{"value":{"entity-type":"item","numeric-id":3822154,"id":"Q3822154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367413$6D3C9206-BA63-4F78-B11D-A0E476B0054B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9547e59e05241ce90e2002baca31499468810e3","datavalue":{"value":{"entity-type":"item","numeric-id":1577482,"id":"Q1577482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367413$DCE99E95-FDF7-4A5C-ADDC-824FFEAD89D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367413$45587FE2-F635-41D5-B674-726981F3297B","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":"Q2367413$32256AF0-AC73-4EF3-A115-3A87A5F78784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2367413$97CD2E5A-EAB4-46F1-BB69-0D923F0F1D7F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"43786dfb31c8eb9e3ce335ff0e335be2a7e5317b","datavalue":{"value":"https://doi.org/10.1016/0168-0072(93)90188-j","type":"string"},"datatype":"url"},"type":"statement","id":"Q2367413$D3DE3A16-E2CE-4C74-86BB-A3C2D419900E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2009ddc38c76e3511281bf8f57f3b5f4d835ce10","datavalue":{"value":"W2044156752","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2367413$350583DB-3E7A-4702-84FC-6126AC7D8EA8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"705e116050a0b7d8bac2dd51199a018f56175755","datavalue":{"value":{"entity-type":"item","numeric-id":1375747,"id":"Q1375747"},"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":"Q2367413$60785116-83F8-468F-B78E-597EE28C471B","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":"c0450f38f582d3cafe1cfdeb80c505620672e7e2","datavalue":{"value":{"amount":"+0.90456873","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":"Q2367413$0D7058B1-20E2-462F-8EC4-A141A01F09AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"933f31e0f582d4b33184ff8b7c003da49410303c","datavalue":{"value":{"entity-type":"item","numeric-id":1575930,"id":"Q1575930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9208984a7d02a78913949ca477200b8c56f9d459","datavalue":{"value":{"amount":"+0.88899803","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":"Q2367413$C3640CF6-90FF-408C-AEC6-807AC86A7604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09ec02c7d07ea4068b497ad4a87518a0249b32b7","datavalue":{"value":{"entity-type":"item","numeric-id":1029828,"id":"Q1029828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c38620e80a54316480bfa9da7981e67d51b49bc","datavalue":{"value":{"amount":"+0.8813943","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":"Q2367413$15FE8D4D-04BD-4D1C-8697-A7811CA9966B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f7ac57d23a992d88a8dfc8139388242c56f90a5","datavalue":{"value":{"entity-type":"item","numeric-id":1903133,"id":"Q1903133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44ce425db75b05e2ae3d1545cb6f329114e0e993","datavalue":{"value":{"amount":"+0.87920135","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":"Q2367413$19155B32-8589-473D-8657-CB431B315408","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":"df89e9fdc157b551f64f97861365a893be36f4a0","datavalue":{"value":{"amount":"+0.87906563","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":"Q2367413$5D782F3F-46F8-4C55-A68F-1B6980030A4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c599caf01e5abee016c0ed4cd58a814d9b0a546","datavalue":{"value":{"entity-type":"item","numeric-id":4607851,"id":"Q4607851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec5c7e64e0bd3d3042f3b8e2ad290a9d2b85b292","datavalue":{"value":{"amount":"+0.8786488","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":"Q2367413$2D4CEDC9-CCF7-4C51-97C6-371EBEDCBA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6dba9f748e3403d6dcafa58273bddf207696922","datavalue":{"value":{"entity-type":"item","numeric-id":1267849,"id":"Q1267849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0d3002d4ba680bde2dcabd94ef122f024295bb7","datavalue":{"value":{"amount":"+0.8782656","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":"Q2367413$FE286A94-523B-49A6-9860-BAF80050B7A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7aa2766298d4a67b56a1f300df3b109a9b40f45f","datavalue":{"value":{"entity-type":"item","numeric-id":5704814,"id":"Q5704814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a329d77dc43d2e4ec3470f02c94894252af9ff0","datavalue":{"value":{"amount":"+0.87362355","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":"Q2367413$E000F2F2-72CD-4779-85FF-6F3FF87CBA41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e11fdb3fbafb3d15064f88dab69c60ebe7b3da8b","datavalue":{"value":{"entity-type":"item","numeric-id":4944873,"id":"Q4944873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"092003615c9c38c9bf82df40104da3d146c87a61","datavalue":{"value":{"amount":"+0.87345964","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":"Q2367413$A29DCF6D-DB20-450A-B6D2-86445E3B1C21","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2367413","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2367413"}}}}}