Axiomatic Classes of Intuitionistic Models
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.
Written in honour of Douglas Bridges on his 60th birthday.