=Paper=
{{Paper
|id=None
|storemode=property
|title=Kripke-type semantics for G'3 and CG'3
|pdfUrl=https://ceur-ws.org/Vol-1659/paper1.pdf
|volume=Vol-1659
|authors=Verónica Borja Macías,Miguel Pérez-Gaspar
|dblpUrl=https://dblp.org/rec/conf/lanmr/MaciasP16
}}
==Kripke-type semantics for G'3 and CG'3==
https://ceur-ws.org/Vol-1659/paper1.pdf
Kripke-type Semantics for G03 and CG03
Verónica Borja Macı́as and Miguel Pérez-Gaspar
Facultad de Ciencias Fı́sico-Matemáticas
C.U. Avenida San Claudio y 18 Sur, Colonia San Manuel,
Puebla, Pue. 72570 México
vero0304@gmail.com
miguetux@hotmail.com
Abstract. 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 defined CG03 via the three-valued matrix
that defines 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.
Keywords: Many-valued Logics, Paraconsistent Logics, Kripke-Type
Semantics
1 Introduction
Nowadays non-classical logics, particularly intuitionistic logic and paraconsistent
logics, have become a fundamental and powerful tool for knowledge representa-
tion and human-like reasoning. In general there are a lot of applications of these
logics in several topics as we can see in [1, 2], then it is important to study this
kind of logics to have a better understanding of their behavior and properties.
Regardless of what logical system you want to study, it is possible to take two
different 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.
2 Basic Concepts
Let us start by introducing the syntax of the language considered in this article
as well as some definitions. We suppose that the reader has some familiarity
with basic concepts related to mathematical logic such as those given in the first
chapter of [8].
2.1 Logical System
We consider a formal language L built from: an enumerable set of atoms (denoted
as p, q, r, . . .), the set of atoms is denoted as atom(L) and the set of connectives
1
C = {∧, ∨, →, ¬}. Formulas are constructed as usual and will be denoted as
lowercase Greek letters. The set of all formulas of an language L is denoted as
F orm(L). Theories are sets of formulas and will be denoted as uppercase Greek
letters. A logic is simply a set of formulas that is closed under Modus Ponens
(MP) and substitution. The elements of a logic X are called theorems and the
notation `X ϕ is used to state that the formula ϕ is a theorem of X (i.e. ϕ ∈ X).
We say that a logic X is weaker than or equal to a logic Y if X ⊆ Y . Sometimes
we refer to this as Y extends X.
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 Gödel logic and it is obtained by adding the scheme
G3 := (¬ψ → ϕ) → (((ϕ → ψ) → ϕ) → ϕ) to the logic Int.
3 Semantics
As we said we will focus only on two types multi-valued semantics and Kripke-
type semantics. Let us see some general notions about these semantics.
3.1 Multi-valued Semantics
The more adequate manner to define the multi-valued semantics of a logic is by
using a matrix.
Definition 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 := {fc |c ∈ C} is a set of truth functions, with a function for each logical
connective in L.
Definition 2. Given a logic L in the language L, a valuation or an interpre-
tation 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 define the notion of validity in this type
of semantics as follows:
Definition 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(ϕ) ∈ D∗
and we denote it by t L ϕ.
2
In this case the validity depends on the interpretation, but if we want to find
the “logical truths” of the system then the validity should not depend on the
interpretation, in other words we have:
Definition 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 defines a logic via a multi-valued semantics it is usual to define
the set of theorems of the logic as the set of tautologies that are obtained from
the multi-valued semantics, i.e. ϕ ∈ L iff L ϕ.
3.2 Kripke-type Semantics
This semantics were developed by Saul Kripke and André Joyal the late 1950s.
Actually the creation of these semantics was a watershed in the study of the
model theory for non-classical logics.
Definition 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 defined 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.
Definition 6 (Modeling relation). Given an atom p in a logic L and a point
w in a model M we say that “p is true in w in M” if w ∈ v(p) and is denoted
as: (M, w) L p. If ϕ ∈ F orm(L) the modeling relation is defined recursively
depending on the connectives in L and the logic in question.
In general the notion of modeling is only an intermediate step to define the
notion of validity in this type of semantics.
Definition 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 |=L ϕ).
Depending on the logic that we wish to characterize different conditions will
be imposed on: Universe (W ), Accessibility relation (R), Valuation (v), Modeling
relation ().
Table 1. Truth functions of connectives ∧, ∨, → and ¬ in G03 .
f∧ 0 1 2 f∨ 0 1 2 f→ 0 1 2 f¬
0 000 0 012 0 222 0 2
1 011 1 112 1 022 1 2
2 012 2 222 2 012 2 0
3
4 Logic G03
In [3] Carnielly and Marcos define G03 as a paraconsistent logic and use it only
as a tool to prove that (ϕ ∨ (ϕ → ψ)) is not a theorem of Cω (the weakest of
the paraconsistent logics defined by da Costa et. al [5]). In [11, 10] Osorio et
al. define G03 by means of its multi-valued semantics. The matrix of G03 logic
is given by: M = hD, D∗ , F i where: the domain is D = {0, 1, 2} and the set of
designated values is D∗ = {2} and the set F of truth functions for connectives
∧, ∨, → and ¬ consists of the functions shown in Table 1.
We present here a semantical approach for G03 but the reader may be inter-
ested in other approaches, for more references see [9].
4.1 Kripke-type semantics for G03
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 defining Kripke models for
intuitionistic logic.
Definition 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 reflexive, 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 define the function vw : atom(L) → {0, 1} as:
(
1 if w ∈ v(p)
vw (p) =
0 otherwise
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 [4]
hereditary property extends to all formulas in Kripke models for Int.
Definition 9. Let M = hW, R, vi be a Kripke model for Int, w ∈ W and ϕ a
formula.
– If ϕ := p is an atom from Definition 6 we have that: (M, w) Int p iff
w ∈ v(p).
– If ϕ is not an atom the modeling relation is defined recursively as:
Let ϕ, ψ be formulas and for all worlds w ∈ W :
1. (M, w) Int ϕ ∧ ψ iff (M, w) Int ϕ and (M, w) Int ψ,
2. (M, w) Int ϕ ∨ ψ iff (M, w) Int ϕ or (M, w) Int ψ,
3. (M, w) Int ϕ → ψ iff for all w0 such that wRw0 , if (M, w0 ) Int ϕ then
(M, w0 ) Int ψ,
4. (M, w) Int ¬ϕ iff for all w0 such that wRw0 , (M, w0 ) 6Int ϕ.
4
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.
Definition 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 .
T
H
Fig. 1. Kripke model for G3 , whose nodes are H (Here) and T (There).
Kripke-type semantics for daC In [12] Priest defines a logic dualizing the
modeling conditions for the negation in Kripke semantics for intuitionistic logic.
This new system is called da Costa logic daC. Let us see the characterization
of this logic in terms of Kripke models.
Definition 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 reflexive and transitive
– v is a valuation function of atom(L) to P(W ). Given a valuation v and a
point w in W we define
(
1 if w ∈ v(p)
vw (p) =
0 otherwise
and hereditary property must hold, i.e. for each atom p: If wRw0 and vw (p) =
1 then vw0 (p) = 1.
5
As we can see in [12] the hereditary property extends to all formulas in Kripke
models for daC.
Definition 12. Let M = hW, R, vi be a Kripke model for daC, w ∈ W and ϕ
a formula.
– If ϕ := p is an atom, of the Definition 6 we have: (M, w) daC p iff w ∈ v(p).
– If ϕ is not an atom, the modeling relation is defined recursively as in Defini-
tion 9 for connectives ∧, ∨, → and the condition 4 for negation is dualized
in this case, i.e.
4’. (M, w) daC ¬ϕ iff there exists w0 such that w0 Rw, (M, w0 ) 6daC ϕ.
In [7] Osorio et al. demonstrated that the logic G03 is an extension of the logic
daC so it is natural to consider that Kripke models for G03 are a sub collection
of the Kripke models for daC. On the other hand as we can see for the case of
G3 the Kripke models are Kripke models for intuitionistic but only those whose
cardinality is two and the relation is a linear order, a combination of both ideas
give us a characterization for G03 . In fact, we can also find at the end of section 2
of [6] a brief study of extensions of fragments of Heyting Brouwer Logic. This is
the case of the family of logics daCGn , each an extension of daC characterized
by a Kripke frame for daC wich is linearly ordered and has n − 1 points. We
have that G03 corresponds to daCG3 , and clearly the characterizations agree.
Definition 13. A Kripke model for G03 is a Kripke model for daC, M =
hW, R, vi, with the following restrictions: W is a set of cardinality two and R is
a linear order relation on W .
The modeling relation G03 is demarcated by the Definitions 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 .
Definition 14. Let f : D → {∅, {T }, {H, T }} be a bijective function defined as
follow: f (0) → ∅, f (1) → {T }, f (2) → {H, T }.
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(ψ) = {H, T },
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(ψ) = {H, T }. So, by
inductive hypothesis t(ψ) = 2 and by definition t(¬ψ) = 0.
6
ii) [⇒] If t(ϕ) = 2, then t(ψ) ∈ {0, 1}. So, by inductive hypothesis v(ψ) = ∅
or v(ψ) = {T }, then vH (ψ) = 0. So vH (¬ψ) = vT (¬ψ) = 1, then v(¬ψ) =
{H, T }.
[⇐] If v(ϕ) = {H, T }, then in H and T there is evidence below ψ is false,
then vH (ψ) = 0, therefore v(ψ) = ∅ and by inductive hypothesis t(ψ) = 0
and the definition we have that t(ϕ) = 2.
iii) [⇒] It is impossible that t(ϕ) = t(¬ψ) = 1.
[⇐] It is also impossible that v(ϕ) = {T }. If v(ϕ) = {T } then vT (¬ψ) = 1 i.e.
there is evidence below T that ψ is false, then vH (ψ) = 0. Then vH (¬ψ) = 1.
So v(¬ψ) = v(ϕ) = {H, T }, contradiction.
Theorem 1. Let ϕ be a formula in the language of G03 , then:
G03 ϕ iff for any Kripke model M for G03 it holds that M G03 ϕ.
Proof. Both implications by contrapositive. Given a formula ϕ, it is not a tau-
tology 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 Logic CG03
The logic CG03 is a paraconsistent logic that extends G03 . The logical matrix of
CG03 is given by D = {0, 1, 2}, D∗ = {1, 2} 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 define a type for Kripke semantics CG03 in two different ways.
The first based on the semantics of G03 and the second redefining the notion of
validity as discussed below.
Semantics based on G03 semantics
Definition 15. Let M = hW, R, vi be a Kripke model for G03 , w ∈ W and ϕ a
formula. We define 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 se-
mantics and Kripke semantics for CG03 .
Proposition 2. Let ϕ be a formula on the language of CG03 . There exists an
interpretation t : L → {0, 1, 2} 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 Propo-
sition 2.
7
Semantics changing the notion of validity An alternative way of defining
the modeling relation for CG03 is to consider that the kripke models for CG03
are those for G03 but changing Definition 7 by the following one.
Definition 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) |=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 Conclusions
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
definitions 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.
References
1. Diderik Batens, Chris Mortensen, Graham Priest, and Jean Paul Van Bendegem.
Frontiers of Paraconsistent Logic. Studies in logic and computation. Research
Studies Press Limited, 2000.
2. Jean-Yves Béziau. The future of paraconsistent logic. Logical Studies, 1999.
3. Walter A Carnielli and Joao Marcos. A taxonomy of c-systems. arXiv preprint
math/0108036, 2001.
4. Alexander Chagrov. Modal Logic. Oxford logic guides. Clarendon Press, 1997.
5. Newton CA Da Costa et al. On the theory of inconsistent formal systems. Notre
dame journal of formal logic, 15(4):497–510, 1974.
6. Thomas Macaulay Ferguson. Lukasiewicz negation and many-valued extensions
of constructive logics. In 2014 IEEE 44th International Symposium on Multiple-
Valued Logic, pages 121–127. IEEE, 2014.
7. Mauricio Osorio Galindo, Verónica Borja Macı́as, and José Ramón Enrique Arra-
zola Ramı́rez. Revisiting da costa logic. Journal of Applied Logic, 16:111 – 127,
2016.
8. Elliott Mendelson. Introduction to mathematical logic. CRC press, 2009.
9. Mauricio Osorio, José R Arrazola, José L Carballido, and Oscar Estrada. Progra-
mas lógicos disyuntivos y la demostrabilidad de atomos en Cω. Proceedings of the
WS of Logic, Language and Computation, CEUR Vol, 220.
10. Mauricio Osorio, José Luis Carballido, Claudia Zepeda, et al. Revisiting Z. Notre
Dame Journal of Formal Logic, 55(1):129–155, 2014.
11. Mauricio Osorio Galindo and José Luis Carballido Carranza. Brief study of G’3
logic. Journal of Applied Non-Classical Logics, 18(4):475–499, 2008.
12. Graham Priest. Dualising intuitionictic negation. Principia, 13(2):165, 2009.
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 Definition 7
8