Quantifier elimination for a class of intuitionistic theories (Q948760)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Quantifier elimination for a class of intuitionistic theories
scientific article

    Statements

    Quantifier elimination for a class of intuitionistic theories (English)
    0 references
    0 references
    0 references
    0 references
    0 references
    20 October 2008
    0 references
    It has often been assumed that intuitionistic theories admitting quantifier elimination are `nearly classical' since Smoryński 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ïssé-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.
    0 references
    0 references
    quantifier elimination
    0 references
    intuitionistic theory
    0 references
    Kripke model
    0 references
    Fraïssé-homogeneous
    0 references
    countably categorical
    0 references
    intuitionistic universal fragment
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references