lemmatheorem lemma definitiontheorem definition corollarytheorem corollary
propositiontheorem proposition remarktheorem remark notationtheorem notation
exampletheorem example conjecturetheorem conjecture facttheorem fact
claimtheorem claim

# Relative Unification in Intuitionistic Logic:
Towards provability logic of HA

Mojtaba Mojtahedi
University of Tehran, College of science
Department of Mathematics, Statistics and Computer Sciences
http://mmojtahedi.ir

###### Abstract

This paper studies relative unification and admissibility in the
intuitionistic logic. We generalize results of [Ghilardi,, 1999; Iemhoff,
2001a, ] and prove them relative in ${{\sf NNIL}({\sf par})}$ propositions,
the class of propositions with No Nested Implications in the Left made up from
parameters. The main application of such generalization is to characterize
provability logic of Heyting Arithmetic HA and prove its decidability
[Mojtahedi,, 2022].

###### Contents

  1. 1 Introduction
  2. 2 Preliminary definitions and facts
    1. 2.1 propositional language
    2. 2.2 Substitutions
    3. 2.3 Kripke models for intuitionistic logic
    4. 2.4 ${\sf NNIL}$ propositions
    5. 2.5 Notations on sets of propositions
    6. 2.6 Admissibility and preservativity
    7. 2.7 Greatest lower bounds
  3. 3 ${{\sf NNIL}({\sf par})}$-fication: unification to ${{\sf NNIL}({\sf par})}$
    1. 3.1 Relative Projectivity
    2. 3.2 Relative Extendibility
    3. 3.3 ${\sf NNIL}({\sf par})$-projectivity and ${\sf par}$-extendibility
    4. 3.4 Projective resolution
    5. 3.5 Projective resolution for NNIL
  4. 4 ${{\sf NNIL}({\sf par})}$-admissible rules of ${\sf IPC}$
    1. 4.1 The system ${{\sf AR}_{{\sf par}}}\\!\,$
    2. 4.2 ${{\sf AR}_{{\sf par}}}\\!\,$-models
    3. 4.3 ${{\sf NNIL}({\sf par})}$-admissibility
    4. 4.4 ${{\downarrow^{\\!\\!{}^{\,}}}{{\sf NNIL}({\sf par})}}$-preservativity logic
    5. 4.5 ${{\sf NNIL}({\sf par})}$-preservativity logic

##  1 Introduction

Silvio Ghilardi [Ghilardi,, 1999, 2000] studies unification in propositional
logics. More precisely, he describes all solutions for
$A(x_{1},\ldots,x_{n})\leftrightarrow\top$ within a background logic like
intuitionistic logic ${\sf IPC}$ or a modal logic containing ${\sf K4}$. By a
solution we mean a substitution $\theta$ such that
$\theta(A\leftrightarrow\top)$ holds.

On the other hand, we have a related question for
decidability/characterization of admissible rules of ${\sf IPC}$. A rule $A/B$
is admissible to a logic ${\sf L}$ if ${\sf L}\vdash\theta(A)$ implies ${\sf
L}\vdash\theta(B)$ for every substitution $\theta$. Despite classical logic,
in which every admissible rule is also derivable, the case of modal logic and
intuitionistic logic are not trivial. Probably the first such underivable
admissible rule for ${\sf IPC}$ is the following [Harrop,, 1960]:

$\neg A\to(B\vee C)$ $(\neg A\to B)\vee(\neg A\to C)$

Using the tools and results in [Ghilardi,, 1999], Rosalie Iemhoff proves the
completeness of a base for all admissible rules of ${\sf IPC}$ [Iemhoff,
2001b, ; Iemhoff, 2001a, ], which previously conjectured by de Jongh and
Visser. Decidability of admissibility for ${\sf IPC}$ was already known
[Rybakov, 1987b, ; Rybakov,, 1992, 1997]. There are similar results in some
modal logics extending ${\sf K4}$ both for unification [Ghilardi,, 2000] and
admissibility [Jeřábek,, 2005; Iemhoff and Metcalfe,, 2009].

There is yet another related notion, preservativity, an intuitionistic
alternate for the classical notion of interpretability or conservativity
[Iemhoff,, 2003; Visser,, 2002]. Preservativity is a binary relation
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}B$
defined as “$\Gamma\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$}
\put(0.1,1.2){ $$} \put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}A$ implies
$\Gamma\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$} \put(0.1,1.2){
$$} \put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}B$”. Albert Visser in [Visser,,
2002] shows that ${\sf NNIL}$-preservativity and admissibility are tightly
related, in which ${\sf NNIL}$, is the class of No Nested Implications in the
Left, introduced in [Visser et al.,, 1995] and more elaborated in [Visser,,
2002]. This class of propositions are proved to be helpful in the realm of
intuitionistic logic. A crucial result concerning ${\sf NNIL}$ appeared in
[Visser,, 2002] is to provide an algorithm that takes $A\in\mathcal{L}_{0}$
and returns its best ${\sf NNIL}$ approximation $A^{*}$ from below, i.e.,
$\vdash A^{*}\rightarrow A$ and for all ${\sf NNIL}$ formulae $B$ such that
$\vdash B\rightarrow A$, we have $\vdash B\rightarrow A^{*}$. Later in section
4.5 we also provide an algorithm which computes $A^{\star}$, the best ${{\sf
NNIL}({\sf par})}$-approximation of $A$ from below.

The main work of current paper is to extend [Ghilardi,, 1999; Iemhoff, 2001a,
] and prove their results relative in ${{\sf NNIL}({\sf par})}$ propositions,
the class of No Nested Implications in the Left [Visser et al.,, 1995] which
are made up from set of atomic parameters ${\sf par}$. First we imitate
[Ghilardi,, 1999] and study projectivity and extendibility relative in ${{\sf
NNIL}({\sf par})}$-propositions (theorem 3.4). This will lead us to a
relativised version of projective approximations (theorem 3.6). Then we take a
route similar to [Iemhoff, 2001a, ] and provide a base called ${{\sf AR}_{{\sf
par}}}\\!\,$, for ${{\sf NNIL}({\sf par})}$-admissibility of ${\sf IPC}$ and
prove its completeness (theorem 4.4). This last result together with [Ardeshir
and Mojtahedi,, 2018; Mojtahedi,, 2021], lead us to the characterization and
decidability of provability logic of Heyting arithmetic HA, which is splitted
to another manuscript [Mojtahedi,, 2022].

Finally we axiomatize two interesting preservativity predicates
$\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf IPC}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}\ $:
first when $\Gamma$ is considered as the set of ${{\sf NNIL}({\sf
par})}$-projective propositions (this is same as projectivity relative in
${{\sf NNIL}({\sf par})}$, as defined in section 3.1), and second when
$\Gamma:={{\sf NNIL}({\sf par})}$.

##  2 Preliminary definitions and facts

This section is devoted to preliminaries and conventions. Among other well-
known notions, we define ${\sf NNIL}$ propositions, admissibility,
preservativity and greatest lower bounds.

###  2.1 propositional language

The propositional language $\mathcal{L}_{0}$ includes connectives $\vee$,
$\wedge$, $\to$ and $\bot$. Negation $\neg$ is defined as $\neg A:=A\to\bot$
and $\top:=\neg\bot$. By default we assume that $\mathcal{L}_{0}$ includes
finite set of atomic variables ${\sf var}$ and also finite set of atomic
parameters ${\sf par}$. The union ${\sf var}\cup{\sf par}$ is annotated as
${\sf atom}$, the set of atomics. We use ${\vv{p}}$ and ${\vv{q}}$ as a finite
set or list of parameters and ${\vv{x}}$ and ${\vv{y}}$ for a finite set or
list of variables. Finite lists or sets of atomics are annotated by ${\vv{a}}$
and ${\vv{b}}$. We use $x$, $y$ and $z$ (possibly with subscripts) as meta-
variables for variables and also $p$, $q$ and $r$ (possibly with subscripts)
for parameters. Also $a$, $b$ and $c$ (again possibly with subscripts) are
used for both atomic variables and parameters.

Let $\vv{a}=a_{1},\ldots,a_{n}$ be a list of atomics and
$\vv{B}=B_{1},\ldots,B_{n}$. Then $A[\vv{a}:\vv{B}]$ indicate the simultaneous
substitution of $B_{i}$ for $a_{i}$ in $A$.

We also use the notation $\mathcal{L}_{0}(X)$ to indicate the language of all
boolean combinations of propositions in $X$. We consider ${\sf IPC}$ as the
intuitionistic propositional logic [Troelstra and van Dalen,, 1988] and
$\vdash$ indicates derivability in ${\sf IPC}$. All propositional logics
considered in this paper are assumed to be closed under (1) modus ponens and
(2) substitutions

###  2.2 Substitutions

A substitution $\theta$ is a function on propositional language
$\mathcal{L}_{0}$ which commutes with all connectives, i.e.

  * •

$\theta(B\circ C)=\theta(B)\circ\theta(C)$ for every
$\circ\in\\{\vee,\wedge,\to\\}$.

  * •

$\theta(\bot)=\bot$.

By default we assume that all substitutions are identity on the set ${\sf
par}$ of parameters. We say that a substitution is general, if we relax this
condition on ${\sf par}$ and allow the parameters to be substituted as well.

###  2.3 Kripke models for intuitionistic logic

A Kripke model for intuitionistic logic, is a triple
$\mathcal{K}=(W,\prec,\mathrel{V})$ with following properties:

  * •

$W\neq\emptyset$.

  * •

$(W,\prec)$ is a partial order (transitive and irreflexive). We write
$\preccurlyeq$ for the reflexive closure of $\prec$.

  * •

$\mathrel{V}$ is the valuation on atomics, i.e. $V\subseteq W\times{\sf
atom}$.

  * •

$w\preccurlyeq u$ and $w\mathrel{V}a$ implies $u\mathrel{V}a$ for every
$w,u\in W$ and $a\in{\sf atom}$.

The valuation $\mathrel{V}$ may be extended to include all propositions as
follows:

  * •

$\mathcal{K},w\Vdash a$ iff $w\mathrel{V}a$, for $a\in{\sf atom}$.

  * •

$\mathcal{K},w\Vdash A\wedge B$ iff $\mathcal{K},w\Vdash A$ and
$\mathcal{K},w\Vdash B$.

  * •

$\mathcal{K},w\Vdash A\vee B$ iff $\mathcal{K},w\Vdash A$ or
$\mathcal{K},w\Vdash B$.

  * •

$\mathcal{K},w\Vdash A\to B$ iff for every $u\succcurlyeq w$ if we have
$\mathcal{K},w\Vdash A$ then $\mathcal{K},w\Vdash B$.

We also define the following notions for Kripke models:

  * •

Finite: if $W$ is a finite set.

  * •

Rooted: if there is some node $w_{0}\in W$ such that $w_{0}\preccurlyeq w$ for
every $w\in W$.

  * •

Tree: if for every $w\in W$ the set $\\{u\in W:u\preccurlyeq w\\}$ is finite
linearly ordered (by $\preccurlyeq$) set.

By default we assume that all Kripke models of ${\sf IPC}$ in this paper are
finite rooted and tree. As we will see in section 4.2, some other sort of
Kripke semantics are used, called ${{\sf AR}_{{\sf par}}}\\!\,$-models, which
might not be finite or tree. Given $A\in\mathcal{L}_{0}$, we define
$\textup{Mod}(A)$ as the class of all (finite rooted tree) Kripke models of
$A$.

###  2.4 ${\sf NNIL}$ propositions

The class of No Nested Implications in the Left, ${\sf NNIL}$ formulae, was
discovered by Albert Visser and first published in [Visser et al.,, 1995], and
more explored in [Visser,, 2002; Ilin et al.,, 2020]. For simplicity of
notations, we may write ${\sf N}$ for ${\sf NNIL}$. The crucial result of
[Visser,, 2002] is to provide an algorithm that takes $A\in\mathcal{L}_{0}$
and returns its best ${\sf NNIL}$ approximation $A^{*}$ from below, i.e.,
$\vdash A^{*}\rightarrow A$ and for all ${\sf NNIL}$ formulae $B$ such that
$\vdash B\rightarrow A$, we have $\vdash B\rightarrow A^{*}$. Later in this
paper we define another algorithm $A^{\star}$ which calculates the best ${{\sf
NNIL}({\sf par})}$-approximation of $A$ from below (section 4.5). The classes
${\sf NNIL}$ and ${\sf NI}$ of propositions in $\mathcal{L}_{0}$ are defined
inductively:

  * •

$a\in{\sf NNIL}$ and $a\in{\sf NI}$ for every $a\in{\sf atom}$.

  * •

$B\circ C\in{\sf NNIL}$ if $B,C\in{\sf NNIL}$. Also $B\circ C\in{\sf NI}$ if
$B,C\in{\sf NI}$. ($\circ\in\\{\vee,\wedge\\}$)

  * •

$B\to C\in{\sf NNIL}$ if $B\in{\sf NI}$ and $C\in{\sf NNIL}$.

###  2.5 Notations on sets of propositions

In rest of the paper we deal with several sets of propositions and following
notations make life easier. Given $A\in\mathcal{L}_{0}$, let ${\sf sub}(A)$ be
the set of all subformulas of $A$. For simplicity of notations, we write ${\sf
X_{1}\ldots X_{n}}$ for ${\sf X_{1}}\cap\ldots\cap{\sf X_{n}}$, when ${\sf
X_{i}}$ are sets of propositions. For a set $\Gamma$ of propositions define

  * •

$\Gamma^{\vee}:=\\{\bigvee\Delta:\Delta\subseteq_{\text{fin}}\Gamma\text{ and
}\Delta\neq\emptyset\\}.$ ($X\subseteq_{\text{fin}}Y$ indicates that $X$ is a
finite subset of $Y$)

  * •

$\Gamma(X)$ indicates the set $\Gamma\cap\mathcal{L}_{0}(X)$.

  * •

${{\downarrow}^{\\!\\!{\sf T}}\\!\Gamma}:=$ the class of all
$\Gamma$-projective propositions in ${\sf T}$. We say that a proposition $A$
is $\Gamma$-projective in ${\sf T}$, if there is some substitution $\theta$
and $B\in\Gamma$ such that ${\sf T}\vdash\theta(A)\leftrightarrow B$ and
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$} \put(0.1,1.2){ $$}
\put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}x\leftrightarrow\theta(x)$ for
every $x\in{\sf var}$ (see section 3.1). Whenever ${\sf T}={\sf IPC}$, we may
omit the superscript ${\sf T}$ and simply write ${\downarrow}{\Gamma}$.

Also define

  * •

${\sf N}:={\sf NNIL}:=$ as defined in section 2.4.

  * •

${\sf P}^{\sf T}:={\sf Prime}^{\sf T}:=$ the set of all ${\sf T}$-prime
propositions, i.e. the set of propositions $A$ such that for every $B,C$ with
${\sf T}\vdash A\to(B\vee C)$ either we have ${\sf T}\vdash A\to B$ or ${\sf
T}\vdash A\to C$. Whenever ${\sf T}={\sf IPC}$, we may omit the ${\sf
T}$-superscript from notations.

And finally we assume that $(.)^{\vee}$ has the lowest precedence after
${\downarrow}{(.)}$. This means that

${\downarrow}{XY}^{\vee}:=\left({\downarrow}{\left(XY\right)}\right)^{\vee}.$

###  2.6 Admissibility and preservativity

Given a Logic ${\sf T}$, the binary relation
$\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${}$} \end{picture}}$ is defined to hold for
those pairs $A$ and $B$ such that the inference rule $A/B$ is admissible. More
precisely
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${}$} \end{picture}}B$ iff for every
substitution $\theta$, ${\sf T}\vdash\theta(A)$ implies ${\sf
T}\vdash\theta(B)$. The admissibility relationship is trivial when one
considers the classical propositional logic, since every admissible $A/B$ is
also derivable. However this relationship is highly nontrivial when one
considers a modal logic or intuitionistic logic. Probably the first known non-
derivable admissible rule is the following rule [Harrop,, 1960]:

$\neg A\to(B\vee C)$ $(\neg A\to B)\vee(\neg A\to C)$

Harvey Friedman asked in 1975 for decidability of admissibility in the
intuitionistic propositional logic. Then [Rybakov, 1987b, ; Rybakov,, 1992,
1997] answers to this question positively. Although it was shown that no
finite base exists for all admissible rules of the intuitionistic logic ${\sf
IPC}$ [Rybakov, 1987a, ], de Jongh and Visser introduced a recursive base and
conjectured it to generate all admissible rules of ${\sf IPC}$. Then Iemhoff
proved this conjecture [Iemhoff, 2001a, ; Iemhoff, 2001b, ].

Here in this paper, we consider a relativised version of admissibility. Given
a logic ${\sf T}$ and a set $\Gamma$ of propositions define the
$\Gamma$-admissibility relation in ${\sf T}$ as follows

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ iff for every
substitution $\theta$ and $C\in\Gamma$: ${\sf T}\vdash\theta(C\to A)$ implies
${\sf T}\vdash\theta(C\to B)$.

Note that there is a hidden role for the language $\mathcal{L}_{0}$ in the
definition of
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}$, when we consider
substitution $\theta$. However since almost everywhere in the paper we fix the
language $\mathcal{L}_{0}$, by default we assume substitutions over this fixed
language and we do not explicitly mention $\mathcal{L}_{0}$.

There is also another binary relation on propositions, called preservativity,
which is known . The $\Gamma$-preservativity relation in ${\sf T}$ is defined
as follows:

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$}
\end{picture}}}B\quad\text{ iff }\quad\forall\,E\in\Gamma({\sf T}\vdash E\to
A\Rightarrow{\sf T}\vdash E\to B).$

