%\mag=1200
\documentclass[10pt]{amsart}
\usepackage[cp1251]{inputenc}
\usepackage{amssymb,amscd,amsmath}
%\textwidth=130mm
%\advance\hoffset by -1in
%\advance\voffset by -1in
%\usepackage[cp1251]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amsfonts}
%\usepackage{ljm}


\def\udcs{51.643, 517.11}

\newtheorem{teo}{Theorem}[section]
\newtheorem{lem}{Lemma}
\newtheorem{df}{Definition}
\newtheorem{utv}[teo]{Proposition}
\newtheorem{zam}[teo]{the Remark}

\renewcommand{\theutv}{\arabic {utv}}
\renewcommand{\theteo}{\arabic {teo}}
\renewcommand{\thelem}{\arabic {lem}}
%\renewcommand{\thesled}{\arabic {sled}.}

\newcommand{\gl}{{\lambda}}
\newcommand{\ga}{\alpha}
\newcommand{\gb}{\beta}
\newcommand{\grg}{\gamma}
\newcommand{\gd}{\delta}
\newcommand{\gt}{\theta}
\newcommand{\cb}{{\mathcal B}}
\newcommand{\cc}{{\mathcal C}}
\newcommand{\cf}{{\mathcal F}}
\newcommand{\cm}{{\mathcal M}}
\newcommand{\rc}{{\mathcal R}}
\newcommand{\cg}{{\mathcal G}}
\newcommand{\cl}{{\mathcal L}}
\newcommand{\cy}{{\mathcal Y}}
\newcommand{\ct}{{\mathcal T}}
\newcommand{\ca}{{\mathcal A}}
\newcommand{\cx}{{\mathcal X}}
\newcommand{\cd}{{\mathcal D}}
\newcommand{\cz}{{\mathcal Z}}

%


\def\logo{{\bf\huge S\raisebox{0.2ex}{\hspace{0.55ex}\raisebox{0.05ex}e\hspace{-1.65ex}$\bigcirc$}MR}}

\def\top
     {
  \vbox{
     \noindent\logo
     \hspace{80mm}\raisebox{1ex}{ISSN 1813-3304 }

     \vspace{5mm}

     \begin{center}
     {\huge ��������� \ �����������} \\[2mm]
     {\huge �������������� ��������} \\[2mm]
     {\large Siberian Electronic Mathematical Reports} \\[1mm]
     {\LARGE\tt{http://semr.math.nsc.ru}}\\[0.5mm]
%     {\small �������� ���������� ��. �.�.�������� �� ���}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
     \vspace{-3mm}
     \noindent
     \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} \\
     \hline\hline
     \end{tabular}

     \vspace{1mm}
     {\flushleft\it ��� 16, ���. 144--144 (2019) \hspace{50mm}{\rm\small ��� \udcs}}
     \newline
        % \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}{\rm\small MSC\ \ \mscs }
  }%\vbox
}


\begin{document}

\thispagestyle{empty}


\title{A description of modal logics which enjoy the co-cover property}

\author{ \bf  V.V. Rimatskiy}
\address{Siberian Federal University, Krasnojarsk}
\email{Gemmeny@rambler.ru}

\thanks{\sc V.V. Rimatskiy, Description of modal logics which enjoy  co-cover property}
\thanks{\copyright \ 2021 V.V. Rimatskiy}
\thanks{\rm The paper wa supported by RFBR and KRFN grant (project 18-41-240005)}


\vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\sc Abstract. } Here we use admissible rules to characterize modal logics with weak co-cover property.
We prove that an arbitrary logic $\gl$ over $S4$ satisfies such a property iff all the rules in some family are admissible in $\gl$. \medskip

\noindent{\bf Keywords:}  modal logic, inference rule, Kripke frame and model,
  admissible rule.
 \end{quote}
}



%\maketitle


% {\it Key words: } modal logic, inference rule, Kripke frame and model,  admissible rule, basis of  admissible rules.


\section{Introduction}
In modern applications of logic in Computer Science and Artificial Intelligence, one often needs languages capable of representing some knowledge about dynamic systems.
Various non-standard logics (e.g. modal and temporal logics, logic for multi-agent
reasoning) are efficiently used for these applications.
They describe statements by some formulas specific to considered models in general and do not take into consideration variable conditions and changing assumptions.
These conditions and assumptions can be modelled
by distinct variations of the notion of logical consequence.
The problem of such an adequate modeling
is one of the most important problems originated in mathematical logic and mathematics in general.
The most important component of our approach consists of the fact that we study logical consequence in terms of inference rules and clauses, not only of formulas or statements.
The formalism concerning the description of properties by formulas is well--developed, widely spreaded, and well represented in scientific literature.
It is a basis for representing human reasoning.
But formulas describe only stable, static events only;
statements only fix the facts and they are unable to handle changing conditions.

Therefore, the study of (structural) inference rules (or sequents), i.e. expressions which have premises (collections of assumptions) and conclusions,
brings us more flexibility and more expressive power to model
the human reasoning and computing.
Premises give us the current information in the form of assumptions and conclusions representing the knowledge, i.e. the facts which we can obtain from our assumptions.
The study of reasoning (as a part of AI) again requires the understanding of what are consistent
consequences of observable facts.
Within Computer Science, these aspects are
involved in the analysis of correct instructions for %a carrying out
computations, verification of programs, and many other areas. Such rules enable us to study a standard series of questions in the study of logical consequence: what can be obtained from certain given assumptions?


Evidently, the notion of inference rule generalizes the notion of formula, because any formula can be viewed as a structural inference rule without premise and assumption.
But admissible inference rules are actually
stronger then the clauses.
It follows from Harrop's paper \cite{Har} (1960), that even
the intuitionistic logic $H$ is not structurally complete: it has
admissible inference rules which cannot be represented by formulas, which are not inferred.
The same is valid for a broad range of basic modal logics
(see the examples of G. Mints \cite{Min} and J. Port \cite{Port}).

The notion of admissible inference rule goes back to Lorenzen (\cite{Lor}, 1955).
For an arbitrary logic, the admissible rules are exactly those rules under which this logic is closed.
Clearly, any derivable rule is admissible, but generally not vice versa.
Also, directly from the definition we see that the
set of all rules admissible in a logic $\gl$ is the {\em greatest class} of
inference rules by which we can extend an axiomatic system of the logic $\gl$
preserving the theorems of $\gl$.
Derivable rules may replace some fragments of
fixed length in derivations, thereby linearly shortening them. Admissible
rules which are not derivable basically may reduce derivations even more drastically.

