%\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{Description of modal logics which enjoy  co-cover property}

\author{ \bf  V.V. Rimatskiy}
\address{Siberian Federal University, Krasnojarsk}
\email{Gemmeny@rambler.ru}
%\title{� ��������� ��������� ������������� �������}
%\author{{�.�. ������}}%
%\address{���� �������� ������
%\newline\hphantom{iii} �������� ���������� ��. �.~�.~�������� �� ���,
%\newline\hphantom{iii} ��. ��������� ������� 4,
%\newline\hphantom{iii} 630090, �����������, ������}%
%\email{iiivanov@math.nsc.ru}%

\thanks{\sc V.V. Rimatskiy, Description of modal logics which enjoy  co-cover property}
\thanks{\copyright \ 2021 V.V. Rimatskiy}
\thanks{\rm ������ ���������� ���� � ���� (����� 18-41-240005)}
%\thanks{\it ��������� 1 ������ 2004 �., ������������ 31 ������� 2004 �.}%


\top \vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\sc The abstract. } Here we use admissible rules to determine  whenever %given
 modal logic satisfies weak co-cover property. We prove that logic $\gl$ over $S4$ satisfies such property iff the given set of rules 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}
For modern application of logic in  Computer Science and Artificial Intelligence it is
often required that the capable language  of representing the knowledge about dynamic systems.
Distinct non-standard logics (e.g. modal and temporal, logic for multi-agent
reasoning) %very 
efficiently serve these applications. Firstly  they
describe a statements by formulas which are peculiar to studied a models in
general, and do not take to consideration a variable conditions and
a changing assumptions. These conditions and assumptions can be modeled
by distinct variations of the notion of logical consequence. The problem
of such adequate modeling 
%of logical consequence 
is one of extremely  impor\-tant
problems originated from mathematical logic and mathematics in general.
Most important component of our approach consists of the fact that we study
logical consequence in terms of inference rules, clauses, but not only
the formulas or state\-ments.
The formalism concerning description of properties by formulas is
well-develop\-ed, widely spread and well represented in a scientific
literature. It is a representing basis   of human reasoning. But formulas
describe only a stable, static events; the statement only fix the fact, and
isn't able to handle a changing conditions.

Therefore study of (structural) inference rules (or sequents),
expressions which have a premise - a  given collection of assumptions - and
a conclusion, brings us more flexibility and more expressive power to model
human reasoning and computing. Premises gives us a current informations
collected as assumptions and conclusions represent a knowledge, i.e. facts
which we can obtain from our assumptions. The intelligence of reasoning (as a
part of AI) again requires the understanding of what are the 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
allow us to model a standard situation in a study of logical consequence: given
certain assumptions, what does follow from them?

 Evidently the notion of inference rule generalizes the notion of formulas,
and any formula can be viewed as a structural inference rule without
premise and assumption. But admissible inference rules are actually
stronger then the clauses, since Harrop (1960, \cite{Har}) we know that even
the intuitionistic logic $H$ is not structurally complete: it has the
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
since examples of G. Mints \cite{Min} and J. Port \cite{Port}.

Notion of a admissible inference rule goes back to Lorenzen (\cite{Lor},
1955). For arbitrary logic  admissible rules are exactly those, under
which the logic is closed. Clearly any derivable rule is admissible, but, in
general, 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
the fixed length in derivations, thereby linearly shortening them. Admissible
rules, which are not derivable, basically may reduce a derivations even
more drastically.

The history of study an admissible rules
could be dated since H. Fridman's question (\cite{Frid}, 1975) about an
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$ admissible rules
in special form. The Fridman's question about the existence of an algorithm
recognizing admissibility of inference rule 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 of these results   was weak co-cover property. Possible, weak co-cover property, disjunction property and FMP of logic allow us to describe such basis. 
Beside the improvement of deductive power in logic, an admissible rule are able to describe some semantic property of given logic. One of the first attempt was the description of intuitionistic logic $H$ by the set of admissible inference rules (cf. R. Iemhoff \cite{Iem1}). That's why this property is interest of article. Here we use admissible rules to determine  whenever given modal logic satisfy weak co-cover property. We prove that FMP logic $\gl$ over $S4$ satisfy such property iff the given set of rules are admissible in $\gl$.



