Axiomatic Classes of Intuitionistic Models
Date
Authors
Goldblatt,Robert
Journal Title
Journal ISSN
Volume Title
Publisher
Journal of Universal Computer Science
Abstract
Description
A class of Kripke models for intuitionistic propositional logic is 'axiomatic' if it is the class of all models of some set of formulas (axioms). This paper discusses various structural characterisations of axiomatic classes in terms of closure under certain constructions, including images of bisimulations, disjoint unions, ultrapowers and 'prime extensions'. The prime extension of a model is a new model whose points are the prime filters of the lattice of upwardly closed subsets of the original model. We also construct and analyse a 'definable' extension whose points are prime filters of definable sets. A structural explanation is given of why a class that is closed under images of bisimulations and invariant under prime/definable extensions must be invariant under arbitrary ultrapowers. This uses iterated ultrapowers and saturation.
Keywords
intuitionistic logic , Kripke model , bisimulation , disjoint union , prime filter , ultraproduct , iterated ultrapower , saturated model