The history of the study of admissible rules
could be started since H. Fridman's question (\cite{Frid}, 1975) about the existence of an algorithm which could distinguish rules admissible in intuitionistic logic $H$. In the middle of 70-th G. Mints \cite{Min} found
the strong sufficient conditions for derivability in $H$ of admissible rules in special form.
The Fridman's question about the existence of an algorithm
recognizing admissibility of inference rules was answered affirmatively by
V. Rybakov (1984, cf. \cite{Ryb84}) for the intuitionistic logic $H$ and a broad
class of modal logics (e.g. $K4,\ S4,\ GL$, cf. \cite{Rb}).
%Later on S.Gilardi \cite{Ghil} found an another  solution for the intuitionistic logic $H$.

%\bigskip

In 2000-2010 a few results on describing of explicit bases for admissible inference rules for nonstandard logics (S4, K4, H etc.)  appeared (see for example \cite{Rexp}).  The key condition in these results was the weak co-cover property. We hope that the weak co-cover property, the disjunction property, and FMP enable us to describe such a basis.
In addition to the improvement of deductive power in logic,  admissible rules are able to describe some semantic properties of a given logic.
One of the first attempts was the description of intuitionistic logic $H$ by the set of admissible inference rules (cf. R. Iemhoff \cite{Iem1}). That is why this property is in the focus of this article.
Here we use admissible rules to characterize modal logics with weak co-cover property.
We prove that an arbitrary logic $\gl$ over $S4$ with finite model property satisfies such a property iff all the rules in some family are admissible in $\gl$.

\section{Notations, preliminary Facts}
We assume the reader to be aware of the algebraic and Kripke semantics for
modal logics and to have some initial knowledge concerning
the basic facts on inference rules and their admissibility (anyway, we
briefly recall all the necessary facts below).
As a good entry point to the subject
%taking  as a whole
we would recommend among modern literature the monograph by Rybakov \cite{Rb}
for a general techniques as well as for advanced techniques
concerning modal logics and inference rules.
According to modern trends, by a
{\em logic} we mean the set of all theorems provable in a given axiomatic
system or the set of valid formulas for some class of Kripke frames.
In particular, a normal modal logic $\gl$ is a set of modal formulas
which is closed under substitution, modus ponens, and necessitation rule $A\ / \
\Box A$ and including all the theorems of the minimal propositional modal logic $K$.
In the following definitions and results we deal with algebraic propositional
logics extending logic $S4$ with finite model property by a modal logic (cf. \cite{Rb}).


{\it A frame} \  ${\mathcal F}:= \langle F,R \rangle$  is a pair,\, where $F$ is
a nonempty set and $R$ is a binary relation on  $F$.
For simplicity, the basis set of a frame and a frame itself are  often denoted by the same letter.
Further on we consider only frames in which $R$ is transitive
and reflexive.

% Let $P$ de a collecion of the propo
 {\it A model }  is a triple $ \mathcal M = \langle W,\ R,\ V \rangle $, where ${\mathcal F}:= \langle F,R \rangle$ is a frame and $V$ is a valuation of a set of propositional letters $P$ in the frame $\cf$,  that is  $V : P \to 2^W$. The set $Dom (V) = P$ is called the domain of $V$.


A frame ${\cf} = \langle F,\, R \rangle $ is called an open subframe of the frame $ {\cg} = \langle G, \, R \rangle$ (we denote this fact as ${\cf} \sqsubseteq {\cg}$) if $ F \subseteq G$ and $ \forall a \in F \, \forall b \in G \, (aRb \Longrightarrow b \in F)$ holds. If $ \mathcal M_1 = \langle W_1,\ R_1,\ V_1 \rangle $,\
$ \mathcal M_2 = \langle W_2,\ R_2,\ V_2 \rangle $ are models then we call $\mathcal M_1$ an open submodel of $\mathcal M_2$ (and denote this fact as ${\cm}_1 \sqsubseteq {\cm}_2$) if : 1)\ $\langle W_1,\ R_1 \rangle $ is open subframe of $\langle W_2,\ R_2 \rangle$ ; 2)\ $Dom (V_1) = Dom (V_2) $ and $ \forall p \in Dom (V_1)\ V_1(p) = V_2(p) \cap W_1 .$

A mapping $f : \langle F,\, R \rangle \to \langle G, \, S \rangle $  is a called p-morphism if 1) $ aRb \Longrightarrow f(a) S f(b)$;\ 2) $ f(x)Sz \Longrightarrow \exists y \in F : f(y) = z \, \& \, xRy$.

We say that a mapping $f : \mathcal M_1 = \langle W_1,\ R_1,\ V_1 \rangle \to \mathcal M_2 = \langle W_2,\ R_2,\ V_2 \rangle $ is  a p-morfism of the model $\cm_1$ into the $\cm_2$ if 1)\ $f$ is a p-morfism of the frame $ \mathcal F_1 = \langle W_1,\ R_1\rangle $ into the frame $ \mathcal F_2 = \langle W_2,\ R_2 \rangle $ ; 2)\ the valuations $V_1,\ V_2$ are defined on the same set of propositional letters;\ 3)\
 $ \forall \, p \in Dom (V_1) , \forall a \in W_1 ( a \models_{V_1} p \iff f(a) \models_{V_2} p) $.


 The property of primary importance of open submodels and p-morfisms consists of the fact that they preserve the truth of formulas:
 \begin{utv} (cf. \cite{Rb})
 1)\ If $\cm_1$ is an open submodel of a model $\cm_2$ then for every formula $\alpha $,\
 $ \cm_2 \models \ga $ implies $ \cm_1 \models \ga $  ;

 2)\ if $f$ is a p-morfism of the model $\mathcal M_1 = \langle W_1,\ R_1,\ V_1 \rangle$ onto onto model $\mathcal M_2 = \langle W_2,\ R_2,\ V_2 \rangle $ then for any formula $\ga$ which is built from letters from the domain $Dom (V_1)$ holds $\forall a \in W_1 (a \models_{V_1} \ga \iff f(a) \models_{V_2} \ga ) $.
 \end{utv}

Let $\mathcal F_i = \langle W_i,\ R_i \rangle ,\ i \in I  $  be a family of pairwise disjoint frames, i.e. $ W_i \cap W_j = \emptyset $ for $ i \ne j \in I$. The disjoin union of this family is the frame $\sqcup_{i \in I} \cf_i =\langle W,\ R \rangle    $, where $W = \cup_{i \in I} W_i,\ R = \cup_{i \in I} R_i$.
  Disjoint union of models is defined similarly.

  By Lemma 2.5.26 \cite{Rb}, disjoint unions of frames (or models) preserve the truth of formulas:
 $\sqcup_{i \in I} \cf_i \models \ga \ \iff \ \forall i (\cf_i \models \ga)$. The disjoint union of $\gl$-frames is a $\gl$-frame.



