{"entities":{"Q2377348":{"pageid":2388091,"ns":120,"title":"Item:Q2377348","lastrevid":51761867,"modified":"2026-01-19T21:43:09Z","type":"item","id":"Q2377348","labels":{"en":{"language":"en","value":"Gentzen's consistency proof without heightlines"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6182636"}},"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":"Q2377348$B17CAD64-37F9-4F0C-93B0-6BC60D8BD11C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e141149da0974a9306e790126b1e43a588480c8","datavalue":{"value":{"text":"Gentzen's consistency proof without heightlines","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2377348$9223A135-888C-485D-9359-D98E0FD6563C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d5883bcc57d32b5a3680f3bed75de8ea7ccb895b","datavalue":{"value":"1275.03151","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$8FB6F3C8-AD7C-495E-B448-43EE65FDA4DA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ea68be1d5bbf01a939b97478f823720bfc73a97b","datavalue":{"value":{"entity-type":"item","numeric-id":1734261,"id":"Q1734261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$D2B07748-BC70-4C56-8AB7-FBEED3C98FD0","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":"Q2377348$A3378384-173D-4C2A-8ED2-35600CFC031D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b3abb5fb4ae7972a30f51c8d6a09a9ae6d81d017","datavalue":{"value":{"time":"+2013-06-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2377348$BDC2EBE2-1101-4D9F-AB05-288932BB4BBC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b35249b9b6d6139382dc1388866a9987ec2a8fcf","datavalue":{"value":"A proof of the consistency of a sequent calculus for intuitionistic arithmetic is proposed. The proof is based on the Gentzen-style assignment of ordinals to the derivations but does not use the so-called heightline argument, which means that the ordinal assigned to a sequent depends on the height of the sequent. Instead, the techniques proposed by Howard for G\u00f6del's system \\(T\\) [\\textit{W. A. Howard}, in: Intuitionism Proof Theory, Proc. Summer Conf. Buffalo N.Y. 1968, 443--458 (1970; Zbl 0206.28202)] is used. Namely an expression is assigned to every sequent and a vector of expressions is assigned to a derivation. Further, the first expression in the vector is interpreted as an ordinal. The author describes a procedure of transforming derivations of the empty sequent which reduces that ordinal. This provides the consistency of the system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2377348$89B90420-B5D5-488B-9F29-9ADF4CCE2F80","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b1f73afd33192153e94113807fdc62b87cbaa1ee","datavalue":{"value":{"entity-type":"item","numeric-id":234728,"id":"Q234728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$476EC97D-AF4F-4A2A-B922-7F53B0115585","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$E1F11A35-FD02-47DD-A669-8559BE1649E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$98B07D82-D473-4041-A44C-3F29077148D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$656C8437-9B68-45DE-9566-A9E13EBF3B2B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1e43c7a7c33ae9efe92d62ac3d00522b6ce9055f","datavalue":{"value":"6182636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$B7D8FC93-FEF9-4F01-8C2E-B6B4E5379B10","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52c2513afc8941299b07e63a5555cd1e7cb85f4a","datavalue":{"value":"consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q2377348$7EF9E674-ABC9-4448-9CA7-20E70FAC0532","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"880189f3ab141434ac60dc229df6c4a00e086156","datavalue":{"value":"intuitionistic arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2377348$2F46A711-E355-4D11-9221-604BA1F0658F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2377348$AD3B4A9F-95AA-4015-9C7A-34931CD83834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"853379d0912686f111cd19da1a52b80fa8eb82fd","datavalue":{"value":"ordinal assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q2377348$A210FEB6-D897-423E-8179-B2CC1927E5B1","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":"Q2377348$817B0293-2EA6-405B-82BA-4405EE3A34CE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b33ee25636e7d3f09ec0f80a24a7dfa72c2a5e58","datavalue":{"value":"https://doi.org/10.1007/s00153-013-0324-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q2377348$45F1ABF2-3F86-4071-B534-CFDF5B89F15C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8a7ee64cdfa0d75d6648991426d13f24f06013ea","datavalue":{"value":"W2057428959","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$A7386A8B-6DA8-4403-86B3-4E25F957050D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"47e897bc8b0383e0be621508dc47975da8303b0c","datavalue":{"value":{"entity-type":"item","numeric-id":4487267,"id":"Q4487267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$A62EBE38-E161-40D8-95CC-941202F3CAEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"889750e6b63c62516f108fd0d35f770cecc8f256","datavalue":{"value":{"entity-type":"item","numeric-id":1264579,"id":"Q1264579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$34F9A0A3-FE9C-4A01-BA43-7144817C8D1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$4E3303CB-2611-46BA-9BCC-A1BAFAD88518","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"197f75f5cd86020e5cc4ef15f910d8be341c9f00","datavalue":{"value":{"entity-type":"item","numeric-id":5606582,"id":"Q5606582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$D322DEEF-B949-442D-9C14-31B4E9F9F2A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69db4f067537cf0b31837c2e33b8f5372d860fa8","datavalue":{"value":{"entity-type":"item","numeric-id":3066292,"id":"Q3066292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$A7D4A10F-5E31-4FA0-871D-6D418453DED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"361e0f23746829e48ff0ff918b87727856cdb536","datavalue":{"value":{"entity-type":"item","numeric-id":5928308,"id":"Q5928308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$4BA09E90-28E8-4741-88D5-42D8984DDFD8","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":"Q2377348$35C1914F-E05F-45F0-BB48-49DB34FAF55A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41cd514c7fef51007a2f09307276ec6ee7e61b6a","datavalue":{"value":{"entity-type":"item","numeric-id":5361248,"id":"Q5361248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$BBD86E1D-B8BC-43AA-AFB6-4EFC662E4333","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":"Q2377348$4B00E2CE-0F5C-416F-8F6F-EF1A6CE7C36D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"556c63d3d5fbb69adda2aaeb321f31370f38a3b9","datavalue":{"value":{"entity-type":"item","numeric-id":4716271,"id":"Q4716271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$ECFD451A-0406-4240-94FB-77354DA7223C","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":"Q2377348$FFF6E669-477D-497E-8FA8-AD958DF4A0B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9a595a4c9d433fdf3e30cd6620a0174e21c57c3","datavalue":{"value":{"entity-type":"item","numeric-id":2881086,"id":"Q2881086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2377348$1136882B-AE0B-4260-8CD0-5F4F90DC4899","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8f874665581c1317c3018a8b5c25591187be7cbb","datavalue":{"value":"10.1007/S00153-013-0324-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2377348$C9671082-3F31-44EF-8830-6B31CD3F8928","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0864c587ffd0671a32cb3927c84ad701eea3be1f","datavalue":{"value":{"entity-type":"item","numeric-id":5361248,"id":"Q5361248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"756a8d72b50bb0ca59013e0b3b85954f2ef81416","datavalue":{"value":{"amount":"+0.903018355369568","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":"Q2377348$47945DCD-224C-4BEB-B489-029DC0A9DAFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"945ff30d1bfaf814e2be4227312eea6ee3a8471d","datavalue":{"value":{"entity-type":"item","numeric-id":3066292,"id":"Q3066292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a0954aa07855e8ea29f9033a8de8b659ed2879d","datavalue":{"value":{"amount":"+0.8464437127113342","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":"Q2377348$07F30A70-0425-44EA-AA2B-86C0DD6A2E13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9639ab7c12ae1d3ef2752b0098d545c404593755","datavalue":{"value":{"entity-type":"item","numeric-id":5361245,"id":"Q5361245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22590766db5cae340245d540fd3f55cd8a26fef6","datavalue":{"value":{"amount":"+0.8346430063247681","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":"Q2377348$D3923E0C-9184-4430-95AB-2593EF36A5C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"675d2a5c1b5b1fec2702dd72052797e2b642cf07","datavalue":{"value":{"entity-type":"item","numeric-id":4656552,"id":"Q4656552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4dba212fb677986a7ecee9f5d5aae3b7da59700a","datavalue":{"value":{"amount":"+0.8224000930786133","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":"Q2377348$A3215CCC-7C47-4F3D-AF0E-BA893F1284D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18a1363b9fb4769d2729b14d5535843556213fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5221860,"id":"Q5221860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"234346e1cb612815a10cee1421bb445b124c8909","datavalue":{"value":{"amount":"+0.8133878111839294","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":"Q2377348$1C475CA9-FA10-47F6-8A6C-14CD44EF14AA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2377348","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2377348"}}}}}