\section{Denotation, Preliminary Facts}
We assume the reader to be aware of the algebraic and Kripke semantics for
modal logics and to have a certain initial knowledge concerning
the basic facts on inference rules and their admissibility (though we
briefly recall all necessary facts below). As a good entry point to the subject
%taking  as a whole
we  would recommend among modern literature Rybakov \cite{Rb}
for a general technique and  for advanced technique
concerning modal logics and inference rules. According to modern trends by a
{\em logic} we understand the set of all theorems provable in a given axiomatic
system, or the set of valid formulas for a certain 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 theorems of the minimal propositional modal logic $K$.
In the following definitions and results we mean  an algebraic propositional
logic 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$.
The basis set of a frame and a frame itself are  often denoted by the same
letter for simplicity. Further we consider only frames where $R$ is transitive
and reflexive relation. 

% 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$. $Dom (V) = P$ is called the domain of $V$.


A frame ${\cf} = \langle F,\, R \rangle $ is called open subframe of frame $ {\cg} = \langle G, \, R \rangle$ (denote ${\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$ (denote ${\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 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 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 primary property of open submodels and p-morfisms consist 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 model $\mathcal M_1 = \langle W_1,\ R_1,\ V_1 \rangle$ onto model $\mathcal M_2 = \langle W_2,\ R_2,\ V_2 \rangle $ then for any formula $\ga$ which is built out of letters from the domain $Dom (V_1)$, then $\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 analogously.  

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


Any subset $C$  of a frame  $F$, which either a single irreflexive point or a set $C$
satisfying the following properties:
(1) \ $\forall \, x, y \in C (xRy \, \& \, yRx)$;\  (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  $C $ of the frame $ F$}. A cluster is
{\it proper } if \, $|C| > 1$, otherwise that cluster is called %to be
degenerated, 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-compared
by $R$ is called an  antichain. The antichain $\ca$ is nontrivial if it
consists  of  two clusters at least; otherwise $\ca$ is trivial.

We call the  maximal number of clusters in chains of clusters, generated-up by
an element (or a cluster) the {\it depth of an element  (or  a cluster)}.
% in the frame (or the model) W}.
For any transitive frame \, $F $ (or a transitive Kripke model  $M$)
{\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 a depth not more than $n$.

We  say a frame $F$ is an $\gl$--frame for a logic $\gl$ if all theorems
of  $\gl$ are valid at $F$, and $\gl (F)$  -- the set of all formulas valid
in $F$ -- is the logic generated  by $F$. A frame $F$ is rooted if $\exists \,
a \in F$ such that $\forall \, b \in F \ a Rb$. Then we say $C(a)$ is 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$ \,   $X^R$ \ is \,  $\cup \{ x^R | x \in X \}$.
That is subframe  $b^R$ of $F$ is upwards cone generated by $b$,\ and
$X^{R}$ is subframe of $F$ generated by $X$ respectively.
An element \, $ b \in F $ or cluster $C(b)$  \, is {\it a co-cover } for
a set  $ X \subseteq F$,   if \, $b^R  \backslash C(b) = X^R$.
We understand a cluster $C$ as $\gl$-co-cover for $X$
%As $\gl$-co-cover for $X$ we understand %degenerated  a cluster $C$,
 if it generate  $\gl$-frame  $C^R := X^R \cup \{C\}$ as the root.
 We'll identify one-element cluster $C(a)$ and reflexive element $a$ (generating this cluster) as co-cover since the set of R-accessible elements  is the same for both.
 

A subset $\cx$ of the 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) }, $$
is 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$  the assertion \
$$((\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)$$
holds.


The 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 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 not obligatory conversely.
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 theorems of $\gl$. Derivable rules may replace some fragments of the 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 {\it $r$ is valid on $\cf$ wrt $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}

Given logic $\lambda$ has finite model property (FMP for short), if for arbitrary formula $\alpha$ holds: if $\alpha \not\in \lambda $ than    finite $\lambda$-model refuting $\alpha$ exists.

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 up on $ p_1,\dots, p_n$ formula $\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  through their validness in certain special $n$-characteristic Kripke
models. The descrip\-tion of these models $Ch_n ({\gl}) $ and criteria for
recognizing admissibility in ${\gl}$ by means of them are given  in \cite{Rb}, for
instance. As we will strongly occupy 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$, a set $P_n:=\{p_1,...,p_n\}$ of propositional letters, we construct
the first slice $S_1(Ch_n ({\gl})) $ as that follows. It consists of the collection
of all  clusters with all possible valuations $V$ of letters from $P_n$ which
does not have doubling -- elements in the same cluster with the same valuation, and  clusters which
are isomorphic as Kripke models.

Assuming $S_{\le m} (Ch_{n} ({\gl}))$ to be constructed, we put in
$S_{m+1}(Ch_{n }(\gl))$ the clusters  as that 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}) )$ in $S_{m+1}(Ch_n ({\gl}) )$, assuming any $C$ to be
an immediate predecessor for all elements from $\cx$ (co-cover for $\cx$),
such that:

