DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV

Abstract

Rybakov (1984a) proved that the admissible rules of $\mathsf {IPC}$ are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.

1 Introduction

Think of your favorite logic. Now, remember the theorems and forget the rules. Is it possible to reconstruct the rules from this limited information alone? A good first try would be to consider all rules that yield the same set of theorems. ¹ This works out fine if you were thinking of classical propositional logic. Although you might have been thinking of different rules, you can be sure that they generate the just described set.

If intuitionistic logic is your logic of choice, this procedure likely left you sorely disappointed. Indeed, a good deal of the just defined rules will seem unfamiliar, surpassing most of the popular axiomatizations. The rule below is a good example: adding this rule to an axiomatization does not change the set of provable theorems.

(1) $$ \begin{align} {\neg\kern0.75pt} \chi {\rightarrow} {\phi} {\vee} {\psi} / ( {\neg\kern0.75pt} \chi {\rightarrow} {\phi}) {\vee} ( {\neg\kern0.75pt} \chi {\rightarrow} {\psi} ). \end{align} $$

There even is an infinite series of distinct rules present and it would be pretty safe to wager you were thinking of none of them. In the following, we present a proof showing that this set of so-called admissible rules, however wild, is decidable.

The admissible rules of a logic are those rules under which the set of its theorems is closed. They are the valid rules of a logic, defined only in terms of the theorems present, irrespective of axiomatization. This in sharp contrast to derivable rules, those rules where the conclusion can be shown to follow from the assumptions using the specific rules of inference available. Derived rules are strongly bound to an axiomatization, merely present by convention, whereas admissible rules are true invariants.

Although all derivable rules are admissible rules, the converse need not hold. Moreover, whereas derivable rules remain admissible—and indeed, derivable—when adding additional axioms or rules, the same cannot be said for admissible rules in general. This makes the notion of admissibility quite intricate, even in the case of logics as well-behaved as intuitionistic propositional logic.

In the beginning of the twentieth century, the distinction between admissibility and derivability was not yet widely perceived. Moh (1957) observed this confusion. ² He noted that, even though a rule might well be admissible, it need not be a “rule of procedure”; what we now call a derivable rule. Kleene (1952, p. 94) also made the distinction. He called admissible rules derivable and derivable rules directly derivable. He noted, as above, that only the latter kind need be preserved under extensions of the logic. The currently prevalent nomenclature comes from Lorenzen (1955), who introduced the term “Zulässigkeit”. This was quickly translated into the now commonly used term “admissibility” by Craig (1957). ³ Before we continue, let us give a formal definition.

Definition 1.1 (Admissible Rule)

A rule ${\phi } / {\psi }$ is said to be admissible in a logic ${\Lambda }$ when ${\vdash }_{\Lambda }{\mathord {\sigma }(\mathord {\phi })}$ entails ${\vdash }_{\Lambda } {\mathord {\sigma }(\mathord {\psi })}$ for each substitution $\sigma $ .

Early on, it was shown that the admissible rules of the classical propositional calculus ( $\mathsf {CPC}$ ) are all derivable, as discussed by Belnap and Thomason (1963) and Belnap et al. (1963). ⁴ The situation is much more intricate in the intuitionistic propositional calculus ( $\mathsf {IPC}$ ). Let us give a few examples.

First, let us think back to the example (1) given above. It follows through the work of Kreisel and Putnam (1957) that this rule is not derivable, yet Harrop (1956) proved that it is admissible. Recall that the admissibility of a rule need not be preserved when extending the logic. This rule is special in that regard, as Prucnal (1979) proved it to be admissible in all axiomatic extensions of $\mathsf {IPC}$ .

Note that the above rule can be generalized by replacing ${\neg\kern0.75pt} \chi $ with an arbitrary Harrop formula. Minari and Wroński (1988) proved that the resulting rule is admissible in all extensions of $\mathsf {IPC}$ . Not all admissible yet underivable rules are admissible in all intermediate logics. Take, for instance, the following rule which first appeared in the work of Citkin (1977) as a generalization of a rule by Mints (1972).

$$ \begin{align*} (({\phi} {\rightarrow} \chi) {\rightarrow} {\phi} {\vee} {\psi} ) {\vee} \theta/ (({\phi} {\rightarrow} \chi) {\rightarrow} {\phi} ) {\vee} (({\phi} {\rightarrow} \chi) {\rightarrow} {\psi} ) {\vee} \theta. \end{align*} $$

This rule is admissible in $\mathsf {IPC}$ , but it is not admissible in the Kreisel–Putnam logic $\mathsf {KP}$ , which is obtained by adding the implication corresponding to (1) as an axiom to $\mathsf {IPC}$ . ⁵ However, there are several extensions of $\mathsf {IPC}$ in which this rule is derivable, for instance the Gödel–Dummett logic $\mathsf {LC}$ .

The study of admissible rules is related to several fields within mathematical logic. First, the admissible rules of $\mathsf {IPC}$ relate closely to the propositional structure of Heyting Arithmetic. Through De Jongh’s Theorem, it is known that the propositional logic of Heyting Arithmetic is equal to $\mathsf {IPC}$ . This result has been reproven and extended numerous times and appears very robust. ⁶ One may wonder whether the propositional rules of Heyting arithmetic equal the admissible rules of $\mathsf {IPC}$ . Visser (1999) proved this to indeed be the case.

Second, the admissible rules of $\mathsf {IPC}$ are intimately related to the quasi-equations that hold in the quasi-variety generated by the free Heyting algebra. ⁷ A similar connection exists between the admissible rules of any algebraizeble logic and the quasi-variety generated by said logic’s free algebras. Admissible rules correspond, under this perspective, to the Horn sentences that hold in free algebras.

Finally, let us mention unification theory, in the sense of Siekmann (1989) and Baader (1992). In unification theory, one is concerned with unifying two expressions within a given language modulo a given theory. One could, for instance, try to unify an expression in the language of propositional logic to the expression ${\top }$ , modulo the axioms of $\mathsf {IPC}$ . This amounts to finding a substitution, called a “unifier”, that makes a given formula derivable. The problem of finding an algorithm that can generate the most general unifiers of a given formula modulo $\mathsf {IPC}$ was already posed by G.E. Mints in 1984. ⁸ Ghilardi (1997) illustrated how this syntactic endeavor can be expressed in a more algebraic and categorical manner. Using this new perspective, ⁹ Ghilardi (1999) solved the unification problem for $\mathsf {IPC}$ . This approach was later adapted by Iemhoff (2001b) to characterize the admissible rules of $\mathsf {IPC}$ .

It is easy to see that a formula ${\phi }$ is a theorem of $\mathsf {IPC}$ precisely if ${\top } / {\phi }$ is an admissible rule. As such, the study of admissibility encompasses the study of the theorems of $\mathsf {IPC}$ . It is well-known that the set of theorems of $\mathsf {IPC}$ is decidable; in fact, Statman (1979) proved it to be pspace-complete. Recall that admissible rules correspond to quasi-equations that hold in free Heyting algebras. As such, they form a subtheory of the first-order theory of Heyting algebras, which Rybakov (1985b) and Idziak (1989) independently proved to be undecidable. It is thus a natural question to ask the following, paraphrasing Friedman (1975, Problem 40):

Is there a decision procedure to determine whether a rule ${\phi }/{\psi }$ is admissible in $\mathsf {IPC}$ ?

An affirmative answer was given by Rybakov (1984a). His method proved extremely powerful, allowing him to answer analogous questions for numerous modal logics. Among those, the modal logics of the finite slice, treated in Rybakov (1984c), modal logics extending $\mathsf {S}4.2$ , treated in Rybakov (1984b), the modal logic $\mathsf {Grz}$ of Grzegorczyk (1964), treated in Rybakov (1987a,b, 1990b, 1991c), and the provability logic ${\mathsf {GL}}$ of Löb, treated in Rybakov (1990a, 1991a), deserve special mention. Later, Ghilardi (1999, p. 374) answered Friedman’s question through different means. Jeřábek (2005, Theorem 4.3) eventually proved that admissibility in $\mathsf {IPC}$ is coNEXP complete.

Besides answering Friedman’s question, Rybakov’s method can also be applied to tackle many problems related to admissibility, in particular the following four.

1. (i) The decidability of the universal theory of free algebras, treated in Rybakov (1992b, 1996).

2. (ii) Characterizing those extensions of a given logic that inherit all rules, as covered in Rimatskij and Rybakov (2005), Rutskii and Fedorishin (2002), Rybakov (1993), Rybakov et al. (1999a), Rybakov and Rimatskij (2002).

3. (iii) Describing a set of rules from which all others follow, as discussed in Rybakov (1985a, 1987b, 1995, 1999, 2001, 2004), Rybakov et al. (1999c, 2000a, 2000b), and Fedorishin (2007).

4. (iv) Giving a set of most general unifiers for a given formula, as treated in Babenyshev and Rybakov (2011), Odintsov and Rybakov (2013), and Rybakov (2011, 2013a,b).

In this paper, we describe Rybakov’s solution to Friedman’s problem. His original solution is expressed in the modal logic $\mathsf {S4}$ and transferred to $\mathsf {IPC}$ via the Gödel–Tarski translation. We present a direct solution, loosely based on the reasoning of Odintsov and Rybakov (2013).

The proof rests on one central concept, analogous to the notion of the bounded model property. One of the ways in which one can prove that the set of theorems of $\mathsf {IPC}$ is decidable is by constructing some complexity measure on formulae and showing that a formula is derivable in $\mathsf {IPC}$ if and only if it holds in all models whose size is bounded in terms of the measure of complexity of said formula. As a measure, one can take the number of all subformulae of a given formula. The following is a well-known result due to McKinsey and Tarski (1946, Theorem 1.11).

Theorem 1.2. A formula ${\phi }$ is derivable in $\mathsf{IPC}$ if and only if it holds in any Kripke model whose size is exponentially bounded by the number of subformulae of ${\phi }$ .

The decidability of the set of theorems of $\mathsf {IPC}$ can be derived from the above theorem, using the following two observations. First, one can effectively produce all Kripke models of some bounded size on the basis of this size alone. Second, given a finite model, it is decidable whether this model satisfies a given formula.

We present a notion of semantics for admissible rules in such a way that the above reasoning can be applied, mutatis mutandis, to the problem of deciding the set of admissible rules of $\mathsf {IPC}$ . There are three components to this approach: giving the proper notion of semantics, showing that one can effectively produce all finitely many models of bounded complexity and showing that validity of a formula at a model is decidable. The first three sections will be devoted to the first problem, the last section to the second. Once the appropriate notion of semantics is given, it will be clear that the last matter needs practically no thought. Although the number of sections might suggest otherwise, the technical difficulties lie mostly effectively generating all models of a bounded complexity.

Let us briefly go through the plan in some detail, without delving too deeply into the technicalities. Bear in mind that the plan is aimed at proving the decidability of the admissible rules of $\mathsf {IPC}$ . As argued above, this can be achieved in a natural manner by finding a suitably refined notion of semantics.

We provide an algorithm to effectively construct a set of Kripke models ${\mathcal {K}}_{\Sigma }$ to each finite set of formulae $\Sigma $ , satisfying the following two conditions:

1. Condition 1 The rule ${\phi } / {\psi }$ is admissible in $\mathsf {IPC}$ if and only if it is valid on all members of $\mathcal {K}_{\Sigma }$ , for any pair of formulae ${\phi }, {\psi } \in \Sigma $ .

2. Condition 2 The set of models $\mathcal {K}_{\Sigma }$ is finite.

3. Condition 3 Given a model in $\mathcal {K}_{\Sigma }$ , it is decidable whether a rule is valid on it.

Given a class of models and a notion of validity satisfying the above, the decidability of admissibility in $\mathsf {IPC}$ follows quite readily, as spelled out in Theorem 3.3. Our problem is thus reduced to finding such a class.

In Section 2, we describe, for each set of variables, a Kripke model that is complete with respect to the formulae using only those variables. This model is known as the universal model or characterizing model and is used extensively in the study of admissibility.

We define the notion of validity we wish to consider in Section 3 and inspect two classes of Kripke models that satisfy condition 1. The first class is that of the so-called exact models, which are, intuitively speaking, images of the universal model under maps that preserve the validity of all formulae. This class has the disadvantage of not being intrinsically described, leaving us in need of an effective definition of membership of this class, as required by condition 2.

Attempting to remedy this we switch to the second class, namely the class of extendible models. These extendible models satisfy a significant part of the defining conditions of the universal model. Very roughly speaking, if a nonrooted model can be embedded into an extendible model, then a one-point extension of said model can be embedded, too. When restricting attention to finite extendible models, condition 3 is clearly satisfied. We indicated that this approach is doomed to failure, leaving us in need of a more refined notion of semantics.

In Section 4, we refine the notion of exact models to adequately exact models. These models are, again intuitively speaking, images of universal models under a maps that preserve the validity of but a fixed and finite set of formulae. In general, the validity of all formulae is not guaranteed to be preserved. We show that this notion satisfies both condition 1 and 3. At this point, the difficulty lies in proving the completeness direction in condition 1, which follows from a standard filtration argument. This notion, like that of exact models, is not intrinsically defined, which makes it hard to see whether condition 2 is met.

Finally, in Section 5, we remove this last limitation. We introduce the notion of adequately extendible models, in analogy to the notion of extendibility of Section 3. It is easy to see that this notion satisfies both condition 2 and condition 3, yet the validity of condition 1 is not apparent at all.

We prove that the notions of adequate extendibility and adequate exactness actually coincide. The one direction, from adequate exactness to adequate extendibility, is rather straightforward. The other, however, requires considerable work. We devote a great deal of space to the proof, including many remarks that aim to aid one’s intuition. After this, all conditions have been met and decidability thus follows.

The main contribution of this paper is an exposition of Rybakov’s approach to Friedman’s problem. Rybakov’s approach has proven to be both powerful and of great applicability and it has given rise to numerous results over the past three decades. We explain the concepts used in this approach and explain their usage in one of the most basic settings, that of intuitionistic propositional logic. We claim no originality in the results presented here; instead we offer originality in presentation. The purpose of this exercise is to clarify and celebrate a central result in the study of admissibility, in the hope that connecting it to known concepts in novel ways will lead to alternative avenues of generalization.

2 Universal model

The purpose of this section is to give a description of the structure of the Lindenbaum algebra of $\mathsf {IPC}$ in a language with finitely many variables, which corresponds to the free Heyting algebra on a finite number of generators. We describe, given a finite set of variables, the so-called universal model alluded to in the title of this section. This is an image-finite Kripke model whose definable upsets correspond to the elements of a free Heyting algebra. This model is surprisingly manageable and plays a crucial role in our search for semantics of admissible rules.

Before we continue with the technical contents of this section, let us, for but a moment, reflect upon the history of the universal model. Its origins lie in the work of Rieger (1949), and, independently in that of Nishimura (1960), who gave a full description of the free Heyting algebra on one generator. Urquhart (1973) was the first to give a description of the free Heyting algebra on an arbitrary finite number of generators.

