{"entities":{"Q1407590":{"pageid":1418330,"ns":120,"title":"Item:Q1407590","lastrevid":67372452,"modified":"2026-04-12T17:11:18Z","type":"item","id":"Q1407590","labels":{"en":{"language":"en","value":"A Gentzen-style axiomatization for basic predicate calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1982513"}},"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":"Q1407590$B5D0C98E-5528-4ABC-93EE-CC5A5A941D27","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8099911839f071f4371d4b52bfb36759af8b3e6d","datavalue":{"value":{"text":"A Gentzen-style axiomatization for basic predicate calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1407590$3D6E093C-401A-44D2-A08C-6CE305A7B890","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"741d761cc8dd95344b07aec86c1e41e1fd7b16d7","datavalue":{"value":"1022.03041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$65A3BB88-E201-47E3-B1BB-D2BD099B5212","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97260bea1cba66249f833040ae752d88bb9782d","datavalue":{"value":{"entity-type":"item","numeric-id":227771,"id":"Q227771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1407590$D347ED71-6709-445A-B616-FBE8175C0B36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e63f0f7326486d44dfb43d06e0b528a89a70ef2c","datavalue":{"value":{"entity-type":"item","numeric-id":190271,"id":"Q190271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1407590$06B25563-8A4B-4A7C-8523-C24844EC7F1E","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":"Q1407590$70E753B6-3952-42E8-98C3-B559A36CFB73","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":"Q1407590$1564FCBC-6510-45C7-A929-49F50A247103","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"39c4fb86a2969507100d423d4e7d736d4235b81d","datavalue":{"value":"Basic Predicate Calculus, BQC, was introduced by \\textit{W. Ruitenburg} [Mod. Log. 1, 271-301 (1991; Zbl 0748.03037)] as a first-order extension of Basic Propositional Logic, BPL, invented by \\textit{A. Visser} [Stud. Log. 40, 155-175 (1981; Zbl 0469.03012)]. Basic Logic is a proper subsystem of Intuitionistic Logic, in which Modus Ponens is weakened. The original axiomatization of W. Ruitenburg [loc. cit.] is in sequent notation.   We introduce a Gentzen-style sequent calculus axiomatization for BQC. Our new axiomatization is an improvement of the previous axiomatizations given by the second author [Aspects of basic logic. PhD thesis, Marquette University, Wisconsin, USA (1995)], in the sense that it has the subformula property. In this system the cut rule is eliminated. This cut-free sequent calculus for BQC induces a cut-free sequent calculus for BPL as well.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407590$4DBBC08F-EB9E-4D22-B965-C7039156689C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b9efdfa0f087fce6a282d8b305885f05ac6182e5","datavalue":{"value":{"entity-type":"item","numeric-id":190271,"id":"Q190271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1407590$3C9CCBCE-241B-4555-91D9-A544232AD21C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$892861E3-F6C6-41BB-9B8D-D949871E43F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$F3BED286-0B04-49DA-914A-1EE4D8850F42","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c7a28053b4c9137cd47825e568d35754ca2773e","datavalue":{"value":"1982513","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$C3AC2F4F-BFA6-4402-9EAB-0DD78371D36B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09a28e75ab931b9ffe29155c5e6687d39ffef800","datavalue":{"value":"basic predicate calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407590$2F05E252-87D7-4BCF-BF1A-BCBD8E8EEB31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ea5e6f0e4a8b7d0c9c070cbea310ccb5c3d1521","datavalue":{"value":"Gentzen-style sequent calculus axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407590$B607C85E-AC3D-4D3D-A90E-C3C11905CF71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f74920537862e25960045b173a4c530000d4686b","datavalue":{"value":"subformula property","type":"string"},"datatype":"string"},"type":"statement","id":"Q1407590$1564AFA1-7AFF-415E-843B-5ED19A23EF30","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":"Q1407590$618293BA-2C24-46F6-8521-C5134F53ECDD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0cb2eff0572bea1e583e5f3c4569be81e6002d70","datavalue":{"value":"https://doi.org/10.1007/s001530100132","type":"string"},"datatype":"url"},"type":"statement","id":"Q1407590$7BD879AC-4E02-467A-BDC5-C3D56FF359A3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0159dbd0b76260e48ec4dbf192bbbc1a05e80cbd","datavalue":{"value":"W2087545875","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$BE92266C-E9D3-4B5E-873B-01F557459ED8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f780bd6489d678d15c19bc21af4ef06b1ff04449","datavalue":{"value":"10.1007/S001530100132","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1407590$14A78A85-49EA-4AB3-BF19-EC5A0A50EE3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6df41cd6c74face84bc0ff3cb52f91efcdff94ab","datavalue":{"value":{"entity-type":"item","numeric-id":5954710,"id":"Q5954710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66c23fd65f3deedd12d9c3d369f695340c48631e","datavalue":{"value":{"amount":"+0.7888824343681335","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":"Q1407590$CB20CC60-18DB-4967-BF04-948CE2E55B22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3d941cfe33d3e609a14150a673ce6ef6960cc6f","datavalue":{"value":{"entity-type":"item","numeric-id":5283964,"id":"Q5283964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"999d9e8a6d8dc1c0482b8fc3f53457f765f8b064","datavalue":{"value":{"amount":"+0.7888823747634888","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":"Q1407590$5D18B06C-B678-47ED-9B9C-47BA22B8E3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cb715c729e8655e70cf5553a833fa9957798e06","datavalue":{"value":{"entity-type":"item","numeric-id":1868483,"id":"Q1868483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"980f57e4a8243fe2b26178595b1aa2e2f2c51cd9","datavalue":{"value":{"amount":"+0.7815278768539429","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":"Q1407590$5E843AF3-C01A-4E51-81DF-5E6B84F330A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0af9fb8634c709b6d0b064576ce077b74d56fe7","datavalue":{"value":{"entity-type":"item","numeric-id":5937805,"id":"Q5937805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2a4cca67d4ac6af5782503b47b761fcf0a08eb8","datavalue":{"value":{"amount":"+0.7797520756721497","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":"Q1407590$070770BE-F711-43D0-B241-05C104AF6F77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b63fba6c25cfaaa4ccda4bc08ce583296f8d5264","datavalue":{"value":{"entity-type":"item","numeric-id":1300007,"id":"Q1300007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"895a661fb8ab9f70dc3e4e4466cbe47f4efecfe0","datavalue":{"value":{"amount":"+0.7564935088157654","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":"Q1407590$E5E7BF5F-B6EA-495F-8F9F-C587DA8965D4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Gentzen-style axiomatization for basic predicate calculus","badges":[]}}}}}