Quantifier elimination for a class of intuitionistic theories (Q948760)

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.