Closure algebras stand to the modal logic $\mathsf {S4}$ as Heyting algebras stand to $\mathsf {IPC}$ . The structure of the free closure algebra remained mysterious for quite some time. Indeed, when Horn (1978) described the structure of the Lindenbaum algebras for $\mathsf {S5}$ , he stated: “The free closure algebra with one generator is already so complicated that its structure is unknown.” Blok (1977) wrote, in a paper on the structure of the open elements in free closure algebras: “[…] even a description of the free object on one generator seems to be beyond reach, as yet.” An answer was eventually given by Shehtman (1978), who built on the work of Esakia and Grigolia (1975). An independent description was given, later, by Bellissima (1985).

These types of models have been used extensively in the study of admissibility. Rieger and Nishimura’s description of the free Heyting algebra on one generator was used by de Jongh (1982) to study the admissible rules of $\mathsf {IPC}$ in one variable. Most famously, Rybakov (1984a) used descriptions of free Heyting algebras and free closure algebras to prove the decidability of admissibility in $\mathsf {IPC}$ .

Over time, many descriptions of free Heyting algebras have arisen. The following is not an exhaustive enumeration of the literature; undoubtably, many works are omitted. Although the descriptions are similar—they are, after all, concerned with the same object—they each have their own flavor. In particular, one can discern the approach taken by de Jongh (1968), Urquhart (1973), Rybakov (1984a), and Bellissima (1986). The approach taken by de Jongh (1968) is reflected in the work of de Jongh and Yang (2011) and Bezhanishvili (2006). Hendriks (1996, Section 2.5) is similar in background, but his construction proceeds via the the notion of semantic types. The description of Rybakov (1984a) is used by Gencer (2002) and Odintsov and Rybakov (2013), to name but a few. Finally, the method of Bellissima (1986) is employed by Darnière and Junker (2010) and Elageili and Truss (2012). The description given here will most closely resemble that of Bezhanishvili (2006).

Before we proceed to describe the universal model, we first give some basic definitions. The logics under consideration are propositional in nature. Given a fixed set of variables ${X}$ , we define the set of formulae by the following grammar:

$$ \begin{align*} \mathcal{L}(X) ::= {X} \;|\; {\top} \; | \; {\bot} \; | \; \mathcal{L}(X) {\vee} \mathcal{L}(X) \; | \; \mathcal{L}(X) {\wedge} \mathcal{L}(X) \; | \; \mathcal{L}(X) {\rightarrow} \mathcal{L}(X). \end{align*} $$

We write ${\neg\kern0.75pt} {\phi }$ as an abbreviation for ${\phi } {\rightarrow } {\bot }$ and ${\phi } \equiv {\psi }$ denotes $({\phi } {\rightarrow } {\psi }) {\wedge } ({\psi } {\rightarrow } {\phi })$ . Semantics will be given by Kripke models for intuitionistic logic. Motivation and further background can be found in the text books by Blackburn et al. (2001), Chagrov and Zakharyaschev (1997), and Troelstra and van Dalen (1988).

Definition 2.1 (Kripke model)

A Kripke model consists of a partial order P, called the underlying Kripke frame , and a monotonic function $v: P \to \mathcal {P}(X)$ , called the valuation. We inductively define when a formula $\chi \in \mathcal {L}(X)$ holds at a world $p \in P$ , denoted ${v}, p \Vdash \chi $ , as follows.

$$ \begin{align*} V, P \Vdash {\top} &\quad :=\quad \text{true},\\ V, P \Vdash {\bot} &\quad :=\quad \text{false},\\ V, P \Vdash {x} &\quad :=\quad p \in v(x) \text{ for variables } {x} \in {X}, \\ V, P \Vdash {\phi} {\wedge} {\psi} &\quad :=\quad p {\Vdash} {\phi} \text{ and } p {\Vdash} {\psi}, \\ V, P \Vdash {\phi} {\vee}{\psi} &\quad :=\quad p {\Vdash} {\psi} \text{ or } p {\Vdash} {\psi}, \\ V, P \Vdash {\phi} {\rightarrow} {\psi} &\quad:=\quad \text{ for all } q \geq p, q {\Vdash} {\phi} \text{ implies } q {\Vdash} {\psi}. \end{align*} $$

In the above, we used ${X}$ to denote the set of propositional variables. This is not common practise, but the deviation is neither without precedent nor without purpose. Precedent can be found in Ghilardi (1999), whose notation we follow. The purpose, or point, is that we want to maintain a close analogy to Universal Algebra, where one would consider algebras generated by a set. By analogy, the variables are the generators and are chosen from a set ${X}$ .

We need to fix a bit more notation. We reserve ${v}$ and ${u}$ for names of Kripke models and we use P and ${Q}$ as names of Kripke frames. An arbitrary subset of a Kripke frame will be denoted by W or S. For convenience, we use the corresponding lower-case letters to denote elements of these sets.

A subset $W \subseteq P$ such that the inequality $w \leq p$ entails $p \in W$ for all $w \in W$ and $p \in P$ is said to be an upset. Given an arbitrary subset $W \subseteq P$ , one can consider the upset generated by W and the strict upset generated by W, defined respectively as follows:

$$ \begin{align*} {\mathord{\uparrow}{W}} & := \{ p \in P \;|\; \text{there is a } w \in W \text{ such that } w \leq p \}, \\ {\mathord{\unicode{x21A5}}{W}} & := \{ p \in P \;|\; \text{there is a } w \in W \text{ such that } w < p \}. \end{align*} $$

If $W \subseteq P$ is an antichain, observe that ${\mathord {\unicode{x21A5} }{W}} = {\mathord {\uparrow }{W}} - W$ . Whenever an upset U is equal to the upset generated by a singleton set, we say that U is a principal upset. We simply write ${\mathord {\uparrow }{p}}$ to mean ${\mathord {\uparrow }{\{p\}}}$ and we similarly write ${\mathord {\unicode{x21A5} }{p}}$ for ${\mathord {\unicode{x21A5} }{\{p\}}}$ . When $U \subseteq P$ is an upset, then one can consider the restriction ${v} \restriction U: U \to {\mathcal {P}(X)}$ . The resulting model is said to be a generated submodel of ${v}$ .

The natural type of maps to consider between partial orders are monotonic functions. The sole difference between a Kripke frame and a partial order is that maps of Kripke frames $f: P \to {Q}$ are monotonic maps satisfying ${\mathord {\uparrow }{{f(p)}}} \subseteq f({\mathord {\uparrow }{p}})$ for all $p \in P$ . When ${v}: P \to {\mathcal {P}(X)}$ and ${u}: {Q} \to {\mathcal {P}(X)}$ are Kripke models, then f is a map of Kripke models if it is a map between the underlying frames, and in addition, it satisfies ${v} = u \circ f$ . Such a map is often referred to as a bounded morphism or p-morphism.

Given a model ${v}: P \to {\mathcal {P}(X)}$ and a formula ${\phi } \in \mathcal {L}(X)$ , we write

$$ \begin{align*} {{[\kern-3pt[\phi ]\kern-3pt]}_{v}} := \{p \in P \;|\; {v}, p {\Vdash} {\phi}\}. \end{align*} $$

This set is an upset and it is called the upset defined by ${\phi }$ . Note that whenever ${\phi }$ and ${\psi }$ are equivalent, then ${{[\kern-3pt[ \phi ]\kern-3pt]}_{v}} = {{[\kern-3pt[ \psi ]\kern-3pt]}_{v}}$ . Upsets of this form play a large role in the following, hence Definition 2.2 below.

Definition 2.2 (Definable)

Let ${v}: P \to {\mathcal {P}(X)}$ be a Kripke model. An upset $U \subseteq P$ is said to be definable when there exists a formula ${\phi }$ such that $U = {{[\kern-3pt[ \phi ]\kern-3pt] }_{v}}$ . The formula ${\phi }$ is said to be a defining formula of U and is denoted by ${\mathsf {def}\thinspace U}$ . ¹⁰

Suppose one is given a map of Kripke frames $f: P \to Q$ . Whenever we have valuations on both frames, ${v}: P \to {\mathcal {P}(X)}$ and $u: {Q} \to {\mathcal {P}(Y)}$ say, one can wonder whether the preimage of a definable upset in u under the map f is definable in ${v}$ as well. If this is the case, then we say that f is a definable map $f: v \to u$ . Clearly, for this condition to hold it is both necessary and sufficient that the preimage of ${[\kern-3pt[ y ]\kern-3pt]}_{u}$ is definable for every ${y} \in {Y}$ .

Recall that a Heyting algebra $\mathfrak {A}$ is a bounded distributive lattice, endowed with a binary operation $\Rightarrow $ satisfying the equations

(2) $$ \begin{align} \begin{array}{r@{\quad=\quad}l} (a \Rightarrow b) \wedge a & a \wedge b,\\ (a \Rightarrow b) \wedge b & b, \\ a \Rightarrow (b \wedge c) & (a \Rightarrow b) \wedge (a \Rightarrow c), \\ a \Rightarrow a & 1. \end{array} \end{align} $$

Alternatively, $\mathfrak {A}$ is a partial order, that, when considered as a category, is cartesian closed. The order $\leq $ on $\mathfrak {A}$ is determined by $a \leq b$ iff $a {\wedge } b = a$ . In this reading, the operations $\wedge $ , $\vee $ and $\Rightarrow $ naturally correspond to taking the product, coproduct and exponent respectively.

Maps between Heyting algebras are maps of bounded distributive lattices that respect the operation $\Rightarrow $ . In symbols, a map between Heyting algebras $f: \mathfrak {A} \to \mathfrak {B}$ is a map of bounded distributed lattices, satisfying the following for all $a, b \in \mathfrak {A}$ .

(3) $$ \begin{align} f(a \Rightarrow b) = f(a) \Rightarrow f(b). \end{align} $$

Through de Jongh and Troelstra (1966), it is known that there is an equivalence between the categories of finite Heyting algebras and their maps and the category of finite Kripke frames and their maps. As per this equivalence, a finite Kripke frame corresponds to the partial order of its upsets and this partial order can be endowed with a Heyting algebra structure in a unique manner. In the following, we describe a slightly different connection.

Given a model ${v}: P \to {\mathcal {P}(X)}$ , one can consider ${\mathsf {defs}(v)}$ , the set of its definable upsets. It is an easy matter to verify that this partial order is a bounded distributive lattice, that is to say, it has all finite products and co-products when seen as a category. The operation $\Rightarrow $ can be defined as:

$$ \begin{align*} U \Rightarrow V &= \{p \in P \;|\; q \in U \text{ implies } q \in V \text{ for all } q \geq p \} \\ &= [\kern-3pt[ {\mathsf{def}\thinspace U} {\rightarrow}{\mathsf{def}\thinspace V} ]\kern-3pt]{}_{v}. \end{align*} $$

It is a simple exercise to verify that the equalities of (2) in fact hold. Moreover, a definable map of Kripke frames $f: {v} \to u$ yields a map between the associated Heyting algebras ${\mathsf {defs}(u)}$ and ${\mathsf {defs}(v)}$ . Indeed, when we define:

$$ \begin{align*} {\mathsf{defs}(f)}: {\mathsf{defs}(u)} \to {\mathsf{defs}(v)}, \quad U \mapsto f^{-1}(U), \end{align*} $$

it is easy to verify that the equation (3) is satisfied.

We now have the language to more formally express the purpose of this section. Per finite set ${X}$ , we seek an image-finite model such that its Heyting algebra of definable upsets equals the free Heyting algebra generated by ${X}$ . This model is known as the universal model on ${X}$ .

The key concept in the description of the universal model is that of a cover. Intuitively, a subset of a partial order covers an element in the same partial order if the upsets they both generate differ at most in this latter element. An example would be the set of immediate successors of a given node, which cover said node. The definition below is taken from Ghilardi (2004).

Definition 2.3 (Cover)

Let P be a Kripke frame, let $W \subseteq {P}$ be an arbitrary subset, and let $p \in {P}$ be a point. We say that W covers p, denoted $W\ {\mathrel{\kappa}}\ p$ , whenever the following equivalence holds for all $q \in P$ :

(4) $$ \begin{align} p \leq q \ \textit{iff} \ p = q\quad or\quad q \in {\mathord{\uparrow}{W}}. \end{align} $$

Note that $\emptyset \ {\mathrel {\kappa }}\ p$ precisely if p is maximal. The notion of a cover is not strict, in the sense that $W \ {\mathrel {\kappa }}\ p$ can hold even if $p \in W$ . In fact, we always have $\{ p \} \ {\mathrel {\kappa }}\ p$ . This in contrast to the notion of a total cover, as employed by Grigolia (1995) and Bezhanishvili (2006). Using our definition, W is a total cover of p if $W \ {\mathrel {\kappa }}\ p$ and $p \not \in W$ . Jeřábek (2005) would call p a tight predecessor of W in precisely the same situation. Were the model to be the canonical model, then Iemhoff (2001a) would use the same term.

The following lemma motivates the importance of this notion. Roughly speaking, any map of Kripke frames must preserve covers. The converse need not always hold, but whenever the domain is image finite, it surely does. We omit its proof, as the argument is fairly straightforward.

Lemma 2.4 (Ghilardi, 2004, Lemma 3)

Let ${P}$ and ${Q}$ be Kripke frames, and let $f: {P} \to {Q}$ be a monotonic map. Suppose that ${P}$ is image finite. Now, f is a map of Kripke frames if and only if for all finite $W \subseteq {P}$ and $p \in {P}$ we know that $W \ {\mathrel {\kappa }}\ p$ implies $f(W) \ {\mathrel {\kappa }}\ f(p)$ .

It is well-known that $\mathsf {IPC}$ has the finite model property; a formula is a theorem of $\mathsf {IPC}$ precisely if it holds in all finite, rooted models. Picture a model on a fixed set of variables and assume that it contains a copy of every finite, rooted model on that very set of variables. This model must, by the finite model property, be complete with respect to all formulae on said variables. Each element of the free Heyting algebra generated by the fixed set of variables defines an upset in this model and two distinct elements yield distinct upsets by this model’s completeness.

The above reasoning suggests to define the universal model as being a particular model that contains a copy of each finite, rooted model. Indeed, as can be seen in Corollary 2.9, this is sufficient to prove that its definable upsets correspond in a one-to-one fashion to the elements of a free Heyting algebra. This is precisely the approach we take. First, in Definition 2.5 we give a property which Theorem 2.6 will show to ensure the above described situation. Second, in Corollary 2.7, we observe that there is only one image-finite model with this property up to isomorphism. This leads to Definition 2.8.

Definition 2.5 (Universality)

A model ${v}: {P} \to {\mathcal {P}(X)}$ is said to be universal if for all finite antichains $W \subseteq {P}$ and all ${Y} \subseteq {X}$ with ${Y} \subseteq {v}(w)$ for all $w \in W$ , there exists a unique $p \in {P}$ such that ${v}(p) = {Y}$ and $W \ {\mathrel {\kappa }}\ p$ .

Theorem 2.6. Let ${X}$ be a finite set of variables and let ${{u}}: {Q} \to {\mathcal {P}(X)}$ be universal. For any image-finite model ${v}: {P} \to {\mathcal {P}(X)}$ there exists a unique map of Kripke models $f: {v} \to {u}$ .

