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
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
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