Preservativity could be considered as intuitionistic analogue of classical
interpretability or conservativity. This notion as a propositional logic, well
studied in [Visser,, 2002] and [Iemhoff,, 2003] provided Kripke semantics for
it. [Zhou,, 2003; Iemhoff et al.,, 2005] include some more elaboration on
preservativity and provability, including fixed-point theorem and Beth
property.

Following theorem says that
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}$ and
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$ are
ascending on $\Gamma$. All over this paper we may use this fact without
mentioning.

######  Theorem 2.1.

If $\Gamma\subseteq\Gamma^{\prime}$ then
${\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma^{\prime}}$}
\end{picture}}}\subseteq{\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}}$
and
${\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma^{\prime}}$}
\end{picture}}}\subseteq{\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}}$.

###### Proof.

Left to the reader. ∎

######  Theorem 2.2.

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ implies
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-1.2){ ${{{\downarrow}^{\\!\\!{\sf
T}}\\!\Gamma}}$} \end{picture}}B$.

###### Proof.

Let
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ and
$E\in{{\downarrow}^{\\!\\!{\sf T}}\\!\Gamma}$ such that ${\sf T}\vdash E\to
A$. Since $E\in{{\downarrow}^{\\!\\!{\sf T}}\\!\Gamma}$ there is some $\theta$
and $E^{\dagger}\in\Gamma$ such that
$E\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$} \put(0.1,1.2){ $$}
\put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}\theta(a)\leftrightarrow a$ for
every $a\in{\sf atom}$ and ${\sf T}\vdash\theta(E)\leftrightarrow
E^{\dagger}$. Hence ${\sf T}\vdash E^{\dagger}\to\theta(A)$. Then by
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ we get ${\sf
T}\vdash E^{\dagger}\to\theta(B)$ and thus
$E\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$} \put(0.1,1.2){ $$}
\put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}\theta(E\to B)$. Since $\theta$ is
$E$-projective, we may conclude
$E\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\vdash$} \put(0.1,1.2){ $$}
\put(0.1,-0.4){ ${{\sf T}}$} \end{picture}}E\to B$ and thus ${\sf T}\vdash
E\to B$. ∎

######  Question 1.

What can be said about the other direction of theorem 2.2?

######  Remark .

By theorems 2.2 and 2.1,
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ implies
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$,
however the converse may not hold. As a counterexample let $A$ and $B$ are two
different variables and $\top\in\Gamma$ and ${\sf T}={\sf IPC}$. Then we have
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$
and not
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$.

Later in this paper we axiomatize
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$ and
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}$ for several pairs
$({\sf T},\Gamma)$. Before we continue with this, let us see some basic
axioms.

Let ${\sf T}$ be a logic. The logic $[{\sf T}]$ proves statements $A\rhd B$
for $A,B\in\mathcal{L}_{0}$ and has the following axioms and rules:
Aximos

  * ${\sf Ax}:$

$A\rhd B$, for every ${\sf T}\vdash A\to B$.

Rules

$A\rhd B$ $A\rhd C$ Conj $A\rhd B\wedge C$ |  $A\rhd B$ $B\rhd C$ Cut $A\rhd C$
---|---

The above mentioned axiom and rules are not interesting, because $[{\sf
T}]\vdash A\rhd B$ iff ${\sf T}\vdash A\to B$. However we define several
interesting additional rules:

$B\rhd A$ $C\rhd A$ Disj $B\vee C\rhd A$ |  $A\rhd B$ ($C\in\Delta$) $\textup{Mont}(\Delta)$ $C\to A\rhd C\to B$
---|---

######  Theorem 2.3 (Soundness).

If ${\sf T}$ is closed under substitutions, then $[{\sf T}]$ is sound for
relative admissibility interpretations, i.e. $[{\sf T}]\vdash A\rhd B$ implies
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ and
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$
for every set $\Gamma$ of propositions and every logic ${\sf T}$. Moreover

  1. 1.

if $\Gamma$ is ${\sf T}$-prime i.e. ${\sf T}\vdash A\to(B\vee C)$ implies
either ${\sf T}\vdash A\to B$ or ${\sf T}\vdash A\to C$ for every $A\in\Gamma$
and arbitrary $B,C$, and $\Gamma$ is closed under substitutions, then Disj is
also sound,

  2. 2.

if $\Gamma$ is closed under $\Delta$-conjunctions, i.e. $A\in\Gamma$ and
$B\in\Delta$ implies $A\wedge B\in\Gamma$ (up to ${\sf T}$-provable
equivalence relation), then $\textup{Mont}(\Delta)$ is sound.

###### Proof.

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

######  Theorem 2.4.

${\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$}
\end{picture}}}}={\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma^{\vee}}$}
\end{picture}}\ }$ and
${\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$}
\end{picture}}}}={\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma^{\vee}}$} \end{picture}}}\ }$ .

###### Proof.

We only show
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$
iff $A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma^{\vee}}$}
\end{picture}}B$ and leave the similar argument for
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}B$ iff
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma^{\vee}}$} \end{picture}}}\ B$ to the
reader. The right-to-left direction holds since
$\Gamma\subseteq\Gamma^{\vee}$. For the other direction assume that
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$
and let $E\in\Gamma^{\vee}$ such that ${\sf T}\vdash E\to A$. Then
$E=\bigvee_{i}E_{i}$ with $E_{i}\in\Gamma$. Hence for every $i$ we have ${\sf
T}\vdash E_{i}\to A$. Then
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$
implies ${\sf T}\vdash E_{i}\to B$. Thus ${\sf T}\vdash E\to B$, as desired. ∎

Notation. Whenever ${\sf T}={\sf IPC}$ we may omit the ${\sf T}$ form
notations
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf T}}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}$ and
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$ and
simply write
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}$ and
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$ for them.
Also if $\Gamma:=\\{\top,\bot\\}$ we may omit $\Gamma$ from notations.

###  2.7 Greatest lower bounds

Given a set $\Gamma\cup\\{A\\}$ of propositions, and a logic ${\sf T}$, we say
that $B$ is a lower bound for $A$ w.r.t. $(\Gamma,{\sf T})$, if the following
conditions met:

  1. 1.

$B\in\Gamma$,

  2. 2.

${\sf T}\vdash B\to A$.

Moreover we say that $B$ is the greatest lower bound (glb) for $A$ w.r.t.
$(\Gamma,{\sf T})$, if for every lower bound $B^{\prime}$ for $A$ w.r.t.
$(\Gamma,{\sf T})$ we have ${\sf T}\vdash B^{\prime}\to B$. Note that up to
${\sf T}$-provable equivalence relation, such glb is unique and we annotate it
as $\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}$.
We say that $(\Gamma,{\sf T})$ is downward compact, if every
$A\in\mathcal{L}_{0}$ has glb w.r.t. $(\Gamma,{\sf T})$.

######  Question 2.

One may similarly define the notion of least upper bounds and upward
compactness. Does downward compactness imply upward compactness?

######  Theorem 2.5.

$B$ is the glb for $A$ w.r.t. $(\Gamma,{\sf T})$, iff

  * •

$B\in\Gamma$,

  * •

${\sf T}\vdash B\to A$,

  * •

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$.

Hence we have
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$}
\end{picture}}}\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}$.

###### Proof.

Left to the reader. ∎

######  Question 3.

As we saw in theorem 2.5, the glb may be expressed via preservativity relation
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$.
One may think of its adjoint relation which best suites for lub’s:

$A\mathrel{{}^{{}^{*}}\\!\\!\\!\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$}
\end{picture}}}}B\quad\text{ iff }\quad\forall\,E\in\Gamma({\sf T}\vdash A\to
E\Rightarrow{\sf T}\vdash B\to E).$

[Visser,, 2002, Corollary 7.2] axiomatizes
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}$ for
${\sf T}={\sf IPC}$ and $\Gamma={\sf NNIL}$. We ask for an axiomatization for
$\mathrel{{}^{{}^{*}}\\!\\!\\!\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}}$
when we let ${\sf T}={\sf IPC}$ and $\Gamma={\sf NNIL}$.

######  Corollary .

If $\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}$ exists, then for
every $B\in\mathcal{L}_{0}$ we have

${\sf T}\vdash\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}\to
B\quad\text{ iff }\quad
A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B.$

###### Proof.

First assume that ${\sf T}\vdash\lfloor{A}\rfloor^{{}^{\\!{\sf
T}}}_{{}_{\\!{\Gamma}}}$. Also let $E\in\Gamma$ such that ${\sf T}\vdash E\to
A$. Theorem 2.5 implies
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$}
\end{picture}}}\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}$ and
hence ${\sf T}\vdash E\to\lfloor{A}\rfloor^{{}^{\\!{\sf
T}}}_{{}_{\\!{\Gamma}}}$. Then by ${\sf T}\vdash\lfloor{A}\rfloor^{{}^{\\!{\sf
T}}}_{{}_{\\!{\Gamma}}}\to B$ we get ${\sf T}\vdash E\to B$, as desired.
For the other direction let
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$.
By definition we have $\lfloor{A}\rfloor^{{}^{\\!{\sf
T}}}_{{}_{\\!{\Gamma}}}\in\Gamma$ and ${\sf
T}\vdash\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}\to A$. Hence by
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){ ${\Gamma}$} \end{picture}}}B$ we
get ${\sf T}\vdash\lfloor{A}\rfloor^{{}^{\\!{\sf T}}}_{{}_{\\!{\Gamma}}}\to
B$, as desired. ∎

##  3 ${{\sf NNIL}({\sf par})}$-fication: unification to ${{\sf NNIL}({\sf
par})}$

Silvio Ghilardi, in [Ghilardi,, 1999] characterizes projective propositions in
the language $\mathcal{L}_{0}({\sf var})$ with the aid of Kripke semantics.
Then he uses this characterization to prove that the unification type of ${\sf
IPC}$ is finitary. Afterwards, Rosalie Iemhoff [Iemhoff, 2001b, ; Iemhoff,
2001a, ] uses this result together with a special sort of Kripke models,
called AR-models, to characterize the admissible rules of ${\sf IPC}$. In this
section we consider a relativised version for those results. The difference
from previous version is that we are not allowed to substitute parameters (a
reserved set of atomics), and also instead of unification, we expect to
simplify the proposition to a ${{\sf NNIL}({\sf par})}$ proposition, called
${{\sf NNIL}({\sf par})}$-fication. In fact, previous results will be an
special case of ours when ${\sf par}=\emptyset$ and hence ${{\sf NNIL}({\sf
par})}=\\{\top,\bot\\}$. The methods of our proof follows main roads took in
[Ghilardi,, 1999; Iemhoff, 2001a, ].
We start with relativised version of projective unification (section 3.1) and
extension property (section 3.2). Then (section 3.3) we prove a correspondence
between relativised projectivity and extendibility. Having such Kripke
semantical charcterization in hand, then we prove that every proposition has a
finitary projective approximation (section 3.4). Actually we prove something
more: every proposition has a finitary projective resolution (section 3.4).
Finally at the end of this section (section 3.5), we prove that in the
specific case, when $A\in{\sf NNIL}$, this finitary projective resolution
takes an elegant form.

###  3.1 Relative Projectivity

Given $A\in\mathcal{L}_{0}$, a substitution $\theta$ is called $A$-projective
(in ${\sf IPC}$) if

(3.1) $\text{For all atomic $a$ we have }\quad A\vdash
a\leftrightarrow\theta(a).$

When one considers unification for propositional logics, projectivity is
proved to be of great help [Ghilardi,, 1997]. As we will see, our study is not
an exception.
If $\Gamma\subseteq\mathcal{L}_{0}({\sf par})$, a substitution $\theta$ is a
$\Gamma$-fier (as a generalization for uni-fier) for $A$, if

$\vdash\theta(A)\in\Gamma\quad\text{i.e.~{}$\theta(A)$ is ${\sf
IPC}$-equivalent to some $A^{\prime}\in\Gamma$.}$

In this case we use the notation
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{\twoheadrightarrow}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}\Gamma$.
If $\Gamma$ is a singleton $\\{A^{\prime}\\}$ we write
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{\twoheadrightarrow}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime}$
instead of
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{\twoheadrightarrow}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}\\{A^{\prime}\\}$.
$\theta$ is a unifier for $A$ if it is $\\{\top\\}$-fier for $A$. We say that
a substitution $\theta$ projects $A$ to $\Gamma$ (notation:
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}\Gamma$)
if $\theta$ is $A$-projective and $\Gamma$-fier. We say that $A$ is
$\Gamma$-projective (notation
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}\Gamma$)
if there is some $\theta$ such that
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}\Gamma$.
We say that $A$ is projective, if it is $\\{\top\\}$-projective. Also
${\downarrow^{\\!\\!{}^{\,}}}{\Gamma}$ indicates the set of all propositions
which are $\Gamma$-projective.

#### Uniqueness of $\Gamma$-projections

Let
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime}$
and
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\tau}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime\prime}$
and $A^{\prime},A^{\prime\prime}\in\Gamma\subseteq\mathcal{L}_{0}({\sf par})$.
From the $A$-projectivity of $\theta$ and $\tau$, for every atomic $a$ we have
$A\vdash\theta(a)\leftrightarrow\tau(a)$. Hence
$A\vdash\theta(A)\leftrightarrow\tau(A)$ and then $A\vdash
A^{\prime}\leftrightarrow A^{\prime\prime}$. By applying $\theta$ to both
sides of this derivation, we have
$\theta(A)\vdash\theta(A^{\prime})\leftrightarrow\theta(A^{\prime\prime})$.
Since $\theta$ is identity over parameters and
$A^{\prime},A^{\prime\prime}\in\mathcal{L}_{0}({\sf par})$, we have
$A^{\prime}\vdash A^{\prime}\leftrightarrow A^{\prime\prime}$. Hence $\vdash
A^{\prime}\to A^{\prime\prime}$. Similarly we have $\vdash A^{\prime\prime}\to
A^{\prime}$, and hence $\vdash A^{\prime}\leftrightarrow A^{\prime\prime}$.
This argument shows that for every $\Gamma$-projective $A$, there is a unique
(modulo ${\sf IPC}$-provable equivalence) $A^{\dagger}\in\Gamma$ such that for
some $A$-projective substitution $\theta$ we have
$\vdash\theta(A)\leftrightarrow A^{\dagger}$. Such unique $A^{\dagger}$ is
called the $\Gamma$-projection of $A$.

######  Lemma .

Let $A$ be $\Gamma$-projective and $A^{\dagger}\in\Gamma$ its projection. Then
$\vdash A\to A^{\dagger}$.

###### Proof.

Let $\theta$ be the $A$-projective $\Gamma$-fier for $A$, i.e. $A\vdash
B\leftrightarrow\theta(B)$ for every $B$, and $\vdash\theta(A)\leftrightarrow
A^{\dagger}$. Hence we have $A\vdash A\leftrightarrow\theta(A)$ and thus
$A\vdash A\leftrightarrow A^{\dagger}$. This implies $\vdash A\to
A^{\dagger}$, as desired. ∎

######  Lemma .

Let $\Gamma\subseteq\mathcal{L}_{0}({\sf par})$. If
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\dagger}\in\Gamma$
and $B$ is an arbitrary proposition, then we have

$\vdash A\to B\quad\text{ iff }\quad\vdash\theta(A^{\dagger}\to B).$

###### Proof.

The left-to-right direction is obvious. For other direction, let
$\vdash\theta(A^{\dagger}\to B)$. Hence $A\vdash\theta(A^{\dagger}\to B)$ and
then $A\vdash A^{\dagger}\to B$. Section 3.1 implies $\vdash A\to A^{\dagger}$
and thus $\vdash A\to B$. ∎

###  3.2 Relative Extendibility

Given a Kripke model $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ and $w\in W$,
$\mathcal{K}_{w}$ indicates the restriction of $\mathcal{K}$ to the nodes
$u\succcurlyeq w$. For a set ${\vv{a}}\subseteq{\sf atom}$, we say that
$\mathcal{K}^{\prime}=(W^{\prime},\preccurlyeq^{\prime},\mathrel{V}^{\prime})$
is an ${\vv{a}}$-submodel of $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$,
annotated as $\mathcal{K}^{\prime}\preceq^{{{\vv{a}}}}\mathcal{K}$, if there
exists a relation $R\subseteq W^{\prime}\times W$ such that

  * •

$\mathcal{K}^{\prime},w^{\prime}\Vdash a$ iff $\mathcal{K},w\Vdash a$, for
every $a\in{\vv{a}}$ and $(w^{\prime},w)\in R$.

  * •

$v^{\prime}\succcurlyeq^{\prime}w^{\prime}\mathrel{R}w$ implies $\exists\,v\in
W\ (v^{\prime}\mathrel{R}v\succcurlyeq w)$, for every $w\in W$ and
$w^{\prime},v^{\prime}\in W^{\prime}$.

  * •

$\forall\,w^{\prime}\in W^{\prime}\exists\,w\in W(w^{\prime}\mathrel{R}w)$.

Also we say that $\mathcal{K}^{\prime}\preceq_{1}^{{{\vv{a}}}}\mathcal{K}$ if
the above relation $R$, is function. In this case the second condition takes a
more readable face:

  * •

$w^{\prime}\preccurlyeq^{\prime}v^{\prime}$ implies $f(w^{\prime})\preccurlyeq
f(v^{\prime})$.

Moreover define $\mathcal{K}^{\prime}\subseteq^{{{\vv{a}}}}\mathcal{K}$ iff we
have

  * •

$W^{\prime}\subseteq W$,

  * •

${\preccurlyeq^{\prime}}$ is the restriction of $\preccurlyeq$ to
$W^{\prime}$,

  * •

$w\mathrel{V}^{\prime}a$ iff $w\mathrel{V}a$ for every $w\in W^{\prime}$ and
$a\in{\vv{a}}$,

