Quantifier elimination for a class of intuitionistic theories

From classical, Fraisse-homogeneous, (≤ o)-categorical theories over finite relational languages (which we refer to as JRS theories), we construct intuitionistic theories that are complete, prove negations of classical tautologies, and admit quantifier elimination. The technique we use considers Kripke models as functors from a small category to the category of L -structures with morphisms, rather than the usual interpretation wherein the frame of a Kripke model is a partial order. While one can always "unravel" a functor Kripke model to obtain a partial order Kripke model with the same intuitionistic theory, our technique is perhaps an easier way to consider a Kripke model that includes a single classical node structure and all of the endomorphisms of that classical JRS structure. We also determine the intuitionistic universal fragments of these theories, in accordance with the hierarchy of intuitionistic formulas put forth in [9] and expounded on by Fleischmann in [11]. This portion of the thesis (Chapter 1) is the result of joint work with Ben Ellison, Jonathan Fleischmann, and Wim Ruitenburg, as published (up to minor structural changes) in [10].;Given a classical JRS theory, we determine axiomatizations of the corresponding intuitionistic theory in Chapter 2. We first do so by axiomatizing properties apparent from the behavior of the model, and discuss improvements to that axiom system. We then present another axiomatization, this time by axiomatizing the properties of quantifier elimination. We discuss improvements to this system, and show how this system and various subsystems thereof are equivalent to our first axiomatization and corresponding subsystems thereof.;In our original construction, the Kripke models contain every endomorphism of the underlying classical JRS structure and these theories admit quantifier elimination. The classical structure itself can be viewed as a Kripke model as well; one wherein the only morphism is the identity morphism. This intuitionistic theory (that also happens to be classical) also admits quantifier elimination. In Chapter 3, we determine whether other monoids of endomorphisms of JRS models give rise to single-node Kripke models whose theories admit quantifier elimination. We first show that if two monoids of endomorphisms have the same collection of finite subgraphs, then the intuitionistic theories of the corresponding Kripke models are the same. In so doing, we introduce a generalization of "bisimilarity", the standard notion of equivalence between Kripke models. We then give sufficient conditions on a monoid so that the intuitionistic theory of the corresponding Kripke model admits quantifier elimination.;Finally, in Chapter 4, we investigate the ramifications of adding nullary predicates to the language. Syntactically, this gives us a way to combine a classical JRS theory and its corresponding intuitionistic theory. Semantically, this gives us an opportunity to generalize our work to Kripke models with more than one node structure; specifically, where the node structures all satisfy the same "core" JRS theory, only varying in which nullary predicates they satisfy. We show that the theories of these multi-node models again admit quantifier elimination. For a given JRS theory in a language with nullary predicates, we construct a model that is in some sense universal. That is, all other multi-node Kripke models meeting certain other conditions in some sense embed into our model. We briefly discuss a theory that incorporates both a classical JRS theory and the corresponding intuitionistic version.