Any subset $C$  of a frame  $F$ which is either a single irreflexive point or satisfies the properties
(1) \ $\forall \, x, y \in C (xRy \, \& \, yRx)$ and  (2) $ \forall x \in C \forall y \in W (xRy \, \& \, yRx \Longrightarrow y \in C) $
%which consists of all mutually R--comparable elements of $F$
is called a {\it cluster of the frame $ F$}. A cluster is
{\it proper } if \, $|C| > 1$, otherwise this cluster is called %to be
degenerated or singleton. For any element $a \in F$, a cluster generated  by
$a$ is  denoted by $C(a)$. Any  set of clusters of $F$ which are non-comparable
by $R$ is called an antichain. The antichain $\ca$ is nontrivial if it
consists  at least of  two clusters; otherwise we call it trivial.

We call the  maximal number of clusters in chains of clusters generated by
an element (or a cluster) the {\it depth of an element  (or  of a cluster)}.
% in the frame (or the model) W}.
For any transitive frame \, $F $ (or a transitive Kripke model  $M$), its
{\it $n$-slice} \, $ S_n(F)\  (S_n(M))$ is  the set of all elements of depth
$n$ from $F \, (M$ respectively).\ And $S_{ \le n}(F)$ \, is the set of all
elements  from $F$  with depth at most $n$.

We  say that a frame $F$ is a $\gl$--frame for a logic $\gl$ if all the theorems
of  $\gl$ are valid at $F$.
And we call $\gl (F)$  --- the set of all formulas valid
in $F$ --- the logic generated  by $F$.
A frame $F$ is rooted if there exists an $a \in F$ such that for all $b \in F$ holds $a Rb$. We call $C(a)$ the root of $F$.

We put  \  $b^R := \{x | \exists y \in C(b) : yRx \} \cup C(b);\
b^{<R} := \{x | \exists y \in C(b) : yRx \wedge \lnot xRy \}$,\, where \,
$C(b)$ is a cluster of a frame $F$ containing the element $b$.
For any subset $X  \subseteq F$ \,  we let $X^R$ \ to be \,  $\cup \{ x^R | x \in X \}$.
That is, the subframe  $b^R$ of $F$ is the upper cone generated by $b$,\ and
$X^{R}$ is the subframe of $F$ generated by $X$ respectively.
An element \, $ b \in F $ or cluster $C(b)$  \, is said to be {\it a co-cover } for
a set  $ X \subseteq F$   if \, $b^R  \backslash C(b) = X^R$.
We understand a cluster $C$ as a $\gl$-co-cover for $X$
%As $\gl$-co-cover for $X$ we understand %degenerated  a cluster $C$,
 if it generates the $\gl$-frame  $C^R := X^R \cup \{C\}$ as a root.
 We will identify a one-element cluster $C(a)$ and a reflexive element $a$ (generating this cluster) as the co-cover, since they have the same set of R-accessible elements.


A subset $\cx$ of a given model $\cm$ is definable if there is a formula
$\ga$ such  $ \forall \, x \in \cm \, [\, x \in \cx \Longleftrightarrow  x  \models_V
\ga]$. And a valuation $V$ is definable in a model $\cm$ if for any letter $p$,
the set $V(p)$ is definable.

Let $\ga_1, ... ,\ga_n, \gb$ to be some  formulas. We understand the figure $r$,
where
$$ r:=  \frac{\ga_1(x_1,\dots,x_n), ..., \ga_n (x_1,\dots,x_n)}{\gb
(x_1,\dots,x_n) }, $$
as the (structural) inference rule which derives $s(\gb)$ from
$s(\ga_1), ... , s(\ga_n)$ for every substitution $s$.
We say $r$ is {\it derivable} in a logic $\gl$ if there is a derivation $\gb$
in $\gl$ from the set of assumptions $\{ \ga_1, ... , \ga_n\}$.

An {\it inference rule} \
$ r = \{ \alpha_1(x_1,\dots,x_n),\dots,\alpha_k(x_1,\dots,x_n) /
\beta(x_1,\dots,x_n) \} $   is called  {\it admissible in a logic}  $\lambda$,
if for any formulas  $\delta_1,\dots,\delta_n$  holds
$$((\alpha_1(\delta_1,\dots,\delta_n) \in  \lambda) \cdots
 (\alpha_k(\delta_1,\dots,\delta_n) \in  \lambda)
 \ \Longrightarrow \ \beta(\delta_1,\dots,\delta_n) \in \lambda).$$


Admissible inference rules have the following algebraic description:

\begin{utv} \cite{Rb} \label{u1} \quad
An  inference rule
$ r=\{ \alpha_1 , \dots, \alpha_k / \beta \}$
is admissible in a logic $\lambda$ iff the quasi-identity
$r^*=\{ \alpha_1 =1 \ \&  \dots \& \ \alpha_k = 1  \Longrightarrow
\beta =1 \}$
is true on free algebra of countable rank \, ${\mathcal F}_w(\lambda)$\, from
the  variety \, Var$ (\lambda)$ generated by  \, $\lambda$.
\end{utv}

 Any derivable rule is admissible but the converse is not always true.
Also directly from the definition we see that the set of all rules
admissible in a logic $\gl$ is the {\em greatest} class of inference rules
by which we can extend axiomatic system of the logic $\gl$ preserving
the set of theorems of $\gl$. Derivable rules may replace some fragments of fixed
length in derivations, thereby shortening them linearly. Admissible rules
which are not derivable in principle may reduce derivations even
more drastically.

For a given frame $\cf$, valuation $V$, and inference rule $r:=\ga_1,...,\ga_n/\gb$, we
say that {\it $r$ is valid on $\cf$ with respect to  $V$} and write $\cf\models_V r$ if as soon as
$\forall x\in \cf$ and $ \forall i $ $ (x\models_V\ga_i)$ holds, we have
$\forall x\in \cf (x\models_V\gb)$. A rule {\it $r$ is valid on a  frame $\cf$}
if $r$ is valid at $\cf$ under any valuation; we write then $\cf\models r$.

%Given a propositional logic $\gl$,  a rule $r:=\ga_1, ... ,\ga_n /\gb$ is a {\em consequence of a family of rules $\mathcal R$ in $\gl$} (the denotation ${\mathcal R} \vdash_{\gl} r$) if there is a derivation of $\gb$ from $\ga_1, ... ,\ga_n$ as assumptions in the axiomatic system of $\gl$ extended by adding $\mathcal R$ as new rules. A set $ Ad^*(\lambda)$ of admissible rules of logic  $\lambda$ is called {\it the basis of admissible inference rules},\, iff any  admissible inference rule \, $r$\, is derivable from \ $ Ad^*(\lambda)$ \ in~ $\lambda$.