\begin{quote}

(i) $C^R = \cx^R \cup C $ is a $\gl$--frame      and


(ii) if $\cx:=\{C_1 \}$ then  $C$ is not a Kripke submodel of $C_1$.

\end{quote}

Iterating this procedure we get  the model
$Ch_n ({\gl}) $ as the result. To recall a model $\cm$
is $n$-characteristic for a logic $\gl$
if, for any formula $\ga$, which is built up out of letters from $P_n$,
$\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}) $ wrt 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, 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 in Lemma 3.1 \cite{Rexp}. The WCP of logic is a key condition in proof of this statement. Let's reproduce 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 not.    Let 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 a certain 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({\bf 1}) $$

Consequently there exists 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 if all 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 ${\bf (1)}$ $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 to
$b_1 \models_V  \Box \neg  (A_{n} \wedge  B)$  by the assumption~${\bf (1)}$. So, elements $ b_1, \dots , b_n \in  Ch_{\gl } (k)$ generate 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.$$
 By ${\bf (1)}$ \ it follows 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 \}$
that's 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 $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 to
$b \models_V  \Box \neg  (A_{n} \wedge  B)$  by the assumption
${\bf (1)}$. ~\hfill~$\blacksquare$




\medskip

\begin{teo}  \label{t2}
If $\forall n$ the rules $\{ {\rc}_{n},  n > 1 \} $ are admissible in FMP logic $\gl$, over $S4$ then logic $\gl$ enjoys weak co-cover property.
\end{teo}
{ \it Proof.}  Let's suppose all rules  ${\rc}_{n}, \ n >1,n \in N, $ which are admissible in FMP logic $\gl$ over $S4$, but $\gl$ doesn't enjoy weak co-cover property. By definition there exists {\it finite} rooted $\gl$-frame $G = b^R$ and nontrivial antichain of clusters ${\cx} \subset G$ such that   frame $\varepsilon^R :=  \bigcup_{c \in  {\cx}^R }  c^R \cup \{ \varepsilon \}$ which is obtained by adjoining a singleton reflexive co-cover $\varepsilon$ as a root to the frame $ \bigcup_{c \in  {\cx}^R }  c^R,$ is not $\gl$-frame. Let's fix this nontrivial antichain of clusters ${\cx} \subset G$.  We'll prove that in such case at least one rule ${\rc}_{n}$ is not admissible in the logic $\gl$. To do this we construct $\gl$-frame $\mathcal  M$ containing the frame $G$ as open subframe and refuting ${\rc}_{n},  \ n >1,$ under some valuation. Then we define 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 that contradict to admissibility of $\rc_n$. 


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


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

We define $\gl$-successor ${ \mathcal  M}$ of $G\sqcup \{ e \} $   as follows.
Let's fix the nontrivial antichaine $\cx$ from $G$ and define $\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 antichaines 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 $\gl$-frame $t^R= \{ t \} \cup X_t^R $ as a root. So, we obtain  $ { \mathcal  M}_1$. Notice by construction $ { \mathcal  M}_1$ is $\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 antichaines $\{ 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  $\gl$-frame $t^R= \{ t \} \cup X_t^R $ as a root. 
 Notice 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 $\gl$-successor ${ \mathcal  M}= \cup_{k \in N} { \mathcal  M}_k$ of $G\sqcup \{ e \} $. This frame is potentially infinite. 



By construction, the frame ${ \mathcal  M}$ has following properties: 

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

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


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

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

\end{itemize}

\begin{utv} $ { \mathcal  M} \not\models_V {\rc}_{n}$ holds for some $n$ and valuation $V$. 
\end{utv}
{ \it Proof.} We define a valuation $V$ on ${ \mathcal  M}$ as follows. Let's suppose that 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's prove that  premise of ${\rc}_{n}$ is valued on ${ \mathcal  M}$ under $V$ while 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 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)$ can't be a co-cover for 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, that infer  $z \models_V \neg (A_n \wedge B)$. 
 
 Indeed if the cluster $C(z)$ is immediate $R$-predecessor for $\cx$, 
