{"entities":{"Q948760":{"pageid":950608,"ns":120,"title":"Item:Q948760","lastrevid":65562579,"modified":"2026-04-12T03:27:03Z","type":"item","id":"Q948760","labels":{"en":{"language":"en","value":"Quantifier elimination for a class of intuitionistic theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5353774"}},"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":"Q948760$E58BDDD1-4056-40B0-90DE-A722EBFC6923","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cdd393c7464a81fc104a71ad86addf21f58ca97d","datavalue":{"value":{"text":"Quantifier elimination for a class of intuitionistic theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q948760$873F4B62-1787-445A-9D40-ECB3756A037D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae8a5620d60c315234cf3675573f06c30885f314","datavalue":{"value":"1159.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$F121492F-67F8-42CB-9049-1AC0C120850C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"977855a77dd4b2c70c6d151337c7626686eb28d5","datavalue":{"value":"10.1215/00294527-2008-012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$26FA1AC3-C1B1-40BF-88B5-54F7B57A5CFA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad458c6c629fc25ac62cfc6a77aca8b8a64c97c2","datavalue":{"value":{"entity-type":"item","numeric-id":948757,"id":"Q948757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q948760$C8A2C6DD-8218-4896-B663-CFE7435920CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"032d7a0be61b75c74aa24a1bfcdf87c4dc2440df","datavalue":{"value":{"entity-type":"item","numeric-id":948758,"id":"Q948758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q948760$EB412D65-B1CB-4B5A-AC25-FA9422857AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0d39fa0da6f58ae33c03a8e37dc3dedbdaa15937","datavalue":{"value":{"entity-type":"item","numeric-id":948759,"id":"Q948759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q948760$1CE77386-9806-42F6-B29C-E47524A9F845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"02d955a17ce895bcc975b0ea6d4eead2e64dcf81","datavalue":{"value":{"entity-type":"item","numeric-id":190250,"id":"Q190250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q948760$9CA650CB-7763-4E50-8A21-548136CF160E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q948760$6A1FB90B-975F-410C-8A3B-A9AB0ED76EA0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"972c0debb1697683b9c4c88fe396e38e44a8d438","datavalue":{"value":{"time":"+2008-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q948760$B2077C94-56E9-4F04-B498-287E23833647","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"04cc0ed3e88ba2aa67ad53081871dce6e603641b","datavalue":{"value":"It has often been assumed that intuitionistic theories admitting quantifier elimination are `nearly classical' since Smory\u0144ski and Bagheri studied the problem focusing on such theories. In this paper, however, `very intuitionistic' theories are constructed so as to admit quantifier elimination by extending the former work of one of the authors, Ruitenburg. In the classical case, certain theories over finite relational languages, called JRS theories here after Jaskowski, Rabin, and Scott, are known to admit quantifier elimination. So, given a classical JRS theory, the authors construct a Kripke model by featuring that a JRS theory is Fra\u00efss\u00e9-homogeneous and countably categorical. The intuitionistic theories determined by Kripke models thus constructed are, in fact, shown to admit quantifier elimination as well as to be complete including negations of some classical tautologies. Thus the theories enjoy several interesting characteristics, among which their intuitionistic universal fragments are investigated in particular. For example, the axioms to determine them are given explicitly.","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$F1835792-A2A4-4958-ABA6-806E5463BCA3","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":"Q948760$B5D245DE-B0BC-49E8-87C5-4F4F2BA953B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$D0660766-BCC9-4852-B18F-4678F5943E00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d40823595f671f8f347825fd0adc1e31ebeb184f","datavalue":{"value":"03C35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$7BCC3898-7FFA-4BA7-8651-6AF936BE5AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed0e9d16aabdfc4de2754948a872b6ceb30bba56","datavalue":{"value":"03C90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$7A8E98FC-78B0-4512-B125-B39688F3C11E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$B01CC1CB-5599-4DD0-939D-BE0F0D82B209","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8ed05d7b4df695307b2e44041ca6cc77408854cd","datavalue":{"value":"5353774","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$58FA0865-BB79-4177-8358-AEC08085A9F2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ce94254d44045733e962d2861c33d94e3725cca","datavalue":{"value":"quantifier elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$85CEF5FE-C4CD-4CA2-9C60-826A1F439129","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da855445b59cae389fca494b963c3ccb8b3796aa","datavalue":{"value":"intuitionistic theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$7381D13F-3FD8-426E-8FF3-7BB16C559027","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3875c79fa835ac45a1818de05c1bd8b1020c938e","datavalue":{"value":"Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$1102967B-8A47-44F7-B3D8-D534579C40EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc1f1e018c44c237869f692e1ee5690904aa399f","datavalue":{"value":"Fra\u00efss\u00e9-homogeneous","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$E0D2154C-07F8-4222-92BC-16D8B5E8C842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"853260a5a1522d218675c402b7b5ec3c088331d7","datavalue":{"value":"countably categorical","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$5D7B5FC0-F5AD-429F-830D-D5BBAFCFA082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b62133b2f49bbb654c86b3a60774a663b94dc6f3","datavalue":{"value":"intuitionistic universal fragment","type":"string"},"datatype":"string"},"type":"statement","id":"Q948760$F83B2993-E274-44DB-8965-FC23CDB00336","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":"Q948760$B3C03F04-B3C6-45D6-B4D5-D21671D587F7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b38869ffe13c7fb63d54fecfbb449db4ddc8e55f","datavalue":{"value":"https://doi.org/10.1215/00294527-2008-012","type":"string"},"datatype":"url"},"type":"statement","id":"Q948760$50585EC2-08CD-46F0-A991-9489AC41615C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7254cd0475a401e27c18749a329ff99d55657095","datavalue":{"value":"W2141172560","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q948760$C61ED175-9BEE-420E-AB3E-36BA7B06EE26","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e15dd422b4066bc6fe07d73b57cc5fa46096bd0","datavalue":{"value":{"entity-type":"item","numeric-id":487231,"id":"Q487231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33478c904d37ec7939aec12e6939a3f3dc1034d7","datavalue":{"value":{"amount":"+0.8984994292259216","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":"Q948760$702D17AD-6944-4F22-8E16-8F6036F86EE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e2cf4809c433f270014c1fdcfd424b293f573b7","datavalue":{"value":{"entity-type":"item","numeric-id":5393630,"id":"Q5393630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a71271d846cde14beb3ac29ec551379e3931a04","datavalue":{"value":{"amount":"+0.8569570779800415","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":"Q948760$65CBCD2A-2BE2-447B-A613-DE4873DEC777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa04e1abdcff11c16e19bb03d7b93d9984dd5262","datavalue":{"value":{"entity-type":"item","numeric-id":5109215,"id":"Q5109215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8bec81d0d973feade6e7972083655cad9b1aab0","datavalue":{"value":{"amount":"+0.7815536260604858","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":"Q948760$37CCDE1D-2215-4FD9-A421-72382F097C88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ec5213c8f6b5fccca029138e7378d6f4b02e518","datavalue":{"value":{"entity-type":"item","numeric-id":3520241,"id":"Q3520241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3930ab354be451728c574c8d2c82b11bae70b3f","datavalue":{"value":{"amount":"+0.76142817735672","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":"Q948760$5440520A-CA01-478C-BCB3-7F30CD02C2AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7a2f9922d5061b80fae17ab5f2047cc077af168e","datavalue":{"value":{"entity-type":"item","numeric-id":3684111,"id":"Q3684111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aebe76096622a6b065477b2aac49b392c3eb918d","datavalue":{"value":{"amount":"+0.7596832513809204","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":"Q948760$C5605E5D-FDA8-408F-BC4F-B97DCC52BC8F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantifier elimination for a class of intuitionistic theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantifier_elimination_for_a_class_of_intuitionistic_theories"}}}}}