Proof. We prove the first statement with the proviso that ${v}$ is finite, from whence the image-finite case is immediate. Indeed, existence of such a map in the image-finite case follows from taking the union of all such maps in the finite, rooted case. This map is well-defined and unique, anything else would contradict the unicity in the finite, rooted case.

We proceed by induction on the number of elements in ${P}$ . In the base case, we know ${P}$ to be empty and so the desired surely holds. Now, suppose we know the desired for all finite rooted models ${v}$ where ${P}$ is of size at most n. Write p for the root of ${P}$ and consider the upset $U = {\mathord {\unicode{x21A5} }{p}}$ . Induction yields a map of Kripke models $f_{k}: (v \restriction ({\mathord {\uparrow }{k}})) \to {u}$ per $k \in U$ . We know that the desired $f: {v} \to {\mathsf {U}}(X)$ must satisfy $f \restriction ( {\mathord {\uparrow }{k}}) = f_{k}$ for all $k \in U$ .

Consider the function defined by $f_{U} = \bigcup _{k \in U} f_{k} : ({v} \restriction U) \to {u}$ . This function is well-defined due to the uniqueness that is ensured by induction. Moreover, it is a map of Kripke models. We see that $V = f_{U}(U)$ is an upset and note that there must be a finite antichain $W \subseteq V$ such that ${\mathord {\uparrow }{W}} = V$ . Hence, there exists a unique $q \in {\mathsf {U}}(X)$ such that both $W \ {\mathrel {\kappa }}\ q$ and ${\mathsf {u}}(q) = {v}(p)$ . It is clear that $V \ {\mathrel {\kappa }}\ q$ holds. By Lemma 2.4, we know that the map f ought to send p to q. Define $f = f_{U} \cup {\left \langle {p}{q} \right \rangle }$ and the desired follows. ⊣

Corollary 2.7. Up to isomorphism of Kripke models, there is at most one image-finite model on any given finite set of variables that is universal.

Proof. Suppose ${v}: {P} \to {\mathcal {P}(X)}$ and ${u}: {Q} \to {\mathcal {P}(X)}$ are both universal. Through Theorem 2.6, there are maps of Kripke models $f: {v} \to {u}$ and $g: {u} \to {v}$ . The same theorem ensures that $f \circ g = {\mathrm {id}_{u}}$ and $g \circ f = {\mathrm {id}_{v}}$ , proving the desired. ⊣

Definition 2.8 (Universal Model)

The universal model on ${X}$ , denoted ${\mathsf {u}}: {\mathsf {U}}(X) \to {\mathcal {P}(X)}$ , is the unique image-finite model on ${X}$ that is universal.

Intuitively, one starts with an empty model and iteratively adds points such that to each finite subset and to each set of variables that holds at this subset one has some point covered by this subset, at which precisely these variables hold. This yields a sequence of Kripke models ${\mathsf {u}}_{n} : {P}_{n} \to {\mathcal {P}(X)}$ , such that

$$ \begin{align*} {\mathsf{u}} = \bigcup_{n \in {\mathbb{N}}} {\mathsf{u}}_{n}, \quad {\mathsf{U}}(X) = \bigcup_{n \in {\mathbb{N}}} {P}_{n}. \end{align*} $$

At the zeroth stage, we consider an empty Kripke model. Hence ${\mathsf {u}}_{0}$ is the unique function ${P}_{0} = \emptyset \to {\mathcal {P}(X)}$ . The only antichain in ${P}_{0}$ thus is $\emptyset $ . One would have to expand ${P}_{0}$ into ${P}_{1}$ to accommodate more points and one would extend the valuation ${\mathsf {u}}_{0}$ appropriately into ${\mathsf {u}}_{1}$ . There would be points $p_{Y} \in {P}_1$ per ${Y} \subseteq {X}$ satisfying $\emptyset \ {\mathrel {\kappa }}\ p_{Y}$ and ${\mathsf {u}}_1(p_{Y}) = {Y}$ . This means that the universal model must have a maximal point per subset of ${X}$ .

After the ${(n+1)}$ th stage, one inspects each subset $W \subseteq {P}_{n+1}$ . If W would be contained within ${P}_{n}$ and one would add a new point p into ${P}_{n+2}$ such that $W \ {\mathrel {\kappa }}\ p$ , then the uniqueness demanded by universality would be broken. Indeed, a point q satisfying $W \ {\mathrel {\kappa }}\ q$ with ${\mathsf {u}}_{n+1}(q) = {\mathsf {u}}_{n+2}(q)$ already exists, as it was added in a previous step. One thus only considers sets W where the intersection with ${P}_{n+1} - {P}_{n}$ is nonempty. Moreover, if W would be the singleton set $\{p\}$ and one would add a point such that $W \ {\mathrel {\kappa }}\ q$ and ${\mathsf {u}}_{n+2}(q) = {\mathsf {u}}_{n+1}(p)$ , then uniqueness would be violated, too. Indeed, $W \ {\mathrel {\kappa }}\ p$ also holds and so the point q would be superfluous.

The model described by Definition 2.8 is the union of all the models obtained from the above construction. Although we do not consider the concrete details of the above construction in the following, let us spend a few words on the attention we paid to avoiding violating the uniqueness demanded by universality.

In Corollary 2.9, we prove that any two distinct points can be discerned by their theories. Consider a generic Kripke model ${v}: {P} \to {\mathcal {P}(X)}$ and suppose that there are points $p, q \in p$ such that ${v}( p ) = {v}(q)$ holds, and both $W \ {\mathrel {\kappa }}\ p$ and $W \ {\mathrel {\kappa }}\ q$ hold for a given antichain $W \subseteq {P}$ . There exists an obvious map of Kripke models from ${v}$ to the model where p and q are conflated, proving that one could not possibly discern between these points through their theories.

This idea goes back to de Jongh and Troelstra (1966, Definition 4.4). In the case where p and q are comparable, they called the resulting map of Kripke models an $\alpha $ -reduction. If p and q are incomparable, then the resulting map is said to be a $\beta $ -reduction. Similar maps are considered by Anderson (1969, Section 4), respectively called operation 1 and operation 2. ¹¹ Bellissima (1986), too, considers this and speaks of $\alpha $ -degenerate and $\alpha $ -duplicate points respectively. These same notions occur in Odintsov and Rybakov (2013, p. 773), under the names duplicates and twins respectively. Note that the precautions taken against constructing two points covered by the same set, in our loose description of the construction of ${\mathsf {U}}(X)$ above, correspond respectively to preventing the creation of duplicates and twins. For a more extensive treatment of this topic we refer to Goudsmit (2018).

Corollary 2.9. Let ${X}$ be a finite set of variables. The Heyting algebra of definable upset of the universal model ${\mathsf {u}}: {\mathsf {U}}(X) \to {\mathcal {P}(X)}$ is isomorphic to free Heyting algebra generated by ${X}$ via the mappings

$$ \begin{align*} {{[\kern-3pt[ - ]\kern-3pt]}_{\mathsf{u}}}: {\mathsf{F}(X)} \to {\mathsf{defs}({{\mathsf{U}}(X)})} \text{ and } {\mathsf{def}\thinspace (-)}: {\mathsf{defs}({{\mathsf{U}}(X)})} \to {\mathsf{F}(X)}. \end{align*} $$

Proof. It is easy to verify that both functions, as mentioned in the theorem, are maps of Heyting algebras. Let us argue that these maps are mutually inverse. The one direction is straightforward enough. Indeed, ${[\kern-3pt[ {\mathsf {def}\thinspace U} ]\kern-3pt]}_{{\mathsf {u}}} = U$ follows immediately when writing out the definitions.

We focus on the other direction. Know that ${\mathsf {def}\thinspace {{[\kern-3pt[ \phi ]\kern-3pt]}_{{\mathsf {u}}}}}$ is a formula ${\psi }$ such that ${{[\kern-3pt[ \phi ]\kern-3pt]}_{{\mathsf {u}}}} = {{[\kern-3pt[ \psi ]\kern-3pt]}_{{\mathsf {u}}}}$ . We wish to show that ${\phi } = {\psi }$ holds in ${\mathsf {F}(X)}$ , that is to say, that ${\vdash }_{\mathsf {IPC}} {\phi } \equiv {\psi }$ . We reason by contradiction and assume, without loss of generality, that ${\phi } \not {\vdash }_{\mathsf {IPC}} {\psi }$ . By the finite model property, this gives us a finite, rooted Kripke model ${v}: {P} \to {\mathcal {P}(X)}$ such that ${v} \Vdash {\phi }$ and ${v}\not \Vdash {\psi }$ . Through Theorem 2.6 we know there to be a map of Kripke models $f: {v} \to {\mathsf {u}}$ . Consequently, $f(p) \Vdash {\phi }$ yet $f(p) \not \Vdash {\psi }$ . This shows that $f(p) \in {{[\kern-3pt[ \phi ]\kern-3pt]}_{{\mathsf {u}}}}$ and $f(p) \not \in {{[\kern-3pt[ \psi ]\kern-3pt]}_{{\mathsf {u}}}}$ , proving ${{[\kern-3pt[\phi ]\kern-3pt]}_{{\mathsf {u}}}} \not = {{[\kern-3pt[ \psi ]\kern-3pt]}_{{\mathsf {u}}}}$ as desired. ⊣

Naturally, the above has been proven many times over. See Chagrov and Zakharyaschev (1997, Theorem 8.86) and Shehtman (1978, Theorem 6) for modal counterparts of the above theorem. A proof in the intuitionistic case can be found in Urquhart (1973, Theorem 3), Bellissima (1986, Corollary 2.5), and Bezhanishvili (2006, Theorem 3.2.20).

The following Corollary 2.10 is an immediate consequence of Corollary 2.9. This, too, has been proven many times in the past. We point to Rybakov (1997, Theorem 3.3.6) in particular. The first appearance of a statement of this nature in the literature on admissibility appears to be Rybakov (1984a, Theorem 2), concerning the modal logic $\mathsf {S4}$ .

Corollary 2.10. For each finite ${X}$ and each ${\phi } \in \mathcal {L}(X)$ one has ${\mathsf {u}} \Vdash {\phi }$ if and only if $\vdash_{\mathsf{IPC}} \phi $ , where ${\mathsf {u}}: {\mathsf {U}}(X) \to {\mathcal {P}(X)}$ .

The universal model is such that the order between elements is expressible in terms of formulae. On an intuitive level, this is what Theorem 2.12 aims to show. This observation will play a crucial role in our later arguments about the universal model. In particular, this observation entails that, when seen as a general frame, the universal model is refined in the sense of Jeřábek (2009). We choose to include this definition, instead of the more general notion of being refined, as the extra information encapsulated in being order-defined will be crucial in the proof of Theorem 5.5.

Definition 2.11 (Order-defined)

A model is said to be order-defined when all principle upsets and complements of principle downsets are definable.

Theorem 2.12. Let ${X}$ be a finite set of variables. Now, ${\mathsf {u}}: {\mathsf {U}}(X) \to {\mathcal {P}(X)}$ is order-defined.

Proof. We will show, using well-founded induction, that the following equivalences hold for any $p \in {\mathsf {U}}(X)$ . Each atomic part of the right-hand side of these equivalences corresponds to an upset and each of these upsets are definable, be it by induction or on their own right. ¹² For convenience, we write W for the set of immediate successors of p and remark that $W \ {\mathrel {\kappa }}\ p$ .

(5) $$ \begin{align} p \leq q\quad & \text{iff } {v}(p) \subseteq {v}(q) \text{ and} \\ & \text{for all } k \geq q, \text{ if } {v}(p) \subset {v}(k) \text{ or } k \not\leq w \text{ for some } w \in W \nonumber\\ & \text{then } k \in {\mathord{\uparrow}{W}}. \nonumber \end{align} $$

(6) $$ \begin{align} q \not\leq p\quad & \text{iff for all } k \geq q, \text{ if } k \in {\mathord{\uparrow}{p}} \text{ then } k \in {\mathord{\uparrow}{W}}. \end{align} $$

Let us first focus on (5). The implication from left to right is immediate. From right to left, suppose that $p \not \leq q$ yet the right-hand side does hold. Suppose that $q \not \leq w$ for some $w \in W$ . This immediately entails that $q \in {\mathord {\uparrow }{w}} \supseteq {\mathord {\uparrow }{p}}$ , a contradiction.

We may thus assume that q is the maximal node such that $W \subseteq {\mathord {\uparrow }{q}}$ . The right-hand side of (5) still holds for q, as it is upwards closed. We will prove that $W \ {\mathrel {\kappa }}\ q$ and ${v}(q) = {v}(p)$ , proving $p = q$ by the definition of ${\mathsf {U}}(X)$ , quod non.

To this end, take $k \in {\mathsf {U}}(X)$ to be such that $q < k$ . By maximality, we know that $W \not \subseteq {\mathord {\uparrow }{q}}$ . It now follows through (5) that $k \in {\mathord {\uparrow }{W}}$ , which shows that $W \ {\mathrel {\kappa }}\ q$ .

Let us now prove that ${v}(p) = {v}(q)$ . We know that ${v}(p) \subseteq {v}(q)$ , so we need but exclude ${v}(p) \subset {v}(q)$ . If this were the case, then $q \in {\mathord {\uparrow }{W}} \subseteq {\mathord {\uparrow }{p}}$ , a contradiction. This finishes the proof of (5). As the equivalence (6) is clear, we are done. ⊣

Lemma 2.13. Let ${X}$ be a finite set of variables and let ${v}: {P} \to {\mathcal {P}(X)}$ be an image-finite, order-defined model. There exists an upset $U \subseteq {\mathsf {U}}(X)$ such that ${v}$ and ${\mathsf {u}} \restriction U$ are isomorphic as Kripke models.

Proof. By Theorem 2.6, we know of a unique map of Kripke models $f: {v} \to {\mathsf {U}}(X)$ . We first show that f is injective. Indeed, suppose $p_1, p_2 \in {P}$ are given such that $f(p_1) = f(p_2)$ . Note that ${\mathord {\uparrow }{{p_1}}}$ is definable in ${v}$ . We observe that ${v}, p_1 \Vdash \mathsf {def}\thinspace {\mathord {\uparrow }{p_1}}$ and hence ${\mathsf {u}}, f(p_1) \Vdash \mathsf {def}\thinspace {\mathord {\uparrow }{{p_1}}}$ , leading to ${v}, p_2 \Vdash \mathsf {def}\thinspace {\mathord {\uparrow }{{p_1}}}$ . We can thus conclude $p_1 \leq p_2$ and the converse holds for a similar reason. This proves $p_1 = p_2$ , as desired.

To finish the argument, we define $U := f({P})$ . The existence of a map of Kripke models $g: ({\mathsf {u}} \restriction U) \to v$ satisfying $f \circ g = {\mathrm {id}_{v}}$ and $g \circ f = \mathrm {id}_{{\mathsf {u}}}$ readily follows. ⊣

Recall that we defined the universal model to be the least model satisfying certain properties. We might as well replace these properties by the statement that the model be complete with respect to all formulae in $\mathcal {L}(X)$ , that is to say, ${\mathsf {U}}(X)$ is the least Kripke model ${v}: {P} \to {\mathcal {P}(X)}$ such that