% (e.g. $zRt \ \Longrightarrow \ t \in C(z) \vee t \in {\cx}^R $)
  but not 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}$ form antichain for which $C(z)$ is co-cover (there can be a few elements $y_1, \dots, y_k$ with such property -- $C(y_1) \cup \dots \cup C(y_k) \cup {\cx} $ form antichain). Then for this $y$ holds $y \not\in {\cx}^{-R},\ y \not\in {\cx}^R $ and $zRy$.
  
  
  If the cluster $C(z)$ is not immediate $R$-predecessor for $\cx$, then from it is R-accessible some cluster $C(z_1)$ which is immediate $R$-predecessor for $\cx$ or R-accessible some elements $z_1, z_2, \dots , z_k$ which are immediate $R$-predecessor for some subsets of $\cx$ and ${\cx} \subseteq z_1^R \cup \dots \cup z_k^R$. In 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$ be transitivity of $R$). In second case we can take as $y$ element $ z_1$ wich has 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  $ \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  true obviously. 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 proved that the premise of the rule is valued on arbitrary elements of ${ \mathcal  M}$.


As element $b$ is $R$-predecessor for 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 a number of clusters of antichain ${\cx} = \{ C_1, C_2, \dots C_n  \}$.
\end{utv}
{ \it Proof.} Let's choose some (the least) $k$ so that ${ \mathcal  M} \sqsubseteq Ch_k (\gl)$.
Indeed, we can start with model on the {\it finite} frame $\cm_0 = G\sqcup \{ e \} $ and valuation $S$ which compare to 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 valuation $S$  all clusters of ${ \mathcal  M_0}$ are not isomorphic as models and all elements of any cluster have different valuation. 
 % By theorem 3.3.6 \cite{Rb} this model is open submodel of same $k$-characterizing model $Ch_k (\gl)$. 

  It's easy to see that  model $\langle { \mathcal  M_0}, S \rangle$ is 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 cluster $  K \in S_1 (Ch_k (\gl))$ which is isomorphic to cluster $C$ as model. So we have $S_1 (\langle { \mathcal  M_0}, S \rangle)  \sqsubseteq S_1 (Ch_k (\gl)) $ as models. 
 
 (2)\ Let's take some cluster $ C_1 \in S_2 (\langle { \mathcal  M_0}, S \rangle)$ which is co-cover for antichain $A \subseteq S_1 (\langle { \mathcal  M_0}, S \rangle)  $. By (1)  there is antichain $B \subseteq S_1 (Ch_k(\gl)) :  \langle A, S \rangle \cong B $ as models. Since $C_1^R = C_1 \cup A$ is $\gl$-frame by construction of $Ch_k(\gl)$ there is 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 slice by slice this reasoning we conclude $\langle { \mathcal  M_0}, S \rangle \sqsubseteq Ch_k (\gl)  $.  Therefore the frame $\cm_0$ is open subframe of the frame of $ Ch_k (\gl)$. 
 
 
  It's easy to see the process of construction of $\cm$ is the part of one of the frame of $ Ch_k (\gl)$ %for same $k$ 
  and the resulting frame is open subframe of the frame $Ch_k (\gl)$.
  
 (a)\ At first step of construction of $\cm$ we take nontrivial antichain $ X_t \subseteq S_1 ({\cm}_0)$ which don't have singleton co-cover in $ {\cm}_0$ and add such co-cover whenever it generates $\gl$-frame $t^R = \{ t \} \cup X_t $ as a root. Since $\langle { \mathcal  M_0}, S \rangle \sqsubseteq Ch_k (\gl)  $ there is antichain $B \subseteq S_1 (Ch_k(\gl)) :  \langle X_t, S \rangle \cong B $ as models. As $t^R$ is $\gl$-frame by construction of model $ Ch_k(\gl) $ we can find co-cover for $B$ -- cluster $ C_B $ such that $ t^R \cong C_B^R$ as frames. So we can transfer valuation from $C_B$ on $t$ and obtain $\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 $\langle {\cm}_k, S \rangle \sqsubseteq Ch_k(\gl) $. By construction of ${\cm}_{k+1} $  we take nontrivial antichain $ X_t \subseteq S_{\le (k+1)} ({\cm}_k)$ which don't have singleton co-cover in $ {\cm}_k$ and have at least one cluster of depth $k+1$. Then we add such co-cover whenever it generates $\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)) :  \langle X_t^R, S \rangle \cong B^R $ as models. As $t^R$ is $\gl$-frame by construction of model $ Ch_k(\gl) $ we can find co-cover for antichain $B$ -- cluster $ C_B $ such that $ t^R \cong C_B^R$ as frames. So we can transfer valuation from $C_B$ on $t$ and obtain $\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 slice by slice this reasoning we conclude $\langle { \mathcal  M}, S \rangle \sqsubseteq Ch_k (\gl)  $.  Therefore the frame $\cm$ is open subframe of the frame of $ Ch_k (\gl)$.
 
 Note as all elements of model  $ Ch_k (\gl)$ are definable and  $\langle { \mathcal  M}, S \rangle \sqsubseteq Ch_k (\gl)  $ holds then all elements of $\langle { \mathcal  M}, S \rangle $ definable too (the definition and structure of this formula $\beta$ one can find in the proof of Theorem 3.3.7 \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 definable too under 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). $$
  So the sets $V(p_i), 1 \le i \le n,$ and $V(q)$ are definable in model $\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 frame ${ \mathcal  M}$ as follows.


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

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