Also $\mathscr{K}\preceq^{{{\vv{a}}}}\mathcal{K}$ for a class $\mathscr{K}$ of
Kripke models and a Kripke model $\mathcal{K}$ indicates that for every
$\mathcal{K}^{\prime}\in\mathscr{K}$ we have
$\mathcal{K}^{\prime}\preceq^{{{\vv{a}}}}\mathcal{K}$. We have similar
notations for $\mathscr{K}\subseteq^{{{\vv{a}}}}\mathcal{K}$ and
$\mathscr{K}\preceq_{1}^{{{\vv{a}}}}\mathcal{K}$.

Since we only consider Kripke models with finite rooted tree frames, we have
the equivalency of $\preceq_{1}^{{{\vv{a}}}}$ and $\preceq^{{{\vv{a}}}}$:

######  Lemma .

$\mathcal{K}^{\prime}\preceq_{1}^{{{\vv{a}}}}\mathcal{K}$ is equivalent to
$\mathcal{K}^{\prime}\preceq^{{{\vv{a}}}}\mathcal{K}$.

###### Proof.

Let $\mathcal{K}^{\prime}\preceq^{{{\vv{a}}}}\mathcal{K}$ and $R$ is a
relation with above mentioned properties. It is enough to define a function
$f\subseteq R$ such that $f$ and $R$ share the same domain $W^{\prime}$. For
every $\preccurlyeq^{\prime}$-minimal node $w^{\prime}\in W^{\prime}$, define
$f(w^{\prime})$ an arbitrary node $w$ with $w^{\prime}\mathrel{R}w$. Note that
such $w$ always exists. Since $\mathcal{K}^{\prime}$ is tree, for every
$w^{\prime}_{1}\in W^{\prime}$ which is not minimal, there is a unique
predecessor $w^{\prime}_{0}\preccurlyeq^{\prime}w^{\prime}_{1}$. Then by
definition for every $w^{\prime}_{1}\in W^{\prime}$ there is some $w_{1}\in W$
such that $f(w^{\prime}_{0})\preccurlyeq w_{1}$. Define
$f(w^{\prime}_{1}):=w_{1}$ for some such $w_{1}$. Then it is not difficult to
observe that this $f$ satisfies the condition
“$w^{\prime}\preccurlyeq^{\prime}v^{\prime}$ implies
$f(w^{\prime})\preccurlyeq f(v^{\prime})$”. ∎

Although $\subseteq^{{{\vv{a}}}}$ is not equivalent to
$\preceq_{1}^{{{\vv{a}}}}$, we have the following partial equivalency:

######  Lemma .

If $\mathcal{K}_{0}\preceq_{1}^{{{\vv{a}}}}\mathcal{K}_{1}\Vdash A$ then
$\mathcal{K}_{0}\subseteq^{{{\vv{a}}}}\mathcal{K}_{2}\Vdash A$ for some
$\mathcal{K}_{2}$.

###### Proof.

The proof is almost identical to the proof of theorem 6.9 in [Visser et al.,,
1995] 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, lest 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 on the new nodes.

Define $\mathcal{K}_{2}:=(W_{2},\preccurlyeq_{2},\mathrel{V}_{2})$ as follows:

  * •

$W_{2}:=\\{(w_{0},f(w_{0}),w_{1}):w_{0}\in W_{0}\text{ and
}f(w_{0})\preccurlyeq_{1}w_{1}\in W_{1}\\}$.

  * •

$(w_{0},f(w_{0}),w_{1})\preccurlyeq_{2}(w^{\prime}_{0},f(w^{\prime}_{0}),w^{\prime}_{1})$
iff either of the following holds:

    * –

$w_{0}\preccurlyeq_{0}w^{\prime}_{0}$ and $w_{1}=f(w_{0})$,

    * –

$w_{0}=w^{\prime}_{0}$ and $w_{1}\preccurlyeq_{1}w^{\prime}_{1}$.

  * •

$(w_{0},f(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 the root $(\rho,f(\rho),f(\rho))$ in which $\rho$ is
the root of $\mathcal{K}_{0}$. Also $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$
are bisimilar and hence prove the same set of propositions including $A$.
Moreover one may easily show that $g$ as defined in the following, is a 1-1
embedding of $\mathcal{K}_{0}$ into $\mathcal{K}_{2}$:
$g(w_{0}):=(w_{0},f(w_{0}),f(w_{0}))$. ∎

Remember that ${\sf NNIL}({\vv{a}})$ indicate ${\sf
NNIL}\cap\mathcal{L}_{0}({\vv{a}})$. The following theorem is a Kripke
semantical characterization of ${\sf NNIL}$ propositions [Visser et al.,,
1995].

######  Theorem 3.1.

Given ${\vv{a}}\subseteq{\sf atom}$, we have $A\in{\sf NNIL}({\vv{a}})$ iff
the class of Kripke models of $A$ is closed under $\subseteq^{{{\vv{a}}}}$.

###### Proof.

See [Visser et al.,, 1995] or [Visser,, 2002]. ∎

######  Remark .

Modulo ${\sf IPC}$-provable equivalence, ${\sf NNIL}$ is finite.

###### Proof.

Observe that each proposition can be written as $\bigvee\bigwedge C$ in which
$C$ is an atomic or implication, which we call it a component. Observe that
the number of propositions in $n$ atomics, $f(n)$, is less than or equal to
$2^{2^{g(n)}}$, in which $g(n)$ is the number of components in $n$ atomics.
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$ variables, or it is of the form $p$ for some atomic $p$. Hence the
following recursive function is an upperbound for the number of all formulas
in $n$ atomics:

$f(0):=2\quad\quad,\quad\quad f(n+1):=2^{2^{(n+1)(f(n)+1)}}\qed$

Define $[\\![{\mathcal{K}}]\\!]_{{}_{\Gamma}}:=\\{A\in\Gamma:\mathcal{K}\Vdash
A\\}.$

######  Theorem 3.2.

Let $\mathcal{K},\mathcal{K}^{\prime}$ be two Kripke models and
${\vv{a}}\subseteq{\sf atom}$. Then
$\mathcal{K}^{\prime}\Vdash[\\![{\mathcal{K}}]\\!]_{{\sf N}({\vv{a}})}$ iff
$\mathcal{K}^{\prime}\preceq^{{{\vv{a}}}}\mathcal{K}$.

###### Proof.

See [Visser et al.,, 1995, theorem 7.1.2]. ∎

Given a substitution $\theta$ and a Kripke model
$\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$, we define
$\theta(\mathcal{K}):=(W,\preccurlyeq,\mathrel{V}^{\prime})$ as follows. For
every atomic $a$, define $w\mathrel{V}^{\prime}a$ iff
$\mathcal{K},w\Vdash\theta(a)$.

######  Lemma .

Given a general substitution $\theta$, Kripke model $\mathcal{K}$ and
$A\in\mathcal{L}_{0}$, we have

$\mathcal{K},w\Vdash\theta(A)\quad\quad\text{iff}\quad\quad\theta(\mathcal{K}),w\Vdash
A.$

###### Proof.

Use induction on the complexity of $A$. ∎

######  Remark .

Let $\theta$ and $\tau$ be two general substitutions and $(\theta\tau)$ is
their composition. Above lemma, implies that
$(\theta\tau)(\mathcal{K})=\tau(\theta(\mathcal{K}))$. This conflicts with our
standard notation for the composition of functions. This confliction could be
resolved by choosing another name, e.g. $\theta^{*}$ for the operation on
Kripke models corresponding to $\theta$. However, for the simplicity of
notations, we prefer not to do so.

Given Kripke models $\mathcal{K}$ and $\mathcal{K}^{\prime}$, we say that
$\mathcal{K}^{\prime}$ is an ${\vv{a}}$-variant of $\mathcal{K}$, if
$\mathcal{K}^{\prime}$ and $\mathcal{K}$ share the same frame and the same
atomic valuations, except possibly at the root and only for atomics not in
${\vv{a}}$, for which we may have different valuations. We also say that
$\mathcal{K}^{\prime}$ is a variant of $\mathcal{K}$, if it is
$\emptyset$-variant of $\mathcal{K}$. Also for a Kripke model $\mathcal{K}$
with the root $w_{0}$ we define $\mathcal{K}\Vdash^{-}A$ iff
$\mathcal{K},w\Vdash A$ for every $w\neq w_{0}$.
We say that a proposition $A$ is ${\vv{a}}$-extendible if for every Kripke
model $\mathcal{K}\Vdash A$ and every
$\mathcal{K}^{\prime}\subseteq^{{{\vv{a}}}}\mathcal{K}$ with
$\mathcal{K}^{\prime}\Vdash^{-}A$ there is an ${\vv{a}}$-variant
$\mathcal{K}^{\prime\prime}$ of $\mathcal{K}^{\prime}$ such that
$\mathcal{K}^{\prime\prime}\Vdash A$. Also we say that $A$ is extendible if it
is $\emptyset$-extendible.
For later applications in this paper it is helpful to define ${\sf
par}$-extendibility also for a class of Kripke models. Let $\mathscr{K}$ is a
class of Kripke models. Define the Kripke model $\sum(\mathscr{K})$ as the
disjoint union of all Kripke models in $\mathscr{K}$ with a fresh root $w_{0}$
such that for every atomic $a$ we have $\sum(\mathscr{K}),w_{0}\Vdash a$ iff
$\mathscr{K}\Vdash a$. Also for a Kripke model $\mathcal{K}$ with
$\mathscr{K}\subseteq^{{\mathcal{K}}}$ define $\sum(\mathscr{K},\mathcal{K})$
as disjoint union of the Kripke models in $\mathscr{K}$ with a fresh root
$w_{0}$ and following valuation for atomics $a\in{\vv{a}}$:

$\sum(\mathscr{K},\mathcal{K}),w_{0}\Vdash
a\quad\text{iff}\quad\mathcal{K}\Vdash a.$

We say that $\mathscr{K}$ is ${\vv{a}}$-extendible, if for every finite
$\mathscr{K}^{\prime}\subseteq\mathscr{K}$ with
$\mathscr{K}^{\prime}\subseteq^{{{\vv{a}}}}\mathcal{K}\in\mathscr{K}$, there
is an ${\vv{a}}$-variant of $\sum(\mathscr{K}^{\prime},\mathcal{K})$ which
belongs to $\mathscr{K}$. We say that $\mathscr{K}$ is extendible if it is
$\emptyset$-extendible. One may easily observe that $A$ is ${\sf
par}$-extendible iff $\textup{Mod}(A)$ is so.

###  3.3 ${\sf NNIL}({\sf par})$-projectivity and ${\sf par}$-extendibility

In this section we will prove theorem 3.4, an extension of Ghilardi’s
characterization of projective propositions via the notion of extendibility
(see theorem 3.3).
For a proposition $A$ and a set ${\vv{x}}\subseteq{\sf var}$, define the
substitution
$\theta^{\vv{x}}_{\\!\\!A}:\mathcal{L}_{0}\longrightarrow\mathcal{L}_{0}$ as
follows:

$\theta^{\vv{x}}_{\\!\\!A}(x):=\begin{cases}A\to x\quad&:x\in{\sf
var}\cap{\vv{x}}\\\ A\wedge x&:x\in{\sf var}\setminus{\vv{x}}\end{cases}$

Let ${\vv{x}}_{\\!1},\ldots,{\vv{x}}_{\\!s}$ be a list of all subsets of ${\sf
var}$ such that ${\vv{x}}_{\\!i}\subseteq{\vv{x}}_{\\!j}$ implies $i\leq j$.
Finally define

${\theta_{\\!\\!A}}:={\theta^{{\vv{x}}_{\\!s}}_{\\!\\!A}}{\theta^{{\vv{x}}_{\\!s-1}}_{\\!\\!A}}\ldots{\theta^{{\vv{x}}_{\\!1}}_{\\!\\!A}}$

The following theorem, is the main preliminary tool provided in [Ghilardi,,
1999] to characterize the unification type of ${\sf IPC}$. We refer the reader
to [Ghilardi,, 1999, theorem 5] for its proof. We will prove a generalization
of this in theorem 3.4.

######  Theorem 3.3.

For $A\in\mathcal{L}_{0}$, the following conditions are equivalent:

  1. 1.

${\theta_{\\!\\!A}}$ is a unifier for $A$, i.e. $\vdash{\theta_{\\!\\!A}}(A)$,

  2. 2.

$A$ is projective,

  3. 3.

$A$ is extendible.

Before we continue with a generalization of above theorem, let us give another
definition. Let $\mathcal{K}$ be a Kripke model and ${\vv{p}}\subseteq{\sf
par}$. Then define $A^{\dagger}$ as follows: (remember that previously we
defined $A^{\dagger}$ for ${{\sf NNIL}({\sf par})}$-projective $A$ as the
unique $A^{\prime}\in{{\sf NNIL}({\sf par})}$ such that
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime}$.
As we will see in next theorem, these two definitions are the same up to ${\sf
IPC}$-provable equivalence relation.)

$A^{\dagger}:=\bigwedge_{{\vv{p}}\subseteq{\sf
par}}\left(\bigwedge{\vv{p}}\to\bigvee_{\mathcal{K}\Vdash{\vv{p}},A}\bigwedge[\\![{\mathcal{K}}]\\!]_{{}_{{{\sf
N}({\sf par})}}}\right)$

Note that since by section 3.2 the set ${{\sf NNIL}({\sf par})}$ is finite and
$[\\![{\mathcal{K}}]\\!]_{{}_{{{\sf N}({\vv{p}})}}}\subseteq{{\sf NNIL}({\sf
par})}$, the conjunction $\bigwedge[\\![{\mathcal{K}}]\\!]_{{}_{{{\sf N}({\sf
par})}}}$ is a proposition and also the disjunction may considered as a finite
disjunction.

######  Remark .

Note that by above definition, if $\vdash A\to B$ then $\vdash A^{\dagger}\to
B^{\dagger}$.

######  Theorem 3.4.

For $A\in\mathcal{L}_{0}$, the following conditions are equivalent:

  1. 1.

$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{\twoheadrightarrow}{\scriptstyle{\theta_{\\!\\!A}}}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\dagger}$,

  2. 2.

$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}{{\sf
NNIL}({\sf par})}$,

  3. 3.

$A$ is ${\sf par}$-extendible.

###### Proof.

$1\to 2$: From definitions of $A^{\dagger}$, evidently $A^{\dagger}\in{\sf
NNIL}$. Also observe that $\theta^{\vv{x}}_{\\!\\!A}$ is $A$-projective. Then
since $A$-projective substitutions are closed under compositions,
${\theta_{\\!\\!A}}$ are $A$-projective.
$2\to 3$: Let
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime}\in{{\sf
NNIL}({\sf par})}$ and $\mathcal{K}\Vdash A$ and
$\mathcal{K}^{\prime}\subseteq^{{{\sf par}}}\mathcal{K}$ and
$\mathcal{K}^{\prime}\Vdash^{-}A$ seeking some variant
$\mathcal{K}^{\prime\prime}$ of $\mathcal{K}^{\prime}$ such that
$\mathcal{K}^{\prime\prime}\Vdash A$. Let
$\mathcal{K}^{\prime\prime}=\theta(\mathcal{K}^{\prime})$. First note that by
$A$-projectivity of $\theta$, $\mathcal{K}^{\prime\prime}$ is a ${\sf
par}$-variant of $\mathcal{K}^{\prime}$. Since $\mathcal{K}\Vdash A^{\prime}$,
$A^{\prime}\in{{\sf NNIL}({\sf par})}$ and
$\mathcal{K}^{\prime}\subseteq^{{{\sf par}}}\mathcal{K}$, theorem 3.1 implies
that $\mathcal{K}^{\prime}\Vdash A^{\prime}$. Hence
$\mathcal{K}^{\prime}\Vdash\theta(A)$, and by section 3.2 we have
$\mathcal{K}^{\prime\prime}\Vdash A$.
$3\to 1$: Let $A$ is ${\sf par}$-extendible and show $\vdash
A^{\dagger}\leftrightarrow{\theta_{\\!\\!A}}(A)$. We use induction on the
height of Kripke model $\mathcal{K}$ and show $\mathcal{K}\Vdash
A^{\dagger}\leftrightarrow{\theta_{\\!\\!A}}(A)$. Suppose that $w_{0}$ is the
root of $\mathcal{K}$. By induction hypothesis, we have
$\mathcal{K}\Vdash^{-}A^{\dagger}\leftrightarrow{\theta_{\\!\\!A}}(A)$ and
hence by section 3.2,
${\theta_{\\!\\!A}}(\mathcal{K})\Vdash^{-}A^{\dagger}\leftrightarrow A$. We
show ${\theta_{\\!\\!A}}(\mathcal{K})\Vdash A^{\dagger}\leftrightarrow A$. If
${\theta_{\\!\\!A}}(\mathcal{K})\nVdash^{-}A^{\dagger}$, then
${\theta_{\\!\\!A}}(\mathcal{K})\nVdash^{-}A$ and hence
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\nVdash A^{\dagger}$ and
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\nVdash A$. Then
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A^{\dagger}\leftrightarrow A$ and
we are done. So assume that ${\theta_{\\!\\!A}}(\mathcal{K})\Vdash^{-}A\wedge
A^{\dagger}$. It is enough to show the following items:

  * •

