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:
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. .