\item Let's suppose that for all elements $x \in S_{\le t} (Ch_k (\gl) \setminus { \mathcal M})$ of the depth no more than $t$ required p-morphism is defined already. Let's choose arbitrary element $y \in S_{t+1} (Ch_k (\gl) \setminus { \mathcal M})$ which is co-cover for antichain (possible trivial) ${\mathcal A} \subset S_{\le t} (Ch_k (\gl))$.  By the construction of $k$-characteristic model $Ch_k (\gl) $ the frames $y^R = C(y) \cup {\mathcal A}^R $ and ${\mathcal A}^R$ are $\gl$-frames. 

By inductive conjecture p-morphism  $f ({\mathcal A}^R)$ is defined already.  If $f ({\mathcal A}) = C$ is trivial antichain and is a cluster $C$ we define $f(y) := \varepsilon \in f ({\mathcal A})$. 
 
 Assume $f ({\mathcal A}^R)$ is  not trivial. 
 As p-morphism preserves the truth of formulas the subframe $f ({\mathcal A}^R)$ is $\gl$-frame. 
  And the result of adding co-cover (root) to $f ({\mathcal A}^R)$ would be a p-morphic image of $y^R$ and thus also a $\gl$-frame. From this
by construction of $\gl$-successor  $\mathcal  M$ we infer that the antichain of R-minimal clusters from $f ({\mathcal A}^R)$ has singleton reflexive co-cover $\varepsilon$ in $\mathcal  M$ and such element actually exists in ${ \mathcal  M}$.  So we can define $f(y) := \varepsilon$ . As thus co-cover is unique in ${ \mathcal  M} $ so all elements of $C(y)$ will be mapped to it.

  Accordingly to the arbitrariness of $y$ in such way we define  p-morphism $f$ on whole slice $S_{t+1} (Ch_k (\gl)$. 


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

\end{itemize}

Then we transfer the valuation $V$ from ${ \mathcal  M}$ on $Ch_k (\gl)$ as
 $$ \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.$$ 
 
 Note as the sets $V(p_i), 1 \le i \le n,$ and $V(q)$ are definable in model $\langle { \mathcal  M}, S \rangle $ and p-morphism preserves the truth of formulas, hence the sets $f^{-1}(V(p_i)), 1 \le i \le n,$ and $f^{-1}(V(q))$ are definable  in model $Ch_k (\gl)$ too.
 
 
 As 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 $k$-characteristic model $\langle Ch_k (\gl), \ f^{-1} (V) \rangle $ under definable valuation. Consequently the rule ${\rc}_n$ is not admissible in logic $\gl$. Theorem \ref{t2} is proved. ~\hfill~$\blacksquare$
 



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

\begin{teo} \label{t3} Let FMP logic $\gl$ extends $S4$.
All rules ${\rc}_n,\ n > 1, \ n \in N,$ are admissible in $\gl \ \iff $ 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. transletion).



%\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}