(7) $$ \begin{align} {v} {\Vdash} \chi \text{ if and only if } {\vdash}_{\mathsf{IPC}} \chi \text{ for all } \chi \in \mathcal{L}(X). \end{align} $$

From Corollary 2.9 it is clear that the universal model satisfies (7). One can readily prove that it is the smallest such model through (6). Indeed, suppose there is a proper generated submodel ${v} := {\mathsf {u}} \restriction U: U \to {\mathcal {P}(X)}$ satisfying (7), where $U \subset {\mathsf {U}}(X)$ is some upset. This must mean that there is a point $p \in {\mathsf {U}}(X)$ such that $p \not \in {U}$ . By (6) we know of a formula ${\phi } \in \mathcal {L}(X)$ such that ${\mathsf {U}}(X), q \Vdash {\phi }$ if and only if $q \not \leq p$ . If there is a $q \in U$ such that ${\mathsf {u}}, q \not \Vdash {\phi }$ , then $q \leq p$ and $p \in U$ , a contradiction. Hence we know that ${v} \Vdash {\phi }$ and ${\mathsf {u}} \not \Vdash {\phi }$ . By (7) this yields ${\vdash }_{\mathsf {IPC}}{\phi }$ and $\not {\vdash }_{\mathsf {IPC}} {\phi }$ , a clear contradiction.

Some authors introduce the universal model in this manner. An example is Rybakov (1984c), whose n-characterizing model essentially amounts to a model that satisfies (7) for some set of variables ${X}$ with $|{X}| = n$ . Both approaches can be taken for many logics. For intermediate logics, they coincide whenever the logic at hand has the finite model property. We will work with the definition as given above, as the abundance of covers plays a crucial rule in the following.

3 Semantics for rules

In this section, we explore potential notions of semantics for admissible rules. Our first description is extrinsic and our second more intrinsic in nature. Neither meet all the requirements as mentioned in the introduction, yet they do provide motivation for the more sophisticated notion we consider in the next section. As argued in the introduction, our search for semantics amounts to providing an algorithm that generates a class of Kripke models out of a set of formulae that satisfies three particular conditions. Before we proceed any further, let us formalize these desiderata. To this end, we define what we mean when we say that a rule is valid on a model. Moreover, we define a convenient property of sets of formulae. Using these two definitions, we give a more precise formulation of the desiderata on our notion of semantics and provide a proof of decidability under the assumption that said conditions can be met.

Definition 3.1 (Valid)

Let ${v}: {P} \to {\mathcal {P}(X)}$ be a model and let ${\phi }, {\psi } \in \mathcal {L}(X)$ be formulae. We say that the rule ${\phi } / {\psi }$ is valid on v whenever ${v} \Vdash {\phi }$ implies ${v} \Vdash {\psi }$ .

Definition 3.2 (Adequate Set)

A set of formulae $\Sigma \subseteq \mathcal {L}(X)$ is said to be adequate precisely if it is closed under taking subformulae, that is:

$$ \begin{align*} \text{ for all } {\phi}, {\psi} \in \mathcal{L}(X) \text{ and } \mathord{\oplus} = \mathord{{\wedge}}, \mathord{{\vee}}, \mathord{{\rightarrow}}, {\phi} \oplus {\psi} \in \Sigma \text{ implies } {\phi}, {\psi} \in \Sigma. \end{align*} $$

The set of subformulae of a formula ${\phi }$ is denoted $\mathsf {Sub}(\phi )$ and it is the smallest adequate set containing ${\phi }$ .

Theorem 3.3. Suppose that there exists an algorithm that produces a set of Kripke models $\mathcal {K}_{\Sigma }$ whenever one inputs a finite adequate set of formulae $\Sigma \subseteq \mathcal {L}(X)$ subject to the following conditions.

1. Condition 1 The rule ${\phi } / {\psi }$ is admissible in $\mathsf {IPC}$ if and only if it is valid on all members of $\mathcal {K}_{\Sigma }$ , for any pair of formulae ${\phi }, {\psi } \in \Sigma $ .

2. Condition 2 The set of models $\mathcal {K}_{\Sigma }$ is finite.

3. Condition 3 Given a model in ${\mathcal {K}}_{\Sigma }$ , it is decidable whether a rule is valid on it.

Now, the set of admissible rules for $\mathsf {IPC}$ is decidable.

Proof. We provide an algorithm that decides whether a given rule is decidable. On input ${\phi } / {\psi }$ we construct the adequate set $\Sigma := \mathsf {Sub} (\phi ) \cup \mathsf {Sub} (\psi )$ . By assumption, we can effectively produce a class of Kripke models ${\mathcal {K}}_{\Sigma }$ satisfying the three conditions above. Verify whether ${v} \Vdash {\phi }$ implies ${v} \Vdash {\psi }$ for all ${v} \in \mathcal {K}_{\Sigma }$ . The rule is admissible precisely if the above holds, due to Condition 1. Condition 2 ensures that we can effectively run through all models in $\mathcal {K}$ and Condition 3 guarantees we can effectively test validity. This proves the desired. ⊣

Recall that the validity at a universal model corresponds to derivability in $\mathsf {IPC}$ , as expressed in Corollary 2.10. Because admissible rules are concerned with a connection between the derivability in $\mathsf {IPC}$ of two formulae, it makes sense to use universal models as a notion of semantics. A first approximation would be the following characterization of admissibility, using formulae ${\phi }, {\psi } \in \mathcal {L}(X)$ :

(8) $$ \begin{align} \begin{split} & \text{A rule } {\phi} / {\psi} \in \text{ is admissible iff for all substitutions } \sigma: \mathcal{L}(X) \to \mathcal{L}(Y)\\ &{\mathsf{u}} {\Vdash} {\mathord{\sigma}(\mathord{\phi})} \text{ implies } {\mathsf{u}} {\Vdash} {\mathord{\sigma}(\mathord{\phi})} \text{ for } {\mathsf{u}}: {\mathsf{U}}(Y) \to {\mathcal{P}(Y)}. \end{split} \end{align} $$

Although the above is completely true, it is also completely unsatisfactory. Moreover, Theorem 3.3 is even applicable, as the above equivalence does not fit the notion of validity of Theorem 3.1. The idea, however, is close to the desired, so let us improve from here. We aim to define a kind of model that encompasses the right-hand side of (8). To this end, we employ the notion of definable maps of Kripke frames, as described earlier.

Definition 3.4 (Exact Model)

Let ${v}: {P} \to {\mathcal {P}(X)}$ be a model. We say that ${v}$ is exact whenever there is a surjective, definable map $f: {\mathsf {u}} \to {v}$ , where ${\mathsf {u}}: {\mathsf {U}}(Y) \to {\mathcal {P}(Y)}$ is the universal model on some finite set of variables ${Y}$ .

The above definition is adopted from Bezhanishvili and de Jongh (2012, Corollary 4.6), based on exact formulae. We do not go into the details of exact formulae, sufficed to say that a formula is exact whenever the upset it defines in the universal model gives rise to an exact model in our sense above. Such exact formulae derive from de Jongh (1982) and this notion was further developed by de Jongh and Visser (1996, Section 2).

Note that the Kripke frame ${\mathsf {U}}(Y)$ is image-finite and being image-finite is preserved by surjective, monotonic maps. Consequently, all exact models are image-finite. In particular, this means that rooted exact models are necessarily finite.

Example 3.5. Consider the setting where ${X} = \{ {x} \}$ and think of the model ${v}: {P} \to {\mathcal {P}(X)}$ as depicted on the right-hand side of Figure 1. The required definable map of Kripke frames $f: {\mathsf {U}}(X) \to {v}$ is depicted by the dashed lines, whose behavior is partially described by Lemma 2.4. Observe that the following equalities hold. Definability already follows from the first equation, the other two are given for reference.

$$ \begin{align*} f^{-1}\big({[\kern-3pt[ x ]\kern-3pt]}_{v}\big) &= {{[\kern-3pt[ {{\neg\kern0.75pt}{\neg\kern0.75pt}{x}} ]\kern-3pt]}_{{\mathsf{u}}}} \\ f^{-1}\big({{[\kern-3pt[ {{\neg\kern0.75pt} {x}} ]\kern-3pt]}_{v}}\big) &= {{[\kern-3pt[ {{\neg\kern0.75pt}{\neg\kern0.75pt}{\neg\kern0.75pt}{x}} ]\kern-3pt]}_{{\mathsf{u}}}} = {{[\kern-3pt[ {{\neg\kern0.75pt} {x}}]\kern-3pt]}_{{{\mathsf{u}}}}}, \\ f^{-1}\big({{[\kern-3pt[ {{\neg\kern0.75pt}{\neg\kern0.75pt} {x} {\rightarrow} {x}} ]\kern-3pt]}_{{v}}}\big) &= {{[\kern-3pt[ {{\neg\kern0.75pt}{\neg\kern0.75pt}{\neg\kern0.75pt}{\neg\kern0.75pt} {x} {\rightarrow} {\neg\kern0.75pt}{\neg\kern0.75pt}{x}} ]\kern-3pt]}_{{{\mathsf{u}}}}} = {{[\kern-3pt[ {\top} ]\kern-3pt]}_{{{\mathsf{u}}}}}. \end{align*} $$

An exhaustive list of exact models on one variables is not very long. Indeed, up to isomorphism it is given by the upsets in ${\mathsf {U}}(X)$ defined by one of the formulae ${\top }$ , ${x}$ , ${\neg\kern0.75pt}{x}$ , ${\neg\kern0.75pt}{\neg\kern0.75pt} {x}$ and ${\neg\kern0.75pt} {\neg\kern0.75pt} {x} {\rightarrow } {x}$ . For more details on this and for a complete description of all finite exact models, we refer to Arevadze (2001). An exhaustive characterization of exact models in two variables is much harder to give, for this we refer to Bezhanishvili and de Jongh (2012, Theorem 5.21).

Figure 1 An example of an exact model, together with a definable, surjective map of Kripke frames from the universal model.

Exact models are our first attempt at defining semantics for admissible rules. We claim that the assignment which maps $\Sigma \subseteq \mathcal {L}(X)$ to the set of all exact models on ${X}$ satisfies at least the first condition of Theorem 3.3. This is what we prove in Theorem 3.6 below. Descriptions like this occur elsewhere in the literature, the following is comparable in nature to Rybakov (1997, Theorem 3.3.10) and Iemhoff (2001b, Corollary 3.15).

Theorem 3.6 (Soundness and Completeness for Exact Models)

The following are equivalent for each pair of formulae ${\phi }, {\psi } \in \mathcal {L}(X)$ :

1. 1. the rule ${\phi } / {\psi }$ is admissible;

2. 2. the rule ${\phi } / {\psi }$ is valid on every exact model ${v}: {P} \to {\mathcal {P}(X)}$ .

The implication from 1 to 2 corresponds to soundness of admissibility with respect to exact models and its converse, naturally, corresponds to completeness. We first provide a little bit of machinery, of which the theorem is but a simple corollary.

Lemma 3.7. Let ${v}: {P} \to {\mathcal {P}(X)}$ be an exact model. There exists a finite set of variables ${Y}$ and a substitution $\sigma : \mathcal {L}(X) \to \mathcal {L}(Y)$ such that:

(9) $$ \begin{align} {\vdash}_{\mathsf{IPC}} {\mathord{\sigma}(\mathord{\chi})} \text{ iff } v {\Vdash} \chi \text{ for all } \chi \in \mathcal{L}(X). \end{align} $$

Proof. Because ${v}$ is exact, we know there to be a finite set of variables ${X}$ together with a surjective, definable map of Kripke frames $f: {\mathsf {u}} \to {v}$ where ${\mathsf {u}}$ is the universal model ${\mathsf {u}}: {\mathsf {U}}(Y) \to {\mathcal {P}(Y)}$ . Define the substitution

$$ \begin{align*} \sigma : \mathcal{L}(X) \to \mathcal{L}(Y), \quad {x} \mapsto {\mathsf{def}\thinspace {f^{-1}\big({{[\kern-3pt[ {x} ]\kern-3pt]}_{v}}\big)}}. \end{align*} $$

We claim that the following equivalence holds. From here, (9) follows from Corollary 2.10 and the surjectivity of f.

(10) $$ \begin{align} p {\Vdash} {\mathord{\sigma}(\mathord{\chi})} \text{ if and only if } f(p) {\Vdash} \chi. \end{align} $$

We prove (10) by structural induction along $\chi $ . In the atomic case, the desired follows directly from the definitions. The conjunctive and disjunctive cases can immediately be seen to hold through induction. We treat the implicative case $\chi = {\phi } {\rightarrow } {\psi }$ in some detail. Observe that $p \Vdash {\mathord {\sigma }(\mathord {\chi })}$ precisely if for all $q \geq p$ we have that $q \Vdash {\mathord {\sigma }(\mathord {\phi })}$ implies $q \Vdash {\mathord {\sigma }(\mathord {\psi })}$ . By induction, we know this to mean that for each $q \geq p$ we have that $f(q) \Vdash {\phi }$ implies $f(q) \Vdash {\psi }$ . This is equivalent to $f(p) \Vdash {\phi } {\rightarrow } {\psi }$ , as f is a map of Kripke frames, proving the desired. ⊣

Lemma 3.8 (Ghilardi, 1999, Proposition 2)

Let $\sigma : \mathcal {L}(Y) \to \mathcal {L}(X)$ be a substitution and let ${v}: {P} \to {\mathcal {P}(X)}$ be a model. There is a model ${\sigma ^{*}(v)}: {P} \to {\mathcal {P}(Y)}$ such that the identity function ${\mathrm {id}_{P}}: P \to P$ is a definable map ${v} \to {\sigma ^{*}(v)}$ satisfying:

(11) $$ \begin{align} {v}, p {\Vdash} {\mathord{\sigma}(\mathord{\chi})} \text{ iff } {\sigma^{*}(v)}, f(p) {\Vdash} \chi \text{ for all } \chi \in \mathcal{L}(Y) \text{ and } p \in P. \end{align} $$

Proof. We define the valuation ${\sigma ^{*}(v)}$ as

$$ \begin{align*} {\sigma^{*}(v)}(p) = \{y \in Y \;|\; v \Vdash {\mathord{\sigma}(\mathord{y})} \}. \end{align*} $$

One can prove the validity of (11) by structural induction along $\chi $ , the atomic case holds by definition. ⊣

Proof. Proof of Theorem 3.6

Suppose 1 holds and suppose that ${v}: {P} \to {\mathcal {P}(X)}$ is an exact model. Consider the substitution $\sigma $ as ensured by Lemma 3.7, satisfying (9). If ${v} \Vdash {\phi }$ then ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\phi })}$ by (9). By the admissibility of ${\phi } / \chi $ , we know this to entail ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\psi })}$ . Hence (9) ensures ${v} \Vdash {\psi }$ to hold. This proves 2, as desired.