${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A$ implies
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A^{\dagger}$. By section 3.1 we
have $\vdash A\to A^{\dagger}$ and hence we have desired result.

  * •

${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A^{\dagger}$ implies
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A$. Let
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash A^{\dagger}$. Also assume that
${\theta_{\\!\\!A}}(\mathcal{K})$ is ${\vv{p}}$-model, i.e.
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash{\vv{p}}$ and
${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\nVdash\bigvee({\sf
par}\setminus{\vv{p}})$. Since ${\theta_{\\!\\!A}}(\mathcal{K}),w_{0}\Vdash
A^{\dagger}$, for some $\mathcal{K}_{1}\in\textup{Mod}(A)$ with
$\mathcal{K}_{1}\Vdash{\vv{p}}$ we have
${\theta_{\\!\\!A}}(\mathcal{K})\Vdash[\\![{\mathcal{K}_{1}}]\\!]_{{}_{{{\sf
N}({\sf par})}}}$. Theorem 3.2 implies that
${\theta_{\\!\\!A}}(\mathcal{K})\preceq^{{{\sf par}}}\mathcal{K}_{1}$. Then
section 3.2 implies ${\theta_{\\!\\!A}}(\mathcal{K})\preceq_{1}^{{{\sf
par}}}\mathcal{K}_{1}$ and thus by section 3.2 there is some
$\mathcal{K}_{2}\Vdash A$ such that
${\theta_{\\!\\!A}}(\mathcal{K})\subseteq^{{{\sf par}}}\mathcal{K}_{2}$. Since
$A$ is ${\sf par}$-extendible, there is a ${\sf par}$-variant
$\mathcal{K}^{\prime}$ of ${\theta_{\\!\\!A}}(\mathcal{K})$ such that
$\mathcal{K}^{\prime}\Vdash A$. Thus section 3.3 implies
${\theta_{\\!\\!A}}(\mathcal{K})\Vdash A$. ∎

######  Corollary .

${{\sf N}({\sf par})}$-projectivity is decidable. In other words, given
$A\in\mathcal{L}_{0}$, one may algorithmically decide
$A\in{{\downarrow^{\\!\\!{}^{\,}}}{{\sf N}({\sf par})}}$.

###### Proof.

Given $A$, by theorem 3.4 it is enough to decide ${\sf
IPC}\vdash{\theta_{\\!\\!A}}(A)\leftrightarrow A^{\dagger}$, which is
decidable since ${\sf IPC}$ is decidable. ∎

######  Lemma .

If ${\theta_{\\!\\!A}}(\mathcal{K})\Vdash^{-}A$ and $A$ is valid in a ${\sf
par}$-variant of ${\theta_{\\!\\!A}}(\mathcal{K})$ then
${\theta_{\\!\\!A}}(\mathcal{K})\Vdash A$.

###### Proof.

See proof of the theorem 5 in [Ghilardi,, 1999]. ∎

###  3.4 Projective resolution

The main result in [Ghilardi,, 1999] is that the unification type of ${\sf
IPC}$ is finitary. It means that for every $A\in\mathcal{L}_{0}({\sf var})$,
there exists a finite complete set of unifiers for $A$, i.e. a finite set
$\Theta$ of unifiers for $A$ such that every unifier of $A$ is less general
than some $\theta\in\Theta$. We say that $\theta$ is less general than
$\gamma$ if there is some substitution $\lambda$ such that for every $x\in{\sf
var}$ we have

$\vdash\theta(x)\leftrightarrow\lambda(\gamma(x)).$

The proof of above mentioned fact is based on projective approximations which
later [Ghilardi,, 2002] provides a resolution/tableaux method for its
computation. The aim for this subsection is to prove a relativised version of
projective approximations in theorem 3.6.

######  Definition .

Given $\Gamma,\Pi\subseteq\mathcal{L}_{0}$ and $A\in\mathcal{L}_{0}$, we say
that $\Pi$ is $\Gamma$-projective resolution for $A$ if

  * •

$\Pi$ is a set of independent propositions, i.e. for $B,C\in\Pi$, $\vdash B\to
C$ implies $B=C$.

  * •

Every $B\in\Pi$ is $\Gamma$-projective.

  * •

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${\Gamma}$} \end{picture}}}\bigvee\Pi$.

  * •

$\vdash\bigvee\Pi\to A$.

A $\\{\top\\}$-projective resolution is also called projective resolution.

Note that $\emptyset$ is a projective resolution for a proposition which is
not unifiable. The greatest lower bound (glb) for a proposition $A$ is defined
in section 2.7. Intuitively a glb for $A$ w.r.t. $(\Gamma,{\sf T})$ is the
best $\Gamma$-approximation from below inside the logic ${\sf T}$.

######  Remark .

If $\Pi$ is $\Gamma$-projective resolution of $A$ then $\bigvee\Pi$ is a glb
for $A$ w.r.t. $({{\downarrow}\Gamma^{\vee}},{\sf IPC})$.

###### Proof.

By theorem 2.2 we have
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){
${{{\downarrow^{\\!\\!{}^{\,}}}\Gamma}}$} \end{picture}}\bigvee\Pi$ and hence
by theorem 2.4 we have
$A\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${{\sf T}}$} \put(-0.1,-0.8){
${{{\downarrow^{\\!\\!{}^{\,}}}\Gamma}^{\\!\vee}}$} \end{picture}}\bigvee\Pi$.
Thus theorem 2.5 implies desired result. ∎

######  Theorem 3.5.

Whenever ${\sf par}=\emptyset$, every $A\in\mathcal{L}_{0}$ has projective
resolution.

###### Proof.

See [Ghilardi,, 1999, theorem 5]. We will also prove a generalization of this
result in theorem 3.6. ∎

First some preliminary definitions. We refer the reader to [Ghilardi,, 1999]
for more information on these notions.

Let $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ and
$\mathcal{K}^{\prime}=(W^{\prime},\preccurlyeq^{\prime},\mathrel{V}^{\prime})$
are two Kripke models with the roots $w_{0}$ and $w^{\prime}_{0}$. Also let
$\mathcal{K}(w):=\\{a\in{\sf atom}:\mathcal{K},w\Vdash a\\}$ and
$\mathcal{L}_{0}(\mathcal{K})$ be defined as $\mathcal{L}_{0}(\bigcup_{w\in
W}\mathcal{K}(w))$. We say that $\mathcal{K}$ is with finite valuations if for
every $w\in W$ we have $\mathcal{K}(w)$ is finite. Also define:

$\displaystyle\mathcal{K}\sim_{0}\mathcal{K}^{\prime}\quad$
$\displaystyle\text{iff}\quad\mathcal{K}(w_{0})=\mathcal{K}^{\prime}(w_{0}^{\prime})$
$\displaystyle\mathcal{K}\sim_{n+1}\mathcal{K}^{\prime}\quad$
$\displaystyle\text{iff}\quad\forall\,w\in W\,\exists\,w^{\prime}\in
W^{\prime}(\mathcal{K}_{w}\sim_{n}\mathcal{K}^{\prime}_{w^{\prime}})\text{ and
vice versa}$ $\displaystyle\mathcal{K}\leq_{0}\mathcal{K}^{\prime}\quad$
$\displaystyle\text{iff}\quad\mathcal{K}(w_{0})\supseteq\mathcal{K}^{\prime}(w^{\prime}_{0})$
$\displaystyle\mathcal{K}\leq_{n+1}\mathcal{K}^{\prime}\quad$
$\displaystyle\text{iff}\quad\forall\,w\in W\,\exists\,w^{\prime}\in
W^{\prime}(\mathcal{K}_{w}\sim_{n}\mathcal{K}^{\prime}_{w^{\prime}})$

Evidently $\sim_{n}$ is an equivalence relation and $\leq_{n}$ is reflexive
transitive. One may easily observe by induction on $n$ that
$\mathcal{K}\sim_{n+1}\mathcal{K}^{\prime}$ implies
$\mathcal{K}\sim_{n}\mathcal{K}^{\prime}$. Hence
$\mathcal{K}\sim_{n}\mathcal{K}^{\prime}$
($\mathcal{K}\leq_{n}\mathcal{K}^{\prime}$) implies
$\mathcal{K}\sim_{m}\mathcal{K}^{\prime}$
($\mathcal{K}\leq_{m}\mathcal{K}^{\prime}$) for every $m\leq n$.
Let $c_{\\!{}_{\to}\\!}(A)$ indicate the maximum number of nested implications
in $A$:

  * •

$c_{\\!{}_{\to}\\!}(a)=c_{\\!{}_{\to}\\!}(\top)=c_{\\!{}_{\to}\\!}(\bot)=0$
for atomic $a$.

  * •

$c_{\\!{}_{\to}\\!}(A\circ
B):=\max\\{c_{\\!{}_{\to}\\!}(A),c_{\\!{}_{\to}\\!}(B)\\}$, for
$\circ\in\\{\vee,\wedge\\}$.

  * •

$c_{\\!{}_{\to}\\!}(A\to
B):=1+\max\\{c_{\\!{}_{\to}\\!}(A),c_{\\!{}_{\to}\\!}(B)\\}$.

Remember that by default we assume the set ${\sf atom}$ to be a finite set.

######  Remark .

Modulo ${\sf IPC}$-provable equivalence relation, there are finitely many
propositions $A\in\mathcal{L}_{0}$ with $c_{\\!{}_{\to}\\!}(A)\leq n$.

###### Proof.

By induction on $n$, we define an upper bound $f(n)$ for the number of
propositions $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 ${\sf
IPC}$-equivalent to a disjunction of conjunctions of atomics. Hence
$f(0)=2^{2^{m}}$ is an obvious upper bound, in which $m$ is the number of
atomics in ${\sf 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 propositions.
Then since modulo ${\sf IPC}$-provable equivalence every proposition is a
disjunction of conjunctions of atomics or implications, the following
definition is an upperbound:

$f(n+1):=2^{2^{[m+f(n)^{2}]}}.\qed$

######  Lemma .

Every $A\in{\sf NNIL}$ has an ${\sf IPC}$-provable equivalent
$A^{\prime}\in{\sf NNIL}$ with $c_{\\!{}_{\to}\\!}(A^{\prime})\leq\\#{\sf
atom}$.

###### Proof.

Observe that every $A\in{\sf NNIL}$ has an ${\sf IPC}$-equivalent $B\in{\sf
NNIL}$ such that $B=\bigwedge_{i}\bigvee_{j}C_{i}^{j}$ and every implication
in $C^{j}_{i}$ is of the form $a\to E$, with $a\in{\sf atom}$ and $E$ does not
contain $a$. Then one may easily prove the statement of this lemma by
induction on the number of elements in ${\sf atom}$. ∎

######  Lemma .

For every Kripke model $\mathcal{K}$, there exists a proposition
${[\\![{\mathcal{K}}]\\!]_{n}}\in\mathcal{L}_{0}$ with the following
properties:

  * •

$\mathcal{K}^{\prime}\Vdash{[\\![{\mathcal{K}}]\\!]_{n}}$ iff
$\mathcal{K}^{\prime}\leq_{n}\mathcal{K}$.

  * •

$c_{\\!{}_{\to}\\!}({[\\![{\mathcal{K}}]\\!]_{n}})\leq n$.

###### Proof.

We only give the definition of $A$ here, and refer the reader to [Ghilardi,,
1999, proposition 1] for its proof.
Let $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ and define
${[\\![{\mathcal{K}}]\\!]_{0}}:=\bigwedge\mathcal{K}(w_{0})$ and

${[\\![{\mathcal{K}}]\\!]_{n+1}}:=\bigwedge_{\\{\mathcal{K}^{\prime}:\forall\,w\in
W(\mathcal{K}^{\prime}\nsim_{n}\mathcal{K}_{w})\\}}\left({[\\![{\mathcal{K}^{\prime}}]\\!]_{n}}\to\bigvee_{\\{\mathcal{K}^{\prime\prime}:\mathcal{K}^{\prime}\nleq_{n}\mathcal{K}^{\prime\prime}\\}}{[\\![{\mathcal{K}^{\prime\prime}}]\\!]_{n}}\right).\qed$

######  Corollary .

For every Kripke models $\mathcal{K}$ and $\mathcal{K}^{\prime}$, we have
$\mathcal{K}^{\prime}\leq_{n}\mathcal{K}$ iff for every $A\in\mathcal{L}_{0}$
with $c_{\\!{}_{\to}\\!}(A)\leq n$ we have $\mathcal{K}\Vdash A$ implies
$\mathcal{K}^{\prime}\Vdash A$.

###### Proof.

For the left to right direction, use induction on $n$. For the right to left,
if $\mathcal{K}$ is with finite valuations, one may easily use section 3.4 and
have desired result. Otherwise One may restrict $\mathcal{K}$ and
$\mathcal{K}^{\prime}$ to arbitrary finite atomics and then apply previous
argument. ∎

######  Corollary .

$\mathcal{K}^{\prime}\sim_{n}\mathcal{K}$ iff for every $A$ with
$c_{\\!{}_{\to}\\!}(A)\leq n$ we have

$\mathcal{K}\Vdash A$ iff $\mathcal{K}^{\prime}\Vdash A$.

###### Proof.

First observe that $\mathcal{K}\sim_{n}\mathcal{K}^{\prime}$ is equivalent to
$\mathcal{K}\leq_{n}\mathcal{K}^{\prime}\leq_{n}\mathcal{K}$ and then use
section 3.4. ∎

######  Lemma .

A class $\mathscr{K}$ of Kripke models is of the form $\textup{Mod}(A)$ with
$c_{\\!{}_{\to}\\!}(A)\leq n$, iff $\mathscr{K}$ is $\leq_{n}$-downward
closed, i.e. for every Kripke model $\mathcal{K}^{\prime}$ with
$\mathcal{K}^{\prime}\leq_{n}\mathcal{K}\in\mathscr{K}$ we have
$\mathcal{K}^{\prime}\in\mathscr{K}$.

###### Proof.

For the left-to-right direction, let
$\mathcal{K}^{\prime}\leq_{n}\mathcal{K}\in\textup{Mod}(A)$ for some $A$ with
$c_{\\!{}_{\to}\\!}(A)\leq n$. Since $\mathcal{K}\Vdash A$, section 3.4
implies $\mathcal{K}^{\prime}\Vdash A$ and hence
$\mathcal{K}^{\prime}\in\textup{Mod}(A)$.
For the other direction, let $\mathscr{K}$ is $\leq_{n}$-downward closed and
define

$A:=\bigvee_{\mathcal{K}\in\mathscr{K}}{[\\![{\mathcal{K}}]\\!]_{n}}.$

By section 3.4, the disjunction is finite and hence $A$ is indeed a
proposition. One may easily observe that section 3.4 implies that
$c_{\\!{}_{\to}\\!}(A)\leq n$ and $\mathscr{K}=\textup{Mod}(A)$. ∎

######  Lemma .

If a class of Kripke models $\mathscr{K}$ is ${\sf par}$-extendible and
$\theta$ is a substitution, then $\theta(\mathscr{K})$ is also ${\sf
par}$-extendible.

###### Proof.

Easy and left to the reader. ∎

We say that a class $\mathscr{K}$ of Kripke models is stable, if for every
$\mathcal{K}\in\mathscr{K}$ and every node $w$ in $\mathcal{K}$ we have
$\mathcal{K}_{w}\in\mathscr{K}$.

######  Remark .

A class $\mathscr{K}$ of Kripke models is ${\sf par}$-extendible iff for every
finite stable class of models $\mathscr{K}^{\prime}$ which is ${\sf
par}$-submodel of some $\mathcal{K}\in\mathscr{K}$, a ${\sf par}$-variant of
$\sum(\mathscr{K}^{\prime},\mathcal{K})$ belongs to $\mathscr{K}$.

###### Proof.

Easy and left to the reader. ∎

Define
$\langle\mathscr{K}\rangle_{n}:=\\{\mathcal{K}:\exists\,\mathcal{K}^{\prime}\in\mathscr{K}\
(\mathcal{K}\leq_{n}\mathcal{K}^{\prime})\text{ and }\mathcal{K}\text{ is a
Kripke model}\\}$.

######  Lemma .

If $\mathscr{K}$ is ${\sf par}$-extendible stable class of Kripke models, then
so is $\langle\mathscr{K}\rangle_{n}$, for every $n>\\#{\sf par}$. ($\\#{\sf
par}$ indicates the number of elements in ${\sf par}$.)

###### Proof.

We only prove here the ${\sf par}$-extendibility of
$\langle\mathscr{K}\rangle_{n}$ and leave other properties to the reader.
Let $\mathscr{F}^{\prime}=\\{\mathcal{K}^{\prime}_{i}\\}_{i}$ is a finite set
of models in $\langle\mathscr{K}\rangle_{n}$, which are ${\sf par}$-submodels
of some $\mathcal{K}^{\prime}\in\langle\mathscr{K}\rangle_{n}$. By section 3.4
we may also assume that $\mathscr{F}^{\prime}$ is stable. We must show that a
${\sf par}$-variant of $\sum(\mathscr{F}^{\prime},\mathcal{K}^{\prime})$
belongs to $\langle\mathscr{K}\rangle_{n}$. Since
$\mathcal{K}^{\prime}\in\langle\mathscr{K}\rangle_{n}$ and $\mathscr{K}$ is
stable, there is some $\mathcal{K}\in\mathscr{K}$ such that
$\mathcal{K}^{\prime}\sim_{n-1}\mathcal{K}$. Similarly, since
$\mathcal{K}^{\prime}_{i}\in\langle\mathscr{K}\rangle_{n}$, there is some
$\mathcal{K}_{i}\in\mathscr{K}$ 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 ${\sf par}$-submodel of $\mathcal{K}$.
Since $\mathscr{F}^{\prime}$ is a ${\sf par}$-submodel of
$\mathcal{K}^{\prime}$, by theorem 3.2 we have
$\mathcal{K}^{\prime}_{i}\Vdash[\\![{\mathcal{K}^{\prime}}]\\!]_{{}_{{{\sf
N}({\sf par})}}}$. From $\mathcal{K}^{\prime}_{i}\sim_{n-1}\mathcal{K}_{i}$,
sections 3.4 and 3.4 we get
$\mathcal{K}_{i}\Vdash[\\![{\mathcal{K}^{\prime}}]\\!]_{{}_{{{\sf N}({\sf
par})}}}$. Also since $\mathcal{K}^{\prime}\sim_{n-1}\mathcal{K}$, by sections
3.4 and 3.4 we have $[\\![{\mathcal{K}^{\prime}}]\\!]_{{}_{{{\sf N}({\sf
par})}}}=[\\![{\mathcal{K}}]\\!]_{{}_{{{\sf N}({\sf par})}}}$. Hence
$\mathcal{K}_{i}\Vdash[\\![{\mathcal{K}}]\\!]_{{}_{{{\sf N}({\sf par})}}}$,
and by theorem 3.2 we have $\mathcal{K}_{i}$ is a ${\sf par}$-submodel of
$\mathcal{K}$. Hence $\mathscr{F}$ is a ${\sf par}$-submodel of $\mathcal{K}$.
We go back to the main proof. Since $\mathscr{F}$ is ${\sf par}$-submodel of
$\mathcal{K}$, by extendibility of $\mathscr{K}$, there exist a ${\sf
par}$-variant $\hat{\mathcal{K}}$ of $\sum(\mathscr{F},\mathcal{K})$ in
$\mathscr{K}$. Let $w_{0}$ is the root of $\mathcal{K}$ which is also the root
of $\hat{\mathcal{K}}$ and $w^{\prime}_{0}$ is the root of
$\mathcal{K}^{\prime}$. Define the ${\sf par}$-variant
$\hat{\mathcal{K}}^{\prime}$ of
$\sum(\mathscr{F}^{\prime},\mathcal{K}^{\prime})$ for atomic $x\not\in{\sf
par}$ as follows:

$\hat{\mathcal{K}}^{\prime},w^{\prime}_{0}\Vdash
x\quad\Longleftrightarrow\quad\hat{\mathcal{K}},w_{0}\Vdash x.$

It is enough to show that
$\hat{\mathcal{K}}^{\prime}\in\langle\mathscr{K}\rangle_{n}$. For this aim it
is enough to show $\hat{\mathcal{K}}^{\prime}\leq_{n}\hat{\mathcal{K}}$. From
definition of $\hat{\mathcal{K}}$ and $\hat{\mathcal{K}}^{\prime}$, it is
clear that it is enough to show that
$\hat{\mathcal{K}}^{\prime}\sim_{n-1}\hat{\mathcal{K}}$. We use induction on
$k\leq n-1$ and show $\hat{\mathcal{K}}^{\prime}\sim_{k}\hat{\mathcal{K}}$.
If $k=0$, we must show that for every atomic $a$ we have

$\hat{\mathcal{K}}^{\prime},w^{\prime}_{0}\Vdash
a\quad\Longleftrightarrow\quad\hat{\mathcal{K}},w_{0}\Vdash a.$

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

$\hat{\mathcal{K}}^{\prime},w^{\prime}_{0}\Vdash
p\quad\Longleftrightarrow\quad\hat{\mathcal{K}},w_{0}\Vdash p.$

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

  * •

For every node $w^{\prime}$ in $\hat{\mathcal{K}}^{\prime}$, there is some $w$
in $\hat{\mathcal{K}}$ such that
$\hat{\mathcal{K}}^{\prime}_{w^{\prime}}\sim_{k-1}\hat{\mathcal{K}}_{w}$. If
$w^{\prime}$ is the root of $\hat{\mathcal{K}}^{\prime}$, take $w$ also the
root of $\hat{\mathcal{K}}$ and we have desired result by induction
hypothesis. If $w^{\prime}$ is not the root of $\hat{\mathcal{K}}^{\prime}$,
since $\mathscr{F}^{\prime}$ is stable, we may let $w^{\prime}$ 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

$\hat{\mathcal{K}}^{\prime}_{w^{\prime}}=\mathcal{K}^{\prime}_{i}\sim_{n-1}\mathcal{K}_{i}=\hat{\mathcal{K}}_{w}$

Since $k-1\leq n-1$, we have the desired result.

  * •

For every node $w$ in $\hat{\mathcal{K}}$, there is some $w^{\prime}$ in
$\hat{\mathcal{K}}^{\prime}$ such that
$\hat{\mathcal{K}}^{\prime}_{w^{\prime}}\sim_{k-1}\hat{\mathcal{K}}_{w}$.
Again if $w$ is the root, take $w^{\prime}$ 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^{\prime}$ in $\mathcal{K}^{\prime}_{i}$ such that
$(\mathcal{K}^{\prime}_{i})_{w^{\prime}}\sim_{n-2}(\mathcal{K}_{i})_{w}$.
Since $k-1\leq n-2$, we have

$\hat{\mathcal{K}}^{\prime}_{w^{\prime}}=(\mathcal{K}^{\prime}_{i})_{w^{\prime}}\sim_{k-1}(\mathcal{K}_{i})_{w}=\hat{\mathcal{K}}_{w},$

as desired.∎

######  Theorem 3.6.

Every $A\in\mathcal{L}_{0}$ has ${{\sf NNIL}({\sf par})}$-projective
resolution $\Pi$. Moreover for every $B\in\Pi$ we have
$c_{\\!{}_{\to}\\!}(B)\leq\max\\{c_{\\!{}_{\to}\\!}(A),1+\\#{\sf par}\\}$ and
$\Pi$ is a computable function of $A$.

###### Proof.

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

  1. 1.

$B^{A^{\prime}}_{\theta}$ is ${{\sf NNIL}({\sf par})}$-projective.

  2. 2.

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

  3. 3.

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

  4. 4.

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

Then by items 1-3 (an independent subset of) the following set is a ${{\sf
NNIL}({\sf par})}$-projective resolution for $A$:

$\Pi:=\\{B^{A^{\prime}}_{\theta}:A^{\prime}\in{{\sf NNIL}({\sf par})}\text{
and $\theta$ a substitution such that }\vdash A^{\prime}\to\theta(A)\\}.$

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

$\mathscr{K}:=\theta(\textup{Mod}(A^{\prime})):=\\{\theta(\mathcal{K}):\mathcal{K}\in\textup{Mod}(A^{\prime})\\}$

Since $\langle\mathscr{K}\rangle_{n}$ has downward $\leq_{n}$-closure
condition, we may apply section 3.4 and find some proposition, e.g.
$B^{A^{\prime}}_{\theta}$, such that
$c_{\\!{}_{\to}\\!}(B^{A^{\prime}}_{\theta})\leq n$ (so item 4 is satisfied)
and $\langle\mathscr{K}\rangle_{n}=\textup{Mod}(B^{A^{\prime}}_{\theta})$.
Since $A^{\prime}\in{{\sf NNIL}({\sf par})}$, evidently it is ${{\sf
NNIL}({\sf par})}$-projective. Hence by theorem 3.4, $A^{\prime}$ is ${\sf
par}$-extendible. Hence by section 3.4, $\mathscr{K}$ is ${\sf
par}$-extendible. Since $\mathscr{K}$ is stable and $n>\\#{\sf par}$, Section
3.4 implies that $\langle\mathscr{K}\rangle_{n}$ is also ${\sf
par}$-extendible. Hence $B^{A^{\prime}}_{\theta}$ is ${\sf par}$-extendible
and by theorem 3.4, $B^{A^{\prime}}_{\theta}$ is ${{\sf NNIL}({\sf
par})}$-projective. So item (1) is satisfied.
To show item 3 for $B^{A^{\prime}}_{\theta}$, it is enough to show
$\mathcal{K}\Vdash B^{A^{\prime}}_{\theta}\to A$ for every finite rooted model
$\mathcal{K}$. If $\mathcal{K}\Vdash B^{A^{\prime}}_{\theta}$, we have
$\mathcal{K}\in\langle\mathscr{K}\rangle_{n}$. Hence
$\mathcal{K}\leq_{n}\mathcal{K}^{\prime}$ for some
$\mathcal{K}^{\prime}\in\mathscr{K}$. Then
$\mathcal{K}^{\prime}=\theta(\mathcal{K}^{\prime\prime})$ for some finite
rooted $\mathcal{K}^{\prime\prime}$ such that
$\mathcal{K}^{\prime\prime}\Vdash A^{\prime}$. Since $\vdash
A^{\prime}\to\theta(A)$, we have $\mathcal{K}^{\prime\prime}\Vdash\theta(A)$,
and by section 3.2 we get $\theta(\mathcal{K}^{\prime\prime})\Vdash A$, whence
$\mathcal{K}^{\prime}\Vdash A$. Since $c_{\\!{}_{\to}\\!}(A)\leq n$ and
$\mathcal{K}\leq_{n}\mathcal{K}^{\prime}$, section 3.4 implies that
$\mathcal{K}\Vdash A$, as desired.
It remains to show that item 2 holds. It is enough to show $\mathcal{K}\Vdash
A^{\prime}\leftrightarrow\theta(B^{A^{\prime}}_{\theta})$ for arbitrary finite
rooted $\mathcal{K}$. If $\mathcal{K}\Vdash A^{\prime}$, then
$\theta(\mathcal{K})\Vdash A^{\prime}$ and hence
$\theta(\mathcal{K})\in\mathscr{K}\subseteq\langle\mathscr{K}\rangle_{n}=\textup{Mod}(B^{A^{\prime}}_{\theta})$.
Then $\theta(\mathcal{K})\Vdash B^{A^{\prime}}_{\theta}$ and hence
$\mathcal{K}\Vdash\theta(B^{A^{\prime}}_{\theta})$. For the other direction,
let $\mathcal{K}\Vdash\theta(B^{A^{\prime}}_{\theta})$. Hence
$\theta(\mathcal{K})\Vdash B^{A^{\prime}}_{\theta}$ and then
$\theta(\mathcal{K})\in\textup{Mod}(B^{A^{\prime}}_{\theta})=\langle\mathscr{K}\rangle_{n}$.
So there is some $\mathcal{K}^{\prime}\in\mathscr{K}$ such that
$\theta(\mathcal{K})\leq_{n}\mathcal{K}^{\prime}$. Since
$\mathcal{K}^{\prime}\in\mathscr{K}$, there is some
$\mathcal{K}^{\prime\prime}$ such that
$\mathcal{K}^{\prime}=\theta(\mathcal{K}^{\prime\prime})$ and
$\mathcal{K}^{\prime\prime}\Vdash A^{\prime}$. Since
$A^{\prime}=\theta(A^{\prime})$, we have
$\mathcal{K}^{\prime\prime}\Vdash\theta(A^{\prime})$ and hence
$\mathcal{K}^{\prime}\Vdash A^{\prime}$. By section 3.4
$c_{\\!{}_{\to}\\!}(A^{\prime})<n$ and the section 3.4 implies
$\mathcal{K}\Vdash A^{\prime}$.

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

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

Note that $\Pi^{\prime}$ is computable since ${\sf IPC}$ is decidable and by
section 3.3 we can decide $B\in{{\downarrow^{\\!\\!{}^{\,}}}{{\sf N}({\sf
par})}}$. Finally one may easily find $\Pi\subseteq\Pi^{\prime}$ which
includes pairwise ${\sf IPC}$-independent propositions, as required for
projective resolutions. ∎

###  3.5 Projective resolution for NNIL

In this subsection, we will see that projective resolution of a ${\sf
NNIL}$-proposition gets a more elegant form. We will use this form later for
characterization of ${{\sf NNIL}({\sf par})}$-admissible rules of ${\sf IPC}$,
specifically for the validity of disjunction rule. By theorem 3.5 or
equivalently theorem 3.6 with empty ${\sf par}$, there is a finite projective
resolution for every proposition $A$, i.e. a set $\\{A_{1},\ldots,A_{n}\\}$,
with the following properties:

  * •

Every unifier of $A$, is also a unifier of some $A_{i}$, in other words
$A\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!\bigvee A_{i}$.

  * •

$\vdash\bigvee A_{i}\to A$.

  * •

$A_{i}$ is projective for every $i\leq n$.

We will prove here that if $A\in{\sf NNIL}$, the projective resolution can be
chosen such that every $A_{i}$ is ${\sf NNIL}$ and moreover $\vdash
A\leftrightarrow\bigvee A_{i}$.
Given $A\in{\sf NNIL}$, we say that $A$ is a ${\sf T}$-component if
$A=\bigwedge\Gamma\wedge\bigwedge\Delta$ with the following properties:

  * •

Every $B\in\Gamma$ is atomic.

  * •

Every $B\in\Delta$ is an implication $C\to D$ for some atomic $C$ such that
${\sf T}\nvdash\bigwedge\Gamma\to C$.

######  Lemma .

Let ${\sf T}$ be a logic extending ${\sf IPC}$. Every $A\in{\sf NNIL}$ can be
decomposed to ${\sf T}$-components, i.e. there is a finite set of ${\sf
T}$-components $\Gamma_{A}$ such that ${\sf T}\vdash
A\leftrightarrow\bigvee\Gamma_{A}$. Moreover, if $A\in{\sf NNIL}({\vv{a}})$
then $\Gamma_{A}\subseteq{\sf NNIL}({\vv{a}})$.

###### Proof.

We use induction on ${\sf sub^{{\sf atom}}}(A)$ (the set of atomic formulas in
$A$) ordered by $\supset$ and find some finite set $\Gamma_{A}$ of ${\sf
T}$-components with ${\sf sub^{{\sf atom}}}(\Gamma_{A})\subseteq{\sf sub^{{\sf
atom}}}(A)$ and ${\sf T}\vdash\bigvee\Gamma_{A}\leftrightarrow A$. As
induction hypothesis assume that for every ${\sf T}$ and $B\in{\sf NNIL}$ with
${\sf sub^{{\sf atom}}}(B)\subset{\sf sub^{{\sf atom}}}(A)$ there is a finite
set $\Gamma_{B}$ of ${\sf T}$-components such that ${\sf T}\vdash
B\leftrightarrow\bigvee\Gamma$ and ${\sf sub^{{\sf
atom}}}(\Gamma_{B})\subseteq{\sf sub^{{\sf atom}}}(B)$. For the induction
step, assume that $A\in{\sf NNIL}$ is given. Using derivation in ${\sf IPC}$
one may easily find finite sets $\Gamma_{i}$ and $\Delta_{i}$ for $1\leq i\leq
n$ such that

  * •

${\sf 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 propositions.

  * •

$\Gamma_{i}$ includes implications with atomic antecedents.

  * •

${\sf sub^{{\sf atom}}}(\Gamma_{i}\cup\Delta_{i})\subseteq{\sf sub^{{\sf
atom}}}(A)$.

It is enough to decompose every $A_{i}$ to ${\sf T}$-components. If ${\sf
T}\nvdash\bigwedge\Delta_{i}\to E$ for every antecedent $E$ of an implication
in $\Gamma_{i}$, then $A_{i}$ already is a ${\sf T}$-component and we are
done. Otherwise, there is some $E\to F\in\Gamma_{i}$ such that ${\sf
T}\vdash\bigwedge\Delta_{i}\to E$. Then let $A_{i}^{\prime}:=A_{i}[E:\top]$,
i.e. the replacement of every occurrences of $E$ in $A_{i}$ with $\top$. Also
let ${\sf T}^{\prime}:={\sf T}+E$. Hence ${\sf sub^{{\sf
atom}}}(A^{\prime}_{i})\subsetneqq{\sf sub^{{\sf atom}}}(A)$ and by induction
hypothesis we may decompose $A^{\prime}_{i}$ to ${\sf T}^{\prime}$-components:

${\sf T},E\vdash A^{\prime}_{i}\leftrightarrow\bigvee_{j}B_{j}$

It is not difficult to observe that if $B_{j}$ is a ${\sf
T}^{\prime}$-component then $B^{\prime}_{j}:=E\wedge B_{j}$ is a ${\sf
T}$-component. Moreover ${\sf T}\vdash E\wedge
A^{\prime}_{i}\leftrightarrow\bigvee_{j}B^{\prime}_{j}$ and since ${\sf
IPC}\vdash(E\wedge A^{\prime}_{i})\leftrightarrow(E\wedge A_{i})$ and ${\sf
T}\vdash A_{i}\to E$, we get

${\sf T}\vdash A_{i}\leftrightarrow\bigvee_{j}B^{\prime}_{j}$

Hence we have decomposed $A_{i}$ to ${\sf T}$-components $B^{\prime}_{j}$ with
${\sf sub^{{\sf atom}}}(B^{\prime}_{j})\subseteq{\sf sub^{{\sf atom}}}(A)$, as
desired. ∎

######  Lemma .

Every ${\sf IPC}$-component is extendible.

###### Proof.

Let $B=\bigwedge B_{i}$ is an ${\sf IPC}$-component and $\mathscr{K}$ be a
finite class of finite rooted Kripke models for $B$. We must show that a
variant of $\sum(\mathscr{K})$ is a model of $B$. Let $w_{0}$ be the root of
$\sum(\mathscr{K})$ and define a variant $\mathcal{K}$ of $\sum(\mathscr{K})$
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$. ∎

######  Corollary .

For $A\in{\sf NNIL}$ there is a finite set $\Delta$ of projective and ${\sf
NNIL}$ propositions with

$\vdash A\leftrightarrow\bigvee\Delta.$

###### Proof.

Use sections 3.5, 3.5 and 3.3. ∎

######  Lemma .

Every extendible $A$ is ${\sf IPC}$-prime, i.e. if $\vdash A\to(B\vee C)$,
then either $\vdash A\to B$ or $\vdash A\to C$.

###### 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}^{\prime}$ 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)$. ∎

######  Theorem 3.7.

Given $A\in\mathcal{L}_{0}$, the following are equivalent:

  1. 1.

$A$ is an ${\sf IPC}$-component, (modulo ${\sf IPC}$-provable equivalence
relation)

  2. 2.

$A$ is extendible,

  3. 3.

$A$ is ${\sf IPC}$-prime.

###### Proof.

$1\Rightarrow 2$: section 3.5. $2\Rightarrow 3$: section 3.5. $3\Rightarrow
1$: Let $A$ is ${\sf IPC}$-prime. By section 3.5 it can be decomposed to ${\sf
IPC}$-components $\Gamma_{A}$. Thus $\vdash A\leftrightarrow\bigvee\Gamma_{A}$
and by ${\sf IPC}$-primality of $A$ we have $\vdash A\to B$ for some
$B\in\Gamma_{A}$. Then $\vdash A\leftrightarrow B$ and hence $A$ is ${\sf
IPC}$-equivalent to some ${\sf IPC}$-component. ∎

Remember that ${\sf P}{\sf NNIL}({\sf par})$ indicates the set of ${\sf
IPC}$-prime and ${{\sf NNIL}({\sf par})}$-propositions.

######  Corollary .

Up to ${\sf IPC}$-provable equivalence relation, we have ${\sf NNIL}={\sf
P}{\sf NNIL}^{\vee}$ and ${{\sf NNIL}({\sf par})}={\sf P}{\sf NNIL}({\sf
par})^{\vee}$.

###### Proof.

By section 3.5 every $A\in{\sf NNIL}$ can be decomposed to ${\sf
IPC}$-components $\Gamma_{A}$ such that $A\in{{\sf NNIL}({\sf par})}$ implies
$\Gamma_{A}\subseteq{{\sf NNIL}({\sf par})}$. Then theorem 3.7 implies that
every $E\in\Gamma_{A}$ is ${\sf IPC}$-prime. Hence $\bigvee\Gamma_{A}\in{\sf
P}{\sf NNIL}^{\vee}$ and moreover $A\in{{\sf NNIL}({\sf par})}$ implies
$\bigvee\Gamma_{A}\in{\sf P}{\sf NNIL}({\sf par})^{\vee}$. ∎

######  Corollary .

${\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf IPC}}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ \
\
}={\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${{\sf IPC}}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ \
}$.