%\begin{utv} \label{u2} \quad
%$r_1,\dots,r_k$ is a  basis of admissible inference rules   in \ $\lambda$ iff \, $r_1^*,\dots,r_k^*$ \ is a basis of quasi-identities of \, ${\mathcal F}_w(\lambda)$.
%\end{utv}

We say that a logic $\lambda$ has finite model property (FMP for short) if for any  $\alpha \not\in \lambda $ there exists a  finite $\lambda$-model refuting $\alpha$.

A Kripke Model  \ $\langle F, R, V \rangle$,  where \, $V:\, P_n
\rightarrow 2^{F} $ ,\   $P_n =\{ p_1,p_2 ,\dots,p_n \}$, is {\it
$n$- characteristic for a logic $\lambda$} \, iff \, for any formula
$\alpha$ which is  built from $ p_1,\dots, p_n$ holds $\alpha \in \lambda$
 \,  iff \, $\langle F,R,V \rangle \models \alpha$.\

The admissibility of inference rules in modal logic $\gl$ over $S4$ can be
described via their validness in certain special $n$-characteristic Kripke
models.
The descrip\-tion of such models $Ch_n ({\gl}) $ and criteria for
recognizing admissibility in ${\gl}$ by means of them can be found, for instance, \cite{Rb}.
As we will esseentially use these techniques in the
sequel, we briefly recall  the construction of $Ch_n ({\gl}) $ for FMP logic $\gl$ over $S4$ and the semantic criterion for recognizing admissibility.

Given a FMP logic $\gl$ over $S4$ and a set $P_n:=\{p_1,...,p_n\}$ of propositional letters, we construct
the first slice $S_1(Ch_n ({\gl})) $ as follows.
It consists of the collection
of all  clusters with all possible valuations $V$ of letters from $P_n$ which have no doubling (elements in the same cluster with the same valuation and  clusters which
are isomorphic as Kripke models). 

Assume that $S_{\le m} (Ch_{n} ({\gl}))$ is already defined.
We define $S_{m+1}(Ch_{n }(\gl))$ as follows. We take an arbitrary
antichain $\cx$ of clusters from  $S_{\le m} (Ch_{n}({\gl}))$ having at least
one cluster of depth $m$  and put all clusters $C$
from $S_1(Ch_n ({\gl}) )$ into $S_{m+1}(Ch_n ({\gl}) )$, where $C$ is
an immediate predecessor for all elements from $\cx$ (co-cover for $\cx$),
such that
\begin{itemize}
\item[(i)] $C^R = \cx^R \cup C $ is a $\gl$--frame      and
\item[(ii)] if $\cx:=\{C_1 \}$ then  $C$ is not a Kripke submodel of $C_1$.
\end{itemize}
Iterating this procedure we obtain a model
$Ch_n ({\gl}) $ as a result.
Recall that a model $\cm$
is $n$-characteristic for a logic $\gl$
if for any formula $\ga$ which is built from letters from $P_n$ holds
$\ga\in \gl$ iff $\cm \models \ga$.
We need the following facts:

\begin{teo} \label{thm1} (cf. \cite{Rb})
For any FMP logic $\gl$ over $S4$
the model $Ch_n ({\gl}) $ is $n$-characteristic for  ${\gl}$.
\end{teo}

\begin{teo} \label{thm3} (cf. \cite{Rb})
For any inference rule $r$, $r$ is admissible in FMP logic $\gl$ over $S4$ iff $r$ is valid
in the frame of $Ch_n ({\gl}) $ with respect to any definable valuation for any given $n$.
\end{teo}

%\bigskip
%\newpage

\section{ Main results  }


We say that a logic $\gl$, extending logic  $S4$,  has {\it  weak co-cover
property} (WCP for short) whenever for every finite rooted $\gl$-frame
$\cf$  and an arbitrary nontrivial antichain $\cx$  of clusters from
$\cf$, the frame $\cf_1$   which is result of adjoining a
singleton reflexive co-covering as the root to the frame
$ \bigcup_{c \in  {\cx}^R }  c^R$ is  a   $\gl$-frame as well.

Given $n  \in N$ with $n > 1 $, define the formulas:

 $$ \pi_i := p_i \wedge \bigwedge_{j \ne i} \neg %\Diamond ???????
 p_j; \ 1 \le i, j \le n, \quad
  A_n := \bigwedge\limits_{1 \le i \le n} \Diamond \pi_i;     $$
  $$A_{n,1} := \Box \big[ \bigwedge\limits_{1 \le i \le n} (p_i  \rightarrow \neg \Diamond q) \big]; \quad  B :=  q \vee \neg \Diamond q.$$

Also we define  the  rules:
 $$ {\rc}_{n} := \frac{ \Box \big( A_{n,1} \wedge \neg (A_n \wedge B )
\big) }{\Box \neg A_n}; \ n= 2,3,\dots $$


Note that these rules are special case of those from \cite{Rexp} which  gives an explicit basis for admissible rules of logic S4.  Next theorem is almost the same as the statement of Lemma 3.1 \cite{Rexp}. The WCP of logic is a key condition in the proof of this statement. Let us reproduce the common part of that proof.


 \begin{teo}   \label{t1}
 The rules ${\rc}_{n}, \ n > 1 $, are admissible in every FMP logic $\gl$ over $S4$ that enjoys the weak co-cover property.
  \end{teo}
  { \it Proof }
  Assume that the statement is false.
  Suppose that for some $n$ the rule
$$ {\rc}_{n} := \frac{ \Box \big( A_{n,1} \wedge \neg (A_n \wedge B )
\big) }{\Box \neg A_n} $$
is not admissible in $\gl$.
Hence there is a definable valuation
$V$ of variables from ${\rc}_{n}$ in some constructive $k$--characteristic
model $Ch_{\gl } (k)$.
Therefore
$$ Ch_{\gl } (k) \models_V \Box \big( A_{n,1} \wedge \neg (A_n \wedge B)
\big) \ \& \  Ch_{\gl } (k) \not\models_V \Box \neg A_n. \hfil \eqno({1}) $$

Consequently, there exists an element $a \in Ch_{\gl } (k)$ such that $a \not\models_V \Box \neg A_n$. Then there are elements $ b_1, \dots , b_n \in  Ch_{\gl } (k)$ such that
$ a R b_i \ \& \ b_i \models_V p_i$.
 Note that, if all the elements $ b_1, \dots , b_n \in  Ch_{\gl } (k)$ belong to the same cluster (say $C(b_1)$  for example) then $b_1 \models_V A_{n}$ holds and by ${(1)}$ we have $b_1 \models_V  A_{n,1}$.
 Therefore $  b_1 \models_V  \neg \Diamond q$, e.g. we obtain  $b_1 \models_V  A_{n} \wedge  B$ which contradicts the statement
