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