{"entities":{"Q1407599":{"pageid":1418339,"ns":120,"title":"Item:Q1407599","lastrevid":67372533,"modified":"2026-04-12T17:11:21Z","type":"item","id":"Q1407599","labels":{"en":{"language":"en","value":"Two measures for proving Gentzen's Hauptsatz without mix"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1982521"}},"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":"Q1407599$B42DB361-6DE9-4314-80FB-D30ED9BB889F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8dc075d88181800960dc6cf21bc579627ade5555","datavalue":{"value":{"text":"Two measures for proving Gentzen's Hauptsatz without mix","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1407599$A72BED6B-616A-419A-A3D8-8F6994FEA171","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bdca07bfe998b8185a12893ab530509e1ed51136","datavalue":{"value":"1032.03047","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$3266FA1C-EC61-468F-9951-40694BEC5B03","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1804bbd961ab7085fcd6ebdf3ab03cf98686f33e","datavalue":{"value":{"entity-type":"item","numeric-id":818515,"id":"Q818515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1407599$2D574AD9-93C5-4AE9-9BA6-B50FCA740019","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":"Q1407599$0AF86636-7552-476F-A651-1B2FFB3CDD69","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f7841ad7b9ae7c226290004bcfbbaa03cb759e96","datavalue":{"value":{"time":"+2003-09-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1407599$49C87268-502B-4B0C-9D44-7E3BD393CD8B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0636d2108119548313ecc4cda20819b08b67f9d9","datavalue":{"value":"The paper under review continues the investigations of two earlier papers which are concerned with the proof of Gentzen's Hauptsatz without using the mix rule, as Gentzen did, but only the cut rule. While in Ann. Pure Appl. Logic 99, 105-136 (1999; Zbl 0933.03074) the author considered intuitionistic predicate logic, the author, \\textit{K. Do\u0161en} and \\textit{Z. Petri\u0107} introduced in Math. Struct. Comput. Sci. 10, 99-136 (2000; Zbl 0949.03054) besides the degree of a derivation a new definition of the rank of a derivation and treated intuitionistic propositional logic by nested recursion on degree and rank. In the present paper, this method is applied to classical and intuitionistic predicate logic and compared with the procedure of \\textit{J. von Plato} [Arch. Math. Logic 40, 9-18 (2001; Zbl 0968.03065)], who defines the concept of height instead of rank.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407599$F0E293BE-CCC8-45E0-A4C7-743BA58160EB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$11496B25-84E9-488E-9667-AAAC59949A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$EE9D0996-654A-412B-80EF-94411E195CB5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f809be33624fee7eae1ed14b357da8551ce72f53","datavalue":{"value":"1982521","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$41697A83-6EC2-48DC-A503-999C9F1F1141","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a582b271730779c6294f3a3210c34575070cd3db","datavalue":{"value":"proof of Gentzen's Hauptsatz","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407599$4A729DAC-6C2E-48D6-B8AC-BA28EF4C01F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6916fe340f58b9757a3775333a547be8eda738b7","datavalue":{"value":"cut rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407599$6CF5FC4A-2548-4207-9EA4-85C781AEE3AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"71ea74009f3e6aaad2fb0fc06728d00ab11f397c","datavalue":{"value":"predicate logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407599$2B73C858-DEE9-4EFA-96B1-BCA8F8AA92ED","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0580dd4129e5d6439921b513d45494c072f33534","datavalue":{"value":{"entity-type":"item","numeric-id":1288968,"id":"Q1288968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1407599$3F5A4C49-4C15-41F2-9600-C581C4BD79BC","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":"Q1407599$199FE640-8FBA-48AE-B244-E7D2AD691D07","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ad92e44064f8b5b7cbb76ac2bedef95995f5be45","datavalue":{"value":"https://doi.org/10.1007/s00153-002-0155-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q1407599$2F9B9F67-551A-42D9-A03F-FB36E6201EA4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aa9dd37fdbdd6c1465321da6c698150b04763d6a","datavalue":{"value":"W262380895","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$A5A3DC7C-3C4C-41B7-8C1A-198DE7B8A3FA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fe5827d1114b4f9a166f231cc71c98b2f5a07ccb","datavalue":{"value":"10.1007/S00153-002-0155-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407599$9DD6FD37-1117-4E2F-B157-65BB1C500A50","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec41fbcf6227cb9b98d3720513a93678334e98b2","datavalue":{"value":{"entity-type":"item","numeric-id":4451468,"id":"Q4451468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c70d294adbd7d1dd81f7172ab1ba8e37104f22c","datavalue":{"value":{"amount":"+0.8292736411094666","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":"Q1407599$CD2424BD-3E4C-40C1-B375-8AE23D66FF6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d0ad7d09102dd774ae4b161237a1d15424c1d5e","datavalue":{"value":{"entity-type":"item","numeric-id":5928308,"id":"Q5928308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e486466646115aca01f25a2351d9a6a2abd2433","datavalue":{"value":{"amount":"+0.7811366319656372","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":"Q1407599$8DA6CD5D-925B-45D2-9F1F-4297C40871D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b8dcd8df300661aa3bb06e3c099f7fcec67e20b","datavalue":{"value":{"entity-type":"item","numeric-id":1304543,"id":"Q1304543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc55f9cdd8bc97bf583cb0f7dcdf8bcae81a31ed","datavalue":{"value":{"amount":"+0.7703618407249451","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":"Q1407599$62604598-4C48-4D91-8986-428212DF5487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4174c62b7c21511ab671733659148743a7870e3","datavalue":{"value":{"entity-type":"item","numeric-id":5187274,"id":"Q5187274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2647d9a8ec3b871cfe043453f5baadfcf24a610a","datavalue":{"value":{"amount":"+0.7700155973434448","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":"Q1407599$2914D280-30B9-490B-B9F1-9552C9D01020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46c7a541b68918b526a220e9952b282fb0a3d087","datavalue":{"value":{"entity-type":"item","numeric-id":2377348,"id":"Q2377348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7ccc6acb48ebdef275117de991a3a1f6dc47166","datavalue":{"value":{"amount":"+0.7443215250968933","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":"Q1407599$4E757BAF-1175-4501-B758-067571151764","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Two measures for proving Gentzen's Hauptsatz without mix","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Two_measures_for_proving_Gentzen%27s_Hauptsatz_without_mix"}}}}}