{"entities":{"Q284219":{"pageid":285986,"ns":120,"title":"Item:Q284219","lastrevid":60642696,"modified":"2026-04-10T18:14:51Z","type":"item","id":"Q284219","labels":{"en":{"language":"en","value":"A semantic approach to conservativity"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6581386"}},"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":"Q284219$9D89AAB1-5533-4BBB-9B5E-D4196709823A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"df18a6e301126c682993125c042c652ecee03c42","datavalue":{"value":{"text":"A semantic approach to conservativity","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q284219$8CF5F927-3358-44FB-9CFA-34D3FDB81057","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"78347f98a8335cca17d0f0496f3121f8164ff0b8","datavalue":{"value":"1414.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$1EF7A44C-C00C-48ED-843C-DA493A25DC54","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a35120a6a454e23e128ae3826feb53523f2ec7d","datavalue":{"value":{"entity-type":"item","numeric-id":190318,"id":"Q190318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$3AB38200-FE08-43DA-B7A8-9606C935B410","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$04008859-5D6E-4933-BF7F-C9CA44642BC2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f158d900e6e0544baa84834e48185c69f362c02f","datavalue":{"value":{"time":"+2016-05-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q284219$E9830E55-2E18-4C38-95E5-176374782990","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"21502805e24ce12bbeb27faedf128ff69357c314","datavalue":{"value":"http://hdl.handle.net/20.500.12128/12862","type":"string"},"datatype":"url"},"type":"statement","id":"Q284219$E05FAAE3-5AD3-4CB4-B5C6-D05AA9E3F25A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bfda15a1afd1090ea077a2b46fd085df86cd9462","datavalue":{"value":"If \\(\\mathsf T\\) is a set of first-order sentences, then \\(\\mathsf T^c\\) and \\(\\mathsf T^i\\) are closures of \\(\\mathsf T\\) under classical and intuitionistic derivability, respectively. \\(\\mathsf T^c\\) is conservative over \\(\\mathsf T^i\\) with respect to a class of formulae \\(\\Gamma\\) iff \\(\\mathsf T^c\\) and \\(\\mathsf T^i\\) contain the same formulae in \\(\\Gamma\\). In the paper, the problem of conservativity is described from a semantical point of view. A Kripke model \\(\\mathcal M\\) is called \\(\\mathsf T^c\\)-normal if every world in \\(\\mathcal M\\) is a classical model of \\(\\mathsf T^c\\). The class of formulae \\(\\mathcal P(\\mathsf T^i)\\) is defined as the smallest class that contains all atomic formulae, all formulae decidable in \\(\\mathsf T^i\\) and is closed under disjunctions, conjunctions and existential quantification. The class of formulae \\(\\mathcal G(\\mathsf T^i)\\) is the smallest extension of \\(\\mathcal P(\\mathsf T^i)\\) closed under the following rules:  \\begin{itemize} \\item[1)]~if \\(B,C\\in\\mathcal G(\\mathsf T^i)\\), then \\(B\\land C,B\\lor C,\\exists x\\,B,\\forall x\\,B\\in\\mathcal G(\\mathsf T^i)\\);  \\item[2)] if \\(B\\in\\mathcal P(\\mathsf T^i)\\) and \\(C\\in\\mathcal G(\\mathsf T^i)\\), then \\(B\\to C\\in\\mathcal G(\\mathsf T^i)\\). \\end{itemize} The class \\(\\mathcal A(\\mathsf T^i)\\) is defined as the class of formulae of the form \\(\\forall\\bar x\\,(C(\\bar x)\\to\\forall y\\,D(\\bar x,y))\\), where \\(C\\in\\mathcal G(\\mathsf T^i)\\) and \\(D\\in\\mathcal P(\\mathsf T^i)\\).   The first main result is Theorem 4.10. If \\(\\mathsf T^i\\) is complete with respect to a class of \\(\\mathsf T^c\\)-normal Kripke models, then \\(\\mathsf T^c\\) is conservative over \\(\\mathsf T^i\\) with respect to the class \\(\\mathcal A(\\mathsf T^i)\\). This result provides a new proof of \\(\\Pi_2\\)-conservativity of \\(\\mathsf{PA}\\) over \\(\\mathsf{HA}\\), that can be proved by the negative translation together with the Friedman translation. Another consequence is \\(\\Pi_2\\)-conservativity of the fragment \\(\\mathsf i\\Delta_0\\) of \\(\\mathsf{PA}\\), where induction is restricted to bounded formulae, over its intuitionistic counterpart.   The second main result is Theorem 5.6. If \\(\\mathsf T^i\\) is closed under the Friedman translation and complete with respect to a class of conversely well-founded Kripke models, then \\(\\mathsf T^c\\) is conservative over \\(\\mathsf T^i\\) with respect to the class of formulae of the form \\(\\forall x\\exists y\\,A\\), where \\(A\\in\\mathcal P(\\mathsf T^i)\\). If, in addition, \\(\\mathsf T^i\\) is complete with respect to a class of conversely well-founded Kripke models with constant domains, then \\(\\mathsf T^c\\) is conservative over \\(\\mathsf T^i\\) with respect to the class of prenex formulae whose matrix is built from atoms by means of disjunctions and conjunctions.   Applications of the presented results to the constructive set theory \\(\\mathsf{CZF}\\) are considered.","type":"string"},"datatype":"string"},"type":"statement","id":"Q284219$F2487EE4-2A39-4B23-BF8A-FD7AD1CFAC1C","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":"Q284219$385B7AA7-D45B-4008-B611-4BF448CD172A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$DF92F978-1119-4CDF-81AD-22F9325D40DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$DE0B56A1-10C0-44E0-93F8-2F7E518C34D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$833052AB-FFB6-4186-B887-CE38691E9059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$2ACEBA5B-8BE5-4832-AB35-E6A91E6DD413","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$EEB8A150-9A27-4A5A-BF41-48E3ACC5A71B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$A15F11B3-25EC-4EF9-8FE8-D110A43E2C59","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ffa82400ebe348e226a9a07c6b5788ced1936d97","datavalue":{"value":"6581386","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$CE6B2A3F-B9F6-436F-9FD0-A212B800F5EA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc250090bedef36702b8d1834607bcddf9d768f5","datavalue":{"value":"classical first-order theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q284219$76905CC3-632A-4C99-B61A-BBA4B4F8B98F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4178b3ba5a81639d9a1bc80c0409ce6f093b5f06","datavalue":{"value":"intuitionistic first-order theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q284219$9E92BC23-86A5-4C32-856D-2D0F40956335","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4108cecd289b9cafbcb28752da70c2315de2efa0","datavalue":{"value":"conservativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q284219$6A162D97-5F42-4C7B-9DF5-FDA43482DE74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4078614c737f77e34731be764c56affada452b","datavalue":{"value":"Kripke models","type":"string"},"datatype":"string"},"type":"statement","id":"Q284219$302C0861-A52E-48FD-93A3-06EB4B57E302","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":"Q284219$7BB28698-A48A-4935-A89F-623FEDC5F6C9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d2e7118f9470f2155c4757890943393fd30d94b0","datavalue":{"value":"W2259501815","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$D872B0D1-BEA5-43FD-84D5-291EA18B3BF3","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e8d6f68046b1a17044210cf98e4c517d195280a1","datavalue":{"value":"Q59472670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$25EF600A-AF2E-4F07-BEAA-DE51F5BB1059","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"74605135c388db78d4d0ca86dc0cd54881585bea","datavalue":{"value":{"entity-type":"item","numeric-id":4073362,"id":"Q4073362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$FC434DF9-BAFC-4456-8028-48EE7D18EBD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb13f0e26bedc43a55f423a26969b5bdef66af80","datavalue":{"value":{"entity-type":"item","numeric-id":2710607,"id":"Q2710607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$FC27182A-D6B2-4B8A-91BA-32DF22DC6BD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80ccd5e47c36eb1694ba8279960f4a7853e4783b","datavalue":{"value":{"entity-type":"item","numeric-id":4458699,"id":"Q4458699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$91647126-43FE-4EB9-9460-A4B43C0FD434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeabed2c5dd7a8e91b52e149a40328caf3f8ee89","datavalue":{"value":{"entity-type":"item","numeric-id":685055,"id":"Q685055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$9FEFCAE5-4DC8-41C8-A2E8-AA4DFC12D96D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a20b645023a8d04cad0a14618e2426e86442be9","datavalue":{"value":{"entity-type":"item","numeric-id":4704759,"id":"Q4704759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$BC616A9A-23FB-40FF-B29B-63E2B47B39FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3166a1df231f17c0eace0ec4a3cd14533d6a0c5e","datavalue":{"value":{"entity-type":"item","numeric-id":1095140,"id":"Q1095140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$C192DDE4-3568-4ED0-907A-D8C6056761C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20078d69304e2df97ca3f40332c8d92086a6b541","datavalue":{"value":{"entity-type":"item","numeric-id":4179016,"id":"Q4179016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$44AF8092-CF81-4470-B762-9B6F1DED1DE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b90652611bb87db6f860be6c2c24c2aff0b53d0","datavalue":{"value":{"entity-type":"item","numeric-id":2267746,"id":"Q2267746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$BB17D717-A118-4DB0-889F-2784F05169F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4cd05a5bb7d332da97edf12f388e172ca0e59424","datavalue":{"value":{"entity-type":"item","numeric-id":1165235,"id":"Q1165235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$01648B2E-77FD-46DB-8EDF-6A2B2FE1BD71","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":"Q284219$189C99DD-8B06-442E-956C-CB039941C78C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"921b0db5e3dfc0c82f961ade9450e75882bb3a65","datavalue":{"value":{"entity-type":"item","numeric-id":5944052,"id":"Q5944052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$176C85D9-1801-4D8A-8C8C-7EF1FB5BD11C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88559a63a1c31b5a4a97af4cd21b41e1e98c56c4","datavalue":{"value":{"entity-type":"item","numeric-id":1355126,"id":"Q1355126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$58327244-A2C3-4C67-BC62-BAA40723A0B2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a576b9842e1dca191cecf6ce5aefb7328c79a2b","datavalue":{"value":"10.1007/S11225-015-9639-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q284219$82EDEBFE-79C5-4CEA-B837-3928EAAC537F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37e2e3d3d01d535308144338fdf338dd31042dd0","datavalue":{"value":{"entity-type":"item","numeric-id":2710607,"id":"Q2710607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70f0adbb9c9015de4a410f82291d54e27a8ba3df","datavalue":{"value":{"amount":"+0.8181856870651245","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":"Q284219$8687CD8B-3B9E-4F92-94FA-9258EA818818","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07aac25750eff53e5ccca8bee0eed4f1d1c3ba04","datavalue":{"value":{"entity-type":"item","numeric-id":4254637,"id":"Q4254637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac9d2ec2623c7fba87188ca811986e1299855c1b","datavalue":{"value":{"amount":"+0.8179431557655334","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":"Q284219$08FEA1B5-9A02-4BCB-BBD7-1DD245B7FD11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e84c35779661add7a6abbd96f21884a9be35c2ed","datavalue":{"value":{"entity-type":"item","numeric-id":4458699,"id":"Q4458699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d0f4061b61dbb6579f7261793c17f068c2f83ca","datavalue":{"value":{"amount":"+0.7988027930259705","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":"Q284219$2970C565-6B86-422B-9DC1-F8F5AE3C6382","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"871c9d2b03851eb10cf068fd138c1322c19e796b","datavalue":{"value":{"entity-type":"item","numeric-id":4704759,"id":"Q4704759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fb771e605a9be1e4ec27c0e8cd5e3ee359189dc","datavalue":{"value":{"amount":"+0.7931889295578003","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":"Q284219$5D278674-BDDD-4FD2-B2C5-1CD4515CF522","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe0d34b6b41f86704ba74a39eccb5da6b0970ce2","datavalue":{"value":{"entity-type":"item","numeric-id":964451,"id":"Q964451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a79bafa31d1ce66c062226583bd250d02a13dbb5","datavalue":{"value":{"amount":"+0.7885968089103699","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":"Q284219$63739F09-7365-4DC6-AB3E-7FFF038C211F","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q284219$DA0ECDCD-72C8-4611-AB37-976CFA3A7840","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A semantic approach to conservativity","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_semantic_approach_to_conservativity"}}}}}