Conversely, suppose 1 does not hold. This gives a substitution $\sigma : \mathcal {L}(X) \to \mathcal {L}(Y)$ such that ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\phi })}$ and $\not {\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\psi })}$ . Now, consider the universal model ${\mathsf {u}}: {\mathsf {U}}(Y) \to {\mathcal {P}(Y)}$ and know that ${\mathsf {u}} \Vdash {\mathord {\sigma }(\mathord {\phi })}$ and ${\mathsf {u}} \not \Vdash {\mathord {\sigma }(\mathord {\psi })}$ by Corollary 2.10. Through Lemma 3.8, we learn of a model $\sigma ^{*}({\mathsf {u}}) : {\mathsf {U}}(Y) \to {\mathcal {P}(X)}$ and a surjective, definable map $f: {\mathsf {u}} \to {\sigma ^{*}({\mathsf {u}})}$ satisfying (11). See that ${\sigma ^{*}({{\mathsf {u}}})}$ is exact and the rule ${\phi } / {\psi }$ is not valid on ${\sigma ^{*}({\mathsf {u}})}$ . This proves that 2 does not hold, as desired. ⊣

The above shows that exact models provide sound and complete semantics for the admissible rules of $\mathsf {IPC}$ . It thus makes sense to ask: is the assignment which maps any finite adequate set $\Sigma \subseteq \mathcal {L}(X)$ to the set ${\mathcal {K}}_{\Sigma }$ of all exact models on ${X}$ of the appropriate type to apply Theorem 3.3? In order for this to be true, said assignment has to be effective and it has to satisfy all three conditions posed by this theorem. We go over these conditions and then return to the matter of effectivity.

Condition 1 poses no problem, for this amounts to the soundness and completeness we have just proven in Theorem 3.6. We continue with condition 3 and wish to know whether it is decidable whether a rule holds on an exact model. Perhaps counterintuitively so, this condition is not a major concern. If an exact model is presented by means of the substitution to which it corresponds due to Lemma 3.7 and 3.8, then the validity at said model can be effectively reduced to the derivability in $\mathsf {IPC}$ of the original formula under the given substitution. As the latter is well-known to be decidable, this settles condition 2. An even nicer description of the validity on exact models is possible. Indeed, it follows through the uniform interpolation theorem of Pitts (1992) that any exact model on ${X}$ corresponds to a formula in $\mathcal {L}(X)$ , as proven by de Jongh and Visser (1996, Corollary 2.4). More precisely, to every exact model ${v}: {P} \to {\mathcal {P}(X)}$ one can construct a formula ${\phi } \in \mathcal {L}(X)$ such that:

$$ \begin{align*} {\phi} {\vdash}_{\mathsf{IPC}} \chi \text{ if and only if } {v} {\Vdash} \chi \text{ for all } \chi \in \mathcal{L}(X). \end{align*} $$

Sufficed to say that this argument was not yet known at the time of Rybakov’s original proof, which was originally presented in 1984, a solid seven years before Pitts uniform interpolation theorem was published. His proof gets around this problem; in our further arguments, we do not appeal to the reasoning given in this paragraph.

We continue our inspection of the conditions with condition 2. It poses quite the challenge, to be sure. When the set of variables under consideration is at most one, then there are but finitely many exact models up to isomorphism. The situation changes drastically from two variables onwards, as in this situation there are infinitely many nonisomorphic exact models, as shown by Bezhanishvili and de Jongh (2012). To get around this problem, we switch to a different notion of model in Section 4.

For the sake of argument, let us continue to the matter of effectivity. There has to be some type of algorithm which produces ${\mathcal {K}}_{\Sigma }$ out of $\Sigma $ . In this context, this comes down to the question: when given a model on ${X}$ , how does one know that it is exact? The definition, as it is given above, is in no way intrinsic. Indeed, it refers to a definable map that exist “outside” the model itself and as such it is not clear that one can tell whether a model is exact by “looking at it”. It would be quite helpful to have an intrinsic description of exact models; a description which can be tested on the model itself. Such type of semantics can be found in the extendible extendible models, which arise out of the work of de Jongh (1982). See also Iemhoff (2001b, Definition 1), Bezhanishvili and de Jongh (2012), and Ghilardi (2004, Proposition 4) for comparable notions.

Definition 3.9 (Extendible)

A Kripke frame ${P}$ is said to be extendible when, for each finite antichain $W \subseteq {P}$ , there exists an element $p \in {P}$ such that $W \ {\mathrel {\kappa }}\ p$ .

Any exact model is necessarily extendible, as we show in Lemma 3.10 below. As an immediate consequence of this and Theorem 3.6, we know that extendible models are complete with respect to all admissible rules.

Lemma 3.10. Let ${v}: {P} \to {\mathcal {P}(X)}$ be an exact model. The model ${v}$ is extendible, too.

Proof. As ${v}$ is exact, we know there to be a surjective definable map $f: {\mathsf {u}} \to {v}$ , where ${\mathsf {u}}: {\mathsf {U}}(Y) \to {\mathcal {P}(Y)}$ is the universal model on a finite set of variables Y. Let $W \subseteq {P}$ be a finite antichain. There exists a finite antichain $S \subseteq f^{-1}(W) \subseteq {\mathsf {U}}(Y)$ such that $f(S) = W$ . By the definition of ${\mathsf {U}}(Y)$ , there must be a $q \in {\mathsf {U}}(Y)$ such that $S \ {\mathrel {\kappa }}\ q$ . It now follows that $f(S) = W \ {\mathrel {\kappa }}\ f(q)$ through Lemma 2.4, proving the desired. ⊣

One may wonder whether every model in which all admissible rules are valid must be extendible. This is not plausible in full generality, as the definition of validity depends solely on the theory of the model, whereas extendibility depends on its shape. Indeed, one could easily construct two models with equal theories, of which only one is extendible.

Ghilardi (1999, p. 867), in essence, showed that the notions of exactness and extendibility coincide when restricting to definable upsets of the universal model. ¹³ It thus follows that the definable extendible subsets of the universal model are sound with respect to the admissible rules of $\mathsf {IPC}$ . They are complete as well, as can be seen through Lemma 3.10 and an inspection of the proof of Lemma 3.8. As Ghilardi (2002) already remarked, the approach taken by Ghilardi (1999) leads to a proof of the decidability of admissibility. However, the technique employed here was not yet present at the time of Rybakov (1984a) and his approach is the one we aim to describe.

Note that extendibility, although it is an intrinsic notion, is not a priori an effectively testable property of a model. Were the model to be finite, though, then extendibility can be readily verified. It may seem plausible that one could obtain sound and complete semantics for admissible rules by restricting attention to those finite models that happen to be extendible. This thought is not too outlandish, given that formulae most certainly are complete with respect to finite models. Rules, however, are not. We refer to Fedorishin and Ivanov (2003) and Goudsmit (2016) for a full argument on this and point to Rybakov et al. (1999b) for an argument in the modal case. In the next section, we inspect a weakening of the notion of exactness that can be safely restricted to the finite.

4 Adequately exact models

Filtration is one of the classic techniques used to prove the finite model property for logics, both modal and intuitionistic. The key observation is that, when trying to determine the validity of a given formula, it suffices to distinguish but finitely many truth values within any model. To be a tad more precise, one can restrict attention to a finite set of formulae and only observe a model up to the equivalence relation that identifies nodes which behave identically with respect to that chosen set of formulae. One could employ the same type of observation to the study of admissibility. In fact, one has.

In the previous section, we considered the notion of exact models. These models come equipped with a surjective map of Kripke frames from the universal model, preserving the validity of all formulae in the language. Below, we weaken the notion of exactness, in such a way that only the validity of but a given, specific set of formulae need be preserved. For most of our practical applications, this set will be finite.

When one is only interested in the validity of formulae in a given adequate set $\Sigma $ , many of the above described notions can be weakened. We first reconsider the requirements we impose upon a map and then inspect an appropriately refined notion of exactness. A map $f: {P} \to Q$ between Kripke models ${v}: {P} \to {\mathcal {P}(X)}$ and u was defined in such a way that the equivalence (12) below holds for all formulae. In general, this is much more than we need. We are concerned with maps that are guaranteed to satisfy this only for formulae in $\Sigma $ .

(12) $$ \begin{align} {v}, p {\Vdash} \chi \text{ if and only if } {u}, f(p) {\Vdash} \chi. \end{align} $$

To define maps in such a manner would mix syntax and semantics where no such collusion is necessary. Instead, we make use of maps satisfying the “closed domain condition” of Zakharyaschev (1992), or rather, the intuitionistic variant as described by Bezhanishvili and Bezhanishvili (2017, Section 4). Lemma 4.4 shows that this semantic condition is sufficient to retrieve the desired syntactic information. Take care to note that any map of Kripke frames satisfies this condition.

Definition 4.1 (Closed Domain Condition)

Let $f: {P} \to Q$ be a monotonic map between posets and let D be a subset of ${Q}$ . We say that f satisfies the closed domain condition for D (in short: f has the cdc for D) whenever the following holds.

(13) $$ \begin{align} \text{ if } {\mathord{\uparrow}{{f(p)}}} \cap D \not=\emptyset \text{ then } f({\mathord{\uparrow}{{p}}}) \cap D \not= \emptyset. \end{align} $$

When the above holds for all $D \in {\mathcal {D}}$ and ${\mathcal {D}}$ is a set of subsets of ${Q}$ , then f is said to have the cdc for ${\mathcal {D}}$ .

In the above context, we call D a domain and refer to ${\mathcal {D}}$ as a set of domains. A domain should always be understood as a subset of a given Kripke frame. Maps that satisfy the cdc are closed under composition in the technical sense of Lemma 4.2.

Lemma 4.2. Let $f: {P} \to {Q}$ and $g: {Q} \to K$ be monotonic maps and let ${\mathcal {D}} \subseteq {\mathcal {P}(K)}$ be a set of domains. Suppose that g has the cdc for D and f has the cdc for $g^{-1}(D)$ . Now, $g \circ f$ has the cdc for D.

Proof. Suppose that ${\mathord {\uparrow }{{(g \circ f)(p)}}} \cap D \not =\emptyset $ . By assumption, we get $g ({\mathord {\uparrow }{{f(p)}}} ) \cap D \not = \emptyset $ . We can thus readily deduce that ${\mathord {\uparrow }{f(p)}} \cap g^{-1}(D) \not = \emptyset $ , proving $f({\mathord {\uparrow }{p}}) \cap g^{-1}(D)$ to be nonempty. We obtain $(g\circ f)({\mathord {\uparrow }{p}}) \cap D \not =\emptyset $ , as desired. ⊣

Out of all the potential domains one could define on a model, we are particularly interested in those domains that arise syntactically as in Definition 4.3. These domains are precisely the sets of points where certain implications fail to hold. Note that such domains need not be upsets, as illustrated by Figure 2.

Figure 2 A model on the variables ${X} = \{ {x} \}$ , where the marked subset is the domain on which the implication ${\neg\kern0.75pt}{\neg\kern0.75pt} {x} {\rightarrow } {x}$ is not valid.

Definition 4.3. Let ${v}: {P} \to {\mathcal {P}(X)}$ be a model and let $\Sigma \subseteq \mathcal {L}(X)$ be an adequate set. We define the domains specified by $\Sigma $ as ${\mathcal {D}}_{v}^{\Sigma } := \left \{{ [\kern-3pt[\phi ]\kern-3pt]}_{v} - {{ [\kern-3pt[ \psi ]\kern-3pt]}_{v}} \;\middle |\; {\phi } {\rightarrow } {\psi } \in \Sigma \right \}$ .

Lemma 4.4 shows that a monotonic map respects the validity of $\Sigma $ precisely if it satisfies the cdc for ${\mathcal {D}}^{\Sigma }_{v}$ , much like a map of Kripke models respects the validity of all formulae. Moreover, monotonic maps that satisfy the cdc are a generalization of maps of Kripke frames, which we illustrate in Lemma 4.6 below. Intuitively speaking, a monotonic map into an order-defined Kripke model is a map of Kripke frames precisely whenever it satisfies the cdc for all domains that can be specified in the sense of Definition 4.3.

Lemma 4.4. Let $\Sigma \subseteq \mathcal {L}(X)$ be an adequate set of formulae, let ${v}: {P} \to {\mathcal {P}(X)}$ and $u: {Q} \to {\mathcal {P}(X)}$ be models, and let $f: {P} \to {Q}$ be a monotonic map such that for all $p \in {P}$ and ${x} \in {X} \cap \Sigma $ we have ${x} \in {v}(p)$ iff ${x} \in ({u} \circ f)(p)$ . ¹⁴ The following are equivalent:

1. 1. the function f has the cdc for ${\mathcal {D}}^{\Sigma }_{u}$ ;

2. 2. the equivalence (14) holds.

   (14) $$ \begin{align} {v}, p {\Vdash} \chi \text{ if and only if } u, f(p) {\Vdash} \chi \text{ for all } \chi \in \Sigma \text{ and } p \in {P}. \end{align} $$

Proof. Suppose that 1 holds. We prove (14) for all $p \in {P}$ by structural induction along $\chi \in \Sigma $ . In the base case, the desired is immediate by definition. Both the conjunctive and disjunctive case follow straightforwardly by induction. Now, suppose $\chi = {\phi } {\rightarrow } {\psi }$ and note that ${\phi }, {\psi } \in \Sigma $ holds as $\Sigma $ was assumed to be adequate. Consider $p \in {P}$ and $q \in {Q}$ such that ${v}, p \Vdash {\phi } {\rightarrow } {\psi }$ , $f(p) \leq q$ and $u, q \Vdash {\phi }$ . If ${u}, q \not \Vdash {\psi }$ then we know:

$$ \begin{align*} {\mathord{\uparrow}{f(p)}} \cap \big( {[\kern-3pt[ \phi ]\kern-3pt]}_{u} - {{[\kern-3pt[ {\psi} ]\kern-3pt]}_{u}}\big) \not= \emptyset. \end{align*} $$

Through the cdc for ${\mathcal {D}}^{\Sigma }_{u}$ , we have some $k \geq p$ such that $u, f(k) \Vdash {\phi }$ and ${v}, f(k) \not \Vdash {\psi }$ . By induction, (14) allows us to deduce that ${v}, k \not \Vdash {\phi } {\rightarrow } {\psi }$ , a contradiction. This proves the implication from left to right in (14); the other direction is immediate.

Conversely, suppose 2 holds. We assume that ${\mathord {\uparrow }{{f(p)}}} \cap D \not = \emptyset $ for some $D \in {\mathcal {D}}^{\Sigma }_{u}$ . This gives us some ${\phi } {\rightarrow } {\psi } \in \Sigma $ such that $D = {{[\kern-3pt[\phi ]\kern-3pt]}_{u}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{u}}$ . As a consequence, we immediately know that $u, f(p) \not \Vdash {\phi } {\rightarrow } {\psi }$ . It follows through (14) that ${v}, p \not \Vdash {\phi } {\rightarrow } {\psi }$ , so there is some $q \geq p$ such that ${v}, q \Vdash {\phi }$ and ${v}, q \not \Vdash {\psi }$ . Using (14) again, we obtain ${u}, f(q) \Vdash {\phi }$ and ${u}, f(q) \not \Vdash {\psi }$ . This, in turn, yields $f({\mathord {\uparrow }{p}}) \cap D \not = \emptyset $ , proving 1 as desired. ⊣

