R, Fuzzy R, and Algebraic Kripke-Style: Semantics
R, Fuzzy R, and Algebraic Kripke-Style: Semantics
R, Fuzzy R, and Algebraic Kripke-Style: Semantics
207221
R, fuzzy R, and Algebraic Kripke-style
Semantics
* **
1)
Eunsuk Yang
AbstractThis paper deals with Kripke-style semantics for FR, a fuzzy
version of R of Relevance. For this, first, we introduce FR, define the
corresponding algebraic structures FR-algebras, and give algebraic
completeness results for it. We next introduce an algebraic Kripke-style
semantics for FR, and connect it with algebraic semantics. We furthermore
show that such semantics does not work for R.
Key WordsKripke-style semantics, Algebraic semantics, Many-valued
logic, Fuzzy logic, R, FR.
* :2012.04.01 :2012.05.20 :2012.05.29
** This paper was supported by research funds of Chonbuk National University
in 2012. I must thank the anonymous referees for their helpful comments.
Eunsuk Yang
208
1. Introduction
It is well known that many relevance logicians have had
difficulties in providing binary relational Kripke-style semantics,
i.e., semantics with binary accessibility relations, for relevance
logics (see e.g. [3, 4]). To the best of my knowledge, any
satisfactory such semantics for R has not yet been introduced. In
this paper we show that such semantics can be provided for a
fuzzy version of the system R of Relevance, although not R
itself.
Actually, this is a free continuation of the paper [11]. In it the
author provided algebraic Kripke-style semantics for Uninorm
logic UL. Here we introduce algebraic Kripke-style semantics for
FR, a fuzzy version of R.
1)
For this, first, in Section 2 we
introduce FR, define the corresponding algebraic structures
FR-algebras, and give algebraic completeness results for it. In
Section 3 we introduce an algebraic Kripke-style semantics for
FR, and connect them with algebraic semantics. We furthermore
show that this semantics does not work for R (see Example 3.9).
For convenience, we shall adopt the notation and terminology
similar to those in [5, 7, 8, 10], and assume familiarity with
them (together with the results found in them).
2. The logic FR and its algebraic semantics
We base FR on a countable propositional language with
1)
To see why algebraic Kripke-style semantics are interesting, see [12].
R, fuzzy R, and Algebraic Kripke-style Semantics
209
formulas FOR built inductively as usual from a set of
propositional variables VAR, binary connectives , &, , ,
and constants f, t, with defined connectives:
2)
df1. := f
df2. := ( ) ( ).
We moreover define
t
:= t. For the remainder we shall
follow the customary notation and terminology. We use the axiom
systems to provide a consequence relation.
We start with the following axiomatization of FR.
Definition 2.1 FR consists of the following axiom schemes and
rules:
3)
A1. (self-implication, SI)
A2. ( ) , ( ) (-elimination, -E)
A3. (() ()) (()) (-introduction, -I)
A4. ( ), ( ) (-introduction, -I)
A5. (() ()) (()) (-elimination, -E)
A6. (())(()()) (-distributivity,
-D)
A7. ( & ) ( & ) (&-commutativity, &-C)
A8. ( & t) (push and pop, PP)
2)
Note that while is the extensional conjunction connective, & is the
intensional conjunction one.
3)
A6, indeed, is redundant in FR. But we introduce this in order to show that
R is the FR omitting A13. Note that the system omitting both A6 and A13
is not R (cf see [1, 2, 4]).
Eunsuk Yang
210
A9. ( ) (( ) ( )) (suffixing, SF)
A10. ( ( )) (( & ) ) (residuation, RE)
A11. ( & ) (contraction, CR)
A12. (double negation elimination, DNE)
A13. ( )
t
( )
t
(t-prelinearity, PL
t
)
, (modus ponens, mp)
, (adjunction, adj).
A13 is the axiom scheme for linearity, and logics being
complete w.r.t. linearly ordered (corresponding) algebras are said
to be fuzzy logics (see e.g. [3]).
Note that the system R is the FR omitting A13. Note also that
in R (and so FR), can be defined as ( & )
(df3), and & as ( ) (df4).
Proposition 2.2 FR proves:
(1) ( & ( & )) (( & ) & ) (&-associativity, AS)
(2) ( ) ( & )
(3) ( & ( )) (( & ) ( & ))
(4) ( ( )) (( ) ( ))
(5) (( ( )) ( )) ( ).
Proof: The proof for (1) to (3) is easy, just noting that in
order to prove (3) we need A13 (cf. see [1]). We prove (4) and
(5).
For the proof of (4), first note that in R, we can easily prove
( ( )) ( ( )) and ( (
R, fuzzy R, and Algebraic Kripke-style Semantics
211
)) (( & ( )) f). Then, using (3), we
can prove (( & ( )) f) (( & ) (
& )), and using de Morgan laws, we get (( & )
( & )) ( & ) ( & ). Hence, by df3,
we obtain ( ( )) (( ) ( )), as
required.
For the proof of (5), first note that in R, we can easily prove
(( ) ( )) ( ) using (2). Then, since ((
) ( )) ( ), we can obtain ((( )
( )) (( ) ( ))) ( ). Thus,
using A6, we get (( ) (( ) ( ))) (
). Hence, using (4), we can obtain that (( ( ))
( )) ( ), as wished.
Note that R does not prove (5) in Proposition 2.2 (see [5]).
In FR, f can be defined as t. A theory over FR is a set T
of formulas. A proof in a theory T over FR is a sequence of
formulas whose each member is either an axiom of FR or a
member of T or follows from some preceding members of the
sequence using the two rules in Definition 2.1. T , more
exactly T
FR
, means that is provable in T w.r.t. FR, i.e.,
there is a FR-proof of in T. The relevant deduction theorem
(RDT
t
) for FR is as follows:
Proposition 2.3 ([7]) Let T be a theory, and , formulas.
(RDT
t
) T {} iff T
t
.
Eunsuk Yang
212
For convenience, , , , and are used
ambiguously as propositional connectives and as algebraic
operators, but context should make their meaning clear.
The algebraic counterpart of FR is the class of FR-algebras.
Let x
t
:= x t. They are defined as follows.
Definition 2.4 (i) A pointed commutative residuated distributive
lattice is a structure A = (A, t, f, , , *, ) such that:
(I) (A, , ) is a distributive lattice.
(II) (A, *, t) is a commutative monoid.
(III) y xz iff x * y z, for all x, y, z A
(residuation).
(ii) (Dunn-algebras, [1, 2]) A Dunn-algebra is a pointed
commutative residuated distributive lattice satisfying:
(IV) x x * x (contraction).
(V) (x f) f x (double negation elimination).
(iii) (FR-algebras) A FR-algebra is a Dunn-algebra satisfying:
(VI) t (x y)
t
(y x)
t
(pl
t
).
Note that the class of Dunn-algebras characterizes the system
R. Note also that Dunn-algebras are also called De Morgan
monoids.
Additional (unary) negation and (binary) equivalence operations
are defined as in Section 2.1: x := x f and x y := (x
y) (y x).
The class of all FR-algebras is a variety which will be denoted
by FR.
R, fuzzy R, and Algebraic Kripke-style Semantics
213
FR-algebra is said to be linearly ordered if the ordering of its
algebra is linear, i.e., x y or y x (equivalently, x y =
x or x y = y) for each pair x, y.
Definition 2.5 (Evaluation) Let A be an algebra. An
A-evaluation is a function v : FOR A satisfying: v( ) =
v() v(), v( ) = v() v(), v( ) = v()
v(), v( & ) = v() * v(), v(f) = f, (and hence v(~) =
~v() and v(t) = t).
Definition 2.6 Let A be a FR-algebra, T a theory, a formula,
and K a class of FR-algebras.
(i) (Tautology) is a t-tautology in A, briefly an A-tautology
(or A-valid), if v() t for each A-evaluation v.
(ii) (Model) An A-evaluation v is an A-model of T if v() t
for each T. By Mod(T, A), we denote the class of A-models
of T.
(iii) (Semantic consequence) is a semantic consequence of T
w.r.t. K, denoting by T
K
, if Mod(T, A) = Mod(T {},
A) for each A K.
Definition 2.7 (FR-algebra) Let A, T, and be as in Definition
2.6. A is a FR-algebra iff whenever is FR-provable in T (i.e.
T
FR
), it is a semantic consequence of T w.r.t. the set {A}
(i.e. T
), A a FR-algebra. By MOD
(l)
(FR), we denote the
class of (linearly ordered) FR-algebras. Finally, we write T
(l)
FR
in place of T
MOD
(l)
(FR)
.
Eunsuk Yang
214
Note that since each condition for the FR-algebra has a form
of equation or can be defined in equation (exercise), it can be
ensured that the class of all FR-algebras is a variety.
We first show that classes of provably equivalent formulas
form a FR-algebra. Let T be a fixed theory over FR. For each
formula , let []
T
be the set of all formulas such that T
FR
(formulas T-provably equivalent to ). A
T
is the set of
all the classes []
T
. We define that []
T
[]
T
= [ ]
T
,
[]
T
* []
T
= [ & ]
T
, []
T
[]
T
= [ ]
T
, []
T
[]
T
= [ ]
T
, t = [t]
T
, and
f
= [f]
T
. By A
T
, we denote
this algebra.
Proposition 2.8 For T a theory over FR, A
T
is a FR-algebra.
Proof: Note that A1 to A6 ensure that and satisfy (I) in
Definition 2.4; that A7, A8, and AS ensure that & satisfies (II);
that A10 ensures that (III) holds; and that A11, A12, and A13
ensure that (IV), (V), and (VI), respectively, hold. It is obvious
that []
T
[]
T
iff T
FR
( ) iff T
FR
.
Finally recall that A
T
is a FR-algebra iff T
FR
implies T
FR
, and observe that for in T, since T
FR
t , it
follows that [t]
T
[]
T
. Thus it is a FR-algebra.
We next note that the nomenclature of the prelinearity condition
is explained by the subdirect representation theorem below.
Proposition 2.9 (Cf. [10]) Each FR-algebra is a subdirect
R, fuzzy R, and Algebraic Kripke-style Semantics
215
product of linearly ordered FR-algebras.
Theorem 2.10 (Strong completeness) Let T be a theory, and
a formula. T
FR
iff T
FR
iff T
l
FR
.
Proof: (i) T
FR
iff T
FR
. The left-to-right direction
follows from definition. The right-to-left direction is as follows:
from Proposition 2.8, we obtain A
T
MOD(FR), and for
A
T
-evaluation v defined as v() = []
T
, it holds that v
Mod(T, A
T
). Thus, since from T
FR
we obtain that []
T
= v
() t, T
FR
t . Then, since T
FR
t, by (mp) T
FR
, as required.
(ii) T
FR
iff T
l
FR
. It follows from Proposition 2.9.
3. Kripke-style semantics for FR
Here we consider algebraic Kripke-style semantics for FR.
Definition 3.1 (Algebraic Kripke frame) An algebraic Kripke
frame is a structure X = (X, t, f, , , ) such that (X, t, f,
, , ) is a linearly ordered residuated pointed commutative
monoid. The elements of X are called nodes.
Definition 3.2 (FR frame) A FR frame is an algebraic Kripke
frame, where x = (x f) f, and is contractive, i.e., x
x * x.
Eunsuk Yang
216
An evaluation or forcing on an algebraic Kripke frame is a
relation between nodes and propositional variables, and
arbitrary formulas subject to the conditions below: for every
propositional variable p,
(AHC) if x p and y x, then y p; and
for arbitrary formulas,
(t) x t iff x t;
(f) x f iff x f;
() x = iff x and x ;
() x iff x or x ;
(&) x & iff there are y, z X such that y ,
z , and x y z;
() x iff for all y X, if y , then x y
.
Definition 3.3 (i) (Algebraic Kripke model) An algebraic
Kripke model is a pair (X, ), where X is an algebraic Kripke
frame and is a forcing on X.
(ii) (FR model) A FR model is a pair (X, ), where X is a
FR frame and is a forcing on X.
Definition 3.4 (Cf. [9]) Given an algebraic Kripke model (X,
), a node x of X and a formula , we say that x forces to
express x . We say that is true in (X, ) if t , and
R, fuzzy R, and Algebraic Kripke-style Semantics
217
that is valid in the frame X (expressed by X models ) if
is true in (X, ) for every forcing on X.
For soundness and completeness for FR, let
FR
be the
theoremhood of in FR. First we note the following lemma.
Lemma 3.5 (Hereditary Lemma, HL) Let X be an algebraic
Kripke frame. For any sentence and for all nodes x, y X,
if x and y x, then y .
Proof: Easy.
Proposition 3.6 (Soundness) If
FR
, then is valid in
every FR frame.
Proof: We prove the validity of A11 as an example: it suffices
to show that if x , then x & . Assume x .
Then, since x x x, using (&), we can obtain x & ,
as required.
The proof for the other cases is left to the interested reader.
By a chain, we mean a linearly ordered algebra. The next
proposition connects algebraic Kripke semantics and algebraic
semantics for FR (cf. see [9]).
Proposition 3.7 (i) The {t, f, , , } reduct of a
FR-chain A is a FR frame.
Eunsuk Yang
218
(ii) Let X = (X, t, f, , , ) be a FR frame. Then the
structure A = (X, t, f, max, min, , ) is a FR-algebra (where
max and min are meant w.r.t. ).
(iii) Let X be the {t, f, , , } reduct of a FR-chain A,
and let v be an evaluation in A. Let for every atomic formula p
and for every x A, x p iff x v(p). Then (X, ) is a
FR model, and for every formula and for every x A, we
obtain that: x iff x v().
Proof: The proof for (i) and (ii) is easy. For the proof of (iii),
see Proposition 3.8 in [10].
Theorem 3.8 (Strong completeness) FR is strongly complete
w.r.t. the class of all FR-frames.
Proof: It follows from Proposition 3.7 and Theorem 2.10.
Let an R frame X be an FR frame on a partially ordered
monoid in place of a linearly ordered monoid, let an evaluation
or forcing on an R frame be the same as that on a FR
frame, and let (X, ) be an R model. Then, at first glance, (X,
) seems to be a model for R. But actually it is not. The
following example verifies it.
Example 3.9 An R model (X, ) validates Proposition 2.2 (5),
i.e., t (( ( )) ( )) ( ).
R, fuzzy R, and Algebraic Kripke-style Semantics
219
Proof: By () and (), we assume x ( ( ) and
x , and show x . For this last, we further
assume y and show x * y . By the suppositions and
(), we have x * y , therefore x * y or x * y
by (). Let x * y . Then, since x , by
() we obtain x * (x * y) , therefore (x * x) * y by
the associativity of *. Then, since x x * x, using Lemma 3.5,
we get x * y .
This sentence is not a theorem of R but a theorem of FR.
Thus this model is not for R.
4. Concluding remark
We investigated algebraic Kripke-style semantics for FR, a
fuzzy version of R. We proved soundness and completeness
theorems. But we did not provide algebraic Kripke-style semantics
for R. This is an open problem left in this paper.
Eunsuk Yang
220
References
[1] Anderson, A. R., and Belnap, N. D. (1975), Entailment: The
Logic of Relevance and Necessity, vol. 1, Princeton, Princeton
Univ. Press.
[2] Anderson, A. R., Belnap, N. D., and Dunn, J. M. (1992),
Entailment: The Logic of Relevance and Necessity, vol. 2,
Princeton, Princeton Univ. Press.
[3] Cintula, P. (2006), Weakly Implicative (Fuzzy) Logics I:
Basic properties, Archive for Mathematical Logic, pp.
673-704.
[4] Dunn, J. M. (1976), A Kripke-style semantics for R-Mingle
using a binary accessibility relation, Studia Logica, 35, pp.
163-172.
[5] Dunn, J. M. (1986), Relevance logic and entailment,
Handbook of Philosophical Logic, vol. III, D. Gabbay and F.
Guenthner (eds.), Dordrecht, D. Reidel Publ. Co., pp.
117-224.
[6] Dunn, J. M. (2000), Partiality and its Dual, Studia Logica,
66, pp. 5-40.
[7] Meyer, R. K., Dunn, J. M., and Leblanc, H. (1976),
Completeness of relevant quantification theories, Notre
Dame Journal of Formal Logic, 15, pp. 97-121.
[8] Montagna, F. and Sacchetti, L. (2003), Kripke-style semantics
for many-valued logics, Mathematical Logic Quaterly, 49, pp.
629-641.
[9] Montagna, F. and Sacchetti, L. (2004), Corrigendum to
R, fuzzy R, and Algebraic Kripke-style Semantics
221
Kripke-style semantics for many-valued logics, Mathematical
Logic Quaterly, 50, pp. 104-107.
[10] Tsinakis, C., and Blount, K. (2003), The structure of
residuated lattices, International Journal of Algebra and
Computation, 13, pp. 437-461.
[11] Yang, E. (2012), Kripke-style semantics for UL, Korean
Journal of Logic, 15/1, pp. 1-15.
[12] Yang, E., Algebraic Kripke-style semantics for relevance
logics, manuscript.
Department of Philosophy, Chonbuk National University
eunsyang@jbnu.ac.kr
R, fuzzy R, and Algebraic Kripke-style Semantics
R FR
. FR
FR- FR
. FR
.
R .
: R, FR, () , ,
,