$b_1 \models_V  \Box \neg  (A_{n} \wedge  B)$  by the assumption~${(1)}$. So, the elements $ b_1, \dots , b_n \in  Ch_{\gl } (k)$ generate a nontrivial antichain.


By the weak co-cover property,  there exists a
reflexive element $b \in Ch_{\gl } (k)$ which is a co-cover for the set of R-minimal clusters from the set
$ \{ C(b_1), \dots, C(b_n) \}$, that is
 $$ \{ b \}^R := \{b \} \cup \bigcup\limits_{1 \le i \le n } (b_i)^R.$$
 It follows from ${(1)}$ that $b \models_V  A_{n,1}$ and $b \models_V
A_{n}$. Since $b$ is a co-cover for   $ \{ b_1, \dots, b_n \}$, it is clear that $b \models_V  B$. Indeed $b_i \models_V  p_i$ and $b \models_V  A_{n,1}$ holds, therefore $ \forall i \le n \ b_i \models_V  \neg \Diamond q$. From this we conclude that $b \models_V q$ or $b \models_V \neg q$ and hence $b \models_V \neg \Diamond q$.
Therefore we obtain  $b \models_V  A_{n} \wedge  B$ which contradicts the statement
$b \models_V  \Box \neg  (A_{n} \wedge  B)$  by the assumption
${(1)}$. ~\hfill~$\blacksquare$




\medskip

\begin{teo}  \label{t2}
If for all $n$ the rules $\{ {\rc}_{n},  n > 1 \} $ are admissible in FMP logic $\gl$, over $S4$ then the logic $\gl$ enjoys the weak co-cover property.
\end{teo}
{ \it Proof.}  Suppose all the rules  ${\rc}_{n}, \ n >1,n \in N, $ to be admissible in FMP logic $\gl$ over $S4$, but $\gl$ doesn't enjoy the weak co-cover property.
By definition, there exists a {\it finite} rooted $\gl$-frame $G = b^R$ and a nontrivial antichain of clusters ${\cx} \subset G$ such that the frame $\varepsilon^R :=  \bigcup_{c \in  {\cx}^R }  c^R \cup \{ \varepsilon \}$ obtained by adjoining a singleton reflexive co-cover $\varepsilon$ as a root to the frame $ \bigcup_{c \in  {\cx}^R }  c^R$ is not a $\gl$-frame. Fix this nontrivial antichain of clusters ${\cx} \subset G$.  We will prove that in such a case at least one rule ${\rc}_{n}$ is not admissible in the logic $\gl$. To do this, we construct a $\gl$-frame $\mathcal  M$ containing the frame $G$ as an open subframe and refuting ${\rc}_{n},  \ n >1,$ under some valuation. Then we define a p-morphism from the frame of $k$-characteristic model $Ch_k({\gl})$ for some $k$ on $\mathcal  M$.  Transferring this valuation from $\mathcal  M $ onto  $Ch_k({\gl})$, we refute this rule ${\rc}_{n},  \ n >1,$ on $Ch_k({\gl})$ under some valuation, which contradicts the admissibility of $\rc_n$.


%-------------------------------------------------------------------------------------------


Let us take a frame $G\sqcup \{ e \} $ where $\{ e \}$ is a reflexive singleton which is not R-comparable to any element in $G$.
The frame $\{ e \}$ is a $\gl$-frame as a p-morfic image of $G$.
So the frame $G\sqcup \{ e \} $ is a $\gl$-frame as a disjoint union of $\gl$-frames.

We define the $\gl$-successor ${ \mathcal  M}$ of $G\sqcup \{ e \} $   as follows.
Fix a nontrivial antichain $\cx$ from $G$ and define a $\gl$-frame $ { \mathcal  M}_0 = G \sqcup \{ e \}$.
% Let's define $S_{1 } ({ \mathcal  M})  = S_{1 } ({G \sqcup \{ e \}})  $.
 Then we choose all nontrivial antichains of clusters $\{ X_t \subseteq S_{1 } ({ \mathcal  M}_0) \}$ which don't have singleton co-cover in ${ \mathcal  M}_0$ and add such co-cover $t$ whenever it generates a $\gl$-frame $t^R= \{ t \} \cup X_t^R $ as a root. So we obtain  $ { \mathcal  M}_1$. Notice that by the construction $ { \mathcal  M}_1$ is a $\gl$-frame (we add elements generating $\gl$-frame as a root to $\gl$-frame $G\sqcup \{ e \} $) and $G \sqsubseteq  {G \sqcup \{ e \}} \sqsubseteq { \mathcal  M}_1$ as we add new elements as co-covers to  $G\sqcup \{ e \} $.


Assuming that ${ \mathcal  M}_{k }$ has already been constructed and $ {G \sqcup \{ e \}} \sqsubseteq { \mathcal  M}_k$, we obtain ${ \mathcal  M}_{k+1} $ %of depth $k+1$
as follows:
 we choose in $S_{\le (k +1) } ({ \mathcal  M}_k)$ all nontrivial antichains $\{ X_t \subseteq S_{\le (k+1) } ({ \mathcal  M}_{k}) \}$ which don't have singleton co-cover
 %in $G \sqcup \{ e \} \cup S_{\le k } ({ \mathcal  M})$
 and have at least one cluster of depth $k+1$. Then we add singleton reflexive element $t$ as co-cover to each chosen antichain whenever it generates the $\gl$-frame $t^R= \{ t \} \cup X_t^R $ as a root.
 Note that by construction $ { \mathcal  M}_{k+1}$ is $\gl$-frame and $ {G \sqcup \{ e \}} \sqsubseteq { \mathcal  M}_{k+1}$ as we add new elements as $\gl$-co-covers to ${ \mathcal  M}_{k }$ and
 $ {G \sqcup \{ e \}} \sqsubseteq { \mathcal  M}_k$.

  Continuing this process we obtain the $\gl$-successor ${ \mathcal  M}= \cup_{k \in N} { \mathcal  M}_k$ of $G\sqcup \{ e \} $. This frame is potentially infinite.



It follows from the construction that the frame ${ \mathcal  M}$ has the following properties:

\begin{itemize}
\item  first slice $S_1 ({ \mathcal  M})$ of  ${ \mathcal  M}$  contains at least one singleton cluster $C(e)=\{ e \} $;

\item the fixed antichain ${\cx} \subset G$ does not have co-cover in ${ \mathcal  M}$ as on each step of construction we adjoin only a co-cover generating $\gl$-frame as a root;


\item the frame $G$ is an open subframe of ${ \mathcal  M}$;

\item every nontrivial antichain of clusters of ${ \mathcal  M}$ (different from $\cx$) has  singleton $\gl$-co-cover in ${ \mathcal  M}$ (whenever it generates a $\gl$-frame as a root).

\end{itemize}

