Proof. Left to the reader.

Proof. Let $A$ $B$ and $E\in {{\downarrow }^{\!{\varLambda }}\Gamma }$ such that ${\varLambda }\vdash E\to A$ . Since $E\in {{\downarrow }^{\!{\varLambda }}\Gamma }$ there is some $\theta $ and $E^\dagger \in {\Gamma (\mathsf {par})}$ such that $E$ $\theta (a)\leftrightarrow a$ for every $a\in \mathsf {atom}$ and ${{\varLambda }\vdash \theta (E)\leftrightarrow E^\dagger }$ . Hence by ${\varLambda }\vdash E\to A$ we have ${\varLambda }\vdash \theta (E)\to \theta (A)$ and thus ${{\varLambda }\vdash E^\dagger \to \theta (A)}$ . Since $E^\dagger \in \mathcal {L}_{0}(\mathsf {par})$ we have $\theta (E^\dagger )=E^\dagger $ and thus we may conclude ${\varLambda }\vdash \theta (E^\dagger \to A)$ . Then by $A$ $B$ we get ${\varLambda }\vdash \theta (E^\dagger \to B)$ and thus $E$ $\theta (E^\dagger \to B)$ . Since $E$ $\theta (a)\leftrightarrow a$ , we may conclude $E$ $E^\dagger \to B$ . Then since ${\varLambda }\vdash \theta (E)\leftrightarrow E^\dagger $ , we have $E$ $\theta (E)\to B$ . Again from $E$ $\theta (a)\leftrightarrow a$ we may conclude $E$ $E\to B$ and thus ${\varLambda }\vdash E\to B$ .

Question 1. What can be said about the other direction of Theorem 2.2?

Proof. Easy induction on the complexity of proof $[{\varLambda }]\vdash A\rhd B$ and left to the reader.

Proof. We only show $A$ $B$ iff $A$ $B$ and leave the similar argument for $A$ $B$ iff $A$ $B$ to the reader. The right-to-left direction holds since $\Gamma \subseteq \Gamma ^\vee $ . For the other direction assume that $A$ $B$ and let $E\in \Gamma ^\vee $ such that ${\varLambda }\vdash E\to A$ . Then $E=\bigvee _i E_i$ with $E_i\in \Gamma $ . Hence for every i we have ${\varLambda }\vdash E_i\to A$ . Then $A$ $B$ implies ${\varLambda }\vdash E_i\to B$ . Thus ${\varLambda }\vdash E\to B$ , as desired.

Proof. Left to the reader.

Question 2. As we saw in Theorem 2.5, the glb may be expressed via preservativity relation . One may think of $\Gamma $ -conservativity relation:

[Reference Visser23, Corollary 7.2] axiomatizes for ${\varLambda }=\mathsf {IPC}$ and $\Gamma =\mathsf {N}$ . We ask for an axiomatization for when we let $ {\varLambda }=\mathsf {IPC} $ and $ \Gamma =\mathsf {N} $ .

Proof. First assume that ${\varLambda }\vdash \lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}} \to B$ . Also let $E\in \Gamma $ such that ${\varLambda }\vdash E\to A$ . Theorem 2.5 implies $A$ $\lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}$ and hence ${\varLambda }\vdash E\to \lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}$ . Then by ${\varLambda }\vdash \lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}\to B$ we get ${\varLambda }\vdash E\to B$ , as desired.

For the other direction let $A$ $B$ . By definition we have $\lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}{\kern-1.2pt}\in{\kern-1.2pt} \Gamma $ and ${{\varLambda }\vdash {\kern-1.2pt}\lfloor{\kern-1.2pt} {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}{\kern-1.2pt}\to A}$ . Hence by $A$ $B$ we get ${\varLambda }\vdash \lfloor {A}\rfloor ^{{}^{\!{\varLambda }}}_{_{\!{\Gamma }}}\to B$ , as desired.

