In [10] Osorio et al. introduced a paraconsistent three-valued logic, the logic CG03 which was named after the logic G03 due to the close relation between them. Authors de ned CG03 via the three-valued matrix that de nes G03 but changing the set of designated truth values. In this article we present a brief study of the Kripke-type semantics for some logics related with CG03 before constructing a Kripke-type semantics for it.
Nowadays non-classical logics, particularly intuitionistic logic and paraconsistent
logics, have become a fundamental and powerful tool for knowledge
representation and human-like reasoning. In general there are a lot of applications of these
logics in several topics as we can see in [
Regardless of what logical system you want to study, it is possible to take two
di erent approaches: the syntactic one or the semantic one. In this article we will
proceed in a semantical way, and we will only consider two kinds of semantics:
many-valued semantics and Kripke-type semantics.
Let us start by introducing the syntax of the language considered in this article
as well as some de nitions. We suppose that the reader has some familiarity
with basic concepts related to mathematical logic such as those given in the rst
chapter of [
In this article we will work with multiple logical systems so it is appropriate to specify the names we will use for some systems.
{ Pos is the positive fragment of intuitionistic logic. { C! is the extension of logic Pos obtained by adding the schemes Cw1 := ' _ :' and Cw2 := ::' ! '. { Int is the intuitionistic logic and it is obtained by adding the schemes Int1 := (' ! ) ! ((' ! : ) ! :') and Int2 := :' ! (' ! ) to Pos. { G3 is the three-valued Godel logic and it is obtained by adding the scheme
G3 := (: ! ') ! (((' ! ) ! ') ! ') to the logic Int. 3
As we said we will focus only on two types multi-valued semantics and Kripketype semantics. Let us see some general notions about these semantics. 3.1
The more adequate manner to de ne the multi-valued semantics of a logic is by using a matrix.
De nition 1. Given a logic L in the language L, the matrix of L is a structure M := hD; D ; F i: { D is a nonempty set of truth values (domain) { D is a subset of D (set of designated values) { F := ffcjc 2 Cg is a set of truth functions, with a function for each logical connective in L.
De nition 2. Given a logic L in the language L, a valuation or an interpretation is a function t : atom(L) ! D that maps the atoms to elements in the domain.
An interpretation t can be extended to a one function t : F orm(L) ! D as usual. The interpretations allow us to de ne the notion of validity in this type of semantics as follows: De nition 3. Given a formula ' and an interpretation t in a logic L we say that the formula ' is valid under the interpretation t in the logic L, if t(') 2 D and we denote it by t L '.
In this case the validity depends on the interpretation, but if we want to nd the \logical truths" of the system then the validity should not depend on the interpretation, in other words we have: De nition 4. Given a formula ' in the language of a logic L we say that this is a tautology in L (or simply it is valid) if for every possible interpretation, the formula ' is valid and we denote this by L '.
When one de nes a logic via a multi-valued semantics it is usual to de ne the set of theorems of the logic as the set of tautologies that are obtained from the multi-valued semantics, i.e. ' 2 L i L '. 3.2
This semantics were developed by Saul Kripke and Andre Joyal the late 1950s. Actually the creation of these semantics was a watershed in the study of the model theory for non-classical logics.
De nition 5. A Kripke model for a logic L in the language L is a triple M = hW; R; vi where: { W is a non empty set (universe) { R is a binary relation on W (accessibility relation). { v is a valuation in M, i.e., is a function v : atom(L) ! P(W ).
Once a model is de ned it is necessary to establish a relation between the model and the formulas in order to state which formulas are valid in the model and which ones are not.
w in a model M we say that \p is true in w in M" if w 2 v(p) and is denoted as: (M; w) L p. If ' 2 F orm(L) the modeling relation is de ned recursively depending on the connectives in L and the logic in question.
In general the notion of modeling is only an intermediate step to de ne the notion of validity in this type of semantics.
De nition 7. A formula ' is said to be valid on a model M for logic L if ' is valid in all points x in M and we denote it by (M j=L ').
Depending on the logic that we wish to characterize di erent conditions will be imposed on: Universe (W ), Accessibility relation (R), Valuation (v), Modeling relation ( ).
3
In [
We present here a semantical approach for G03 but the reader may be
interested in other approaches, for more references see [
If we wish to obtain a Kripke-type semantics for CG03 we can begin our labor by observing Kripke-type semantics for some logical systems closely related to this logic.
Kripke-type semantics for Int Let us start by de ning Kripke models for intuitionistic logic.
De nition 8. A Kripke model for (Int) is a structure hW; R; vi, where: { W is a non-empty set of worlds { R is a relation on the worlds that is re exive, transitive and anti-symmetric { v is a valuation function of atom(L) to P(W ). Given a valuation and a point w in W we de ne the function vw : atom(L) ! f0; 1g as: The valuation must satisfy the following restriction for each atom p: If wRw0 and vw(p) = 1 then vw0 (p) = 1.
The latter restriction imposed on valuations is called hereditary property
(Heredity Constraint or Monotonicity). As we can see in Proposition 2.1 in [
{ If ' := p is an atom from De nition 6 we have that: (M; w) Int p i w 2 v(p). { If ' is not an atom the modeling relation is de ned recursively as: Let ', be formulas and for all worlds w 2 W : 1. (M; w) Int ' ^ i (M; w) Int ' and (M; w) Int , 2. (M; w) Int ' _ i (M; w) Int ' or (M; w) Int , 3. (M; w) Int ' ! i for all w0 such that wRw0, if (M; w0) Int ' then (M; w0) Int , 4. (M; w) Int :' i for all w0 such that wRw0, (M; w0) 6 Int '. Kripke-type semantics for G3. As it is well-known G3 is an extension of Int, and Kripke-type semantics for both systems are related, in fact the Kripke models for G3, is just a subset of the Kripke models for Int.
De nition 10. A Kripke model for G3 is a Kripke model for Int, M = hW; R; vi, with the followings restrictions: { W is a set of cardinality two { R is a linear order relation.
Then to depict a Kripke model for G3 is an easy task, it is just a directed graph where worlds in W are the nodes, the relation R corresponds to the graph's edges, in this case there are two nodes as shown in Figure 1. In fact G3 is also known as HT or Here and There Logic due to the characterization in terms of the Kripke models.
In this case the modeling relation remains without changes respect to the
intuitionistic case. Usually a subscript G3 is used to identify that the modeling
relation is based on a Kripke model for G3, i.e. G3 .
Kripke-type semantics for daC In [
De nition 11. A Kripke model for daC is an structure hW; R; vi, where: { W is a non-empty set { R is a relation on the worlds that is re exive and transitive { v is a valuation function of atom(L) to P(W ). Given a valuation v and a point w in W we de ne and hereditary property must hold, i.e. for each atom p: If wRw0 and vw(p) = 1 then vw0 (p) = 1.
As we can see in [
De nition 12. Let M = hW; R; vi be a Kripke model for daC, w 2 W and ' a formula.
{ If ' := p is an atom, of the De nition 6 we have: (M; w) daC p i w 2 v(p). { If ' is not an atom, the modeling relation is de ned recursively as in De nition 9 for connectives ^, _, ! and the condition 4 for negation is dualized in this case, i.e. 4'. (M; w) daC :' i there exists w0 such that w0Rw, (M; w0) 6 daC '.
In [
The modeling relation G03 is demarcated by the De nitions 12 and 13. Let us see now that in fact the set of theorems (tautologies) in the multi-valued logic G03 corresponds to the set of valid formulas in Kripke models for G03. De nition 14. Let f : D ! f;; fT g; fH; T gg be a bijective function de ned as follow: f (0) ! ;, f (1) ! fT g, f (2) ! fH; T g.
Proposition 1. If there exists an interpretation t such that t(') = a, then exists a valuation v such that v(') = f (a). In the same way if there exists a valuation v such that v(') = b, then there exists an interpretation t such that t(') = f 1(b). Proof. The proof is by induction on the length of the formula '. We present in detail the case of the negation.
If ' = : , then i) [)] If t(') = 0, then t( ) = 2. So, by inductive hypothesis v( ) = fH; T g, therefore vH (: ) = 0 = vT (: ) since there is no evidence below H nor below T that is false. [(] If v(') = ;, then vH (: ) = vT (: ) = F . So, there is no evidence in H or T of is false. Hence vH ( ) = vT ( ) = V and v( ) = fH; T g. So, by inductive hypothesis t( ) = 2 and by de nition t(: ) = 0. ii) [)] If t(') = 2, then t( ) 2 f0; 1g. So, by inductive hypothesis v( ) = ; or v( ) = fT g, then vH ( ) = 0. So vH (: ) = vT (: ) = 1, then v(: ) = fH; T g. [(] If v(') = fH; T g, then in H and T there is evidence below is false, then vH ( ) = 0, therefore v( ) = ; and by inductive hypothesis t( ) = 0 and the de nition we have that t(') = 2. iii) [)] It is impossible that t(') = t(: ) = 1.
[(] It is also impossible that v(') = fT g. If v(') = fT g then vT (: ) = 1 i.e. there is evidence below T that is false, then vH ( ) = 0. Then vH (: ) = 1.
So v(: ) = v(') = fH; T g, contradiction.
Theorem 1. Let ' be a formula in the language of G03, then:
G03 ' i for any Kripke model M for G03 it holds that M G03 '.
Proof. Both implications by contrapositive. Given a formula ', it is not a tautology in G03, equivalently there exist an interpretation such that v(') 6= 2, by Proposition 1 this condition occurs if and only if there is a model in which the formula is not valid in all worlds. 5
3 The logic CG03 is a paraconsistent logic that extends G03. The logical matrix of CG03 is given by D = f0; 1; 2g, D = f1; 2g and the truth functions are those of G03 that can be found in the Table 1. Given the narrow relation between G03 and CG03 is natural to de ne a type for Kripke semantics CG03 in two di erent ways. The rst based on the semantics of G03 and the second rede ning the notion of validity as discussed below.
De nition 15. Let M = hW; R; vi be a Kripke model for G03, w 2 W and ' a formula. We de ne the modeling relation (denoted as CG03 ) as follows: (M; w) CG03 ' if and only if there is wRw0 such that (M; w0) G03 '. Theorem 2. If (M; x) CG03 ' and xRy, then (M; y) CG03 '.
The following theorem establishes an equivalence between multi-valued semantics and Kripke semantics for CG03.
Proposition 2. Let ' be a formula on the language of CG03. There exists an interpretation t : L ! f0; 1; 2g such that t(') = 0, if and only if there is a Kripke model for CG03 whose valuation v is such that v(') = ;.
Proof. The proof is by induction on the length of the formula ', it is similar to the proof of Proposition 1.
Theorem 3. Let ' be a formula in the language of CG03, then: CG03 ' if and only if for any Kripke model M for CG03 it holds that M CG03 '.
Proof. The proof is similar to the proof of Theorem 1 in this case using Proposition 2.
the modeling relation for CG03 is to consider that the kripke models for CG03 are those for G03 but changing De nition 7 by the following one. De nition 16. A formula ' is said to be e1-valid on a model M for logic CG03 if exists a point x in M such that (M; x) j=G03 '.
Lemma 1. Let ' be a formula in the language of CG03, then:
CG03 ' if and only if for any Kripke model M for CG03 it holds that ' is e-valid. 6 We studied some non-classical logics from a semantic point of view. First we did a study of the semantics of some logics such as Int, G3 and daC. After that, we focused in G03 and we obtained a characterization of it in terms of Kripke models. Finally using this result and making some variations to some of the de nitions we got a characterization of CG03 using Kripke models. After getting a Kripke-type semantics for these logics we got a new tool that can help us to have a better understanding of these paraconsistent logics. 1 The use of the letter e is to refer to the characterization of the validity depends on an existential connective and to distinguish the notion of validity in the De nition 7