\begin{utv} $ { \mathcal  M} \not\models_V {\rc}_{n}$ holds for some $n$ and a valuation $V$.
\end{utv}
{ \it Proof.} We define a valuation $V$ on ${ \mathcal  M}$ as follows. Suppose that the fixed antichain ${\cx} \subset b^R$ consists of clusters $  \{ C_1,\ C_2,\ \dots, C_n\}$.
% and
%the clusters $K_1, \dots, K_t \in {{ \mathcal  M} \setminus {\cx}^R}$ are immediate R-predecessor for same nonempty subsets from $A_i \subset {\cx}^R$ and same (possible empty) set $Y \subset {{ \mathcal  M} \setminus {\cx}^R} $  , e.g.\,  $$ \forall \, K_i \exists\, A_i \subset {\cx}^R \& Y_i \subset {{ \mathcal  M} \setminus {\cx}^R} \, : K_i^R = \{ K_i \} \cup A_i^R \cup Y_i^R \ \& \ K_i \not\in {\cx}^R .$$
%
% By the choice of antichain ${\cx}$ and clusters $K_i$, any $K_i$ is not   co-cover for ${\cx}$.

 Now we define
 ${\cx}^{-R} = \{x \ : \ xRC_1 \& xRC_2 \& \dots xRC_n \}$ and
 $$V(q) := \{y \in {\cm} \setminus {\cx}^R : y \not\in {\cx}^{-R} \ \& \exists x \in {\cx}^{-R} (xRy)\},\
 %S_1 ( {{ \mathcal  M}} \setminus {\cx}^R) \cup \{ K_1, \dots, K_t \};\
  V(p_i) := C_i ,$$ e.g. $ \forall x \in C_i \ x \models_V p_i $. Let us prove that the premise of ${\rc}_{n}$ is valued on ${ \mathcal  M}$ under $V$ while the conclusion is not.


\medskip

By definition of $V$ we obtain:
$$  \forall x \in {\cx}^R \ x \models_V \neg \Diamond q; \quad \forall x \in {{ \mathcal  M}}\ x \models_V p_i \iff x \in C_i.$$
 % \forall e \in {{ \mathcal  M}} \setminus  {\cx}^R  \ e \models_V \Diamond q;\
 If some element $ z \in {{ \mathcal  M}}$ $R$-sees the fixed antichain $ {\cx} = \{ C_1,\ C_2,\ \dots, C_n\}$ and $z \models_V  A_n$ holds, then $z \in {\cx}^{-R} $. Therefore $z \models_V \neg q$ holds by definition of $V(q)$.
 Since the cluster $C(z)$ cannot be a co-cover for the antichain $\cx$ by construction of $\cm$,  there should be some $y$ such that $y \not\in {\cx}^{-R},\ y \not\in {\cx}^R $, and $zRy$, in which case $y \models_V q$ and   $z \models_V \neg q \wedge \Diamond q $ holds too, which gives us  $z \models_V \neg (A_n \wedge B)$.

 Indeed, if the cluster $C(z)$ is an immediate $R$-predecessor for $\cx$,
% (e.g. $zRt \ \Longrightarrow \ t \in C(z) \vee t \in {\cx}^R $)
  but not a co-cover for $\cx$ (that is the depth $d(C(z))$ of $C(z)$ is $\max_{i \in \cx}d(i) + 1$),
   then there should be at least one element $y$ such that $zRy$ and $C(y) \cup {\cx}$ forms an antichain for which $C(z)$ is a co-cover (there can be some elements $y_1, \dots, y_k$ such that $C(y_1) \cup \dots \cup C(y_k) \cup {\cx} $ forms an antichain). Then for this $y$ hold $y \not\in {\cx}^{-R},\ y \not\in {\cx}^R $, and $zRy$.


  If the cluster $C(z)$ is not an immediate $R$-predecessor for $\cx$,
  then some cluster $C(z_1)$ which is an immediate $R$-predecessor for $\cx$ is R-accessible from it or some elements $z_1, z_2, \dots , z_k$ are R-accessible which are immediate $R$-predecessors for some subsets of $\cx$ and ${\cx} \subseteq z_1^R \cup \dots \cup z_k^R$.
  In the first case (as before) we obtain some element $y$ such that $y \not\in {\cx}^{-R},\ y \not\in {\cx}^R $, and $z_1Ry$ (and hence $zRy$ by transitivity of $R$). In the second case we can take $y$ to be the element $ z_1$ wich has the desirable property.



% $e$ sees at least one from $K_i$ as well, and $\forall y \in K_i \ y \models_V q$.  Consequently as $e \models_V A_n$ holds then  $e \models_V \neg q \wedge \Diamond q $ holds too that infer  $e \models_V \neg (A_n \wedge B)$.  If $e \models_V \neg A_n$ holds then $e \models_V \neg (A_n \wedge B)$.

 So, we conclude that $ \forall x \in { \mathcal  M} \ x \models_V \neg (A_n \wedge B)$.

By the definition of valuation $V$, $ \forall x \in { \mathcal  M}$ $ x \not\models_V \bigvee_{1 \le i  \le n} p_i \wedge \Diamond q$  is obviously  true. In force of
$$ \Box A_{n,1} \equiv \Box \bigwedge_{1,n} ( p_i \to \neg \Diamond q) \equiv \Box  \bigwedge_{1,n}
(\neg p_i \vee \neg \Diamond q) \equiv \Box  \neg [ \bigvee_{1,n} (p_i \wedge \Diamond q)],$$
 we have $ \forall x \in { \mathcal  M} \ x \models_V \Box A_{n,1}$. Consequently, we have proved that the premise of the rule is valued on arbitrary elements of ${ \mathcal  M}$.


Since $b$ is an $R$-predecessor for the fixed antichain $\cx = \{ C_1,\ C_2,\ \dots, C_n\}$  and $\forall x \in C_i \  x \models_V p_i$ holds, we have $b  \models_V \bigwedge_{1 \le i  \le n} \Diamond  p_i$, e.g. $b  \models_V A_n$.
From this we infer  $b  \not\models_V \Box \neg A_n$. ~\hfill~$\blacksquare$

\bigskip