###### Proof.

Sections 3.5 and 2.4. ∎

A consequence of the results in this subsection is that now we have uniqueness
of the projective resolutions:

######  Theorem 3.8 (Projective Resolution).

Every $A\in\mathcal{L}_{0}$ has a ${\sf P}{\sf NNIL}({\sf par})$-projective
resolution. Moreover this resolution is computable and unique up to ${\sf
IPC}$-provable equivalency, i.e. for every two ${\sf P}{\sf NNIL}({\sf
par})$-projective resolutions $\Delta=\\{B_{1},\ldots,B_{m}\\}$ and
$\Delta^{\prime}=\\{C_{1},\ldots,C_{n}\\}$ for $A$, we have $m=n$ and there is
some permutation $\sigma$ such that for every $i$, $\vdash
B_{i}\leftrightarrow C_{\sigma(i)}$.

###### Proof.

Given $A$, by theorem 3.6 there is a ${{\sf NNIL}({\sf par})}$-projective
resolution $\Delta$ for $A$. Then define

$\Pi_{0}:=\\{E\wedge E^{\prime}:E\in\Delta\text{ and
}E^{\prime}\in\Gamma_{E^{\dagger}}\\}$

in which $E^{\dagger}\in{{\sf NNIL}({\sf par})}$ is the ${{\sf NNIL}({\sf
par})}$-projection of $E$ and $\Gamma_{E^{\dagger}}$ is the decomposition of
$E^{\dagger}$ to ${\sf IPC}$-components, as provided by section 3.5. Finally
let $\Pi\subseteq\Pi_{0}$ be some $\subseteq$-minimal set with
$\vdash\bigvee\Pi_{0}\leftrightarrow\bigvee\Pi$. Then by section 3.5 and the
following fact one may easily observe that $\Pi$ is a ${\sf P}{\sf NNIL}({\sf
par})$-projective resolution for $A$: if
$A\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}A^{\prime}\in{{\sf
NNIL}({\sf par})}$ and $E\in{\sf P}{\sf NNIL}({\sf par})$, then $(A\wedge
E)\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}(A^{\prime}\wedge
E)$.
For the uniqueness, it is enough to show that for every ${\sf P}{\sf
NNIL}({\sf par})$-projective $E$, if
$E\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \
}\bigvee_{i}F_{i}$ then for some $i$ we have $\vdash E\to F_{i}$. Let
$E\ensurestackMath{\mathrel{\stackengine{1pt}{\stackengine{0pt}{{\rightarrowtail}\\!\\!\\!\\!\\!{\twoheadrightarrow}}{\scriptstyle\theta}{O}{c}{F}{F}{S}}{\scriptstyle}{U}{c}{F}{F}{S}}}E^{\dagger}$.
Then by
$E\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \
}\bigvee_{i}F_{i}$ we have $\vdash\theta(E^{\dagger}\to\bigvee_{i}F_{i})$.
Hence $\vdash E^{\dagger}\to\bigvee_{i}\theta(F_{i})$ and since $E^{\dagger}$
is ${\sf IPC}$-prime, we have $\vdash E^{\dagger}\to\theta(F_{i})$ for some
$i$. Thus section 3.1 implies $\vdash E\to F_{i}$, as desired. ∎

##  4 ${{\sf NNIL}({\sf par})}$-admissible rules of ${\sf IPC}$

In [Iemhoff, 2001b, ], the admissibility relation
$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$ is characterized by
means of preservation relation $\rhd$ and its Kripke semantics, called ${\sf
AR}$-models. In this section we will characterize and prove the decidability
of
$\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }$ , the
${{\sf NNIL}({\sf par})}$-admissible rules of ${\sf IPC}$ (see section 2.6).
For this end, we imitate the route in [Iemhoff, 2001b, ], i.e. we define a
system ${{\sf AR}_{{\sf par}}}\\!\,$ for the ${{\sf NNIL}({\sf
par})}$-admissible rules of ${\sf IPC}$ and also introduce a Kripke semantic
for it and prove the soundness and completeness. Finally using this and the
results in section 3 we prove that ${{\sf AR}_{{\sf par}}}\\!\,$ is sound and
complete for both ${{\sf NNIL}({\sf par})}$-admissibility and
${{\downarrow^{\\!\\!{}^{\,}}}{{\sf NNIL}({\sf par})}}$-preservativity, i.e.
${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ iff
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ iff
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mid\\!\approx$}
\put(-0.1,1.3){ ${}$} \put(-0.1,-0.8){ ${{{\downarrow^{\\!\\!{}^{\,}}}{{\sf
N}({\sf par})}}}$} \end{picture}}\ \ \ }B$.

###  4.1 The system ${{\sf AR}_{{\sf par}}}\\!\,$

${{\sf AR}_{{\sf par}}}\\!\,$ is a system which proves propositions in the
form $A\rhd B$, and $A,B\in\mathcal{L}_{0}$. Before we continue with the
axioms and rules of the system ${{\sf AR}_{{\sf par}}}\\!\,$, let us first
define a notation.

$\\{A\\}_{{}_{\\!{\sf par}}}(B):=\begin{cases}B\quad&:B\in{\sf
par}\cup\\{\bot\\}\\\ A\to B&:\text{otherwise}\end{cases}$

Then ${{\sf AR}_{{\sf par}}}\\!\,$ is defined as $[{\sf IPC}]$ (as defined in
section 2.6) plus the following axiom and rule:

  * ${\sf V}^{\sf par}_{\\!\text{{\sf AR}}}:$

$B\to C\rhd\bigvee_{i=1}^{n+m}\\{B\\}_{{}_{\\!{\sf par}}}(E_{i})$, in which
$B=\bigwedge_{i=1}^{n}(E_{i}\to F_{i})$ and $C=\bigvee_{i=n+1}^{n+m}E_{i}$.

$A\rhd B$ ($p\in{\sf par}$)  $\textup{Mont}({\sf par})$ $p\to A\rhd p\to B$

######  Remark .

The system ${\sf AR}$, as defined in [Iemhoff, 2001b, ], is ${{\sf AR}_{{\sf
par}}}\\!\,$ with ${\sf par}=\emptyset$. The Visser rule ${\sf V}^{\sf
par}_{\\!\text{{\sf AR}}}$ in this case is proved to be of central importance
[Iemhoff,, 2005].

######  Remark .

As we will see in section 4.3, the following extension of the Montagna’s rule
is admissible in ${{\sf AR}_{{\sf par}}}\\!\,$:

$A\rhd B$ ($E\in{{\sf NNIL}({\sf par})}$) . $E\to A\rhd E\to B$

######  Remark .

${{\sf AR}_{{\sf par}}}\\!\,$ is closed under general substitutions $\theta$
with $\theta(p)\in\\{\top,\bot\\}\cup{\sf par}$ for every $p\in{\sf par}$,
i.e. ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ implies ${{\sf AR}_{{\sf
par}}}\\!\,\vdash\theta(A)\rhd\theta(B)$.

###### Proof.

Use induction on the complexity of proof ${{\sf AR}_{{\sf par}}}\\!\,\vdash
A\rhd B$. All cases are easy and left to the reader. ∎

The following theorem is from [Iemhoff, 2001b, ].

######  Theorem 4.1.

$A\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!B$ iff ${\sf AR}\vdash
A\rhd B$.

######  Lemma .

${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ implies
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$.

###### Proof.

We use induction on the complexity of the proof ${{\sf AR}_{{\sf
par}}}\\!\,\vdash A\rhd B$. All cases are easy except for the axiom ${\sf
V}^{\sf par}_{\\!\text{{\sf AR}}}$ and the rules ${\textup{Mont}({\sf par})}$
and Disj.

  * •

${\sf V}^{\sf par}_{\\!\text{{\sf AR}}}$: Let $C=\bigwedge_{i=1}^{n}(E_{i}\to
F_{i})$ and $D=\bigvee_{i=n+1}^{n+m}E_{i}$. We show $C\to
D\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \
}\bigvee_{i=1}^{n+m}\\{C\\}_{{}_{\\!{\sf par}}}(E_{i})$. So assume that
$\theta$ is a substitution and $G\in{{\sf NNIL}({\vv{p}})}$ and show that
$\vdash G\to\theta(C)$ implies $\vdash
G\to\theta(\bigvee_{i=1}^{n+m}\\{C\\}_{{}_{\\!{\sf par}}}(E_{i}))$. We reason
by contraposition. Let $\nvdash
G\to\theta(\bigvee_{i=1}^{n+m}\\{C\\}_{{}_{\\!{\sf par}}}(E_{i}))$. Hence for
every $i\leq n+m$ we have $\nvdash\theta(G\to\\{C\\}_{{}_{\\!{\sf
par}}}(E_{i}))$. Then for every $i$ there is some Kripke model
$\mathcal{K}_{i}$ with the root $w_{i}$ such that $\mathcal{K}_{i}\Vdash G$
and $\mathcal{K}_{i}\nVdash\theta({E_{i}})$ and moreover for every $i$ with
$E_{i}\not\in{\sf par}\cup\\{\bot\\}$ we have $\mathcal{K}_{i}\Vdash C$. Since
$G$ is projective, by theorem 3.3 it is extendible. Let $\mathcal{K}$ be a
variant of $\sum(\\{\mathcal{K}_{i}\\}_{i})$ such that $\mathcal{K}\Vdash G$
and $w_{0}$ be its root. Also define $\mathcal{K}^{\prime}$ as follows: for
every $i$ such that $E_{i}\in{\sf par}\cup\\{\bot\\}$, eliminate
$\mathcal{K}_{i}$ (we mean its nodes) from $\mathcal{K}$. Then evidently
$\mathcal{K}^{\prime}$ is a submodel of $\mathcal{K}$. Since $G$ is ${\sf
NNIL}$, by theorem 3.1, we have $\mathcal{K}^{\prime}\Vdash G$. It is enough
to show that $\mathcal{K}^{\prime}\Vdash\theta(C)$ and
$\mathcal{K}^{\prime}\nVdash\theta(D)$. Since for every node $w$ in
$\mathcal{K}^{\prime}$ other than $w_{0}$, we have
$\mathcal{K}^{\prime},w\Vdash\theta(C)$, if we show
$\mathcal{K}^{\prime},w_{0}\nVdash\theta(E_{i})$ for every $i$, we have both
$\mathcal{K}^{\prime}\Vdash\theta(C)$ and
$\mathcal{K}^{\prime}\nVdash\theta(D)$ and we are done. We have two cases. (1)
$E_{i}\in{\sf par}\cup\\{\bot\\}$. In this case we have $\theta(E_{i})=E_{i}$,
and since $\mathcal{K},w_{i}\nVdash E_{i}$ we have $\mathcal{K},w_{0}\nVdash
E_{i}$ and hence $\mathcal{K}^{\prime},w_{0}\nVdash E_{i}$. (2)
$E_{i}\not\in{\sf par}\cup\\{\bot\\}$. Since $w_{i}$ in this case is a node of
$\mathcal{K}^{\prime}$ and $\mathcal{K}^{\prime},w_{i}\nVdash\theta(E_{i})$,
we have $\mathcal{K}^{\prime},w_{0}\nVdash\theta(E_{i})$.

  * •

$\textup{Mont}({\sf par})$: Let
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ and
show $p\to
A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }p\to B$
for every $p\in{\sf par}$. Let $\theta$ be a substitution and $E\in{{\sf
NNIL}({\vv{p}})}$ such that $\vdash E\to\theta(p\to A)$. Hence $\vdash(E\wedge
p)\to\theta(A)$. Then by
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ we have
$\vdash(E\wedge p)\to\theta(B)$ and hence $\vdash E\to\theta(p\to B)$, as
desired.

  * •

Disj: Let
$B\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$ and
$C\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$ and
show $B\vee
C\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$.
Section 3.5 and
$B\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$ and
$C\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$ imply
$B\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }A$ and
$C\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }A$. Let
$E\in{\sf P}{\sf NNIL}({\vv{p}})$ and $\theta$ a substitution such that
$\vdash E\to\theta(B\vee C)$. Since $E$ is ${\sf IPC}$-prime, either we have
$\vdash E\to\theta(B)$ or $\vdash E\to\theta(C)$. In either of the cases, by
$B\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }A$ and
$C\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }A$ we
have $\vdash E\to\theta(A)$. So by this argument we may conclude that $(B\vee
C)\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }A$ and
then by Section 3.5 we have $(B\vee
C)\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }A$. ∎

######  Corollary .

$A\rhd B$ implies
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{\sf PN}({\sf par})}$} \end{picture}}\ \ \ }B$.

###### Proof.

Use sections 4.1 and 3.5. ∎

######  Corollary .