In the previous sections, we worked with definable maps between Kripke frames. Consider models ${v}: {P} \to {\mathcal {P}(X)}$ and $u: {Q} \to {\mathcal {P}(Y)}$ . When we merely know a monotonic map $f: {P} \to {Q}$ to satisfy the cdc for ${\mathcal {D}}^{\Sigma }_{u}$ , it is not reasonable to require that the preimage of every definable set is definable. The most one could reasonably expect is the preservation of definability under preimages of f for upsets defined by formulae from $\Sigma $ . It is both sufficient and necessary to require this for the variables in $\Sigma $ , which is how we define it.

Definition 4.5 (Adequate map)

Let ${v}: {P} \to {\mathcal {P}(Y)}$ and $u: {Q} \to {\mathcal {P}(X)}$ be Kripke models, let ${\mathcal {D}}$ be a set of subsets of ${Q}$ , and let $f: {P} \to {Q}$ be a monotonic map. We say that f is a ${\mathcal {D}}$ -adequate map $f: {v} \to u$ whenever f has the cdc for ${\mathcal {D}}$ and the set $f^{-1}({{[\kern-3pt[ x ]\kern-3pt]}_{u}})$ is definable for all ${x} \in {X}$ . If $f: v \to u$ is a ${\mathcal {D}}^{\Sigma }_{u}$ -adequate map, we say that it is a $\Sigma $ -adequate map.

In the previous section, we defined the notion of an exact model. Definition 4.7 below generalizes this, replacing maps of Kripke models by maps satisfying an instance of the cdc. The old notion can be retrieved, as follows immediately from the next lemma.

Lemma 4.6. Let ${P}$ be a poset and let ${u}: {Q} \to {\mathcal {P}(X)}$ be an image-finite order-defined model. Suppose $f: {P} \to {Q}$ satisfies the cdc for ${\mathcal {D}}^{\Sigma }_{u}$ , where $\Sigma := \mathcal {L}(X)$ . Then f is a map of Kripke frames.

Proof. Take $p \in {P}$ and $q \in {Q}$ to be such that $f(p) \leq q$ . Now consider the formulae

$$ \begin{align*} {\phi} := {\mathsf{def}\thinspace { {\mathord{\uparrow}{q}} }} \text{\;and\;} {\psi} := {\mathsf{def}\thinspace { {Q} - \downarrow {q} }}. \end{align*} $$

It is clear that $q \Vdash {\phi }$ and $q \not \Vdash {\psi }$ , hence ${\mathord {\uparrow }{{f(q)}}} \cap ({{[\kern-3pt[ \phi ]\kern-3pt]}_{u}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{u}})$ is nonempty. By assumption, this yields us some $k \geq p$ such that ${u}, f(k) \Vdash {\phi }$ and ${u}, f(k) \not \Vdash {\psi }$ . The former proves $q \leq f(k)$ , whereas the latter proves $f(k) \leq q$ . We thus derive $f(k)= q$ , as desired. ⊣

Definition 4.7 (Adequately Exact)

Let ${v}: {P} \to {\mathcal {P}(X)}$ be a Kripke model and let ${\mathcal {D}}$ be a set of subsets of ${P}$ . We say that ${v}$ is adequately exact for ${\mathcal {D}}$ whenever there exists a finite set of variables ${Y}$ and a surjective, ${\mathcal {D}}$ -adequate map $f: {\mathsf {u}} \to {v}$ where ${\mathsf {u}}: {\mathsf {U}}(Y) \to {\mathcal {P}(Y)}$ .

Theorem 3.6 showed us that exact models can serve as sound and complete semantics for arbitrary admissible rules. When restricting attention to admissible rules drawn from a particular adequate set, it suffices to consider adequately exact models instead. The major upside of this, is that there is an obvious bound on the sensible size of an adequately exact model. Indeed, as we are only interested in the validity of formulae of a given adequate set, the size of all models one needs to be concerned with can be bound in terms of the size of this adequate set. As such, the first and third condition as mentioned in the introduction are clearly satisfied; the next section of this paper is devoted to proving the second.

Theorem 4.8 (Soundness and Completeness for Adequately Exact Models)

Let $\Sigma $ be an adequate set. The following are equivalent for any ${\phi }, {\psi } \in \Sigma $ :

1. 1. the rule ${\phi } / {\psi }$ is admissible;

2. 2. the rule ${\phi } / {\psi }$ is valid on every model ${v}: {P} \to {\mathcal {P}(X)}$ that is adequately exact with respect to ${\mathcal {D}}^{\Sigma }_{v}$ with ${P} \subseteq {\mathcal {P}(\Sigma )}$ .

In order to prove the above Theorem 4.8, we proceed in a manner similar to the proof of Theorem 3.6. Lemma 4.10 and 4.11 below play analogous roles to Lemma 3.7 and 3.8 respectively. Their proofs are omitted, as they can be obtained through straightforwardly generalizing the proofs of their forebears. Lemma 4.9 is a fresh ingredient and it plays a key role in Theorem 4.8. Moreover, in combination with Lemma 3.8 it gives rise to many examples of adequately exact models.

Lemma 4.9 (Filtration)

Let ${v}: {P} \to {\mathcal {P}(X)}$ be a model and let $\Sigma $ be an adequate set. There exists a model ${u}: {Q} \to {\mathcal {P}(Y)}$ and a surjective, $\Sigma $ -adequate map $f: v \to u$ , such that $Q \subseteq {\mathcal {P}(\Sigma )}$ .

Proof. We define the partial order ${Q}$ as the following set of subsets of ${\mathcal {P}(\Sigma )}$ , ordered by inclusion.

$$ \begin{align*} {Q} := \left\{\left\{ \phi \in \Sigma \;|\; v, p \Vdash \phi \right\} \;|\; p \in {P} \right\}. \end{align*} $$

The valuation ${u}: {Q} \to {\mathcal {P}(X)}$ is defined by ${u}(q) = q \cap {X}$ . There is an obvious surjective, monotonic map $f: {P} \to {Q}$ . The desired follows from Lemma 4.4 and a straightforward inductive argument.⊣

Lemma 4.10. Let $\Sigma \subseteq \mathcal {L}(X)$ be an adequate set and let ${v}: {P} \to {\mathcal {P}(X)}$ be a $\Sigma $ -adequately exact model. There exists a finite set of variables ${Y}$ and a substitution $\sigma : \mathcal {L}(X) \to \mathcal {L}(Y)$ such that:

(15) $$ \begin{align} {\vdash}_{\mathsf{IPC}} {\mathord{\sigma}(\mathord{\chi})}\quad \text{iff}\quad {v} {\Vdash} \chi, \text{ for all } \chi \in \Sigma. \end{align} $$

Lemma 4.11. Let $\sigma : \mathcal {L}(Y) \to \mathcal {L}(X)$ be a substitution, let $\Sigma \subseteq \mathcal {L}(X)$ be an adequate set, and let ${v}: {P} \to {\mathcal {P}(X)}$ be a model. There is a model ${\sigma ^{*}(v)}: P \to {\mathcal {P}(Y)}$ such that the identity function ${\mathrm {id}_{P}}: P \to P$ is a $\Sigma $ -adequate map ${v} \to {\sigma ^{*}(v)}$ satisfying:

(16) $$ \begin{align} {v}, p {\Vdash} {\mathord{\sigma}(\mathord{\chi})} \ \text{iff}\ {\sigma^{*}(v)}, f(p) {\Vdash} \chi, \text{ for all } \mathord{\chi} \in \Sigma \text{ and } p \in {P}. \end{align} $$

Proof. Proof of Theorem 4.8

Suppose that 1 holds and let ${v}: P \to {\mathcal {P}(X)}$ be adequately exact with respect to ${\mathcal {D}}^{\Sigma }_{v}$ . This provides us with a finite set ${Y}$ and a surjective, $\Sigma $ -adequate map $f: {\mathsf {u}} \to {v}$ , where ${\mathsf {u}}: {\mathsf {U}(Y)} \to {\mathcal {P}(Y)}$ is a universal model. Through Lemma 4.10, there exists a substitution $\sigma : \mathcal {L}(X) \to \mathcal {L}(Y)$ satisfying (15). If ${v} \Vdash {\phi }$ then ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\phi })}$ follows from (15), so the admissibility of ${\phi } / {\psi }$ yields ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\psi })}$ . Applying (15) yet again shows ${v} \Vdash {\psi }$ , proving 2.

Conversely, suppose that 1 does not hold. We thus obtain a substitution $\sigma : \mathcal {L}(X) \to \mathcal {L}(Y)$ such that ${\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\phi })}$ and $\not {\vdash }_{\mathsf {IPC}} {\mathord {\sigma }(\mathord {\psi })}$ , where ${Y}$ can safely be assumed to be finite. As a consequence, we know ${\mathsf {u}}: {\mathsf {U}(Y)} \to {\mathcal {P}(Y)}$ to be such that ${\mathsf {u}} \Vdash {\mathord {\sigma }(\mathord {\phi })}$ and ${\mathsf {u}} \not \Vdash {\mathord {\sigma }(\mathord {\psi })}$ via Corollary 2.10. Now apply Lemma 4.11, in order to obtain the model ${\sigma ^{*}({\mathsf {u}})} : {\mathsf {U}(Y)} \to {\mathcal {P}(X)}$ and a $\Sigma $ -adequate map $f: {\mathsf {u}} \to {\sigma ^{*}({\mathsf {u}})}$ . The desired is obtained through Lemma 4.9. ⊣

5 Decidability of admissibility

Even though we now know that adequately exact models suffice to determine the admissible rules of $\mathsf {IPC}$ , the problem of decidability is not yet solved. The definition of adequate exactness is in no way intrinsic and it is not at all apparent that one can decide whether a model is adequately exact. In this section, we give an intrinsic description of adequate exactness. This description is to be sufficiently concrete, so that it can clearly be decided on finite models.

Roughly speaking, the notion of adequate extendibility we introduce here stands to adequate exactness as extendibility stands to exactness. We show that a model is adequately exact precisely if it is adequately extendible. As a consequence, admissibility of $\mathsf {IPC}$ is decidable. Furthermore, the proofs given in this section can be used to reprove some popular results in the literature, among which the characterization of finite projective Heyting algebras.

We first introduce a generalization of the concept of a cover, as treated in Definition 2.3. It is an easy exercise to show that this new notion is indeed a generalization of Definition 2.3. Definition 5.1 is a semantic way of looking at the notion that Rybakov uses. The correspondence between this semantic notion and the more syntactic approach as taken by Rybakov is given in Lemma 5.2.

Definition 5.1 (Adequate Cover)

Let P be a poset, let ${\mathcal {D}}$ be a set of subsets, let $p \in P$ , and let $W \subseteq P$ . We say that W is a ${\mathcal {D}}$ -adequate cover of p, denoted ${W}{\!\mathrel {\kappa _{\mathcal {D}}}}p$ , whenever:

(17) $$ \begin{align} \text{if } {\mathord{\uparrow}{p}} \cap D \not= \emptyset \text{ then } p \in D \text{ or } {\mathord{\uparrow}{W}} \cap D \not=\emptyset, \text{ for all } D \in {\mathcal{D}}. \end{align} $$

In the following, we write $W\!{\mathrel {\kappa _{\Sigma }}} p$ to mean that ${W}\!{\mathrel {\kappa _{{\mathcal {D}}}}} p$ for ${\mathcal {D}} = {\mathcal {D}}^{\Sigma }_{v}$ . Recall Definition 2.3, where we defined $W \ {\mathrel {\kappa }}\ p$ . The above definition is a generalization of this concept. Indeed, if the ambient model is order-defined, then $W \ {\mathrel {\kappa }}\ p$ is equivalent to ${W}\!{\mathrel {\kappa _{\Sigma }}} p$ for $\Sigma := \mathcal {L}(X)$ . ¹⁵

Lemma 5.2. Let ${v}: P \to {\mathcal {P}(X)}$ be a model, let $\Sigma \subseteq \mathcal {L}(X)$ be an adequate set, and let ${\mathcal {D}} = {\mathcal {D}}^{\Sigma }_{v}$ . The following are equivalent for all $p \in P$ and finite $W \subseteq P$ :

1. 1. ${W}\!{\mathrel {\kappa _{\Sigma }}} p$ ;

2. 2. the equivalence (18) holds for all ${\phi } {\rightarrow } {\psi } \in \Sigma $ and $p \in P$ .

   (18) $$ \begin{align} v, p \Vdash \phi \rightarrow \psi \text{ iff } v, W \Vdash \phi \rightarrow \psi \text{ and } (v, p \Vdash \phi \text{ implies } v, p \Vdash \psi). \end{align} $$

Proof. Suppose 1 holds and let ${\phi } {\rightarrow } {\psi } \in \Sigma $ be arbitrary. The implication from left to right in (18) is immediate, as $W \subseteq {\mathord {\uparrow }{p}}$ . In order to prove the other direction, we assume that ${v}, p \not \Vdash {\phi } {\rightarrow } {\psi }$ . It is clear that ${\mathord {\uparrow }{p}} \cap ({{[\kern-3pt[ {\phi } ]\kern-3pt]}_{v}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{v}}) \not =\emptyset $ , hence we know that either $p \in {{[\kern-3pt[ {\phi } ]\kern-3pt]}_{v}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{v}}$ or ${\mathord {\uparrow }{W}} \cap ({{[\kern-3pt[ {\phi } ]\kern-3pt]}_{v}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{v}}) \not = \emptyset $ . The former entails ${v}, p \Vdash {\phi }$ and ${v}, p \not \Vdash {\psi }$ , whereas the latter ensures ${v}, W \not \Vdash {\phi } {\rightarrow } {\psi }$ . This proves 2.

Conversely, suppose 2 holds. Take an arbitrary $D \in {\mathcal {D}}^{\Sigma }_{v}$ , a point $p \in P$ , and suppose that ${\mathord {\uparrow }{p}} \cap D \not = \emptyset $ . We know that $D = {{[\kern-3pt[ {\phi } ]\kern-3pt]}_{v}} - {{[\kern-3pt[ \psi ]\kern-3pt]}_{v}}$ for some ${\phi } {\rightarrow } {\psi } \in \Sigma $ . It thus follows that ${v}, p \not \Vdash {\phi } {\rightarrow } {\psi }$ . By (18), we know that ${v}, W \not \Vdash {\phi } {\rightarrow } {\psi }$ or ${v}, p \Vdash {\phi }$ and ${v}, p \not \Vdash {\psi }$ . The latter disjunct entails $p \in D$ , whereas the former entails ${\mathord {\uparrow }{W}} \cap D \not =\emptyset $ . This proves 1, as desired. ⊣

Recall that we motivated the usefulness of the notion of covers via Lemma 2.4. The following Lemma 5.3 plays an analogous role in justifying the purpose of adequate covers.

Lemma 5.3. Let P and ${Q}$ be Kripke frames, let ${\mathcal {D}}$ be a set of subsets of ${Q}$ , and let $f: P \to {Q}$ be a monotonic map. Suppose that P is image finite. The following are equivalent:

1. 1. the function f satisfies the cdc for ${\mathcal {D}}$ ;