\begin{utv} The rule ${\rc}_{n}$ is not admissible in logic $\gl$, where $n >1$ is the number of clusters of the antichain ${\cx} = \{ C_1, C_2, \dots C_n  \}$.
\end{utv}
{ \it Proof.} Choose some (the least) $k$ so that ${ \mathcal  M} \sqsubseteq Ch_k (\gl)$.
We can start with a model on the {\it finite} frame $\cm_0 = G\sqcup \{ e \} $ and a valuation $S$ which assigns each  element $c_i \in {\cm}_0,\ i \in I, |I| = |{\cm}_0| < w, $ an individual variable $p_i$:
 $$ \forall i \in I \ c_i \models_S p_i;\  c_i \not\models p_j, i \ne j. $$
 Under such a valuation $S$, all the clusters of ${ \mathcal  M_0}$ are not isomorphic as models and all the elements of any cluster have different valuations.
 % By theorem 3.3.6 \cite{Rb} this model is open submodel of same $k$-characterizing model $Ch_k (\gl)$.

  It is easy to see that the model $\langle { \mathcal  M_0}, S \rangle$ is an open submodel of $Ch_k (\gl)$ for $k= |\cm_0 | $:

 (1)\ For each cluster $ C \in S_1 (\langle { \mathcal  M_0}, S \rangle)$ we can find a cluster $  K \in S_1 (Ch_k (\gl))$ which is isomorphic to cluster $C$ as a model. So we have $S_1 (\langle { \mathcal  M_0}, S \rangle)  \sqsubseteq S_1 (Ch_k (\gl)) $ as models.

 (2)\ Take some cluster $ C_1 \in S_2 (\langle { \mathcal  M_0}, S \rangle)$ which is a co-cover for antichain $A \subseteq S_1 (\langle { \mathcal  M_0}, S \rangle)  $. By (1),  there is an antichain $B \subseteq S_1 (Ch_k(\gl))$ such that  $\langle A, S \rangle \cong B $ as models. Since $C_1^R = C_1 \cup A$ is a $\gl$-frame, by construction of $Ch_k(\gl)$ there is a cluster $ K_1 \in S_2 (Ch_k (\gl)) $ such that $ \langle C_1^R , S \rangle \cong K_1^R \sqsubseteq Ch_k(\gl)$ as models. So we have $ \langle S_{\le 2} (\mathcal M), S \rangle \sqsubseteq  Ch_k(\gl) $.

 (3)\ Continuing this reasoning slice by slice we conclude that $\langle { \mathcal  M_0}, S \rangle \sqsubseteq Ch_k (\gl)  $.  Therefore the frame $\cm_0$ is an open subframe of the frame of $ Ch_k (\gl)$.


  It is easy to see that the process of construction of $\cm$ is a part of the process of construction of one of the frames of $ Ch_k (\gl)$ %for same $k$
  and the resulting frame is an open subframe of the frame $Ch_k (\gl)$.

 (a)\ At the first step of the construction of $\cm$ we take a nontrivial antichain $ X_t \subseteq S_1 ({\cm}_0)$ which does not have singleton co-cover in $ {\cm}_0$ and add such a co-cover whenever it generates a $\gl$-frame $t^R = \{ t \} \cup X_t $ as a root. Since $\langle { \mathcal  M_0}, S \rangle \sqsubseteq Ch_k (\gl)  $, there is an antichain $B \subseteq S_1 (Ch_k(\gl))$ such that $\langle X_t, S \rangle \cong B $ as models. As $t^R$ is a $\gl$-frame, by the construction of the model $ Ch_k(\gl) $ we can find a co-cover for the $B$ --- a cluster $ C_B $ --- such that $ t^R \cong C_B^R$ as frames. So we can transfer a valuation from $C_B$ on $t$ and obtain that $\langle t^R, S \rangle \cong C_B^R $  as models. Hence we have $\langle {\cm}_1, S \rangle \sqsubseteq Ch_k(\gl) $.

 (b)\  Assume that $\langle {\cm}_k, S \rangle \sqsubseteq Ch_k(\gl) $. By the construction of ${\cm}_{k+1} $,  we take a nontrivial antichain $ X_t \subseteq S_{\le (k+1)} ({\cm}_k)$ which does not have singleton co-cover in $ {\cm}_k$ and has at least one cluster of depth $k+1$. Then we add such a co-cover whenever it generates a $\gl$-frame $t^R = \{ t \} \cup X_t $ as a root. For this antichain    $ X_t  $ there is antichain $B \subseteq S_{k+1} (Ch_k(\gl))$ such that $\langle X_t^R, S \rangle \cong B^R $ as models. As $t^R$ is a $\gl$-frame, by construction of model $ Ch_k(\gl) $, we can find a co-cover for the antichain $B$ --- cluster $ C_B $ --- such that $ t^R \cong C_B^R$ as frames. So we can transfer the valuation from $C_B$ on $t$ and obtain that $\langle t^R, S \rangle \cong C_B^R $  as models. Hence we have $\langle {\cm}_{k+1}, S \rangle \sqsubseteq Ch_k(\gl) $.

 (c)\ Continuing this reasoning slice by slice we conclude that $\langle { \mathcal  M}, S \rangle \sqsubseteq Ch_k (\gl)  $.  Therefore the frame $\cm$ is an open subframe of the frame of $ Ch_k (\gl)$.

 Since all the elements of $ Ch_k (\gl)$ are definable and  $\langle { \mathcal  M}, S \rangle \sqsubseteq Ch_k (\gl)  $, all the elements of $\langle { \mathcal  M}, S \rangle $ are also definable (one can find the definition and the structure of this formula $\beta$ in the proof of Theorem 3.3.7 in \cite{Rb}):
  $$  \forall \, x \in { \mathcal  M} \exists \, \beta_x : x \models_S \beta_x \ \& \ (y \ne x \Longrightarrow y \not\models_S \beta_x).  $$
  So we conclude that any (finite) subset $A \subseteq {\cm}$ is also definable under the valuation $S$: $ \beta(A) = \bigvee_{a \in A} \beta_a .  $ Hence, now we can define

   $$ {\bf V(p_i) } = \bigvee_{x \in C_i} \beta_x, 1 \le i \le n ;\ {\bf V(q)} = \{y \in {\cf} \setminus X^R : y \not\in X^{-R} \& \exists z \in X^{-R} (zRy) \} = $$
 $$ =  V \bigg( \neg \bigwedge_{\beta_j \in \cx} \Diamond \beta_j \wedge
 \neg \Box \big( \bigvee_{\beta_j \in {\cx}^R} \beta_i \big) \wedge \bigvee
  \{\beta_y : \exists \beta_z (z \models_S \bigwedge_{\beta_j \in \cx} \Diamond \beta_j \Longrightarrow z \models_S \Diamond \beta_y \} \bigg). $$
  It follows that the sets $V(p_i), 1 \le i \le n,$ and $V(q)$ are definable in $\langle { \mathcal  M}, S \rangle $.


  % $$  V(p_i) = \bigvee_{x \in C_i} \phi_x ;\ .   $$
 %  = \bigvee \{ \phi_y : y \models_V q   \}
% (\bigcup\limits_{ \phi \in {\cd} } ( {\gt}_1 (\phi) \cup {\gt}_2 (\phi)) \subseteq {\gt}_2 (\phi_z) \& $$
%  $$ \& ({\gt}_1 (\phi_y) \cup {\gt}_2 (\phi_y)) \subseteq {\gt}_2 (\phi_z)  )  \}   \bigg)  . $$








  % which is isomorphic to



