{"entities":{"Q701722":{"pageid":703571,"ns":120,"title":"Item:Q701722","lastrevid":48390352,"modified":"2026-01-04T14:11:46Z","type":"item","id":"Q701722","labels":{"en":{"language":"en","value":"Proof-theoretical analysis of order relations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2123149"}},"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":"Q701722$138467AA-5F18-4F7E-8670-16C8451AE893","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f213e129b466ef1995553280703f1356e748377f","datavalue":{"value":{"text":"Proof-theoretical analysis of order relations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q701722$6318FB6A-D1F6-4E8A-8359-508F4C2B362F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8569f7cc93b8c4241d09553880318d4018ab3d47","datavalue":{"value":"1062.03055","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$CA8349D5-11BB-4277-8432-3D3E1CCB8AA4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dd7f07ec51ef78a8fa09e4f3e464a2e7da011da3","datavalue":{"value":{"entity-type":"item","numeric-id":283114,"id":"Q283114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701722$3CF77A63-BCE8-4343-9F9C-9C76B9DCBBBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cc8bf89138092366dba76fbdf018c3e853b377d","datavalue":{"value":{"entity-type":"item","numeric-id":167888,"id":"Q167888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701722$25786120-6E0D-4A0E-B29D-659A2D0FD4EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5aad179d365c253d181fa8115a831f46e7923370","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701722$E58E9EAD-9A88-4836-9249-9D85E8F94F73","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":"Q701722$2A016298-5DFE-4E74-ABD3-6A8A8998F2E1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"df1e508a21ee9936a7a8f9defc1512d58443c3e3","datavalue":{"value":{"time":"+2004-12-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":"Q701722$B266BA51-3220-497F-BDBC-D65E8E448115","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2371fb39982ddb3289dd5731597947bb4cfc2d8f","datavalue":{"value":"In a previous work, the first and second author proposed a proof-theoretical treatment of axiomatic systems in a general setting by showing that a wide class of mathematical axioms are convertible into rules of inference added to certain contraction-free sequent calculi so that we can apply several establised methods of proof analysis in sequent calculi.   In this paper, the argument is enriched by some developments on duality of mathematical rules and on Harrop theories, and then applied to a concrete analysis of elementary theories of order relations. The main result obtained by the analysis is a conservativity theorem which gives rise to a proof-theoretical version of Szpilrajn's theorem on the extension of a partical order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is also shown by giving terminating methods of proof-search. Finally the third author discusses these results by an alternative approach, featuring the notion of entailment relation introduced by D. Scott.","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$7506E6E1-88E7-4254-ADB7-491397580D08","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701722$09992ABA-411B-4172-836C-AC5414CF42F6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$0AC21331-B01D-473F-AEAD-A468520E7CEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$F244D7AB-2EC5-4348-B562-2A7876A50C42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$B4C1281A-A13E-4E9A-803C-7A4A135F4328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24363e421bb7b6dfa7fe7a9b1ee54d8da8a06bf1","datavalue":{"value":"06A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$C71E2E3E-A2D6-464D-8A3C-2E9DF07964CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e037813de56311048f7e0a208650360505bf4d4e","datavalue":{"value":"06A06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$7FCC68F1-9087-48EA-878B-5DE3679CCB20","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ac74be9e4c67372ba70b58698f0d39dc4e263b61","datavalue":{"value":"2123149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$FE3E8356-C9E2-42FB-939B-0594FFD3CDA9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b8d03688e1e7c2319b370752e92f681b500fd30","datavalue":{"value":"sequential formulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$DE309D5E-E98A-41FA-92C0-96B6B26D65A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c2456278f9e0bda7a54d0c22c3615609094229a","datavalue":{"value":"proof-theoretical analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$AEB99AF5-3F16-4326-88AC-169622A39D4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15450cd7319138521c510d920a7e6edfc71eef83","datavalue":{"value":"elementary theory of order relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$CADC87C1-0548-4B4B-AADF-BE1F41593C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96293d2789e4b37fae1f0bf873740982c3157881","datavalue":{"value":"Szpilrajn's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$680DB8C7-A441-4AEE-BFC4-F5B99023551A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$1B8E896F-548C-46A7-9002-8B0D0F6C3D66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e641b2f2f094759207e4457d5599c8b1bae1e68","datavalue":{"value":"entailment relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q701722$85148D69-0DC9-4255-BFED-46ADC03C4138","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":"Q701722$D9D9F225-0DB9-474E-89AD-3469721E8057","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c7e8e69a5b8c912bab2940a8b49a0c08e3d411bb","datavalue":{"value":"https://doi.org/10.1007/s00153-003-0209-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q701722$DBD4DC0C-A3D1-47A9-B385-7B4048387ED9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"729b85e3a2c25a8fbecd610b980d75c02447e1ef","datavalue":{"value":"W1977180425","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$ACFF86E3-73AA-4EB6-864E-FE1B4314CEC9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"643dbe3b69f02959e6e6afd014fed65a80d0094e","datavalue":{"value":"10.1007/S00153-003-0209-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701722$A3FB81D5-313F-4E7C-849D-31E492D52965","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c56046bdc72732e22aa9317e29ec26f4633807b","datavalue":{"value":{"entity-type":"item","numeric-id":1818431,"id":"Q1818431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1452be582279990eacc9b0c62506575f65ffa50e","datavalue":{"value":{"amount":"+0.7706199884414673","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":"Q701722$D178B2F0-7ACE-4782-BEA7-AC80B1EA7DDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89155710b6e2357f5acf6e56c4462bc6488eca7d","datavalue":{"value":{"entity-type":"item","numeric-id":4552743,"id":"Q4552743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61f56cc3ab6f2a66f25bbdcaf7735129fbfba94f","datavalue":{"value":{"amount":"+0.7475720047950745","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":"Q701722$1F89B8EB-92F0-4AA6-8FA2-5B3EF296700A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7309f5abe6c6c959cb5d8cad420198bae933d237","datavalue":{"value":{"entity-type":"item","numeric-id":2743638,"id":"Q2743638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6dce8b423465a6fb91f845f207a7ac63023b937","datavalue":{"value":{"amount":"+0.7255282998085022","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":"Q701722$9DB2DCA4-B3BD-437B-98E8-EFA33757DE47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cc00a7e91cd4994df0dc90d1fe60cafbce2137a","datavalue":{"value":{"entity-type":"item","numeric-id":1425651,"id":"Q1425651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64511b7491f77f3170a4a18a79e216d306c83d28","datavalue":{"value":{"amount":"+0.725125253200531","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":"Q701722$8CD8353D-2E25-498C-BD33-F82343E64C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc88ee9e3471d08d60b99865d983c66b2380185c","datavalue":{"value":{"entity-type":"item","numeric-id":5739973,"id":"Q5739973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3635d8e60421a9bc59e9423a7a6022631e1b739e","datavalue":{"value":{"amount":"+0.7199999690055847","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":"Q701722$69833434-32D9-4CCB-B256-F740ED901151","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:701722","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:701722"}}}}}