{"entities":{"Q2503325":{"pageid":2514068,"ns":120,"title":"Item:Q2503325","lastrevid":44227956,"modified":"2025-11-21T01:35:31Z","type":"item","id":"Q2503325","labels":{"en":{"language":"en","value":"Eigenvariables, bracketing and the decidability of positive minimal predicate logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5054317"}},"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":"Q2503325$BBC2B799-D0D0-42B5-A4DC-05A3C3BA39D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"615410c61453c93692a7c7e270e552f104276ae7","datavalue":{"value":{"text":"Eigenvariables, bracketing and the decidability of positive minimal predicate logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2503325$E934E484-85F9-4ED1-8819-CC32E61C3228","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4ea3e4ab6a489585b9db3463d9bef51f259adeef","datavalue":{"value":"1106.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503325$2A614B5C-7218-43A4-B027-D67174BE93CC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$DDDCB1C2-59F3-4F94-8E4B-92BFE1E111CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c9994e22132749d99397bc99150caa21bed2ae3","datavalue":{"value":{"entity-type":"item","numeric-id":457561,"id":"Q457561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$9008D206-3F8C-445C-896F-3FD153EE0D19","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$E4CB2C6F-629D-4C7F-A4D6-036E5785B406","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f4ffc608ada8e4a14c4a7ac75bb9921c404be25","datavalue":{"value":{"time":"+2006-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2503325$AB950F2B-380A-4AA4-91EC-B934DA5EB282","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f924dcea16395a9ba1cd62c4733475f99d957860","datavalue":{"value":"Positive formulas of predicate logic considered here are constructed from atomic formulas by \\(\\&,\\to,\\forall\\) in such a way that all occurrences of \\(\\forall\\) are positive. The authors give a new proof of the result by the reviewer [Proc. Steklov Inst. Math. 98, 135--145 (1968; Zbl 0208.01101); translation from Tr. Mat. Inst. Steklova 98, 121--130 (1968; Zbl 0179.01102)] that the derivability problem for such formulas in the intuitionistic logic is decidable. As a consequence a new proof of decidability of the inhabitation problem for positive types in system F is obtained. The new proof like the old one establishes that every sufficiently high derivation \\(d\\) contains a pair of sequents, \\(S\\), \\(S'\\), such that \\(S'\\) is situated above \\(S\\) but can be contracted to \\(S\\) by some substitution for variables. In this case the derivation \\(d\\) can be simplified by (making the substitution and) throwing away the part between \\(S'\\) and \\(S\\). Now this is done by introducing a scoping mechanism into cut-free rules and proving the new formulation has a kind of a subformula property.   In the reviewer's opinion, the proof is still not transparent enough. Scoping looks like replacement of universal quantifiers (in the conclusion) by existential quantifiers (in the premise). According to a recent result by Baaz and Iemhof positive existential quantifiers admit Skolemization in intuitionistic logic with the existence predicate. This is probably enough to prove decidability for formulas with only such quantifiers. It is to be seen whether these considerations allow one to simplify the author's proof.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$D19949B4-E80A-4D50-901D-0757D2751DD2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503325$DF78FB82-EB40-4188-A094-292E35AD3043","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eb862b60966c5bb2682b7e76306ca437decd4560","datavalue":{"value":"5054317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503325$11114F40-19CC-4FF2-9E53-60D91BF7BD03","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab7456a6500678da2c11297409c3d94f7b6af242","datavalue":{"value":"minimal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$D01AF341-F596-4797-8D92-6B7E2EE01212","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"826cb17a61389397478ca005848e294acb35a0eb","datavalue":{"value":"system F","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$BC0F496F-6E57-421F-B4DF-B6DFD8BC9DFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$543C9153-FB03-49A3-8DFC-C19267E75B2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d4794e4bf81f1d7560698ea49a899e8054e49af","datavalue":{"value":"positive quantifier","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$A9865CC5-5F47-4512-B85F-1BF49FA7B7A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"940be6b117e12709d851ae4ad68c25d16c23957d","datavalue":{"value":"bound variable","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$9C8ADF27-A645-4DDB-B244-F3CFB9811DEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503325$D3D795FC-FABA-4F35-BB82-B384A36CD817","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$DDFCD49C-958C-4060-BD81-5305BDFB0C6A","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":"Q2503325$38797805-D296-48CF-9041-A36EB6FEAF34","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e82dfad3847d6c075c5e65c8fc2db75bd9f5e13","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2006.01.053","type":"string"},"datatype":"url"},"type":"statement","id":"Q2503325$D373A635-0EFB-4BD2-BB6C-031524D850BD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f710fd97a8c69aee8c700d6b77df38fc146cdf3a","datavalue":{"value":"W1988222104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503325$C3842A7E-EA08-4B1B-8832-43ACFCBA43F3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$1CBF70B5-FFD9-48CF-A04F-983F87831474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$54736709-33BF-4A89-BE3D-CCBD79CCC2CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bfe9da59c4fc807075c2be119f4491e61f66a45f","datavalue":{"value":{"entity-type":"item","numeric-id":4924544,"id":"Q4924544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$2D18FD37-34FD-483E-B57D-02C93AD4EF7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe4c1ea89bc5854f421d3a6b161146d5aecefa12","datavalue":{"value":{"entity-type":"item","numeric-id":4032862,"id":"Q4032862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$69CE1963-05DE-456F-8DDC-B8CAB43D8AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$F04F1538-BE7B-4A47-AFE4-CAC9DC168C82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff96c37a66afe1add790c14afe39b8faf5825da","datavalue":{"value":{"entity-type":"item","numeric-id":4133591,"id":"Q4133591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$3064B216-D368-4DFC-9B9F-359673034D3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f09c5d69de1399b2c035e1c5f68d80d6f8fc608","datavalue":{"value":{"entity-type":"item","numeric-id":2543316,"id":"Q2543316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503325$567AAD36-ACE2-4BB9-9AB0-09ACBA8BD94D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"facca931b618dde183e6d6ae505a11403dc45531","datavalue":{"value":"10.1016/J.TCS.2006.01.053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503325$85BF5810-AE09-4FA4-B8B3-78F54E995AA8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e78eb6d32875241f8067dfa254eae86c137df5a","datavalue":{"value":{"entity-type":"item","numeric-id":4924544,"id":"Q4924544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa3fdd9b304bfa10b863f4f93b6e696246db4589","datavalue":{"value":{"amount":"+0.81175053","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$AC0EF5D3-8C53-405E-9BBB-433CB7A11C38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"695f34571625ca38cd79b2228faa0850d88fd21b","datavalue":{"value":{"entity-type":"item","numeric-id":2773020,"id":"Q2773020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44af92bd94ea0f566f2c2da36adad8e32ccb73ef","datavalue":{"value":{"amount":"+0.7847856","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$C2ACC6A5-B6A6-4993-BFFF-81BBEB3EFEEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ebc073a48b6987817115c78d815f192b93a56d6","datavalue":{"value":{"entity-type":"item","numeric-id":5013624,"id":"Q5013624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"607ec8834c49921eccb862cad8afbdc59adb36da","datavalue":{"value":{"amount":"+0.74466974","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$60A692C8-9011-4950-AAC9-5F0BFA42638E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"294459af80b98063f91bf0b4cd53afee0990ec82","datavalue":{"value":{"entity-type":"item","numeric-id":4934025,"id":"Q4934025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f21446d9a7e6883917226bd05a4129c13904eb47","datavalue":{"value":{"amount":"+0.7397659","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$911B28FC-7FDE-4CBC-9BFB-AD0500BA44DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c31b0dbb454505d2a45dde5949ba09b184f05e9b","datavalue":{"value":{"entity-type":"item","numeric-id":4451641,"id":"Q4451641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6c5facbf915d637f5002f5b568b1b1b05f27bf5","datavalue":{"value":{"amount":"+0.7355225","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$041F1D31-3CB9-4B61-9378-967CCD3B3A40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"406a1b1e13b995afab3f3ac7e9a54d6e9fe89571","datavalue":{"value":{"entity-type":"item","numeric-id":3455187,"id":"Q3455187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eec63d4157377a68b9038cedf72340b43044ecca","datavalue":{"value":{"amount":"+0.73491955","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$83A1B42F-9F21-4AB5-8359-C5426AB80252","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78ad54f389797b2ee7a4ccd1ba1858a39c2fbfda","datavalue":{"value":{"entity-type":"item","numeric-id":2115288,"id":"Q2115288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0b4a46cd12d24f2f4936395c38c11636909d96e","datavalue":{"value":{"amount":"+0.7345961","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$3F0527D0-AF57-4CB7-9064-FF3EE3E734A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d0da00c684ba2a68bf78df92650025cd849d39e","datavalue":{"value":{"entity-type":"item","numeric-id":813081,"id":"Q813081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1368385cd3fd5d8d1a823cbc5a43011552c48cdf","datavalue":{"value":{"amount":"+0.7332977","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$F3263B8C-26CE-4695-8729-6CC9167E7D8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a4864029d3f3e7ef13a37a39590e6ca060fe0cf","datavalue":{"value":{"entity-type":"item","numeric-id":5241405,"id":"Q5241405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e179a38bd60cf04316ddbbdca25461717dbc86d","datavalue":{"value":{"amount":"+0.73304874","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2503325$6142380D-9515-45AD-AD32-03FF29B33EEB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2503325","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2503325"}}}}}