=Paper=
{{Paper
|id=Vol-2585/paper11
|storemode=property
|title=Completeness for the paraconsistent logic CG'3
based on maximal theories
|pdfUrl=https://ceur-ws.org/Vol-2585/paper11.pdf
|volume=Vol-2585
|authors=Miguel Pérez-Gaspar,Everardo Bárcenas
|dblpUrl=https://dblp.org/rec/conf/lanmr/Perez-GasparB19
}}
==Completeness for the paraconsistent logic CG'3
based on maximal theories==
https://ceur-ws.org/Vol-2585/paper11.pdf
Completeness for the paraconsistent logic CG03
based on maximal theories
Miguel Pérez-Gaspar and Everardo Bárcenas
Universidad Nacional Autónoma de México, México
miguel.perez@fi-b.unam.mx
ebarcenas@unam.mx
Abstract. G03 is a recently developed three-valued logic with a sole type
of true value. CG03 is also a three-valued paraconsistent logic extending
G03 with two true values. The current state of the art of CG03 com-
prises Kripke-type semantics. In this work, we further extend studies on
the syntactic-semantic relation of CG03 . More precisely, we developed a
Hilbert-type axiomatization inspired by the Lindenbaum-Los technique
on maximal theories applied to completeness. Furthermore, we also prove
soundness.
Keywords: Many-valued logics · Paraconsistent logics · CG0 3
1 Introduction
Many-valued logics are non-classical logics. As in classical logics, many-valued
logics also enjoy of the truth-functionality principle, namely, the truth value of a
compound sentence is determined by the truth values of its component sentences,
it remains the same when one of its component sentences is replaced by another
sentence with the same truth value. However, contrastingly with the classical
case, many-valued logics do not restrict the number of truth values to only two, a
larger set of truth degrees is then the distinctive feature in the many-valued con-
text. In [2], we can find a detailed analysis of many-valued logics. Some systems
of many-valued logics are presented as families of uniformly defined finite-valued
and infinite-valued systems, for example, Lukasiewicz logic, Gödel logic, t-Norm
based systems, three-valued system, Dunn-Belnap’s 4-valued system, Product
systems. The main types of logical calculus for systems of Many-valued logics
are Hilbert type calculus, Gentzen type sequent calculus or Tableaux [2]. The
art for a wide class of infinitely valued logics is presented in [9].
In 1954, F. Asenjo in his Ph.D. dissertation proposes for the first time to
use Many-valued logics to generate paraconsistent logics (logics whose semantic
or proof-theoretic logical consequence relation is not explosive [7]). The many-
valued approach is to drop this classical assumption and allow more than two
truth values. The most common strategy is to use three truth values: true, false,
and both (true and false) for the evaluations of formulas [7].
The CG03 logic is a three-valued paraconsistent logic of recently developed
by [5] with a many-valued semantics. Both CG03 and G03 are defined in terms of
Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0)
119
three-valued matrices, the unique difference among these logics is on their sets
of designated values. In this paper, we further extend studies on the syntactic-
semantic relation of CG03 . Our main contributions are briefly summarized as
follows:
· A formal axiomatic theory CG03h . This theory has four primitive connectives,
twelve axioms, and Modus Ponens as the only inference rule.
· It is shown that the formal axiomatic theory CG03h is sound and complete
with respect to CG03 , see Theorems 2 and Corollary 1. To prove complete-
ness theorem for CG03h , we use the Lindenbaum-Los technique on maximal
theories.
2 Background
We first introduce the syntax of the logical formulas considered in this paper. We
follow common notation and basic definitions as W. Carnielli and M. Coniglio
in [1].
Definition 1 (Propositional signatures). A propositional signature is a set
Θ of symbols called connectives, together with the information concerning to the
arity of each connective.
The following symbols will be used for logical connectives: ∧ (conjunction,
binary); ∨ (disjunction, binary); → (implication, binary); ¬ (weak negation,
unary); • (inconsistency operator, unary); ∼ (strong negation, unary); ⊥ (bottom
formula, 0-ary).
Definition 2 (Propositional language). Let V ar = {p1 , p2 , . . .} be a denu-
merable set of propositional variables, and let Θ be any propositional signature.
The propositional language generated by Θ from V ar will be denoted by LΘ .
Definition 3 (Tarskian logic). A logic L defined over a language L which has
a consequence relation `, is Tarskian if it satisfies the following three properties,
for every Γ ∪ ∆ ∪ {α} ⊆ L:
(i) if α ∈ Γ then Γ ` α;
(ii) if Γ ` α and Γ ⊆ ∆ then ∆ ` α;
(iii) if ∆ ` α and Γ ` β for every β ∈ ∆ then Γ ` α.
A logic satisfying item (ii) above is called monotonic. Moreover, a logic L
is said to be finitary if it satisfies the following:
(iv) if Γ ` α then there exists a finite subset Γ0 of Γ such that Γ0 ` α.
A logic L defined over a propositional language L generated by a signature
from a set of propositional variables is called structural if it satisfies the
following property:
(v) if Γ ` α then σ[Γ ] ` σ[α], for every substitution σ of formulas for variables.
A propositional logic is standard if it is Tarskian, finitary, and structural.
120
From now on, a logic L will be represented by a pair L = hL, `i, where L
and ` denote the language and the consequence relation of L, respectively. If L
is generated by a propositional signature Θ from V ar, this is L = LΘ then we
will write L = hΘ, `i.
Let L = hL, `i be a logic, α be a formula in L and X1 . . . Xn be a finite
sequence (for n ≥ 1) such that each Xi is either a set for formulas in L or a
formula in L. Then, as usual, X1 , . . . , Xn ` α will stand for X10 ∪ · · · ∪ Xn0 ` α,
where, for each i, Xi0 is Xi , if Xi is a set of formulas, or Xi0 is {Xi }, if Xi is a
formula.
Definition 4 (Paraconsistent logic). A Tarskian logic L is paraconsistent
if it has a (primitive or defined) negation ¬ such that α, ¬α 6`L β for some
formulas α and β in the language of L .
The most adequate manner to define the many-valued semantics of logic
is through a matrix. We introduce the definition of the deterministic matrix,
also known as the logical matrix or simply as a matrix. In [4], we can find an
exhaustive discussion about many-valued logic and some examples.
Definition 5 (Matrix). Given a logic L in the language L, the matrix of L
is a structure M = hD, D∗ , F i, where:
(i) D is a non-empty set of truth values (domain).
(ii) D∗ is a subset of D (set of designated values).
(iii) F = {fc |c ∈ C} is a set of truth functions, with one function for each logical
connective c of L.
Definition 6 (Interpretation). Given a logic L in the language L, an in-
terpretation t, is a function t : V ar → D that maps propositional variables to
elements in the domain.
Any interpretation t can be extended to a function on all formulas in LΣ as
usual, i.e. applying recursively the truth functions of logical connectives in F . If t
is a valuation in the logic L , we will say that t is an L -valuation. Interpretations
allow us to define the notion of validity in this type of semantics as follows:
Definition 7 (Valid formula). Given a formula ϕ and an interpretation t in
a logic L , we say that the formula ϕ is valid under t in L , if t(ϕ) ∈ D∗ , and
we denote it as t |=L ϕ.
Let us note that validity depends on the interpretation, but if we want to
talk about “logical truths” in the system, then the validity should be absolute,
as stated in the next definition:
Definition 8 (Tautology). Given a formula ϕ in the language of a logic L ,
we say ϕ is a tautology in L , if for every possible interpretation, the formula ϕ
is valid, and we denote it as |=L ϕ.
If ϕ is a tautology in the logic L , we say that ϕ is an L -tautology. When logic
is defined via a many-valued semantics, it is usual to define the set of theorems
of L as the set of tautologies obtained from the many-valued semantics, i.e. ϕ ∈
L if and only if |=L ϕ.
121
3 The logic CG03
In this section, we present a summary of the state of the art of logic CG’3.
Starting with the many-valued semantics defined by Osorio et al. and ending with
Kripke semantics of the CG03 logic as well as some important results proposed
by Borja and Pérez-Gaspar.
Many-valued semantic of CG03
The logic CG03 was introduced in [5] the authors, defined it as a three-valued logic
where the matrix is given by the structure M = hD, D∗ , F i, where D = {0, 1, 2},
the set D∗ of designated values is {1, 2}, and F is the set of truth functions
defined in Table 3.
Table 1. Truth functions for the connectives ∨, ∧, →, and ¬ in CG03 .
f∨ 0 1 2 f∧ 0 1 2 f→ 0 1 2 f¬
0 012 0 000 0 222 0 2
1 112 1 011 1 022 1 2
2 222 2 012 2 012 1 0
Kripke-type semantic for CG03
In [3] Borja and Pérez-Gaspar proposed Kripke-type semantics for CG03 . This
semantics is defined in two different ways. The first one is based on the semantics
of G03 as follows:
Definition 9. 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) |=∗CG0 ϕ if and only if there is wRw0 such that (M, w0 ) |=∗G0 ϕ. 1
3 3
Theorem 1. Let ϕ be a formula in the language of CG03 , then:
|=CG03 ϕ iff for any Kripke model M for CG03 it holds that M |=∗CG0 ϕ.
3
The second Kripke-type semantics is given by redefining the modeling rela-
tion for CG03 considering that the Kripke models for CG03 are those for G03 but
changing the definition by the following one.
Definition 10. A formula ϕ is said to be e-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.
1
We use the symbol |=∗ to define the modeling relation and avoid confusion with the
symbol |= that is used for tautologies.
122
4 Axiomatization of CG03
In this section, we present an axiomatization for the CG03 logic. We begin by
defining a formal axiomatic theory whose language has four connective, bottom
formula, conjunction, disjunction, and implication. Note that the connective dis-
junction is determined by the primitive connective.
Let CG03h be a formal axiomatic theory for CG03 logic defined over the signa-
ture Σ = {⊥, ∧, →, ¬}, we define some other connectives, that can be considered
as abbreviations as follows:
∼ϕ := ϕ → ⊥ (Strong negation)
•ϕ := ∼∼ϕ ∧ ¬ϕ (Inconsistency operator)
ϕ ∨ ψ := ((ϕ → ψ) → ψ) ∧ ((ψ → ϕ) → ϕ) (Disjunction logic)
ϕ ↔ ψ := (ϕ → ψ) ∧ (ψ → ϕ) (Equivalence logic)
The set of well-formed formulas is constructed as usual, it is denoted as LΣ .
Definition 11 (CG03h ). The logic CG03h is defined over the language LΣ by
the Hilbert calculus:
Axiom schemas:
α → (β → α) Ax1
(α → (β → γ)) → ((α → β) → (α → γ)) Ax2
(α ∧ β) → α Ax3
(α ∧ β) → β Ax4
α → (β → (α ∧ β)) Ax5
α → (α ∨ β) Ax6
β → (α ∨ β) Ax7
(α → γ) → ((β → γ) → (α ∨ β) → γ) Ax8
(α → β) ∨ α Ax9
α ∨ ¬α Ax10
¬ϕ → (¬¬ϕ → ψ) Ax11
•α → α Ax12
Inference rule:
α α→β
MP
β
Definition 12 (Derivation). Let Γ ∪{ϕ} ⊆ LΣ be a set of formulas. A deriva-
tion of ϕ from Γ in CG03h is a finite sequence ϕ1 , . . . , ϕn of formulas in LΣ such
that ϕn is ϕ and, for every 1 ≤ i ≤ n, the following holds:
1. ϕi is a instance of an axiom schema of CG03h , or
2. ϕi ∈ Γ , or
3. there exist j, k such that ϕk = ϕj → ϕi (and so ϕi follows from ϕj and ϕk
by MP).
We say that ϕ is derivable from Γ in CG03h , denoted by Γ `CG03h ϕ, if there
exists a derivation of ϕ from Γ in CG03h .
123
The following meta-theorems of CG03h will prove to be quite useful, their
demonstrations are straightforward.
Proposition 1. The calculus CG03h satisfies the following properties:
(i) Γ, α `CG03h β iff Γ `CG03h α → β (Deduction meta-theorem, DMT).
(ii) If Γ, α `CG03h ϕ and Γ, β `CG03h ϕ then Γ, α ∨ β `CG03h ϕ.
(iii) If Γ, α `CG03h ϕ and Γ, ¬α `CG03h ϕ then Γ `CG03h ϕ (Proof-by-cases).
Proof.
(i) To prove that a Hilbert calculus satisfies DMT, it suffices to derive axioms
Ax1 and Ax2, while MP must be the unique inference rule.
(ii) The demonstration is straightforward by applying axiom Ax8 and MP
twice.
(iii) It is a direct consequence of item (ii) and axiom Ax10.
Definition 13 (Valuations for CG03 ). A function v : LΣ → {0, 1, 2} is a
valuation for CG03 , or a CG03 -valuation, if it satisfies the following clauses:
−v(¬α) = 0 when v(α) = 2
−v(α ∧ β) ∈ {1, 2} iff v(α) ∈ {1, 2} and v(β) ∈ {1, 2}
−v(α → β) ∈ {1, 2} iff v(α) = 0 or v(β) = 2 or
v(α) = v(β) = 1 or v(α) = 2, v(β) = 1
0
The set of all such valuations will be designated by V CG3 .
For every Γ ∪{ϕ} ⊆ LΣ , the following semantical consequences relation w.r.t.
0
the set V CG3 of CG03 -valuations can be defined:
0
Γ |=CG03 ϕ if and only if, for every v ∈ V CG3 ,
if v(γ) ∈ {1, 2} for every γ ∈ Γ then v(ϕ) ∈ {1, 2}.
Theorem 2 (Soundness). For every Γ ∪ {ϕ} ⊆ LΣ :
If Γ `CG03h ϕ then Γ |=CG03 ϕ.
Proof. It suffices to verify that each axiom schema is a tautology in CG03 and if
α and β are formulas such that v(α), v(α → β) ∈ {1, 2} then v(β) ∈ {1, 2} i.e.
MP preserves tautologies.
The proof of completeness needs some definitions and results related to
Tarskian Logic, see definition 3.
Definition 14 (Maximal set). For a given Tarskian logic L over the language
L, let Γ ∪ {ϕ} ⊆ L. The set Γ is maximal non-trivial with respect to ϕ in L if
Γ 6`L ϕ but Γ, ψ ` ϕ for any ψ ∈
/ Γ.
124
Definition 15 (Closed theory). Let L be a Tarskian logic, A be a set of
formulas Γ is closed in L , or a closed theory of L , if the following holds for
every formula ψ; Γ `L ψ if and only if ψ ∈ Γ .
Lemma 2. Any set of formulas maximal non-trivial with respect to ϕ in L is
closed, provided that L is Tarskian.
Proof. Straightforward from Definition 3 and Definition 14.
Theorem 3 (Lindenbaum-Los). Let L be a Tarskian and finitary logic over
the language L. Let Γ ∪ {ϕ} ⊆ L be such that Γ 6`L ϕ. There exists then a set
∆ such that Γ ⊆ ∆ ⊆ L with ∆ maximal non-trivial with respect to ϕ in L .
Proof. The demonstration can be found in [10, Theorem 22.2] and [1, Theorem
2.2.6].
CG03h is a Tarskian and finitary because CG03h is defined by a Hilbert cal-
culus, so Theorem 3 holds. On the other hand, the following properties it holds:
Lemma 3. If ∆ is a maximal non-trivial set with respect to ϕ ∈ CG03h , then
for every formulas ψ and γ, ∆ satisfies the following properties:
(i) ∆ `CG03h ψ if and only if ψ ∈ ∆.
(ii) (ψ ∨ γ) ∈ ∆ if and only if ψ ∈ ∆ or γ ∈ ∆.
(iii) (ψ ∧ γ) ∈ ∆ if and only if ψ ∈ ∆ and γ ∈ ∆.
(iv) ψ ∈ ∆ if and only if ¬ψ 6∈ ∆ if and only if ¬¬ψ ∈ ∆.
Proof. The proof of each item can be seen in [1].
Proposition 2. The following formulas are theorems in CG03h .
(i) ϕ ∧ ¬ϕ ↔ ⊥
(ii) ¬ • ϕ → ¬ • ¬ϕ
(iii) (¬¬ϕ ∧ ¬γ) → ¬(ϕ → γ)
(iv) (•ϕ ∧ ¬ • ψ) → ¬ • (ϕ → ψ)
(v) (¬ • ϕ ∧ ¬ • ψ) → ¬ • (ϕ → ψ)
(vi) (ϕ ∧ ψ) → (ϕ → ψ)
(vii) (ϕ ∧ •ψ) → •(ϕ → ψ)
(viii) (¬ϕ ∧ ¬ • ϕ) → (ϕ → ψ)
(ix) ¬ϕ → ¬ • (ϕ → ψ)
(x) ¬ • ψ → ¬ • (ϕ → ψ)
(xi) (•ϕ ∧ •ψ) → ¬ • (ϕ → ψ)
(xii) ¬ϕ → ¬(ϕ ∧ ψ)
(xiii) (¬ϕ ∧ ¬ • ϕ) → ¬ • (ϕ ∧ ψ)
(xiv) ¬ψ → ¬(ϕ ∧ ψ)
(xv) (¬ψ ∧ ¬ • ψ) → ¬ • (ϕ ∧ ψ)
(xvi) (•ϕ ∧ •ψ) → •(ϕ ∧ ψ)
(xvii) (•ϕ ∧ ψ ∧ ¬ • ψ) → •(ϕ ∧ ψ)
(xviii) (ϕ ∧ ¬ • ϕ ∧ •ψ) → •(ϕ ∧ ψ)
125
(xix) (¬ • ϕ ∧ ¬ • ψ) → ¬ • (ϕ ∧ ψ)
The proofs of each item in the Proposition 2 can be demonstrated using the
axiom schemas and Modus Ponens.
Lemma 4 (The truth lemma). Let h : V ar → D be a homomorphism from
V ar in D such that for every propositional variable p
0 iff p 6∈ ∆, •p 6∈ ∆
h(p) = 1 iff p ∈ ∆, •p ∈ ∆
2 iff p ∈ ∆, •p 6∈ ∆
where ∆ is a maximal non-trivial set with respect to ϕ ∈ CG03h . Then for all
α ∈ LΣ is verified:
0 iff α 6∈ ∆, •α 6∈ ∆
h(α) = 1 iff α ∈ ∆, •α ∈ ∆
2 iff α ∈ ∆, •α 6∈ ∆
Proof. Let α be a formula and let v be a valuation in CG03h . The proof is done
by induction on the complexity of α.
Base case. If α = p, where p is a propositional variable, then affirmation holds
by definition.
Induction hypothesis. Assume that the statement is verified for each formula
of complexity less than α; that is, if β is a formula that is less complex than α,
then it is true that:
h(β) = 0 if and only if β 6∈ ∆, •β 6∈ ∆
h(β) = 1 if and only if β ∈ ∆, •β ∈ ∆
h(β) = 2 if and only if β ∈ ∆, •β 6∈ ∆
Note that it is sufficient to prove the “only if ” part of the statement, since
the three conditions on the right side are incompatible in pairs, also h(β) can
only take one of the following values 0, 1, 2. For example, if the first condition
on the right side of the statement holds for a β formula, then the other two
conditions are false and therefore h(β) ∈/ {1, 2}. Thus, h(β) must be 0.
Case1 negation. Let α = ¬β, for some formula β. We analyze three cases.
I. Assume that h(α) = 0. Given that h(α) = h(¬β) = ¬h(β), we have that
¬h(β) = 0. By the table of negation, h(β) = 2. Note that β has less
complexity than α, then by induction hypothesis β ∈ ∆ and •β 6∈ ∆.
Given that β ∈ ∆ by Lemma 3, ¬β 6∈ ∆. So α 6∈ ∆. On the other hand, we
have that •β 6∈ ∆ by Lemma 3, ¬ • β ∈ ∆. By Proposition 2(ii) and MP,
we conclude ¬ • ¬β ∈ ∆.
126
II. Assume that h(α) = 1. Note that, this case is not verified, there is no
formula whose negation takes the value of 1.
III. Assume that h(α) = 2. Given that h(α) = h(¬β) = ¬h(β), we have that
¬h(β) = 2. By the table of negation, h(β) = 0. Note that β has less
complexity than α, then by induction hypothesis β 6∈ ∆ and •β 6∈ ∆.
Given that β 6∈ ∆ by Lemma 3, ¬β ∈ ∆. So α ∈ ∆. On the other hand, we
have that •β 6∈ ∆ by Lemma 3, ¬ • β ∈ ∆. By Proposition 2(ii) and MP,
we conclude ¬ • ¬β ∈ ∆.
Case2 implication. Let α = β → γ, for some formulas β, γ. We analyze three
cases.
I. Assume that h(α) = 0. Given that h(α) = h(β → γ) = h(β) → h(γ), we
have that h(β) → h(γ) = 0. By the table of implication, we analyze two
cases.
(a) h(β) = 1, h(γ) = 0. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β ∈ ∆ and γ 6∈ ∆, •γ 6∈ ∆. Given
that β ∈ ∆ and γ 6∈ ∆ by Lemma 3, ¬¬β ∧ ¬γ ∈ ∆, applying the
Proposition 2(iii) and MP we get ¬(β → γ) ∈ ∆. On the other hand,
we have •β ∈ ∆ and •γ 6∈ ∆ by Lemma 3 we have •β ∧ ¬ • γ ∈ ∆
applying the Proposition 2(iv) and MP we get ¬ • (β → γ) ∈ ∆, i.e.
•(β → γ) 6∈ ∆.
(b) h(β) = 2, h(γ) = 0. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β 6∈ ∆ and γ 6∈ ∆, •γ 6∈ ∆. This case
is similar to the previous one applying the Proposition 2(v).
II. Assume that h(α) = 1. Given that h(α) = h(β → γ) = h(β) → h(γ), we
have that h(β) → h(γ) = 1. By the table of implication, we analyze one
case.
(a) h(β) = 2, h(γ) = 1. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β 6∈ ∆ and γ ∈ ∆, •γ ∈ ∆. Given that
β ∈ ∆ and γ ∈ ∆ then by Lemma 3, β ∧ γ ∈ ∆, applying Proposition
2(vi) and MP we conclude that β → γ ∈ ∆. On the other hand, we
have that β ∈ ∆ and •γ ∈ ∆ then β ∧ •γ ∈ ∆ by Lemma 3. Then
applying Proposition 2(vii) and MP we obtain, •(β → γ) ∈ ∆.
III. Assume that h(α) = 2. Given that h(α) = h(β → γ) = h(β) → h(γ), we
have that h(β) → h(γ) = 2. By the table of implication, we analyze three
cases.
(a) h(β) = 0. Note that β has less complexity than α, then by induction
hypothesis β 6∈ ∆ and •β 6∈ ∆. Then ¬β ∧ ¬ • β ∈ ∆. Then applying
Proposition 2(viii) and MP we obtain, (β → γ) ∈ ∆, On the other
hand, we have that ¬β ∈ ∆, then applying Proposition 2(ix) and MP
we obtain, ¬ • (β → γ) ∈ ∆ i.e. •(β → γ) 6∈ ∆.
(b) h(γ) = 2. Note that γ has less complexity than α, then by induction
hypothesis γ ∈ ∆, •γ 6∈ ∆. Note that γ ∈ ∆, applying Ax1 and MP
we obtain, ¬(β → γ) ∈ ∆. On the other hand, ¬ • γ ∈ ∆, applying
Proposition 2(x) and MP we obtain, ¬•(β → γ) ∈ ∆ i.e. •(β → γ) 6∈ ∆.
127
(c) h(β) = 1, h(γ) = 1. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β ∈ ∆ and γ ∈ ∆, •γ ∈ ∆. Given
that β ∈ ∆ and γ ∈ ∆, then β ∧ γ ∈ ∆. Applying Proposition 2(vi)
and MP we obtain, (β → γ) ∈ ∆. On the other hand, (•β ∧ •γ) ∈ ∆
and applying Proposition 2(xi) and MP we obtain, ¬ • (β → γ) ∈ ∆
i.e. •(β → γ) 6∈ ∆.
Case3 conjunction. Let α = β ∧ γ, for some formulas β, γ. We analyze three
cases.
I. Assume that h(α) = 0. Given that h(α) = h(β ∧ γ) = h(β) ∧ (γ), we have
that h(β) ∧ h(γ) = 0. By the table of conjunction, we analyze two cases.
(a) h(β) = 0. Note that β has less complexity than α, then by induction
hypothesis β 6∈ ∆ and •β 6∈ ∆. Given that β 6∈ ∆, then ¬β ∈ ∆,
applying Proposition 2(xii) and MP we obtain, ¬(β ∧ γ) ∈ ∆. There-
fore, (β ∧ γ) 6∈ ∆. On the other hand, given that β 6∈ ∆ and •β 6∈ ∆,
then ¬β ∧ ¬ • β ∈ ∆, applying Proposition 2(xiii) and MP we obtain,
¬ • (β ∧ γ) ∈ ∆
(b) h(γ) = 0. Note that γ has less complexity than α, then by induction
hypothesis γ 6∈ ∆ and •γ 6∈ ∆. Given that γ 6∈ ∆, then ¬γ ∈ ∆.
Applying Proposition 2(xiv) and MP we obtain, ¬(β ∧ γ) ∈ ∆, so
(β ∧ γ) ∈ ∆. On the other hand, ¬γ ∈ ∆ and •γ 6∈ ∆, then ¬γ ∧ ¬ • γ ∈
∆, applying Proposition 2(xv) and MP we obtain, ¬ • (β ∧ γ) ∈ ∆.
Therefore, •(β ∧ γ) 6∈ ∆.
II. Assume that h(α) = 1. Given that h(α) = h(β ∧ γ) = h(β) ∧ h(γ), we have
that h(β) ∧ h(γ) = 1. By the table of conjunction, we analyze three cases.
(a) h(β) = 1, h(γ) = 1. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β ∈ ∆ and γ ∈ ∆, •γ ∈ ∆. Given
that β ∈ ∆ and γ ∈ ∆ then β ∧ γ ∈ ∆. On the other hand •β ∈ ∆ and
•γ ∈ ∆, then •β ∧ •γ ∈ ∆. Applying Proposition 2(xvi) and MP we
obtain, •(β ∧ γ) ∈ ∆.
(b) h(β) = 1, h(γ) = 2. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β ∈ ∆ and γ ∈ ∆, •γ 6∈ ∆. Given
that β ∈ ∆ and γ ∈ ∆ then β ∧ γ ∈ ∆. On the other hand, given that
•β ∈ ∆, γ ∈ ∆ and ¬ • γ ∈ ∆ then •β ∧ γ ∧ ¬ • γ ∈ ∆. Applying
Proposition 2(xvii) and MP we obtain, •(β ∧ γ) ∈ ∆.
(c) h(β) = 2, h(γ) = 1. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β 6∈ ∆ and γ ∈ ∆, •γ ∈ ∆. This case
is similar to the previous one applying the Proposition 2(xviii).
III. Assume that h(α) = 2. Given that h(α) = h(β ∧ γ) = h(β) ∧ h(γ), we have
that h(β) ∧ h(γ) = 2. By the table of conjunction, we analyze one case.
(a) h(β) = 2, h(γ) = 2. Note that β and γ has less complexity than α, then
by induction hypothesis β ∈ ∆, •β 6∈ ∆ and γ ∈ ∆, •γ 6∈ ∆. Given
that β ∈ ∆ and γ ∈ ∆ then β ∧ γ ∈ ∆. On the other hand, ¬ • β ∈ ∆
and ¬ • γ ∈ ∆ then ¬ • β ∧ ¬ • γ ∈ ∆. Applying Proposition 2(xix) and
MP we obtain, ¬ • (β ∧ γ) ∈ ∆. Hence •(β ∧ γ) 6∈ ∆.
128
Theorem 4. Let Γ ∪ {ϕ} ⊆ LΣ , with Γ maximal non-trivial with respect to ϕ
in CG03 . The mapping v : LΣ → {0, 1, 2} defined by:
v(ψ) ∈ {1, 2} if and only if ψ ∈ Γ
for all ψ ∈ LΣ , is a valuation for CG03 .
Proof. The demonstration is straightforward. It suffices prove that v satisfies all
the clauses of Definition 13
The completeness of CG03h is then an immediate consequence of Theorem 4
and Theorem 3.
Corollary 1 (Completeness of CG03h ). For every Γ ∪ {ϕ} ⊆ LΣ :
If Γ |=CG03 ϕ then Γ `CG03h ϕ.
Proof. Assume that Γ 6`CG03 ϕ by Theorem 3, let ∆ be a maximal non-trivial
set with respect to ϕ in CG03 extending Γ . By Theorem 4, there is an CG03 -
valuation v, such that v[Γ ] ⊆ {1, 2} as Γ ⊆ ∆, but v(ϕ) = 0 as ϕ 6∈ ∆. Therefore,
Γ 6|=CG03 ϕ and the theorem follows by contraposition.
5 Conclusions
The logic CG03 was first developed by Osorio et al., in 2014 [5]. CG03 is defined by
its many-valued semantics the matrix of CG03 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∗ = {1, 2}.
This logic is a paraconsistent logic that can be viewed as an extension of the well-
known logic G03 also introduced by Osorio, in 2008 [6]. A Kripke-type semantics
for CG03 was later developed, by Borja et al., in 2016 [3]. Recently in 2019,
Pérez-Gaspar et al. gave an axiomatization Hilbert type for CG03 using the
Kalmár technique [8]. In this paper, we extend studies on this logic by presenting
some results relating deductive notions with its model-theoretic counterparts. We
summarize results in this paper as follows.
– We developed a Hilbert-type axiomatization inspired by the Lindenbaum-
Los technique.
– Soundness is also proved.
– The main result of the paper is a completeness proof. Contrastingly with
the proof using Kalmár’s technique, this proof is based on maximal theories
concerning a sentence.
References
1. Carnielli, W.A., Coniglio, M.E.: Paraconsistent logic: Consistency, contradiction
and negation. Springer (2016)
129
2. Gottwald, S.: Many-valued logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia
of Philosophy. Metaphysics Research Lab, Stanford University, winter 2017 edn.
(2017)
3. Macı́as, V.B., Pérez-Gaspar, M.: Kripke-type semantics for cg30 . Electronic Notes
in Theoretical Computer Science 328, 17–29 (2016)
4. Malinowski, G.: Many-Valued Logics. Oxford University Press (1993)
5. Osorio, M., Carballido, J.L., Zepeda, C., et al.: Revisiting Z. Notre Dame Journal
of Formal Logic 55(1), 129–155 (2014)
6. Osorio Galindo, M., Carballido Carranza, J.L.: Brief study of g’3 logic. Journal of
Applied Non-Classical Logics 18(4), 475–499 (2008)
7. Priest, G., Tanaka, K., Weber, Z.: Paraconsistent logic. In: Zalta, E.N. (ed.) The
Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford Univer-
sity, summer 2018 edn. (2018)
8. Pérez-Gaspar, M., Hernández-Tello, A., Arrazola, J., Osorio, M.: An axiomatic
approach to CG03 , vol. . to appear, Oxford University Press (2019)
9. Wieckowski, B.: G. metcalfe, n. olivetti and d. gabbay. proof theory for fuzzy logics.
applied logic series, vol. 36. springer, 2009, viii+ 276 pp. Bulletin of Symbolic Logic
16(3), 415–419 (2010)
10. Wójcicki, R., Nauk, P.A., i Socjologii, I.F.: Lectures on propositional calculi. Os-
solineum Wroclaw (1984)
130