Fine Selection for Intuitionistic Modal Logic

Abstract

We extend Fine's selection method to the setting of intuitionistic modal logic and use it to provide a model-theoretic proof that Fischer Servi-style intuitionistic $K4$ has the finite model property.

arXiv commentThis version corrects various typos and inaccuracies which, while minor, affected legibility. Notably, the definition of $\Sigma$-trees was missing, the definition of admissibility had an order relation reversed, and the ordinal assignment required adding one to ensure monotonicity