Proof. We only reason for the left-to-right direction. Let and R is a relation with the above mentioned properties. We define $f (w')$ by induction on the distance of a $w'\in W'$ from the minimal elements such that $w'\mathrel {R} f(w')$ and for every $v'\preccurlyeq ' w'$ we have $f(v')\preccurlyeq f(w')$ .

For every $\preccurlyeq '$ -minimal node $w'\in W'$ , define $f(w')$ an arbitrary $w\in W$ with $w' \mathrel {R} w$ . Note that such a w always exists and satisfies all required properties.

Then we define $f(w')$ for $w'\in W'$ , which is not minimal. As induction hypothesis, we assume that for every $u'\prec ' w'$ we already defined $f(u')\in W$ such that $u' \mathrel {R} f(u')$ and $v'\preccurlyeq ' u'$ implies $f(v')\preccurlyeq f(u')$ . Since $\mathcal {K}'$ is tree, there is a unique predecessor $u'\prec ' w'$ . Then by the induction hypothesis and properties of R, there is some $w\in W$ such that $f(u')\preccurlyeq w $ and $w'\mathrel {R}w$ . For some such w, define $f(w'):=w$ .

Proof. We first prove the left-to-right direction. The proof is almost identical to the proof of Theorem 6.9 in [Reference Visser, van Benthem, de Jongh and de Lavalette24] and we refer the reader to it for more details. Let $\mathcal {K}_i=(W_i,\preccurlyeq _i,\mathrel {V}_i)$ for $i\in \{0,1\}$ and $f:W_0\to W_1$ be the embedding of $\mathcal {K}_0$ in $\mathcal {K}_1$ . Moreover we may assume that f is surjective, otherwise we add a copy of $\mathcal {K}_1$ to $\mathcal {K}_0$ with a fresh root in beneath of them and then extend the embedding to the new nodes.

Define $\mathcal {K}_2:=(W_2,\preccurlyeq _2,\mathrel {V}_2)$ as follows:

• • $W_2:=\{ (w_0, w_1): w_0\in W_0 \text { and } f(w_0)\preccurlyeq _1 w_1\in W_1\}$ .

• • $(w_0, w_1)\preccurlyeq _2 (w^{\prime }_0, w^{\prime }_1)$ iff either of the following holds:

  1. – $w_0\preccurlyeq _0 w^{\prime }_0$ and $w_1=f(w_0)$ ;

  2. – $w_0=w^{\prime }_0$ and $w_1\preccurlyeq _1 w^{\prime }_1$ .

• • $(w_0, w_1)\mathrel {V}_2 a$ iff $w_1\mathrel {V}_1 a$ .

It is straightforward to show that $\mathcal {K}_2$ is a finite rooted tree-frame Kripke model with root $(\rho , f(\rho ))$ in which $\rho $ is the root of $\mathcal {K}_0$ . Also $\mathcal {K}_1$ and $\mathcal {K}_2$ are bisimilar. Moreover one may easily show that $g,$ as defined in the following, is an injective embedding of $\mathcal {K}_0$ into $\mathcal {K}_2$ : $g(w_0):=(w_0, f(w_0))$ .

For the proof of other direction, assume that and ${\mathcal {K}_i=(W_i,\preccurlyeq _i,\mathrel {V}_i)}$ for $i\in \{0,1,2\}$ . Let $f:W_0\longrightarrow W_2$ be the injective function witnessing . By induction on $w\in W_2$ ordered by $\prec _2$ , we also define the function $g:W_2\longrightarrow W_1$ such that for every $w\in W_2$ .

• • As the basic step of induction, for the root w of $W_2$ , define $g(w)$ as the root of $W_1$ .

• • For any $w\in W_2$ other than the root, we do as follows. Let w be the immediate successor of $v\in W_2$ . This means that $v\prec _2 w$ and there is no $v'$ such that $v\prec _2 v'\prec _2 w$ . By induction hypothesis, $g(v)$ is already defined and . Hence there is some $u\in W_1$ such that . Define $g(w)$ as some such u.

Then it can easily observed that the composition function $g\circ f:W_0\longrightarrow W_1$ is a function witnessing .

Proof. See [Reference Visser, van Benthem, de Jongh and de Lavalette24] or [Reference Visser23].

Proof. Observe that each formula can be written as $\bigvee \bigwedge C$ in which C is an atomic or implication, which we call it a component. We assume that disjunction and conjunction over empty set of formulas are defined as $\bot $ and $\top $ , respectively. Observe that the number of formulas in n atoms, $f(n)$ , is less than or equal to $2^{2^{g(n)}}$ , in which $g(n)$ is the number of components in n atoms. Then observe that $g(n+1)\leq (n+1)f(n)+ n+1$ , because one may assume that each component is either of the form $p\to A$ for some atomic p and some A in n atoms, or it is atomic. Hence the following recursive function is an upper bound for the number of all formulas in n atoms:

$$\begin{align*}f(0):=2,\quad \quad \quad \quad f(n+1):=2^{2^{(n+1)(f(n)+1)}}.\\[-33pt] \end{align*}$$

Proof. See [Reference Visser, van Benthem, de Jongh and de Lavalette24, Theorem 7.1.2].

Proof. Use induction on the complexity of A.

Proof. The first statement is due to this fact that the validity of -formulas is preserved under -submodels (see Theorem 3.5).

To see why B is $\mathsf {par}$ -subextendible, let $\mathcal {K}\Vdash A$ and $\mathcal {K}'\subseteq _{}^{{\mathsf {par}}} \mathcal {K}$ and $\mathcal {K}'\Vdash ^{^{\!\!-}} B$ seeking to find some $\mathcal {K}"\Vdash B$ which is $\mathsf {par}$ -variant of $\mathcal {K}'$ . Since $\mathcal {K}'\subseteq _{}^{{\mathsf {par}}} \mathcal {K}\Vdash p$ , we get $\mathcal {K}'\Vdash p$ . However, it might not be the case that $\mathcal {K}'\Vdash x$ , in which case we define $\mathcal {K}"$ by changing the valuation of $\mathcal {K}'$ on x at the root. Since $\mathcal {K}'\Vdash ^{^{\!\!-}} B$ , the resulted model $\mathcal {K}"$ is a Kripke model indeed (in the sense of having monotonicity of truth on atomics). Moreover obviously $\mathcal {K}"$ is a $\mathsf {par}$ -variant of $\mathcal {K}'$ and $\mathcal {K}"\Vdash B$ . This finishes showing $\mathsf {par}$ -subextendibility of B.

Finally to see why C is not $\mathsf {par}$ -subextendible, consider $\mathcal {K}:=(W,\prec ,\mathrel {V})$ as follows. Define $W:=\{0,1\}$ with $0\prec 1$ as the only accessibility relation. Also $1\mathrel {V} p$ and $0,1\mathrel {V} x$ are only valuations for atomics. Then we have $\mathcal {K}\Vdash C$ . Moreover the model $\mathcal {K}':=(W',\prec ',\mathrel {V}')$ defined as $W':=\{0\}$ and and $0\mathrel {V} x$ as only atomic valuation. Then $\mathcal {K}'\Vdash ^{^{\!\!-}} C$ (actually $\mathcal {K}'\Vdash ^{^{\!\!-}} D$ for every D) while there is no $\mathsf {par}$ -variant $\mathcal {K}"$ of $\mathcal {K}'$ such that $\mathcal {K}"\Vdash C$ (note that any $\mathsf {par}$ -variant of $\mathcal {K}'$ should validate $\neg p$ and hence not validating $\neg \neg p$ ).

Proof. For the left-to-right direction: let and $\mathscr {C}$ is a finite set of models of A. Then obviously $\sum (\mathscr {C},\mathcal {K})\Vdash ^{^{\!\!-}} A$ and hence by -subextendibility of A, there is an -variant of $\sum (\mathscr {C},\mathcal {K})\Vdash ^{^{\!\!-}} A$ which validates A.

For the right-to-left direction: let $\mathcal {K}\Vdash A$ and and $\mathcal {K}'\Vdash ^{^{\!\!-}} A$ . Without loss of generality, we also may assume that $\mathcal {K}$ and $\mathcal {K}'$ have the same valuations for atomics in , otherwise we may replace $\mathcal {K}_{f(w')}$ for $\mathcal {K}$ with f as the function witnessing and $w'$ as the root of $\mathcal {K}'$ . Obviously, we also have $\mathcal {K}_{f(w')}\Vdash A$ and . Let $w_i$ for $0\leq i\leq n$ be all the immediate successorsFootnote ¹ of the root of $\mathcal {K}'$ . Define $\mathscr {C}:=\{\mathcal {K}^{\prime }_{w_i}: 0\leq i\leq n\}$ . Then and $\mathscr {C}\Vdash A$ . Hence by -subextendibility of $\text {Mod}(A)$ , there is an -variant $\mathcal {K}"$ of $\sum (\mathscr {C},\mathcal {K})$ such that $\mathcal {K}"\Vdash A$ . Since $\mathcal {K}'$ and $\mathcal {K}$ validate the same atomics in , this implies that $\mathcal {K}"$ is also an -variant of $\mathcal {K}'$ .

Proof. First assume that A is extendible. It is obvious that then A is -subextendible. It remains only to show that A is satisfiable. Let $\mathcal {K}$ be an arbitrary single-node Kripke model. Then obviously $\mathcal {K}\Vdash ^{^{\!\!-}} A$ and hence by extendibility, there is a variant $\mathcal {K}'$ of $\mathcal {K}$ such that $\mathcal {K}'\Vdash A$ . Thus A is satisfiable.

For the other direction, assume that A is satisfiable and -subextendible. Also assume that $\mathcal {K}'$ is a Kripke model such that $\mathcal {K}'\Vdash ^{^{\!\!-}} A$ . Define the Kripke model $\mathcal {K}$ as follows. $\mathcal {K}$ and $\mathcal {K}'$ share the same frame and the atomic valuation of $\mathcal {K}$ at all nodes is the same and equal to the valuation which classically validates A (which is guaranteed by satisfiability condition on A). Then we have and hence by -subextendibility of A we get some variant $\mathcal {K}"$ of $\mathcal {K}'$ such that $\mathcal {K}"\Vdash A$ .

Proof. See the proof of Theorem 5 in [Reference Ghilardi3].

Proof. $1\to 2$ : From the definitions of $A^\ddagger $ , evidently $A^\ddagger \in {\mathsf {N}(\mathsf {par})}$ . Also observe that is A-identity. Then since A-identity substitutions are closed under composition, ${\theta ^{}_{\!\!A}}$ is A-identity.

$2\to 3$ : Let and $\mathcal {K}\Vdash A$ and $\mathcal {K}'\subseteq _{}^{{\mathsf {par}}} \mathcal {K}$ and $\mathcal {K}'\Vdash ^{^{\!\!-}} A$ . We are seeking some variant $\mathcal {K}"$ of $\mathcal {K}'$ such that $\mathcal {K}"\Vdash A$ . Let $\mathcal {K}"=\theta (\mathcal {K}')$ . First note that since $\theta $ is A-identity, $\mathcal {K}"$ is a $\mathsf {par}$ -variant of $\mathcal {K}'$ . Since $\mathcal {K}\Vdash A'$ , $A'\in {\mathsf {N}(\mathsf {par})}$ and $\mathcal {K}'\subseteq _{}^{{\mathsf {par}}}\mathcal {K}$ , Theorem 3.5 implies that $\mathcal {K}'\Vdash A'$ . Hence $\mathcal {K}'\Vdash \theta (A)$ , and by Lemma 3.8 we have $\mathcal {K}"\Vdash A$ .

$3\to 1$ : Let A be $\mathsf {par}$ -subextendible. We show $ \vdash A^\ddagger \leftrightarrow {\theta ^{}_{\!\!A}}(A)$ . We use induction on the height of the Kripke model $\mathcal {K}$ and show $\mathcal {K}\Vdash A^\ddagger \leftrightarrow {\theta ^{}_{\!\!A}}(A)$ . Suppose that $w_0$ is the root of $\mathcal {K}$ . By the induction hypothesis $\mathcal {K}\Vdash ^{^{\!\!-}} A^\ddagger \leftrightarrow {\theta ^{}_{\!\!A}}(A)$ , and since $A^\ddagger $ does not have any atomic variables, we have $\mathcal {K}\Vdash ^{^{\!\!-}} {\theta ^{}_{\!\!A}}(A^\ddagger \leftrightarrow A)$ . Then by Lemma 3.8, ${\theta ^{}_{\!\!A}}(\mathcal {K})\Vdash ^{^{\!\!-}} A^\ddagger \leftrightarrow A$ . We show ${\theta ^{}_{\!\!A}}(\mathcal {K})\Vdash A^\ddagger \leftrightarrow A$ . If ${\theta ^{}_{\!\!A}}(\mathcal {K})\nVdash ^- A^\ddagger $ , then ${\theta ^{}_{\!\!A}}(\mathcal {K})\nVdash ^- A$ and hence ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\nVdash A^\ddagger $ and ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\nVdash A$ . Then ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger \leftrightarrow A$ and we are done. So assume that ${\theta ^{}_{\!\!A}}(\mathcal {K})\Vdash ^{^{\!\!-}} A\wedge A^\ddagger $ . It is sufficient to show the following items:

• • ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A$ implies ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger $ . We use the definition of $A^\ddagger $ . Consider some . Also assume that for some node w of $\mathcal {K}$ . Then since and ${\theta ^{}_{\!\!A}}(\mathcal {K}),w\Vdash A$ , the following formula is one of the disjuncts in the definition of $A^\ddagger $ :

  $$ \begin{align*} \bigwedge [{\kern-1pt}[{{\theta^{}_{\!\!A}}(\mathcal{K})_w}]{\kern-1pt}]_{_{{\mathsf{N}(\mathsf{par})}}}, \end{align*} $$
  in which ${\theta ^{}_{\!\!A}}(\mathcal {K})_w$ is the restriction of ${\theta ^{}_{\!\!A}}(\mathcal {K})$ to w and its upward nodes. Obviously ${\theta ^{}_{\!\!A}}(\mathcal {K}),w\Vdash \bigwedge [{\kern-1pt}[{{\theta ^{}_{\!\!A}}(\mathcal {K})_w}]{\kern-1pt}]_{_{{\mathsf { N}(\mathsf {par})}}}$ and hence ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger $ .

• • ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger $ implies ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A$ . Let ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger $ . Also assume that ${\theta ^{}_{\!\!A}}(\mathcal {K})$ is -model, i.e., and . Since ${\theta ^{}_{\!\!A}}(\mathcal {K}),w_0\Vdash A^\ddagger $ , for some $\mathcal {K}_1\in \text {Mod}(A)$ with we have ${\theta ^{}_{\!\!A}}(\mathcal {K})\Vdash [{\kern-1pt}[{\mathcal {K}_1}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}$ . Theorem 3.7 implies that ${\theta ^{}_{\!\!A}}(\mathcal {K}) \preceq ^{{\mathsf {par}}}\mathcal {K}_1$ . Then Lemma 3.3 implies ${\theta ^{}_{\!\!A}}(\mathcal {K}) \preceq _1^{{\mathsf {par}}}\mathcal {K}_1$ and thus by Lemma 3.4 there is some $\mathcal {K}_2\Vdash A$ such that ${\theta ^{}_{\!\!A}}(\mathcal {K}) \subseteq _{}^{{\mathsf {par}}}\mathcal {K}_2$ . Since A is $\mathsf {par}$ -subextendible, there is a $\mathsf {par}$ -variant $\mathcal {K}'$ of $ {\theta ^{}_{\!\!A}}(\mathcal {K})$ such that $\mathcal {K}'\Vdash A$ . Thus Lemma 3.14 implies ${\theta ^{}_{\!\!A}}(\mathcal {K})\Vdash A$ .

Proof. Given A, by Theorem 3.16 it is sufficient to decide $\mathsf {IPC}\vdash {\theta ^{}_{\!\!A}}(A)\leftrightarrow A^\ddagger $ , which is decidable since $\mathsf {IPC}$ is decidable.

Proof. By Theorem 2.2 we have $A$ $\bigvee \Pi $ and hence by Theorem 2.4 we have $A$ $\bigvee \Pi $ . Thus Theorem 2.5 implies the desired result.

Proof. See [Reference Ghilardi3, Theorem 5]. We will also prove a generalization of this result in Theorem 3.30.

Proof. By induction on n, we define an upper bound $f(n)$ for the number of formulas $A\in \mathcal {L}_{0}$ with $c_{\!_\to \!}(A)\leq n$ .

1. 1. $f(0):$ Observe that any A with $c_{\!_\to \!}(A)=0$ is $\mathsf {IPC}$ -equivalent to a disjunction of conjunctions of atoms. Hence $f(0)=2^{2^m}$ is an obvious upper bound, in which m is the number of atoms in $\mathsf {atom}$ .

2. 2. $f(n+1):$ For every implication $B\to C$ with $c_{\!_\to \!}(B\to C)\leq n+1$ , we have $c_{\!_\to \!}(B),c_{\!_\to \!}(C)\leq n$ , and hence $f(n)^2$ is an upper bound for the number of inequivalent such formulas. Then since modulo $\mathsf {IPC}$ -provable equivalence every formula is a disjunction of conjunctions of atoms or implications, the following definition is an upper bound:

   $$ \begin{align*} f(n+1):=2^{2^{[m+f(n)^2]}}.\\[-51pt] \end{align*} $$

Proof. First we show that every $A\in \mathsf {N}$ has an $\mathsf {IPC}$ -equivalent $B\in \mathsf {N}$ such that in B only atoms of A are appeared and $B=\bigwedge _i\bigvee _j B_i^j$ and every implication in $B^j_i$ is of the form $a\to C$ , with $a\in \mathsf {atom}$ and C does not contain a. We will prove the above claim by induction on complexity of A. The cases for atomic, conjunction, and disjunction are easy and left to the reader. So assume that $A=E\to F$ . Since $A\in \mathsf {N}$ , E does not have implications. Hence it is equivalent to some formula of the form $\bigvee \Gamma $ such that every $D\in \Gamma $ is of the form $\bigwedge \Delta _D$ and $\Delta _D$ is a non-empty set of atomic formulas for every $D\in \Gamma $ . Thus A is equivalent to $\bigwedge _{D\in \Gamma }(\bigwedge \Delta _D\to F)$ . For every $D\in \Gamma $ , fix some $p_D\in \Delta _D$ and let $\Delta ^{\prime }_D:=\Delta _D\setminus \{p_D\}$ . Hence A is equivalent to $\bigwedge _{D\in \Gamma }(p_D\to (\bigwedge \Delta ^{\prime }_D\to F[p_D:\top ]))$ , in which $F[p_D:\top ]$ is the replacement of $\top $ for $p_D$ in F. This formula is of required shape and we are done.

Then one may easily prove the statement of this lemma by induction on the number of elements in $\mathsf {atom}$ : by induction hypothesis, for every $B^i_j=p\to C$ , we have $c_{\!_\to \!}(C)\leq \#\mathsf {atom} -1$ and hence $c_{\!_\to \!}(B^i_j)\leq \#\mathsf {atom}$ . This implies $c_{\!_\to \!}(B)\leq \# \mathsf {atom}$ .

Proof. Here we only give the definition of ${[{\kern-1pt}[{\mathcal {K}}]{\kern-1pt}]_{n}} $ by induction on n, and refer the reader to [Reference Ghilardi3, Proposition 1] for its proof.

Let $\mathcal {K}=(W,\preccurlyeq ,\mathrel {V})$ and define ${[{\kern-1pt}[{\mathcal {K}}]{\kern-1pt}]_{0}}:=\bigwedge \mathcal {K}(w_0)$ and

$$ \begin{align*} {[{\kern-1pt}[{\mathcal{K}}]{\kern-1pt}]_{n+1}}:=\bigwedge_{\{\mathcal{K}':\forall\, w\in W(\mathcal{K}'\nsim_n\mathcal{K}_w)\}} \left( {[{\kern-1pt}[{\mathcal{K}'}]{\kern-1pt}]_{n}}\to \bigvee_{\{\mathcal{K}": \mathcal{K}'\nleq_n\mathcal{K}"\}} {[{\kern-1pt}[{\mathcal{K}"}]{\kern-1pt}]_{n}} \right) .\\[-51pt] \end{align*} $$

Proof. For the left-to-right direction, use induction on n. For the right-to-left direction, use Lemma 3.23.

Proof. First observe that $\mathcal {K}\sim _n \mathcal {K}'$ is equivalent to $\mathcal {K}\leq _n\mathcal {K}'\leq _n\mathcal {K}$ and then use Corollary 3.24.

Proof. For the left-to-right direction, let $\mathcal {K}'\leq _n\mathcal {K}\in \text {Mod}(A)$ for some A with $c_{\!_\to \!}(A)\leq n$ . Since $\mathcal {K}\Vdash A$ , Corollary 3.24 implies $\mathcal {K}'\Vdash A$ and hence $\mathcal {K}'\in \text {Mod}(A)$ .

For the other direction, let $\mathscr {C}$ be $\leq _n$ -downward closed and define

$$ \begin{align*} A:=\bigvee_{\mathcal{K}\in\mathscr{C}}{[{\kern-1pt}[{\mathcal{K}}]{\kern-1pt}]_{n}}. \end{align*} $$

By Remark 3.21, the disjunction is finite and hence A is indeed a formula. One may easily observe that Lemma 3.23 implies that $c_{\!_\to \!}(A)\leq n$ and $\mathscr {C}=\text {Mod}(A)$ .

Proof. Easy and left to the reader.

Proof. Easy and left to the reader.

Proof. We only prove here the $\mathsf {par}$ -subextendibility of $\langle \mathscr {C}\rangle _n$ and leave other properties to the reader.

Let $\mathscr {F}'=\{\mathcal {K}^{\prime }_i\}_i$ be a finite set of models in $\langle \mathscr {C}\rangle _n$ , which are $\mathsf {par}$ -submodels of some $\mathcal {K}'\in \langle \mathscr {C}\rangle _n$ . By Remark 3.28 we may also assume that $\mathscr {F}'$ is stable. We must show that a $\mathsf {par}$ -variant of $\sum (\mathscr {F}',\mathcal {K}')$ belongs to $\langle \mathscr {C}\rangle _n$ . Since $\mathcal {K}'\in \langle \mathscr {C}\rangle _n$ and $\mathscr {C}$ is stable, there is some $\mathcal {K}\in \mathscr {C}$ such that $\mathcal {K}'\sim _{n-1}\mathcal {K}$ . Similarly, since $\mathcal {K}^{\prime }_i\in \langle \mathscr {C}\rangle _n$ , there is some $\mathcal {K}_i\in \mathscr {C}$ such that $\mathcal {K}^{\prime }_i\sim _{n-1}\mathcal {K}_{i}$ . Let $\mathscr {F}:=\{\mathcal {K}_i\}_i$ .

First we show that $\mathscr {F}$ is a $\mathsf {par}$ -submodel of $\mathcal {K}$ . Since $\mathscr {F}'$ is a $\mathsf {par}$ -submodel of $\mathcal {K}'$ , by Theorem 3.7 we have $\mathcal {K}^{\prime }_i\Vdash [{\kern-1pt}[{\mathcal {K}'}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}$ . From $\mathcal {K}^{\prime }_i\sim _{n-1}\mathcal {K}_i$ , Lemma 3.22, and Corollary 3.25 we get $\mathcal {K}_i\Vdash [{\kern-1pt}[{\mathcal {K}'}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}$ . Also since $\mathcal {K}'\sim _{n-1}\mathcal {K}$ , by Lemma 3.22 and Corollary 3.25 we have $ [{\kern-1pt}[{\mathcal {K}'}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}=[{\kern-1pt}[{\mathcal {K}}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}$ . Hence $\mathcal {K}_i\Vdash [{\kern-1pt}[{\mathcal {K}}]{\kern-1pt}]_{_{{\mathsf {N}(\mathsf {par})}}}$ , and by Theorem 3.7 we have $\mathcal {K}_i$ is a $\mathsf {par}$ -submodel of $\mathcal {K}$ . Hence $\mathscr {F}$ is a $\mathsf {par}$ -submodel of $\mathcal {K}$ .

We go back to the main proof. Since $\mathscr {F}$ is a $\mathsf {par}$ -submodel of $\mathcal {K}$ , by extendibility of $\mathscr {C}$ , there exists a $\mathsf {par}$ -variant $\hat {\mathcal {K}}$ of $\sum (\mathscr {F},\mathcal {K})$ in $\mathscr {C}$ . Let $w_0$ be the root of $\mathcal {K,}$ which is also the root of $\hat {\mathcal {K}}$ and let $w^{\prime }_0$ be the root of $\mathcal {K}'$ . Define the $\mathsf {par}$ -variant $\hat {\mathcal {K}}'$ of $\sum (\mathscr {F}',\mathcal {K}')$ for atomic $x\not \in \mathsf {par}$ as follows:

$$ \begin{align*} \hat{\mathcal{K}}',w^{\prime}_0\Vdash x \quad \Longleftrightarrow \quad \hat{\mathcal{K}},w_0\Vdash x. \end{align*} $$

It is sufficient to show that $\hat {\mathcal {K}}'\in \langle \mathscr {C}\rangle _n$ . For this aim it is sufficient to show $\hat {\mathcal {K}}'\leq _n \hat {\mathcal {K}}$ . From the definition of $\hat {\mathcal {K}}$ and $\hat {\mathcal {K}}'$ , it is clear that it is sufficient to show that $\hat {\mathcal {K}}'\sim _{n-1}\hat {\mathcal {K}}$ . We use induction on $k\leq n-1$ and show $\hat {\mathcal {K}}'\sim _{k}\hat {\mathcal {K}}$ .

If $k=0$ , we must show that for every atomic a we have

$$ \begin{align*} \hat{\mathcal{K}}',w^{\prime}_0\Vdash a \quad \Longleftrightarrow \quad \hat{\mathcal{K}},w_0\Vdash a. \end{align*} $$

For atomic variables x, by definition of $\hat {\mathcal {K}}'$ , we already have this. Also since $\hat {\mathcal {K}}$ is a $\mathsf {par}$ -variant of $\sum (\mathscr {F},\mathcal {K})$ , $\hat {\mathcal {K}}'$ is a $\mathsf {par}$ -variant of $\sum (\mathscr {F}',\mathcal {K}')$ and $\mathcal {K}\sim _{0}\mathcal {K}'$ , for every $p\in \mathsf {par}$ we also have

$$ \begin{align*} \hat{\mathcal{K}}',w^{\prime}_0\Vdash p \quad \Longleftrightarrow \quad \hat{\mathcal{K}},w_0\Vdash p. \end{align*} $$

Then let $0<k<n$ and show $\hat {\mathcal {K}}'\sim _k\hat {\mathcal {K}}$ . We have the following items to prove:

• • For every node $w'$ in $\hat {\mathcal {K}}'$ , there is some w in $\hat {\mathcal {K}}$ such that $\hat {\mathcal {K}}^{\prime }_{w'} \sim _{k-1}\hat {\mathcal {K}}_w$ . If $w'$ is the root of $\hat {\mathcal {K}}'$ , take w also the root of $\hat {\mathcal {K}}$ and we have the desired result by induction hypothesis. If $w'$ is not the root of $\hat {\mathcal {K}}'$ , since $\mathscr {F}'$ is stable, we may let $w'$ as a root $w^{\prime }_i$ of some $\mathcal {K}^{\prime }_i$ . Take $w=w_i$ . Then by definition of $\mathcal {K}_i$ , we have

  $$ \begin{align*} \hat{\mathcal{K}}^{\prime}_{w'}=\mathcal{K}^{\prime}_i\sim_{n-1}\mathcal{K}_i=\hat{\mathcal{K}}_{w}. \end{align*} $$
  Since $k-1\leq n-1$ , we have the desired result.

• • For every node w in $\hat {\mathcal {K}}$ , there is some $w'$ in $\hat {\mathcal {K}}'$ such that $\hat {\mathcal {K}}^{\prime }_{w'} \sim _{k-1}\hat {\mathcal {K}}_w$ . Again if w is the root, take $w'$ also the root and we are done by induction hypothesis. If w is not the root, there is some i such that w is a node of $\mathcal {K}_i$ . Since $\mathcal {K}_i\sim _{n-1}\mathcal {K}^{\prime }_i$ , there is some $w'$ in $\mathcal {K}^{\prime }_i$ such that $(\mathcal {K}^{\prime }_i)_{w'}\sim _{n-2}(\mathcal {K}_i)_w$ . Since $k-1\leq n-2$ , we have

  $$ \begin{align*} \hat{\mathcal{K}}^{\prime}_{w'}=(\mathcal{K}^{\prime}_i)_{w'}\sim_{k-1}(\mathcal{K}_i)_w =\hat{\mathcal{K}}_w, \end{align*} $$
  as desired.

Proof. Given a substitution $\theta $ and $A'\in {\mathsf {N}(\mathsf {par})}$ such that $ \vdash A'\to \theta (A)$ , we will find some $B^{A'}_\theta \in \mathcal {L}_{0}$ , with the following properties:

1. 1. $B^{A'}_\theta $ is ${\mathsf {N}}$ -projective.

2. 2. $ \vdash A'\leftrightarrow \theta (B^{A'}_\theta )$ .

3. 3. $ \vdash B^{A'}_\theta \to A$ .

4. 4. $c_{\!_\to \!}(B^{A'}_\theta )\leq n$ for $n:=\max \{c_{\!_\to \!}(A),1+\#\mathsf {par}\}$ ( $\#\mathsf {par}$ indicates the number of atoms in $\mathsf {par}$ ).

Then by items 1–3 (an independent subset of) the following set is an ${\mathsf {N}}$ -projective resolution for A:

$$ \begin{align*} \Pi:=\{ B^{A'}_\theta: A'\in{\mathsf{N}(\mathsf{par})} \text{ and } \theta \text{ is a substitution such that } \vdash A'\to \theta(A) \}. \end{align*} $$

Moreover Remark 3.21 and item (4) imply that $\Pi $ is finite, as desired. So it remains to find $B^{A'}_\theta $ with mentioned properties. Define

$$ \begin{align*} \mathscr{C}:=\theta(\text{Mod}(A')):=\{\theta(\mathcal{K}): \mathcal{K}\in\text{Mod}(A')\}. \end{align*} $$

Since $\langle \mathscr {C}\rangle _n$ has downward $\leq _n$ -closure condition, we may apply Lemma 3.26 and find some formula, e.g., $B^{A'}_\theta $ , such that $c_{\!_\to \!}(B^{A'}_\theta )\leq n$ (so item 4 is satisfied) and $\langle \mathscr {C}\rangle _n=\text {Mod}(B^{A'}_\theta )$ . Since $A'\in {\mathsf {N}(\mathsf {par})}$ , evidently it is ${\mathsf {N}}$ -projective. Hence by Theorem 3.16, $A'$ is $\mathsf {par}$ -subextendible. Hence by Lemma 3.27, $\mathscr {C}$ is $\mathsf {par}$ -subextendible. Since $\mathscr {C}$ is stable and $n> \#\mathsf {par}$ , Lemma 3.29 implies that $\langle \mathscr {C}\rangle _n$ is also $\mathsf {par}$ -subextendible. Hence $B^{A'}_\theta $ is $\mathsf {par}$ -subextendible and by Theorem 3.16, $B^{A'}_\theta $ is ${\mathsf {N}(\mathsf {par})}$ -projective. So item (1) is satisfied.

To show item 3 for $B^{A'}_\theta $ , it is sufficient to show $\mathcal {K}\Vdash B^{A'}_\theta \to A$ for every finite rooted model $\mathcal {K}$ . If $\mathcal {K}\Vdash B^{A'}_\theta $ , we have $\mathcal {K}\in \langle \mathscr {C}\rangle _n$ . Hence $\mathcal {K}\leq _n \mathcal {K}'$ for some $\mathcal {K}'\in \mathscr {C}$ . Then $\mathcal {K}'=\theta (\mathcal {K}")$ for some finite rooted $\mathcal {K}"$ such that $\mathcal {K}"\Vdash A'$ . Since $\vdash A'\to \theta (A)$ , we have $\mathcal {K}"\Vdash \theta (A)$ , and by Lemma 3.8 we get $\theta (\mathcal {K}")\Vdash A$ , whence $\mathcal {K}'\Vdash A$ . Since $c_{\!_\to \!}(A)\leq n$ and $\mathcal {K}\leq _n\mathcal {K}'$ , Corollary 3.24 implies that $\mathcal {K}\Vdash A$ , as desired.

It remains to show that item 2 holds. It is sufficient to show $\mathcal {K}\Vdash A'\leftrightarrow \theta (B^{A'}_\theta )$ for arbitrary finite rooted $\mathcal {K}$ . If $\mathcal {K}\Vdash A'$ , then $\theta (\mathcal {K})\Vdash A'$ and hence $\theta (\mathcal {K})\in \mathscr {C}\subseteq \langle \mathscr {C}\rangle _n=\text {Mod}(B^{A'}_\theta )$ . Then $\theta (\mathcal {K})\Vdash B^{A'}_\theta $ and hence $\mathcal {K}\Vdash \theta (B^{A'}_\theta )$ . For the other direction, let $\mathcal {K}\Vdash \theta (B^{A'}_\theta )$ . Hence $\theta (\mathcal {K})\Vdash B^{A'}_\theta $ and then $\theta (\mathcal {K})\in \text {Mod}(B^{A'}_\theta )=\langle \mathscr {C}\rangle _n$ . So there is some $\mathcal {K}'\in \mathscr {C}$ such that $\theta (\mathcal {K})\leq _n\mathcal {K}'$ . Since $\mathcal {K}'\in \mathscr {C}$ , there is some $\mathcal {K}"$ such that $\mathcal {K}'=\theta (\mathcal {K}")$ and $\mathcal {K}"\Vdash A'$ . Since $A'=\theta (A')$ , we have $\mathcal {K}"\Vdash \theta (A')$ and hence $\mathcal {K}'\Vdash A'$ . By Lemma 3.22 we have $c_{\!_\to \!}(A')<n$ ; and hence Corollary 3.24 implies $\mathcal {K}\Vdash A'$ .

Finally we provide an algorithm which computes $\Pi $ . Given A, compute the finite set

$$ \begin{align*} \Pi':=\{B\in\mathcal{L}_{0}: c_{\!_\to\!}(B)\leq\max\{c_{\!_\to\!}(A),1+\#\mathsf{par}\} \text{ and } \vdash B\to A \text{ and } B\in{{{\downarrow^{\!\!^{\,}}}\mathsf{N}}}\}. \end{align*} $$

Note that $\Pi '$ is computable since $\mathsf {IPC}$ is decidable and by Corollary 3.17 we can decide $B\in {{{\downarrow ^{\!\!^{\,}}}\mathsf {N}}}$ . Finally one may easily find $\Pi \subseteq \Pi '$ , which includes pairwise $\mathsf {IPC}$ -independent formulas, as required for projective resolutions.

Proof. We use induction on ${\mathsf {atom}}(A)$ (the set of atomic formulas in A) ordered by $\supset $ and find some finite set $\Gamma _A$ of X-components with ${\mathsf {atom}}(\Gamma _A)\subseteq {\mathsf {atom}}(A)$ and $X\vdash \bigvee \Gamma _A\leftrightarrow A$ . As induction hypothesis assume that for every ${\varLambda }$ and $B\in \mathsf {N}$ with ${\mathsf {atom}}(B)\subset {\mathsf {atom}}(A)$ there is a finite set $\Gamma _B$ of X-components such that $X\vdash B\leftrightarrow \bigvee \Gamma $ and ${\mathsf {atom}}(\Gamma _B)\subseteq {\mathsf {atom}}(B)$ . For the induction step, assume that $A\in \mathsf {N}$ is given. Using derivation in $\mathsf {IPC}$ one may easily find finite sets $\Gamma _i$ and $\Delta _i$ for $1\leq i\leq n$ such that:

• • $\mathsf {IPC}\vdash A\leftrightarrow \bigvee _{i=1}^n A_i$ , in which $A_i:=\bigwedge \Gamma _i\wedge \bigwedge \Delta _i$ .

• • $\Delta _i$ includes only atomic formulas.

• • $\Gamma _i$ includes implications with atomic antecedents.

• • ${\mathsf {atom}}(\Gamma _i\cup \Delta _i)\subseteq {\mathsf {atom}}(A)$ .

It is sufficient to decompose every $A_i$ to X-components. If $X\nvdash \bigwedge \Delta _i\to E$ for every antecedent E of an implication in $\Gamma _i$ , then $A_i$ is already an X-component and we are done. Otherwise, there is some $E\to F\in \Gamma _i$ such that $X\vdash \bigwedge \Delta _i\to E$ . Then let $A_i':=A_i[E:\top ]$ , i.e., the replacement of every occurrences of E in $A_i$ with $\top $ . Also let $X':=X\cup \{E\}$ . Hence ${\mathsf {atom}}(A^{\prime }_i)\subsetneqq {\mathsf {atom}}(A)$ and by induction hypothesis we may decompose $A^{\prime }_i$ to $X'$ -components:

$$ \begin{align*} X'\vdash A^{\prime}_i\leftrightarrow \bigvee_j B_j. \end{align*} $$

It is not difficult to observe that if $B_j$ is an $X'$ -component then $B^{\prime }_j:=E\wedge B_j$ is an X-component. Moreover $X\vdash E\wedge A^{\prime }_i\leftrightarrow \bigvee _j B^{\prime }_j$ and since $\mathsf {IPC}\vdash (E\wedge A^{\prime }_i)\leftrightarrow (E\wedge A_i) $ and $X\vdash A_i\to E$ , we get

$$ \begin{align*} X\vdash A_i\leftrightarrow \bigvee_j B^{\prime}_j. \end{align*} $$

Hence we have decomposed $A_i$ to X-components $B^{\prime }_j$ with ${\mathsf {atom}}(B^{\prime }_j)\subseteq {\mathsf {atom}}(A)$ , as desired.

Proof. Let $B=\bigwedge B_i$ is a component and $\mathscr {C}$ be a finite set of finite rooted Kripke models for B. We must show that a variant of $\sum (\mathscr {C})$ is a model of B. Let $w_0$ be the root of $\sum (\mathscr {C})$ and define a variant $\mathcal {K}$ of $\sum (\mathscr {C})$ as follows. $\mathcal {K},w_0\Vdash a$ iff $a=B_i$ for some i. Then it is easy to observe that $\mathcal {K},w_0\Vdash B$ .

Proof. Use Lemmas 3.31 and 3.32 and Theorem 3.13.

Proof. We prove this by contraposition. Let $ \nvdash A\to B$ and $ \nvdash A\to C$ . Then there are some Kripke models $\mathcal {K}_1 $ and $\mathcal {K}_2$ such that $\mathcal {K}_1\Vdash A$ , $\mathcal {K}_1\nVdash B$ , $\mathcal {K}_2\Vdash A,$ and $\mathcal {K}_2\nVdash B$ . Since A is extendible, there is some variant $\mathcal {K}'$ of $\sum (\{\mathcal {K}_1,\mathcal {K}_2\})$ such that $\mathcal {K}\Vdash A$ . Since $\mathcal {K}_1\nVdash B$ we have $\mathcal {K}\nVdash B$ . Similarly $\mathcal {K}\nVdash C$ . Hence $\mathcal {K}\nVdash B\vee C$ and then ${\mathcal {K}\nVdash A\to (B\vee C)}$ .

Proof. $1\Rightarrow 2$ : Lemma 3.32. $2\Rightarrow 3$ : Lemma 3.34. $3\Rightarrow 1$ : Let A be prime. By Lemma 3.31 it can be decomposed to components $\Gamma _A$ . Thus $\vdash A\leftrightarrow \bigvee \Gamma _A$ and by primality of A we have $\vdash A\to B$ for some $B\in \Gamma _A$ . Then $\vdash A\leftrightarrow B$ and hence A is $\mathsf {IPC}$ -equivalent to some component.

Proof. By Lemma 3.31 every $A\in \mathsf {N}$ can be decomposed to components $ \Gamma _A$ such that $A\in {\mathsf {N}(\mathsf {par})}$ implies $\Gamma _A\subseteq {\mathsf {N}(\mathsf {par})}$ . Then Theorem 3.35 implies that every $E\in \Gamma _A$ is prime. Hence $\bigvee \Gamma _A\in \mathsf {P}\mathsf {N}^\vee $ and moreover $A\in {\mathsf {N}(\mathsf {par})}$ implies $\bigvee \Gamma _A\in \mathsf {P}\mathsf {N}(\mathsf {par})^\vee $ .

Proof. Use Corollary 3.36 and Theorem 2.4.