2. 2. for every $p \in P$ and for every finite $W \subseteq P, if\ W \ {\mathrel {\kappa }}\ p$ , then $f(W) {\mathrel {\kappa _{\mathcal {D}}}} f(p)$ .

Proof. Suppose 1 holds. Let $p \in P$ and $W \subseteq P$ be such that W is finite and $W \ {\mathrel {\kappa }}\ p$ . Via monotonicity, it follows that $f(W) \subseteq {\mathord {\uparrow }{{f(p)}}}$ . Fix a $D \in {\mathcal {D}}$ and suppose that ${\mathord {\uparrow }{f(p)}} \cap D \not =\emptyset $ . As f is assumed to have the cdc for D, we know that $f({\mathord {\uparrow }{p}}) \cap D \not = \emptyset $ , so we can take some $q \geq p$ such that $f(q) \in D$ . Because $W \ {\mathrel {\kappa }}\ p$ , we now know that either $p = q$ or $q \in {\mathord {\uparrow }{W}}$ . In the former case, we know that $f(p) = f(q) \in D$ . In the latter case, there is a $w \in W$ such that $w \leq q$ . Consequently, $f(q) \geq f(w)$ and so $f(q) \in {\mathord {\uparrow }{f(W)}} \cap D$ , as desired.

Conversely, suppose 2 holds. Let $p \in P$ and $D \in {\mathcal {D}}$ be such that ${\mathord {\uparrow }{f(p)}} \cap D \not = \emptyset $ . We proceed by well-founded induction along $n := | {\mathord {\uparrow }{p}} | $ . Suppose that we know:

(19) $$ \begin{align} {\mathord{\uparrow}{f(k)}} \cap D \not=\emptyset \text{ implies } f({\mathord{\uparrow}{k}}) \cap D \not=\emptyset \text{ for all } k \in P \text{ with } | {\mathord{\uparrow}{k}}| < n. \end{align} $$

Our goal is to prove that $f({\mathord {\uparrow }{p}}) \cap D \not = \emptyset $ . First, note that $W := {\mathord {\unicode{x21A5} }{p}}$ is finite and satisfies $W \ {\mathrel {\kappa }}\ p$ . By 2, we thus know $f(W) {\mathrel {\kappa _{\mathcal {D}}}} f(p)$ . We gather that $f(p) \in D$ or ${\mathord {\uparrow }{{f(W)}}} \cap D \not = \emptyset $ . In the former case, we are done, so assume we are in the latter case. This yields some $w \in W$ such that ${\mathord {\uparrow }{f(w)}} \cap D \not =\emptyset $ . We know that:

$$ \begin{align*} \bigcup_{s \in W} f({\mathord{\uparrow}{s}}) \subseteq f({\mathord{\uparrow}{p}}),\\[-20pt] \end{align*} $$

hence (19) finishes the argument when instantiating $k = w$ . We have thus proven 1, as desired. ⊣

The following Definition 5.4 is a generalization of Definition 3.9. When instantiating ${\mathcal {D}}$ to ${\mathcal {D}}^{\Sigma }_{v}$ for some adequate set $\Sigma \subseteq \mathcal {L}(X)$ , one can see reflections of this notion in Rybakov (1990b, Theorem 15.3) and Odintsov and Rybakov (2013, Proposition 4.1.b) through the lens of Lemma 5.2.

Definition 5.4 (Adequately Extendible)

Let P be a poset and let ${\mathcal {D}}$ be a set of subsets of P. We say that P is adequately extendible for ${\mathcal {D}}$ whenever there is a point $p \in P$ to each finite $W \subseteq P$ such that $W {\mathrel {\kappa _{\mathcal {D}}}} p$ .

A function $\mu : {\mathcal {P}(P)} \to P$ is said to be an adequate choice of covers for ${\mathcal {D}}$ , whenever $W {\mathrel {\kappa _{\mathcal {D}}}} \mu (W)$ for all $W \subseteq P$ . Clearly, a finite poset is adequately extendible precisely if it has an adequate choice of covers. This might make the latter notion appear redundant, yet it is quite convenient in practise. We use this notion in the proof of Theorem 5.6 below, where it gives us a handle on the choices involved.

Theorem 5.5 is the main conclusion of this section. It shows that adequately exact models are the same as adequately extendible models. The proof in one direction is relatively straightforward and quite reminiscent of Lemma 3.10. The remainder of this section is devoted to the other direction.

Theorem 5.5. Let $v: P \to {\mathcal {P}(X)}$ be a finite model and let ${\mathcal {D}}$ be a set of subsets of P. The following are equivalent:

1. 1. the model ${v}$ is adequately exact for ${\mathcal {D}}$ ;

2. 2. the model ${v}$ is adequately extendible for ${\mathcal {D}}$ .

Proof. Proof of Theorem 5.5, 1 implies 2

Suppose 1 holds. We know there to be a finite set of variables ${Y}$ , together with a surjective ${\mathcal {D}}$ -adequate map $f: {\mathsf {u}} \to {v}$ , where ${\mathsf {u}}: {\mathsf {U}(Y)} \to {\mathcal {P}(Y)}$ is the universal model on Y. Let $W \subseteq {P}$ be a finite subset, we need to find some $p \in {P}$ such that $W {\mathrel {\kappa _{{\mathcal {D}}}}} p$ .

Consider the set $f^{-1}(W)$ . Fix a finite antichain $S \subseteq f^{-1}(W)$ satisfying the equation ${\mathord {\uparrow }{S}} = {\mathord {\uparrow }{{f^{-1}(W)}}}$ . We know there to be a point $q \in {\mathsf {U}(Y)}$ such that $S \ {\mathrel {\kappa }}\ q$ . It is easy to see that $f^{-1}(W) \ {\mathrel {\kappa }}\ q$ holds as well. By Lemma 5.3, we know that $f\left (\big .f^{-1}(W)\right ) = W {\mathrel {\kappa _{{\mathcal {D}}}}} f(q) =: p$ , proving 2. ⊣

Instead of proving the other direction directly, we take a detour through the following Theorem 5.6.

Theorem 5.6 (Extension Theorem)

Let ${v}: P \to {\mathcal {P}(X)}$ be an order-defined finite model, let ${\mathcal {D}} \subseteq {\mathcal {P}(P)}$ be a set of subsets, and let $\mu : {\mathcal {P}(P)} \to {P}$ be an adequate choice of covers for ${\mathcal {D}}$ . Consider the universal model ${\mathsf {u}}: {\mathsf {U}(Y)} \to {\mathcal {P}(Y)}$ on a finite set of variables ${Y}$ and the submodel ${u}: U \to {\mathcal {P}(Y)}$ generated by a definable upset $U \subseteq {\mathsf {U}(Y)}$ . If there is a ${\mathcal {D}}$ -adequate map $g: u \to v$ , then there exists a ${\mathcal {D}}$ -adequate map $f: {\mathsf {u}} \to {v}$ satisfying $f \restriction U = g$ .

Proof. Proof of Theorem 5.5, 2 implies 1

Suppose 2 holds. We define ${Y} := {X} + {P}$ and construct a model ${u}^*$ as:

$$ \begin{align*} u^{*}: {P} \to {\mathcal{P}(Y)}, \quad p \mapsto {v}(p) \cup \big\{ q \in {P} \;|\; p \leq q \big\}. \end{align*} $$

Note that the model ${u}^*$ is order-defined. Indeed, one can readily verify that the following equivalences hold for all $p, q \in {P}$ :

$$ \begin{align*} p \leq q &\quad \text{iff } q \Vdash p;\\ q \not\leq p & \quad \text{iff } q \Vdash k \text{ for some } k \not\leq p. \end{align*} $$

Hence, through Lemma 2.13, there is an upset $U \subseteq {\mathsf {U}(Y)}$ such that the model ${u} := {\mathsf {u}} \restriction U: U \to {\mathcal {P}(Y)}$ is isomorphic to ${u}^*$ , where ${\mathsf {u}}: {\mathsf {U}(Y)} \to {\mathcal {P}(X)}$ . Write $g: u \to u^{*}$ and $g^{-1}: {u}^{*} \to u$ for the maps of Kripke models we thus know to exist.

By Theorem 5.6, there exists some ${\mathcal {D}}$ -adequate map $f: {\mathsf {u}} \to {u}^*$ such that $f \restriction U = g$ . The latter condition guarantees that the $\Sigma $ -adequate map f is surjective. Finally, observe that the map ${\mathrm {id}_{P}}: {P} \to {P}$ is a definable map $h: u^{*} \to {v}$ , simply because every upset in ${u}^*$ is definable. We can thus construct a surjective ${\mathcal {D}}$ -adequate map $h \circ f : {\mathsf {u}} \to {v}$ through Lemma 4.2. This shows that ${v}$ is adequately exact for ${\mathcal {D}}$ , proving 1. ⊣

The Extension Theorem 5.6 is the core of Rybakov’s method towards obtaining decidability of admissibility. Indeed, it has been proven many time over, in many different guises. Our formulation of the proof is mostly inspired by Odintsov and Rybakov (2013, Theorem 4.2), although the presentation is quite different.

The earliest occurrence of this technique in the literature came from Rybakov (1984a, Lemma 4), where a similar statement is proven for $\mathsf {S4}$ . ¹⁶ It is not straightforward to recognize the statement of Theorem 5.6 in Lemma 4 of Rybakov (1984a). Indeed, this lemma makes no mention of the notion of adequate extendibility, or anything similar to it. Instead, it concretely describes six properties, some of which (property 4 and 6 to be precise) are analogous to what we encompass by adequate extendibility. A more honest description would be to say that this lemma proves the implication from 1 to 2 of Theorem 5.5, immediately followed by the observation that adequately exact models are sound with respect to admissibility.

Before we move on to the actual proof, let us first give a rough exposition of the technique involved. To this end, we consider the edge-case where g is the identity map ${\mathrm {id}_{U}}: U \to U$ . To satisfy all prerequisites, the upset $U \subseteq {\mathsf {U}(X)}$ of the universal model ${\mathsf {u}}: {\mathsf {U}(X)} \to {\mathcal {P}(X)}$ ought to be finite. The goal of the theorem thus becomes constructing a definable map $f: {\mathsf {u}} \to U$ such that f satisfies the cdc for ${\mathcal {D}}$ and f obeys the equality $f \restriction U = {\mathrm {id}_{U}}$ . This goal is attainable no matter the choice of ${\mathcal {D}}$ ; indeed, it is possible to make f a definable map.

Let us first illustrate why there exists a map of Kripke frames and defer thoughts of definability. We have thus reduced the Extension Theorem 5.6 to the following, which is but a reformulation of Ghilardi (2004, Proposition 4).

Theorem 5.7. Let $U \subseteq {\mathsf {U}(X)}$ be an upset that is both finite and extendible. ¹⁷ Now, there exists a map of Kripke frames $f: {\mathsf {U}(X)} \to U$ such that $f \restriction U = {\mathrm {id}_{U}}$ .

Proof. Proof by Ghilardi (2004)

Observe that, if the map f were to exist, it ought to preserve covers by Lemma 2.4. We can thus define the value of the map f on $q \in {\mathsf {U}(X)}$ inductively along the height of q. If $q \in U$ then $f(q)$ is defined to be q. Otherwise, we know that $f({\mathord {\unicode{x21A5} }{q}})$ already has been defined. This subset of U must cover at least one node, define $f(q)$ to equal one of these. The resulting function is a map of Kripke frames. ⊣

The above construction is quite elegant in its simplicity, yet it does have two major drawbacks. First, at no finite stage in the process can the map f be seen as completed or fully determined. Second, it does not show that f is definable. One can fill both of these lacunae by using the method given in the proof below.

Observe that there exists a finite number N, such that every point in U generates an upset of size at most N. In general, the number $N := |U|$ certainly does the trick. We construct a definable upset ${\mathsf {A}(W)} \subseteq {\mathsf {U}(X)}$ per subset $W \subseteq U$ . These upsets will be such that their union equals the entire universal model. Moreover, the value of $f: {\mathsf {U}(X)} \to U$ at $q \in {\mathsf {U}(X)}$ is determined by the smallest $S \subseteq U$ such that $q \in {\mathsf {A}(W)}$ and this value will be covered by W. This also makes it clear that W must generate the same upset as $f({\mathord {\unicode{x21A5} }{q}})$ .

In the proof below, we take an approach similar to the above. Do note that the prerequisites are quite different; Theorem 5.6 never actually assumes that ${P}$ is extendible. Indeed, the theorem requires that ${P}$ is adequately extendible for ${\mathcal {D}}$ , given some fixed ${\mathcal {D}}$ . This matters not, as in the reasoning above one could replace cover by adequate cover for ${\mathcal {D}}$ and the argument applies mutatis mutandis.

For the applicability of this theorem, it is crucial that preimages of upsets under f are definable. As illustrated above, the crux of the matter is that such preimages are unions of ${\mathsf {A}(W)}$ for suitably chosen $W \subseteq {P}$ . These sets ${\mathsf {A}(W)}$ are constructed inductively along the size of W, together with partial definitions of the desired map f. The majority of the work lies in making sure that these sets ${\mathsf {A}(W)}$ behave coherently and that their union equals the entirety of ${\mathsf {U}(X)}$ .

In the proof below, we construct a sequence of maps such that five conditions are satisfied. Let us make a few remarks on these conditions. The conditions of Compatibility and Closed Domain are quite straightforward; the former is a natural ingredient of a piece-wise construction and the latter is the piece-wise formulation of the closed domain condition f ought to satisfy.

The condition Domain Growth ensures that the sequence converges to a map which has all of the universal model in its domain. Image bound, on the other hand, ensures that the division of ${\mathsf {U}(X)}$ into the not necessarily disjoint upsets ${\mathsf {A}(W)}$ for $W \subseteq {P}$ contains enough information to specify the behavior of f. Finally, the condition Identity ensures that the resulting map satisfies $f \restriction U = g$ .

Proof. Proof of Theorem 5.6

We construct a finite sequence of monotonic maps with increasing domains, in such a way that the final map in this series is the desired ${\mathcal {D}}$ -adequate map $f: {\mathsf {u}} \to {v}$ . For greater notational convenience, let us write

$$ \begin{align*} {\mathcal{P}}_{n}(P) := \{ W \subseteq {P} \;|\; n = |W| \}. \end{align*} $$

We also define the natural number $N := | {P} | + 1$ . We claim that for each $n \leq N$ and each $W \subseteq {\mathcal {P}}_{n}(P)$ there exists a definable upset ${\mathsf {A}(W)} \subseteq {\mathsf {U}(X)}$ and a ${\mathcal {D}}$ -adequate map $f_{n}: {\mathop {\mathrm {dom} f_{n}}} \to {P}$ , satisfying the following conditions for all $n \leq N$ .

1. Compatibility For all $m \leq n$ we have that: ${f_{m}} \subseteq {\mathop {\mathrm {dom}\ f_{n}}} \subseteq {U(X)}$ and $ f_{m} = f_{n} \restriction {\mathop {\mathrm {dom}\ f_{m}}}$ .