For every $A\in{{\sf NNIL}({\sf par})}$ and $B\in\mathcal{L}_{0}$, if ${{\sf
AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ then $\vdash A\to B$.

###### Proof.

Let ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$. Then by section 4.1, we have
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$. Let
$\theta$ be identity substitution. Then we have $\vdash A\to\theta(A)$. Hence
$\vdash A\to\theta(B)$, which implies $\vdash A\to B$, as desired. ∎

###  4.2 ${{\sf AR}_{{\sf par}}}\\!\,$-models

Before we define ${{\sf AR}_{{\sf par}}}\\!\,$-models, the Kripke models for
which ${{\sf AR}_{{\sf par}}}\\!\,$ is sound and complete, let us present some
definitions. Let $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ is a Kripke model,
possibly infinite or not tree. All over the rest of this subsection we assume
that in general a Kripke model might be infinite or not tree. Given a set
$\Gamma$ of propositions, two nodes $v,w\in W$ are called $\Gamma$-similar,
notation $v\equiv_{\Gamma}w$, if for every $A\in\Gamma$ we have
$\mathcal{K},v\Vdash A$ iff $\mathcal{K},w\Vdash A$. Let $W^{\prime}\subseteq
W$ is a set of nodes and $w\in W$. The notation $w\preccurlyeq W^{\prime}$,
means $w\preccurlyeq w^{\prime}$ for every $w^{\prime}\in W^{\prime}$. We say
that $w\in W$ is a tight predecessor of $W^{\prime}$, if $w\preccurlyeq
W^{\prime}$ and for every $u\succcurlyeq w$, either $u=w$ or $u\succcurlyeq v$
for some $v\in W^{\prime}$. A node $w$ is called a base, if for every finite
set $W^{\prime}\subseteq W$ such that $w\preccurlyeq W^{\prime}$, there is
some $w^{\prime}\in W$ such that: $w\preccurlyeq w^{\prime}\preccurlyeq
W^{\prime}$ and $w\equiv_{\sf par}w^{\prime}$ and $w^{\prime}$ is a tight
predecessor of $W^{\prime}$. And finally, a Kripke model
$\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ is an ${{\sf AR}_{{\sf
par}}}\\!\,$-model if it is rooted (let $w_{0}$ be its root) and there is some
set $W_{b}\subseteq W$ with the following properties:

  * •

$w_{0}\in W_{b}$,

  * •

every $w\in W_{b}$ is a base,

  * •

for every $w^{\prime}\in W_{b}$ and $w\succcurlyeq w^{\prime}$, there is some
$v\in W_{b}$ such that $v\equiv_{\sf par}w$ and $w^{\prime}\preccurlyeq
v\preccurlyeq w$.

Such $W_{b}$ is called a base-set for $\mathcal{K}$.
We say that $\mathcal{K}$ is good, if for every finite set of nodes
$W^{\prime}$, and every $X\subseteq{\sf par}$ such that
$\mathcal{K},W^{\prime}\Vdash X$, there is some $w^{\prime}\in W_{b}$ such
that $w^{\prime}\preccurlyeq W^{\prime}$ and $\mathcal{K}(w^{\prime})\cap{\sf
par}=X$.

######  Remark .

Let $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ is an ${{\sf AR}_{{\sf
par}}}\\!\,$-model with a base-set $W_{b}$, and $w\in W_{b}$. Then
$\mathcal{K}_{w}$ is also an ${{\sf AR}_{{\sf par}}}\\!\,$-model with the
base-set $W^{\prime}_{b}:=\\{v\in W_{b}:v\succcurlyeq w\\}$.

######  Theorem 4.2.

(Soundness) ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ implies
$\mathcal{K}\Vdash B$, for every ${{\sf AR}_{{\sf par}}}\\!\,$-model
$\mathcal{K}$ with $\mathcal{K}\Vdash A$.

###### Proof.

We use induction on the proof ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$. All
cases are trivial except for the axiom ${\sf V}^{\sf par}_{\\!\text{{\sf
AR}}}$ and the rule Mont. First we treat the Montagna’s rule. As induction
hypothesis, let $\mathcal{K}\Vdash A$ implies $\mathcal{K}\Vdash B$, for every
${{\sf AR}_{{\sf par}}}\\!\,$-model $\mathcal{K}$. Also let $\mathcal{K}\Vdash
p\to A$ for some $p\in{\sf par}$ and ${{\sf AR}_{{\sf par}}}\\!\,$-model
$\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ with the base-set $W_{b}$. We will
show $\mathcal{K}\Vdash p\to B$. Let $w\in W$ such that $\mathcal{K},w\Vdash
p$. Since $\mathcal{K}$ is an ${{\sf AR}_{{\sf par}}}\\!\,$-model, there is
some $w^{\prime}\in W_{b}$ such that $w\equiv_{\sf par}w^{\prime}$ and
$w^{\prime}\preccurlyeq w$. Then $\mathcal{K},w^{\prime}\Vdash p$ and hence
$\mathcal{K},w^{\prime}\Vdash A$. Observe that $\mathcal{K}_{w^{\prime}}$ is
also an ${{\sf AR}_{{\sf par}}}\\!\,$-model and
$\mathcal{K}_{w^{\prime}}\Vdash A$. Hence by induction hypothesis
$\mathcal{K}_{w^{\prime}}\Vdash B$, which implies $\mathcal{K},w\Vdash B$, as
desired.
Next we show $\mathcal{K}\Vdash{\sf V}^{\sf par}_{\\!\text{{\sf AR}}}$ for
every ${{\sf AR}_{{\sf par}}}\\!\,$-model
$\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ with the root $w_{0}$. Let
$B=\bigwedge_{i=1}^{n}(E_{i}\to F_{i})$ and $C=\bigvee_{i=n+1}^{n+m}E_{i}$.
Also assume that
$\mathcal{K},w_{0}\nVdash\bigvee_{i=1}^{n+m}\\{B\\}_{{}_{\\!{\sf
par}}}(E_{i})$. We show that $\mathcal{K},w_{0}\nVdash B\to C$. By definition
of $\\{B\\}_{{}_{\\!{\sf par}}}(E_{i})$, for every $E_{i}\in{\sf
par}\cup\\{\bot\\}$, we have $\mathcal{K},w_{0}\nVdash E_{i}$, and for every
$E_{i}\not\in{\sf par}\cup\\{\bot\\}$, there is some $w_{i}\succcurlyeq w_{0}$
such that $\mathcal{K},w_{i}\Vdash B$ and $\mathcal{K},w_{i}\nVdash E_{i}$.
Let $W^{\prime}:=\\{w_{i}:E_{i}\not\in{\sf par}\cup\\{\bot\\}\\}$. There is
some $w^{\prime}\in W_{b}$ which is a tight predecessor of $W^{\prime}$ and
$w^{\prime}\equiv_{\sf par}w_{0}$. We show that $\mathcal{K},w^{\prime}\nVdash
B\to C$ by showing $\mathcal{K},w^{\prime}\Vdash B$ and
$\mathcal{K},w^{\prime}\nVdash C$. Let $E_{i}$ be some disjunct in $C$. If
$E_{i}\in{\sf par}\cup\\{\bot\\}$, then since $w^{\prime}\equiv_{\sf
par}w_{0}$ and $\mathcal{K},w_{0}\nVdash E_{i}$, we have
$\mathcal{K},w^{\prime}\nVdash E_{i}$. Otherwise, since
$\mathcal{K},w_{i}\nVdash E_{i}$ and $w^{\prime}\preccurlyeq w_{i}$, we have
$\mathcal{K},w^{\prime}\nVdash E_{i}$. This finishes showing
$\mathcal{K},w^{\prime}\nVdash C$. Then we show $\mathcal{K},w^{\prime}\Vdash
B$. Let $E_{i}\to F_{i}$ is a conjunct in $B$. Consider some $w\succcurlyeq
w^{\prime}$ such that $\mathcal{K},w\Vdash E_{i}$. Since $w^{\prime}$ is a
tight predecessor of $W^{\prime}$, either we have $w=w^{\prime}$ or
$w\succcurlyeq w_{j}$ for some $w_{j}\in W^{\prime}$. If $w\succcurlyeq
w_{j}$, since $\mathcal{K},w_{j}\Vdash B$, we have $\mathcal{K},w\Vdash B$ and
then $\mathcal{K},w\Vdash E_{i}\to F_{i}$, whence $\mathcal{K},w\Vdash F_{i}$.
Also if $w=w^{\prime}$, then by the following argument, we have
$\mathcal{K},w^{\prime}\nVdash E_{i}$, a contradiction with our first
assumption $\mathcal{K},w\Vdash E_{i}$. Finally, the argument for
$\mathcal{K},w^{\prime}\nVdash E_{i}$: if $E_{i}\in{\sf par}\cup\\{\bot\\}$,
then since $w^{\prime}\equiv_{\sf par}w_{0}$ and $\mathcal{K},w_{0}\nVdash
E_{i}$, we have $\mathcal{K},w^{\prime}\nVdash E_{i}$. Otherwise, since
$\mathcal{K},w_{i}\nVdash E_{i}$ and $w^{\prime}\preccurlyeq w_{i}$, we have
$\mathcal{K},w^{\prime}\nVdash E_{i}$. ∎

We follow the methods in [Iemhoff, 2001b, ] to prove the completeness theorem.
This proof is almost identical to the one for [Iemhoff, 2001b, , proposition
7.2.2]. First some definitions and lemmas. A set $w$ of propositions is ${\sf
IPC}$-saturated if

  * •

$w\vdash A$ implies $A\in w$,

  * •

$\bot\not\in w$,

  * •

$A\vee B\in w$ implies either $A\in w$ or $B\in w$.

Also $w$ is called ${{\sf AR}_{{\sf par}}}\\!\,$-saturated if it is ${\sf
IPC}$-saturated and

  * •

If ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$ and $A\in w$, then $B\in w$.

Let $*(.)$ is a property on sets of propositions. We say that $*(.)$ is an
extendible property if the following conditions hold:

  * •

If $*(w)$ and $w\vdash A$, then $*(w\cup\\{A\\})$.

  * •

If $*(w\cup\\{A\vee B\\})$ then either $*(w\cup\\{A\\})$ or $*(w\cup\\{B\\})$
hold.

If also the following condition holds, we say that $*(.)$ is ${{\sf AR}_{{\sf
par}}}\\!\,$-extendible property.

  * •

If $*(w)$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash w\rhd A$, then
$*(w\cup\\{A\\})$.

In the above expression, ${{\sf AR}_{{\sf par}}}\\!\,\vdash w\rhd A$ is a
shorthand for ${{\sf AR}_{{\sf par}}}\\!\,\vdash(\bigwedge_{i}B_{i})\rhd A$
for some finite set $\\{B_{i}\\}_{i}\subseteq w$.

######  Lemma .

For every extendible property $*(.)$, if $*(w)$ for some set $w$ of
propositions holds, there is some maximal ${\sf IPC}$-saturated
$w^{\prime}\supseteq w$ such that $*(w^{\prime})$. Moreover if $*(.)$ is
${{\sf AR}_{{\sf par}}}\\!\,$-extendible, then $w^{\prime}$ is also ${{\sf
AR}_{{\sf par}}}\\!\,$-saturated.

###### Proof.

Let $A_{1},A_{2},\ldots$ be a list of all propositions such that each
proposition occurs infinitely often. We define a sequence $w=w_{0}\subseteq
w_{1}\subseteq w_{2}\subseteq\ldots$ and then define
$w^{\prime}:=\bigcup_{i}w_{i}$.

$w_{n+1}:=\begin{cases}w_{n}\cup\\{A_{n}\\}\quad&:*(w_{n}\cup\\{A_{n}\\})\\\
w_{n}&:\text{otherwise}\end{cases}$

It can be easily proved that this $w^{\prime}$ satisfies all required
conditions. ∎

######  Corollary .

If ${{\sf AR}_{{\sf par}}}\\!\,\nvdash A\rhd B$, then there is some ${{\sf
AR}_{{\sf par}}}\\!\,$-saturated $w$ such that $A\in w$ and $B\not\in w$.

###### Proof.

Define the property $*(.)$ as follows:

$*(y):{{\sf AR}_{{\sf par}}}\\!\,\nvdash y\rhd B$

Then it is straightforward to observe that $*(.)$ is ${{\sf AR}_{{\sf
par}}}\\!\,$-extendible and $*(\\{A\\})$ holds. Hence section 4.2 implies the
desired result. ∎

######  Theorem 4.3.

(Completeness) ${{\sf AR}_{{\sf par}}}\\!\,$ is complete for good ${{\sf
AR}_{{\sf par}}}\\!\,$-models, i.e. if for every good ${{\sf AR}_{{\sf
par}}}\\!\,$-model $\mathcal{K}$, we have $\mathcal{K}\Vdash A$ implies
$\mathcal{K}\Vdash B$, then ${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$.

###### Proof.

As usual, we reason corapositively. Let ${{\sf AR}_{{\sf par}}}\\!\,\nvdash
A\rhd B$. Define the Kripke model $\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$
as follows. Since ${{\sf AR}_{{\sf par}}}\\!\,\nvdash A\rhd B$, by section 4.2
there is some ${{\sf AR}_{{\sf par}}}\\!\,$-saturated set $w_{0}$ such that
$A\in w_{0}$ and $B\not\in w_{0}$. Then define

$W:=\\{w\supseteq w_{0}:w\text{ is a ${\sf IPC}$-saturated set of
propositions}\\}$

Also define $u\preccurlyeq v$ iff $u\subseteq v$. Finally define
$w\mathrel{V}a$ iff $a\in w$ for atomic $a$. We will show that this model is a
good ${{\sf AR}_{{\sf par}}}\\!\,$-model such that $\mathcal{K}\Vdash A$ and
$\mathcal{K}\nVdash B$. First note that by a standard argument, one may easily
prove by induction on the complexity of $A$ that $A\in w$ iff
$\mathcal{K},w\Vdash A$. Then since $A\in w_{0}$ and $B\not\in w_{0}$, we have
$\mathcal{K}\Vdash A$ and $\mathcal{K}\nVdash B$. So it remains to show that
$\mathcal{K}$ is a good ${{\sf AR}_{{\sf par}}}\\!\,$-model. Let $W_{b}$ as
follows:

$W_{b}:=\\{w\in W:w\text{ is ${{\sf AR}_{{\sf par}}}\\!\,$-saturated}\\}$

We will show that $W_{b}$ is a base-set, i.e. has the following properties:

  * •

$w_{0}\in W_{b}$,

  * •

every $w\in W_{b}$ is a base,

  * •

for every $w^{\prime}\in W_{b}$ and $w\succcurlyeq w^{\prime}$, there is some
$v\in W_{b}$ such that $v\equiv_{\sf par}w$ and $w^{\prime}\preccurlyeq
v\preccurlyeq w$.

The first property is obvious. For the second property we will need ${\sf
V}^{\sf par}_{\\!\text{{\sf AR}}}$ and for the third one we will use Mont’s
rule.
Let $w\in W_{b}$ and $w\preccurlyeq\\{w_{1},\ldots,w_{n}\\}$. We find some
tight predecessor $u$ such that $u\equiv_{\sf par}w$ and $w\preccurlyeq
u\preccurlyeq\\{w_{1},\ldots,w_{n}\\}$. Let $\hat{w}:=\bigcap_{i}w_{i}$ and
define

$\Delta:=\\{E\to F:E\to F\in\hat{w}\text{ and }(E\not\in\hat{w}\vee E\in{\sf
par}\setminus w)\\}$

Define the property $*(.)$ as follows:

$*(y):y\vdash\bigvee_{i}A_{i}\vee\bigvee_{i}p_{i}\text{ and $\forall\,i\
(p_{i}\in{\sf par})$ implies }\exists\,i\ (A_{i}\in\hat{w})\vee\exists\,i\
(p_{i}\in w).$

Note that by letting the second disjunction as empty, from $*(y)$ we have
$y\vdash\bigvee_{i}A_{i}$ implies $\exists\,i\ (A_{i}\in\hat{w})$. Similarly
and by considering the first disjunction as empty disjunction, from $*(y)$ we
get $y\vdash\bigvee_{i}p_{i}$ implies $\exists\,i\ (p_{i}\in w)$. It is not
difficult to observe that $*(.)$ is an extendible property. Then we show
$*(w\cup\Delta)$. Let $w\cup\Delta\vdash\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i}$
and $p_{i}\in{\sf par}$. Then $w\vdash
G\to(\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i})$ in which $G=\bigwedge_{i}(E_{i}\to
F_{i})$ and $E_{i}\to F_{i}\in\Delta$. Since $w\in W_{b}$, and

${{\sf AR}_{{\sf
par}}}\\!\,\vdash\left(G\to(\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i})\right)\rhd\left(\bigvee_{i}\\{G\\}_{{}_{\\!{\sf
par}}}(E_{i})\vee\bigvee_{i}\\{G\\}_{{}_{\\!{\sf
par}}}(C_{i})\vee\bigvee_{i}\\{G\\}_{{}_{\\!{\sf par}}}(p_{i})\right),$

we have $w\vdash\bigvee_{i}\\{G\\}_{{}_{\\!{\sf
par}}}(E_{i})\vee\bigvee_{i}\\{G\\}_{{}_{\\!{\sf
par}}}(C_{i})\vee\bigvee_{i}\\{G\\}_{{}_{\\!{\sf par}}}(p_{i})$. Since $w$ is
${\sf IPC}$-saturated, either $w\vdash\\{G\\}_{{}_{\\!{\sf par}}}(E_{i})$ or
$w\vdash\\{G\\}_{{}_{\\!{\sf par}}}(C_{i})$ or $w\vdash\\{G\\}_{{}_{\\!{\sf
par}}}(p_{i})$, for some $i$. If $w\vdash\\{G\\}_{{}_{\\!{\sf par}}}(E_{i})$,
then $w,\Delta\vdash E_{i}$ and since $w\cup\Delta\subseteq\hat{w}$, we have
$E_{i}\in\hat{w}$, a contradiction. So either we have
$w\vdash\\{G\\}_{{}_{\\!{\sf par}}}(C_{i})$ or $w\vdash\\{G\\}_{{}_{\\!{\sf
par}}}(D)$, in which we have $w,\Delta\vdash C_{i}$ or $w\vdash p_{i}$. Hence
either $C_{i}\in\hat{w}$ or $p_{i}\in w$. This finishes showing
$*(w\cup\Delta)$.
Now let $u\supseteq(w\cup\Delta)$ be a maximal ${\sf IPC}$-saturated set such
that $*(u)$, as provided by section 4.2. Then we show that $u$ satisfies all
required conditions:

  * •

$w\preccurlyeq u\preccurlyeq\\{w_{1},\ldots,w_{n}\\}$. Since $w\subseteq u$,
we have $w\preccurlyeq u$. Also from $*(u)$, we get $u\subseteq\hat{w}$ and
hence for every $i$ we have $u\preccurlyeq w_{i}$.

  * •

$w\equiv_{\sf par}u$. Since $w\subseteq u$, we have $w\cap{\sf par}\subseteq
u\cap{\sf par}$. For the other direction, let $p\in{\sf par}\cap u$. Then
$u\vdash p$ and from $*(u)$ we have $p\in w$.

  * •

$u$ is a tight predecessor of $\\{w_{1},\ldots,w_{n}\\}$. We reason by
contraposition. Let $v\supsetneqq u$ such that for every $i$,
$w_{i}\not\subseteq v$. Then for every $i$ there is some $C_{i}\in
w_{i}\setminus v$ and hence $\bigvee C_{i}\in\hat{w}\setminus v$. On the other
hand, since $u$ is a maximal saturated set with $*(u)$ and $v\supsetneqq u$
and $v$ is ${\sf IPC}$-saturated, we have $\neg*(v)$. Hence
$v\vdash\bigvee_{i}A_{i}\vee\bigvee_{i}p_{i}$ and for every $i$ we have
$p_{i}\in{\sf par}$ and $A_{i}\not\in\hat{w}$ and $p_{i}\not\in w$. From
$v\vdash\bigvee_{i}A_{i}\vee\bigvee_{i}p_{i}$, there is some $E$ such that
either we have $E\in v\setminus\hat{w}$ or $E\in{\sf par}\setminus w$. In
either of the cases, by definition of $\Delta$ we have $E\to\bigvee
C_{i}\in\Delta$. Hence $E\to\bigvee C_{i}\in v$ and then $\bigvee C_{i}\in v$,
a contradiction.

It finishes showing the second property of base-set $W_{b}$. Next we show that
$W_{b}$ satisfies the third condition. Let $w^{\prime}\in W_{b}$ and
$w^{\prime}\preccurlyeq w$. Define the property $*(.)$ as follows.