%different



 Now we define a p-morphism from the frame of $k$-characteristic model  $Ch_k (\gl)$ onto ${ \mathcal  M}$ as follows.


\begin{itemize}
\item for elements of the frame ${ \mathcal  M} \sqsubseteq C_k (\gl)$, we define p-morphism $f$ to be identical, e.g.  $\forall \ x \in { \mathcal  M} \  f(x) := x$.

\item for all $x \in S_1 (C_k (\gl) \setminus { \mathcal  M})$ we let $f(x) := e$, where $\{ e \}$ is the singleton cluster of the first slice of $G \sqcup \{ e \}$.


\item Suppose that for all $x \in S_{\le t} (Ch_k (\gl) \setminus { \mathcal M})$ of depth at most $t$ the required p-morphism is already defined.
    Choose an arbitrary element $y \in S_{t+1} (Ch_k (\gl) \setminus { \mathcal M})$ which is a co-cover for the antichain (possible trivial) ${\mathcal A} \subset S_{\le t} (Ch_k (\gl))$.  By the construction of the $k$-characteristic model $Ch_k (\gl) $, the frames $y^R = C(y) \cup {\mathcal A}^R $ and ${\mathcal A}^R$ are $\gl$-frames.

By the inductive conjecture, the p-morphism  $f ({\mathcal A}^R)$ is already defined.  If $f ({\mathcal A}) = C$ is a trivial antichain and is a cluster, we define $f(y) := \varepsilon \in f ({\mathcal A})$.

 Assume $f ({\mathcal A}^R)$ is  nontrivial.
 Since p-morphisms preserve the truth of formulas, the subframe $f ({\mathcal A}^R)$ is a $\gl$-frame.
  And the result of adding a co-cover (root) to $f ({\mathcal A}^R)$ is a p-morphic image of $y^R$ and by this it is also a $\gl$-frame.
  From this
by the construction of $\gl$-successor  $\mathcal  M$ we infer that the antichain of R-minimal clusters from $f ({\mathcal A}^R)$ has a singleton reflexive co-cover $\varepsilon$ in $\mathcal  M$ and such an element actually exists in ${ \mathcal  M}$.  So we can define $f(y) := \varepsilon$. Since this co-cover is unique in ${ \mathcal  M} $, all the elements of $C(y)$ will be taken to it.

  Since $y$ was arbitrary, thus we define a p-morphism $f$ on the whole slice $S_{t+1} (Ch_k (\gl)$.


\item Continuing this process, we obtain a p-morphism $f$ from the frame of $k$-characteristic model $Ch_k (\gl)$ onto ${ \mathcal  M} $. Note that the mapping $f$ is defined in a way that preserves the property of being a p-morphism.

\end{itemize}

Then we transfer the valuation $V$ from ${ \mathcal  M}$ to $Ch_k (\gl)$ as follows:
 $$ \forall x \in Ch_k (\gl) \ x \models_{f^{-1}(V)} p \ \iff \ f(x) \models_V p. $$

 This gives us the p-morphism of models: $$\langle Ch_k (\gl), \ f^{-1} (V) \rangle \longrightarrow_f  \langle { \mathcal  M}, \ V \rangle.$$

 Since the sets $V(p_i), 1 \le i \le n,$ and $V(q)$ are definable in the model $\langle { \mathcal  M}, S \rangle $ and our p-morphism preserves the truth of formulas, the sets $f^{-1}(V(p_i)), 1 \le i \le n,$ and $f^{-1}(V(q))$ are also definable  in $Ch_k (\gl)$.


 Since the p-morphism $f$ preserves the truth of formulas and the rule ${\rc}_n$ is refuted on $\langle { \mathcal  M}, \ V \rangle $ we refute this rule on the $k$-characteristic model $\langle Ch_k (\gl), \ f^{-1} (V) \rangle $ under a definable valuation. Consequently, the rule ${\rc}_n$ is not admissible in logic $\gl$. Theorem \ref{t2} is complete. ~\hfill~$\blacksquare$




 So from theorems \ref{t1} and  \ref{t2} we obtain

\begin{teo} \label{t3} Suppose that an FMP logic $\gl$ extends $S4$.
Then all the rules ${\rc}_n,\ n > 1, \ n \in N,$ are admissible in $\gl$ if and only if the logic $\gl$ enjoys the weak co-cover property.
\end{teo}




%\renewcommand{\refname}{References}


\begin{thebibliography}{}

\bibitem{Rb}
 V.V. Rybakov.   Admissibility of logical inference rules,
{\it Studies in Logic and the Foundations of Mathematics,  Elsevier Sci. Publ.}, New-York -- Amsterdam,\, {136} (1997).


\bibitem{Har} R. Harrop. Concerning Formulas of the Types $A \to B \vee C,\ A \to \exists x B(x),$   Journal of Symbolic Logic,
{25}:1 (1960),  27 -- 32.

\bibitem{Min} G.E. Mints. Derivability of Admissible Rules. {J. of Soviet
Mathematics}, V.6, 1976, No.4,  pp. 417 -- 421.

\bibitem{Port} J. Port. The deducibilities of S5, J. of Phylosophical
Logic, {10}:1 (1981),  409 -- 422.

 \bibitem{Lor} P. Lorenzen. {\it Einfung in Operative Logik und Mathematik}, Berlin -- Gottingen -- Heidelberg, 1955.

 \bibitem{Frid} H. Fridman. One hundred and two problems in mathematical logic,  Journal of Symbolic Logic,  {40}:3 (1975),  113 -- 130.

\bibitem{Ryb84} V.V. Rybakov. A Critarion for Admissibility of Rules in Modal
System S4 and the Intuitionistic Logic. {Algebra and Logic}, \ V.23, 1984,
No. 5, pp. 369 -- 384 (Eng. translation).



%\bibitem{Cit}A.I. Citkin. On Admissible Rules of Intuitionistic Propositional Logic. {\bf Math. USSR Sbornik}, V. 102 (1977), No. 2, c. 314 --  323.


\bibitem{Iem1} R. Iemhoff. A(nother) characterization  of Intuitionistic Propositional Logic, Annals of Pure and Applied Logic, {113}:1-3 (2001),   161 -- 173.


\bibitem{Rexp} V.V. Rybakov.  An explicit basis for rules admissible in modal system S4, Bulletin of the Section of Logic, 28 (3) : 135--144, 1999.

%Construction of an Explicit Basis for Rules admissible in Modal system S4, Mathematical Logic Quarterly,  {47}:4 (2001),   441 --  451.




\end{thebibliography}{}






\end{document}