2. Closed Domain For all $q \in {\mathop {\mathrm {dom}\ f_{n}}}$ and $D \in {\mathcal {D}}$ we have that ${\mathord {\uparrow }{{f_{n}(q)}}} \cap D \not =\emptyset $ implies $f_{n}({\mathord {\uparrow }{q}}) \cap D \not =\emptyset $ .

3. Domain Growth If $|f_{n}({\mathord {\unicode{x21A5} }{q}})| < n$ then $q \in {\mathop {\mathrm {dom}\ f_{n}}}$ .

4. Image Bound For all $W \in {\mathcal {P}}_{n}(P)$ , $q \in {\mathsf {A}(W)}$ implies $f_{n}( {\mathord {\unicode{x21A5} }{q}}) \subseteq W$ .

5. Identity The equality $f_{0} = g$ holds.

Suppose that the above can be constructed. Due to Domain Growth, it is clear that ${\mathop {\mathrm {dom} f_N}} = {\mathsf {U}(X)}$ . Indeed, any $q \in {\mathsf {U}(X)}$ satisfies

$$ \begin{align*} \big| f_N({\mathord{\unicode{x21A5}}{q}}) \big| \leq |{P}| < |{P}| + 1 = N, \end{align*} $$

so $q \in {\mathop {\mathrm {dom}\ f_N}}$ follows. The map $f_N$ satisfies all constraints imposed upon f, as follows immediately from Compatibility, Closed Domain and Identity. Consequently, we know that we need but prove that these constraints can truly be satisfied.

The definitions of ${\mathsf {A}(W)}$ and $f_n$ , combined with their respective proofs of correctness, will proceed by induction along n. Let us first, uniformly for all cases, define

(20) $$ \begin{align} {\mathop{\mathrm{dom}\ f_n}}:= U \cup \bigcup\limits_{i \,<\, n} \bigcup\limits_{S \in {\mathcal{P}}_{i}(P)} {\mathsf{A}(S)}. \end{align} $$

In the case that $n = 0$ , we simply define $f_0 = g$ . We also construct the set ${\mathsf {A}(W)}$ for $W \in {\mathcal {P}}_{0}(P)$ . Know that $W = \emptyset $ , so it suffices to define

$$ \begin{align*} {\mathsf{A}(\emptyset)} := \big\{ q \in {\mathsf{U}(X)} \;|\; \text{ q is maximal} \big\}. \end{align*} $$

This upset is finite and as such definable. Let us now verify that all conditions are satisfied. Indeed, Compatibility holds trivially, Closed Domain is valid by assumption, and Identity holds by construction. See that, if $q \Vdash {\mathsf {A}(\emptyset )}$ , then q is maximal and so ${\mathord {\unicode{x21A5} }{q}} = \emptyset $ , proving Image Bound. Moreover, $\left | \big . f_0({\mathord {\uparrow }{q}}) \right | < 0$ is never satisfied, hence Domain Growth holds vacuously. We have thus verified all conditions.

We now turn to the case where $n = m + 1$ and define the map $f_{m + 1}$ . First note that, through (20), we know

(21) $$ \begin{align} {\mathop{\mathrm{dom}\ f_{m+1}}} = {\mathop{\mathrm{dom}\ f_{m}}} \cup \bigcup_{S \in {\mathcal{P}}_{m}(P)} {\mathsf{A}(S)}. \end{align} $$

Recall that, for any $S \in {\mathcal {P}}_{m}(P)$ , the upset ${\mathsf {A}(S)}$ is known to be definable by induction. Using this, we define $f_{m+1}$ by cases:

(22) $$ \begin{align} f_{m+1}(q) := f_{m}(q) \qquad\quad\qquad \text{if } q \in {\mathop{\mathrm{dom}\ f_{m}}}, \end{align} $$

(23) $$ \begin{align} f_{m+1}(q) := \mu \big(f_m\big( {\mathord{\unicode{x21A5}}{q}} \big) \big) \kern1.5em\qquad \text{if } q \in {\mathop{\mathrm{dom}\ f_{m+1}}} \text{ and } q \not\in{\mathop{\mathrm{dom}\ f_{m}}}. \end{align} $$

Before we continue, we first prove the following.

(24) $$ \begin{align} \begin{split} & \text{if } q \in {\mathop{\mathrm{dom}\ f_{m+1}}} \text{ and } q \not\in {\mathop{\mathrm{dom}\ f_m}}, \\ & \text{then } f_m({\mathord{\unicode{x21A5}}{q}}) \text{ is the unique } S \in {\mathcal{P}}_{m}(P) \text{ with } q \in {\mathsf{A}(S)}. \end{split} \end{align} $$

We know that there exists some $S \in {\mathcal {P}}_{m}(P)$ such that $q \in {\mathsf {A}(S)}$ , due to (21). From Image Bound, we gather that $f_m({\mathord {\unicode{x21A5} }{q}}) \subseteq S$ . If this inclusion were strict, then

$$ \begin{align*} \left| f_m({\mathord{\unicode{x21A5}}{q}}) \right| < |S| = m, \end{align*} $$

so Domain Growth would yield $q \in {\mathop {\mathrm {dom}\ f_m}}$ . Yet we explicitly assumed this not to be the case, a contradiction. This entails $W = f_m({\mathord {\unicode{x21A5} }{q}})$ , proving (24).

Let us now prove that the map $f_{m+1}$ is monotonic. Suppose $q,k \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ are given such that $q \leq k$ holds. We distinguish three cases below, these are both exhaustive and mutually exclusive.

1. 1. Both q and k are in ${\mathop {\mathrm {dom}\ f_{m}}}$ .

2. 2. $q \not \in {\mathop {\mathrm {dom}\ f_{m}}}$ and $k \in {\mathop {\mathrm {dom}\ f_{m}}}$ .

3. 3. Neither q nor k are in ${\mathop {\mathrm {dom}\ f_{m}}}$ .

In the case 1, the desired is immediate, as $f_m$ is monotonic by induction. In the case 2, observe that $f_{m}(k) \in f_m({\mathord {\unicode{x21A5} }{q}})$ . By definition (23) and the assumption on $\mu $ , we know that $f_{m+1}(q) = \mu ( f_m({\mathord {\unicode{x21A5} }{k}}) ) \leq f_m(k)$ , resolving this case.

Finally, we treat the case 3. Because $q \in {\mathop {\mathrm {dom}\ f_{m+1}}} - {\mathop {\mathrm {dom}\ f_{m}}}$ , we know $q \in {\mathsf {A}({f_m({\mathord {\unicode{x21A5} }{q}})})}$ by (24). As $q \leq k$ , it also follows that $k \in {\mathsf {A}({f_m({\mathord {\unicode{x21A5} }{q}})})}$ . Another application of (24) now yields $f_{m}({\mathord {\unicode{x21A5} }{q}}) = f_{m}({\mathord {\unicode{x21A5} }{k}})$ , proving

$$ \begin{align*} f_{m+1}(q) = \mu{} ( f_{m}({\mathord{\unicode{x21A5}}{q}}) ) = \mu{}( f_{m}({\mathord{\unicode{x21A5}}{k}})) = f_{m+1}(k). \end{align*} $$

We have thus shown that $f_{m+1}(q) \leq f_{m+1}(k)$ in all cases 1, 2, 3, hence $f_{m+1}$ is monotonic.

We now proceed to prove that $f_{m+1}$ is definable. To this end, let $U \subseteq {P}$ be a definable upset in ${v}: {P} \to {\mathcal {P}(X)}$ . We claim that $f_{m+1}^{-1}(U)$ can be expressed as:

(25) $$ \begin{align} f_{m+1}^{-1}(U) = f_m^{-1}(U) \cup \bigcup \big\{{\mathsf{A}(W)} \;|\; W \in {\mathcal{P}}_{m}(P) \text{ and } \mu{} (W) \in U\big\}. \end{align} $$

Once we know (25) to hold, the definability is immediate. Indeed, all constituents are known to be definable by induction and the connectives can all readily be internalized.

To prove the inclusion from left to right, suppose that $q \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ is such that $f_{m+1}(q) \in U$ . We distinguish between whether $q \in {\mathop {\mathrm {dom}\ f_m}}$ does or does not hold. If it does, then $f_{m+1}(q) = f_m(q)$ by (22) and hence $q \in f_{m}^{-1}(U)$ . In the case that it does not, we know that $q \in {\mathsf {A}({f_{m}({\mathord {\unicode{x21A5} }{q}})})}$ by (24). By definition (23), we know that

$$ \begin{align*} \mu{} \big( f_{m}({\mathord{\unicode{x21A5}}{q}}) \big) = f_{m+1}(q) \in U, \end{align*} $$

proving the desired.

To prove the other direction, we suppose that $q \in {\mathsf {U}(X)}$ is either such that $q \in {\mathop {\mathrm {dom}\ f_{m}}}$ , or $q \not \in {\mathop {\mathrm {dom}\ f_{m}}}$ and $q \in {\mathsf {A}(W)}$ for some $W \in {\mathcal {P}}_{m}(P)$ with $\mu {}(W) \in U$ . The former case is immediate. In the latter case, fix this W and note that (24) ensures $W = f_{m}({\mathord {\unicode{x21A5} }{q}})$ . Because $\mu {} (W) \in U$ and $f_{m+1}(q) = \mu {} (W)$ holds by definition (23), the desired follows.

Now, let us prove that the conditions are satisfied. It is clear that Compatibility holds. To show that Closed Domain holds, take some $q \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ and $D \in {\mathcal {D}}$ to be such that

$$ \begin{align*} {\mathord{\uparrow}{{f_{m+1}(q)}}} \cap D \not= \emptyset. \end{align*} $$

We distinguish two cases, either $q \in {\mathop {\mathrm {dom}\ f_m}}$ holds or it does not. If it does, then Compatibility and induction ensure that

$$ \begin{align*} f_{m+1}({\mathord{\uparrow}{{q}}}) \cap D = f_{m}({\mathord{\uparrow}{q}}) \cap D \not= \emptyset. \end{align*} $$

In the other case, definition (23) yields $f_{m + 1}(q) = \mu (f_{m}({\mathord {\unicode{x21A5} }{q}}) )$ . Observe that the inequality ${\mathord {\uparrow }{{f_{m+1}(q)}}} \cap D \not = \emptyset $ holds, hence we know of some $p \in {P}$ such that both $f_{m+1}(q) \leq p$ and $p \in D$ hold. By the assumption on $\mu $ , it follows that $f_{m+1}(q) \in D$ or $f_m({\mathord {\unicode{x21A5} }{q}}) \cap D \not = \emptyset $ . One can easily check that both disjuncts ensure

$$ \begin{align*} f_{m+1}({\mathord{\uparrow}{q}}) \cap D \not= \emptyset, \end{align*} $$

proving that the Closed Domain condition holds.

Finally, we construct the sets ${\mathsf {A}(W)}$ for $W \in {\mathcal {P}}_{m+1}(P)$ , prove their definability, and show that both the conditions Domain Growth and Image Bound hold.

(26) $$ \begin{align} {\mathsf{A}(W)} := \left\{ q \in {\mathsf{U}(X)} \;\bigg|\; \begin{array}{l} \text{if } k \in f^{-1}_{m}({\mathord{\uparrow}{p}}) \text{ then } k \in f^{-1}_{m}({\mathord{\unicode{x21A5}}{p}}), \\ \text{for all } k \geq q\ \text{and}\ p \in P - W \end{array}\right\} . \end{align} $$

Because ${v}: {P} \to {\mathcal {P}(X)}$ is assumed to be order-defined, we know that ${\mathord {\uparrow }{p}}$ is definable. We know $f_m$ to be a definable map through induction, hence $f^{-1}_{m}\left ({\mathord {\uparrow }{p}}\right )$ is definable as well. With this information, we can give the defining formula of ${\mathsf {A}(W)}$ as:

$$ \begin{align*} {\mathsf{def}\thinspace {\mathsf{A}(W)}} := \bigwedge\limits_{p \in {P} - W} {\mathsf{def}\thinspace { f^{-1}_{m}({\mathord{\uparrow}{p}}) }} {\rightarrow} {\mathsf{def}\thinspace {f^{-1}_{m}({\mathord{\unicode{x21A5}}{p}})}}. \end{align*} $$

We prove Domain Growth. Let $q \in {\mathsf {U}(X)}$ be such that $| f_{m+1}({\mathord {\unicode{x21A5} }{q}}) | < m + 1$ . If $q \in {\mathop {\mathrm {dom}\ f_{m}}}$ then $q \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ , as readily follows through Compatibility. Consider now the other case, where $q \not \in {\mathop {\mathrm {dom}\ f_{m}}}$ . Through Compatibility, we know that $f_{m}({\mathord {\unicode{x21A5} }{q}}) \subseteq f_{m+1}({\mathord {\unicode{x21A5} }{q}})$ . We distinguish two cases, either $| f_{m}({\mathord {\unicode{x21A5} }{q}}) | < m$ or $| f_{m}({\mathord {\unicode{x21A5} }{q}}) | = m$ . In the former case, we know $q \in {\mathop {\mathrm {dom}\ f_{m}}}$ by induction, a contradiction.

Let us focus on the latter case, that is, we assume $| f_{m}({\mathord {\unicode{x21A5} }{q}}) | = m$ . This ensures us that $f_{m+1}({\mathord {\unicode{x21A5} }{q}}) = f_{m}({\mathord {\unicode{x21A5} }{q}})$ . We argue by contradiction and assume that $q \not \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ . Our goal will be to derive that $q \in {\mathsf {A}({f_{m+1}({\mathord {\unicode{x21A5} }{q}})})}$ , which would ensure $q \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ , an immediate contradiction.

To this end, let $p \in {P} - f_{m+1}({\mathord {\unicode{x21A5} }{q}})$ and $k \geq q$ be given. Assume that $k \in f^{-1}_{m+1}({\mathord {\uparrow }{p}})$ . If $q = k$ holds, then $q \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ follows, a contradiction. So suppose that $k \in {\mathord {\unicode{x21A5} }{p}}$ . If $f_{m+1}(k) = p$ , then we have $p \in f_{m+1}({\mathord {\unicode{x21A5} }{q}})$ , another contradiction. This proves that $k \in f^{-1}_{m+1}({\mathord {\unicode{x21A5} }{p}})$ . We have thus proven that $q \in {\mathsf {A}({f_{m+1}({\mathord {\unicode{x21A5} }{q}})})}$ , as desired.

Finally, we prove that Image Bound holds. Let $W \in {\mathcal {P}}_{m+1}(P)$ be given. We wish to prove that if $q \in {\mathsf {A}(W)}$ , then $f_{m+1}({\mathord {\unicode{x21A5} }{q}}) \subseteq W$ . Suppose the contrary, that is, suppose there is some $k> q$ such that $k \in {\mathop {\mathrm {dom}\ f_{m+1}}}$ yet $f_{m+1}(k) \not \in W$ . We see that $p \in f^{-1}_{m+1}({\mathord {\uparrow }{p}})$ for $p := f_{m+1}(p) \not \in W$ . Clearly, $p < f_{m+1}(k)$ does not hold, a contradiction with $k \in f^{-1}_{m+1}({\mathord {\unicode{x21A5} }{p}})$ . This proves the desired, finishing the argument. ⊣