The sub-language we consider is the negation free fragment of 
. Namely we define an Mv-Horn-Rule as an mv-rule 
such that
and q are atomic symbols and V=[a,1] is an upper interval of
truth-values of 
with a > 0, and 
. Then, we define the restricted many-valued propositional sub-language
as the following 4-tuple:
being 
= Mv-Atoms( 
) 
Mv-Horn-Rules( ), where Mv-Horn-Rules( ) denotes the set
of Mv-Horn-Rules that can be built from 
and . Within this
sub-language, the not-introduction and not-elimination inference rules of
Mv-SC have no sense. Accordingly, we define the sub-calculus Mv-RSC by
axioms A1, A2 and the Weakening, Composition and
Specialisation inference rules. Deduction in Mv-RSC will be denoted by
.
It is interesting to remark that, in the restricted language , the
Specialisation inference rule takes this form:
since it is easy to show from the definition of 
that
.
The soundness of is naturally inherited from
. Moreover, we shall show the following completeness result for
mv-atom deduction.
As usual, we will prove that if 
then
. To do that we shall make use of standard
logical machinery adapted to our particular case.
Therefore, a set of mv-formulas 
will be RSC-consistent if
is not RSC-inconsistent.
In the following we assume that denotes a set of mv-formulas
from 
.
Next step is to prove that if is RSC-consistent then
is satisfiable.
If is RSC-consistent and 
, the only possibility is to have
such that 
, that is
, and thus we also have 
.
Suppose is consistent, otherwise the result is trivial, and
suppose that 
and 
are inconsistent. Then, it must be the case that
with 
and 
. Analogously, with 
and 
. Therefore, 
, 
and
. Thus, we have that
, and so,
is inconsistent.
Suppose 
is inconsistent for any 
.
Then, by repeated application of previous lemma, 
is also inconsistent, but (p, [0,1]) is an axiom, thus
itself should be inconsistent: contradiction.
Let 
be the set of propositional variables
. Define 
, and for i > 0 define 
, a being a truth-value such that
is consistent. By the previous lemma
such an a always exists. Finally, let 
.
Then it is easy to check that 
is maximally atomic-consistent:
is RSC-consistent. Suppose not. Then there exists a finite
subset 
such that 
, for some p. By construction, there is j such that
. Then 
would be inconsistent,
contradiction. is maximally atomic-consistent. By construction.
Let be consistent and let be a maximally atomic
extension of . Define a valuation 
as follows: 
if 
.
Then it is easy to show that 
is a model of .
Namely, we have to show that, for any 
, we have
that 
. We consider only the case 
. Let 
.
We shall show then that 
. If 
, then 
, and obviously, by definition, 
. Suppose otherwise
that a > b. Since is consistent, so 
is. But, using modus ponens,
and thus 
. Since 
is consistent, 
, that is, 
.
In other words, since V is an upper interval
there must exist 
such that 
. Let
. Since V is an upper
interval, 
, and therefore we have 
, and the lemma is proved.
Finally, from this lemma, Theorem 2 is a direct corollary.
If 
then, by Lemma 1,
, i.e.
is RSC-consistent, thus, by Lemma 5,
is satisfiable, thus there exists 
model
of such that 
, i.e.
.