$*(y):\text{ for every $C$, if }{{\sf AR}_{{\sf par}}}\\!\,\vdash y\rhd
C\text{, then }C\in w.$

We show that $*(.)$ is an ${{\sf AR}_{{\sf par}}}\\!\,$-extendible property
and $*(w^{\prime}\cup w_{\sf par})$, in which $w_{\sf par}:=w\cap{\sf par}$.
First let us show why this finishes the proof. From section 4.2 we get some
${{\sf AR}_{{\sf par}}}\\!\,$-saturated $v\supseteq(w^{\prime}\cup w_{\sf
par})$ such that $*(v)$. Hence by definition $v\in W_{b}$. Since $v\supseteq
w^{\prime}$, we have $w^{\prime}\preccurlyeq v$. Then we show $v\preccurlyeq
w$. Let $C\in v$. From $*(v)$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash v\rhd C$,
we have $C\in w$, as desired. So we have $v\preccurlyeq w$. Finally we show
$v\equiv_{\sf par}w$. We must show $v_{\sf par}=w_{\sf par}$, which holds
because $v\supseteq w_{\sf par}$ and $v\subseteq w$.
So it remains to show that $*(.)$ is an ${{\sf AR}_{{\sf
par}}}\\!\,$-extendible property and $*(w^{\prime}\cup w_{\sf par})$. First we
show that $*(.)$ satisfies all required conditions for ${{\sf AR}_{{\sf
par}}}\\!\,$-extendibility:

  * •

If $*(y)$ and $y\vdash E$. We must show $*(y\cup\\{E\\})$. Let ${{\sf
AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\\}\rhd C$. Hence ${{\sf AR}_{{\sf
par}}}\\!\,\vdash E\wedge\bigwedge_{i}F_{i}\rhd C$ for some finite set
$\\{F_{i}\\}_{i}\subseteq y$. Then since $y\vdash E$, we have ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd E\wedge\bigwedge_{i}F_{i}$. Hence ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd C$. Then from $*(y)$ we have $C\in w$, as desired.

  * •

If neither $*(y\cup\\{E\\})$ nor $*(y\cup\\{F\\})$ hold, then we show that
$*(y\cup\\{E\vee F\\})$ does not hold. Let $C,D$ such that ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\cup\\{E\\}\rhd C$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash
y\cup\\{F\\}\rhd D$ and $C\not\in w$ and $D\not\in w$. Hence by disjunction
rule, we have ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\vee F\\}\rhd C\vee
D$. Since $w$ is ${\sf IPC}$-saturated, we also have $C\vee D\not\in w$. Hence
$*(y\cup\\{E\vee F\\})$ does not hold.

  * •

Let $*(y)$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\rhd E$. We must show that
$*(y\cup\\{E\\})$. Let ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\\}\rhd C$.
Then from ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\rhd E$ we have ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd C$. Then from $*(y)$ we have $C\in w$.

Finally we show that $*(w^{\prime}\cup w_{\sf par})$. Let ${{\sf AR}_{{\sf
par}}}\\!\,\vdash w^{\prime}\cup w_{\sf par}\rhd C$. Hence ${{\sf AR}_{{\sf
par}}}\\!\,\vdash\bigwedge w_{\sf par}\wedge E\rhd C$, for some $E\in
w^{\prime}$. Then by Mont’s rule we have ${{\sf AR}_{{\sf
par}}}\\!\,\vdash\bigwedge w_{\sf par}\to E\rhd\bigwedge w_{\sf par}\to C$.
Since $E\in w^{\prime}$, we have $\bigwedge w_{\sf par}\to E\in w^{\prime}$
and hence by ${{\sf AR}_{{\sf par}}}\\!\,$-saturatedness of $w^{\prime}$ we
have $\bigwedge w_{\sf par}\to C\in w^{\prime}$. Since $w^{\prime}\subseteq
w$, we have $\bigwedge w_{\sf par}\to C\in w$ and hence $C\in w$.
It only remains to show that $\mathcal{K}$ is good. Let $w_{1},\ldots,w_{n}\in
W$ and $\hat{w}:=\bigcap_{i}w_{i}$. Also assume that
$X\subseteq\hat{w}\cap{\sf par}$. We find some $w\in W_{b}$ such that
$w\subseteq\hat{w}$ and $w\cap{\sf par}={X}$. Define

$*(y):\text{For every $C_{i}$ and $p_{i}\in{\sf par}$, if }{{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i}\text{, then
}\exists\,i\ C_{i}\in\hat{w}\vee\exists\,i\ p_{i}\in{X}.$

We show that $*(.)$ is an ${{\sf AR}_{{\sf par}}}\\!\,$-extendible property
and $*({X})$. Then by section 4.2 we have some ${{\sf AR}_{{\sf
par}}}\\!\,$-saturated $w$ such that ${X}\subseteq w$ and $*(w)$ holds. From
$*(w)$ it is clear that $w\subseteq\hat{w}$. Also if $p\in{\sf par}\cap w$,
then by $*(w)$ we have $p\in{X}$ and hence $w^{\prime}\cap{\sf par}={X}$.
Hence $w$ satisfies all required conditions. It remains only to show that
$*(.)$ is ${{\sf AR}_{{\sf par}}}\\!\,$-extendible property and $*({X})$.
First the ${{\sf AR}_{{\sf par}}}\\!\,$-extendibility of $*(.)$:

  * •

If $*(y)$ and $y\vdash E$. We must show $*(y\cup\\{E\\})$. Let
$C=\bigvee_{i}C_{i}\bigvee_{i}p_{i}$ and $p_{i}\in{\sf par}$ and ${{\sf
AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\\}\rhd C$. Hence ${{\sf AR}_{{\sf
par}}}\\!\,\vdash E\wedge\bigwedge_{i}F_{i}\rhd C$ for some finite set
$\\{F_{i}\\}_{i}\subseteq y$. Then since $y\vdash E$, we have ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd E\wedge\bigwedge_{i}F_{i}$. Hence ${{\sf AR}_{{\sf
par}}}\\!\,\vdash y\rhd C$. Then from $*(y)$ we have $C_{i}\in\hat{w}$ or
$p_{i}\in{X}$, for some $i$.

  * •

If neither $*(y\cup\\{E\\})$ nor $*(y\cup\\{F\\})$ hold, then we show that
$*(y\cup\\{E\vee F\\})$ does not hold. Let
$C=\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i}$ and
$D=\bigvee_{i}D_{i}\vee\bigvee_{i}q_{i}$ and $p_{i},q_{i}\in{\sf par}$ such
that ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\\}\rhd C$ and ${{\sf
AR}_{{\sf par}}}\\!\,\vdash y\cup\\{F\\}\rhd D$ and for all $i$ we have
$C_{i},D_{i}\not\in\hat{w}$ and $p_{i},q_{i}\not\in{X}$. Hence by disjunction
rule, we have ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\vee F\\}\rhd C\vee
D$, while for all $i$, $C_{i},D_{i}\not\in\hat{w}$ and
$p_{i},q_{i}\not\in{X}$. Hence $*(y\cup\\{E\vee F\\})$ does not hold.

  * •

Let $*(y)$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\rhd E$. We must show that
$*(y\cup\\{E\\})$. Let $C=\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i}$ and
$p_{i}\in{\sf par}$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\cup\\{E\\}\rhd
C$. Then from ${{\sf AR}_{{\sf par}}}\\!\,\vdash y\rhd E$ we have ${{\sf
AR}_{{\sf par}}}\\!\,\vdash y\rhd C$. Then from $*(y)$ we have
$C_{i}\in\hat{w}$ or $p_{i}\in{X}$ for some $i$.

It finishes showing that $*(.)$ is an ${{\sf AR}_{{\sf par}}}\\!\,$-extendible
property. Then we show $*({X})$. Let $C=\bigvee_{i}C_{i}\vee\bigvee_{i}p_{i}$
and $p_{i}\in{\sf par}$ and ${{\sf AR}_{{\sf par}}}\\!\,\vdash{\sf par}\cap
w\rhd C$. Then by section 4.1 we have ${X}\vdash C$. Since $\bigwedge({X})$ is
extendible, by section 3.5 for some $i$ we have ${X}\vdash C_{i}$ or
${X}\vdash p_{i}$. Since ${X}\subseteq\hat{w}$, for some $i$ either we have
$C_{i}\in\hat{w}$ or $p_{i}\in{X}$, as desired. ∎

###  4.3 ${{\sf NNIL}({\sf par})}$-admissibility

######  Lemma .

For every good ${{\sf AR}_{{\sf par}}}\\!\,$-model $\mathcal{K}$ and
$n\in\mathbb{N}$, there is some ${\sf par}$-extendible stable class of finite
rooted models $\mathscr{K}$ such that for every proposition $A$ with $c(A)\leq
n$ we have $\mathcal{K}\Vdash A$ iff $\mathscr{K}\Vdash A$.

###### Proof.

Given a good ${{\sf AR}_{{\sf par}}}\\!\,$-model
$\mathcal{K}=(W,\preccurlyeq,\mathrel{V})$ with $W_{b}\subseteq W$ as its
base-set, we define a stable ${\sf par}$-extendible class $\mathscr{K}$ of
finite rooted Kripke models as follows. $\mathscr{K}$ includes all Kripke
models
$\mathcal{K}^{\prime}=(W^{\prime},\preccurlyeq^{\prime},\mathrel{V}^{\prime})$
with the following properties:

  * •

$\mathcal{K}^{\prime}$ is finite rooted with tree frame.

  * •

$\mathcal{K}^{\prime}$ is embeddable in $\mathcal{K}$, i.e. there is a
function $f:W^{\prime}\longrightarrow W$ such that
$w^{\prime}\mathrel{V}^{\prime}a$ iff $f(w^{\prime})\mathrel{V}a$; and
$w^{\prime}\preccurlyeq^{\prime}v^{\prime}$ implies $f(w^{\prime})\preccurlyeq
f(v^{\prime})$.

  * •

For all $A$ with $c(A)\leq n$ and for every $w^{\prime}\in W^{\prime}$ we have
$\mathcal{K}^{\prime},w^{\prime}\Vdash A$ iff $\mathcal{K},f(w^{\prime})\Vdash
A$.

Obviously $\mathscr{K}$ is stable and $\mathcal{K}\Vdash A$ implies
$\mathscr{K}\Vdash A$ for every $A$ with $c(A)\leq n$. It remains to show:

  1. 1.

$\mathscr{K}\Vdash A$ implies $\mathcal{K}\Vdash A$ for every $A$ with
$c(A)\leq n$. It is enough to show that for a given $n$ and $w_{0}\in W$,
there is a finite rooted (with the root $w^{\prime}_{0}$) tree-frame Kripke
model
$\mathcal{K}^{\prime}=(W^{\prime},\preccurlyeq^{\prime},\mathrel{V}^{\prime})$
which is embeddable in $\mathcal{K}$ with the embedding $f$ such that
$f(w^{\prime}_{0})=w_{0}$ and for every $w^{\prime}\in W^{\prime}$ and $A$
with $c(A)\leq n$ we have $\mathcal{K}^{\prime},w^{\prime}\Vdash A$ iff
$\mathcal{K},w\Vdash A$. First we inductively define sets $W_{i}$ of sequences
of implications $B\to C$ with $c(B\to C)\leq n$, for $0\leq i\leq n$ and the
function $f$ from $W_{i}$ to $W$. Then let
$W^{\prime}:=\bigcup_{i=0}^{n}W_{i}$. Let $W_{0}:=\\{\langle\rangle\\}$ and
$f(\langle\rangle):=w_{0}$. Assume that we already defined $W_{i}$ and define
$W_{i+1}$ as follows. For every sequence $\sigma\in W_{i}$ and implication
$B\to C$ with $c(B\to C)\leq n$ such that $\mathcal{K},f(\sigma)\nVdash
B\vee(B\to C)$, add the new node $\sigma*\langle B\to C\rangle$ to $W_{i+1}$
and define $f(\sigma*\langle B\to C\rangle)=u$ for some $u$ such that
$u\succcurlyeq f(\sigma)$ and $\mathcal{K},u\Vdash B$ and
$\mathcal{K},u\nVdash C$. This finishes definition of $W_{i}$ and $W^{\prime}$
and the embedding $f:W^{\prime}\longrightarrow W$. Finally define
$\sigma\preccurlyeq^{\prime}\gamma$ iff $\sigma$ is an initial segment of
$\gamma$. Since there are only finitely many inequivalent propositions $A$
with $c(A)\leq n$, one may easily observe that $\mathcal{K}^{\prime}$ is
finite. The other required properties for $\mathcal{K}^{\prime}$ are easy and
left to the reader.

  2. 2.

$\mathscr{K}$ is ${\sf par}$-extendible. Let
$\mathscr{K}^{\prime}:=\\{\mathcal{K}_{1},\ldots,\mathcal{K}_{n}\\}\subseteq\mathscr{K}$
be finite such that $\mathscr{K}^{\prime}$ is a ${\vv{p}}$-submodel of some
$\mathcal{K}_{0}\in\mathscr{K}$ and $w^{\prime}_{i}$ be the root of
$\mathcal{K}_{i}$. Let $f_{i}$ be the embedding of $\mathcal{K}_{i}$ in
$\mathcal{K}$ and $w_{i}:=f_{i}(w^{\prime}_{i})$. Since $\mathcal{K}$ is good,
there is some $u\in W$ such that $u\equiv_{\sf par}w_{0}$ and $u\preccurlyeq
w_{1},\ldots,w_{n}$ and $u\in W_{b}$. Since $u$ is a base, there is some tight
predecessor $v\in W$ for the set $\\{w_{1},\ldots,w_{n}\\}$ such that
$u\equiv_{\sf par}v$ and $u\preccurlyeq v\preccurlyeq w_{1},\ldots,w_{n}$.
Define a ${\vv{p}}$-variant $\mathcal{K}^{\prime\prime}$ of
$\mathcal{K}^{\prime}:=\sum(\mathscr{K}^{\prime},\mathcal{K}_{0})$ in this
way: $\mathcal{K}^{\prime\prime},w^{\prime}_{0}\Vdash a$ iff
$\mathcal{K},v\Vdash a$, for every atomic $a$. Then it is not difficult to
observe that $\mathcal{K}^{\prime\prime}\in\mathscr{K}$.

∎

######  Lemma .

If
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ and
$\mathscr{K}\subseteq\textup{Mod}(A)$ is ${\sf par}$-extendible and stable,
then $\mathscr{K}\Vdash B$.

###### Proof.

Let
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ and
$\mathscr{K}$ is a stable class of finite rooted models with tree frames. Let
$\mathscr{K}^{\prime}$ be the restriction of $\mathscr{K}$ to the atomics
appeared in $A,B,{\sf par}$. Obviously
$\mathscr{K}^{\prime}\subseteq\textup{Mod}(A)$ also is a ${\sf
par}$-extendible stable class. Let $n:=\max\\{c(A),\\#{\sf par}\\}$. Then
section 3.4 implies that $\langle\mathscr{K}^{\prime}\rangle_{n}$ is also a
${\sf par}$-extendible stable class of finite rooted models with tree frames.
Section 3.4 implies $\langle\mathscr{K}^{\prime}\rangle_{n}=\textup{Mod}(C)$
for some $C$ with $c(C)\leq n$. Moreover, by theorem 3.4, there is a
substitution $\theta$ and $C^{\prime}\in{{\sf NNIL}({\sf par})}$ such that
$\vdash C^{\prime}\leftrightarrow\theta(C)$ and $C\vdash
E\leftrightarrow\theta(E)$ for every proposition $E$. On the other hand,
section 3.4 implies $\langle\mathscr{K}^{\prime}\rangle_{n}\Vdash A$. Hence
$A$ is valid in $\textup{Mod}(C)$, which implies $\vdash C\to A$. Hence
$\vdash\theta(C)\to\theta(A)$ and then $\vdash C^{\prime}\to\theta(A)$. From
$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$ infer
$\vdash C^{\prime}\to\theta(B)$, or equivalently $\vdash\theta(C\to B)$. Hence
for every $\mathcal{K}$, and of course for every
$\mathcal{K}\in\langle\mathscr{K}^{\prime}\rangle_{n}$ we have
$\mathcal{K}\Vdash\theta(C\to B)$. Since $\mathcal{K}\Vdash C$ and $\theta$ is
$C$-projective, we have $\mathcal{K}\Vdash C\to B$, and hence
$\mathcal{K}\Vdash B$. So we may deduce
$\mathcal{K}\in\langle\mathscr{K}^{\prime}\rangle_{n}\Vdash B$. Since
$\mathscr{K}^{\prime}\subseteq\mathcal{K}\in\langle\mathscr{K}^{\prime}\rangle_{n}$,
we also have $\mathscr{K}^{\prime}\Vdash B$. Whence $\mathscr{K}\Vdash B$, as
desired. ∎

######  Theorem 4.4.

The following statements are equivalent:

  1. 1.

${{\sf AR}_{{\sf par}}}\\!\,\vdash A\rhd B$.

  2. 2.

$A\mathrel{\mathrel{\begin{picture}(2.0,2.0)\put(0.0,0.0){$\mathrel{\begin{picture}(1.65,1.65)\put(0.0,0.0){\line(0,1){1.65}}
\put(0.0,0.3){{\footnotesize{$\sim$}}} \end{picture}}\\!$} \put(-0.3,1.2){
${}$} \put(-0.3,-0.5){ ${{{\sf N}({\sf par})}}$} \end{picture}}\ \ }B$.

  3. 3.

$B$ is valid in every ${\sf par}$-extendible stable class of Kripke models of
$A$.

  4. 4.

$B$ is valid in every good ${{\sf AR}_{{\sf par}}}\\!\,$-model of $A$.

###### Proof.

$1\to 2$: section 4.1.
$2\to 3$: section 4.3.