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 comprises 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.
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
context. In [
In 1954, F. Asenjo in his Ph.D. dissertation proposes for the rst time to
use Many-valued logics to generate paraconsistent logics (logics whose semantic
or proof-theoretic logical consequence relation is not explosive [
The CG03 logic is a three-valued paraconsistent logic of recentlyCdoepvyerilgohpte©d2019 for this paper by its authors. U
Attribution 4.0 International (CC BY 4.0)
by [
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 completeness theorem for CG03h, we use the Lindenbaum-Los technique on maximal theories. 2
We rst introduce the syntax of the logical formulas considered in this paper. We
follow common notation and basic de nitions as W. Carnielli and M. Coniglio
in [
De nition 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).
De nition 2 (Propositional language). Let V ar = fp1; p2; : : :g be a denumerable set of propositional variables, and let be any propositional signature. The propositional language generated by from V ar will be denoted by L . De nition 3 (Tarskian logic). A logic L de ned over a language L which has a consequence relation `, is Tarskian if it satis es the following three properties, for every [ [ f g L: (i) if 2 then ` ; (ii) if ` and then ` ; (iii) if ` and ` for every 2 then ` .
A logic satisfying item (ii) above is called monotonic. Moreover, a logic L is said to be nitary if it satis es the following: (iv) if ` then there exists a nite subset 0 of such that 0 ` .
A logic L de ned over a propositional language L generated by a signature from a set of propositional variables is called structural if it satis es the following property: (v) if ` then [ ] ` [ ], for every substitution of formulas for variables.
A propositional logic is standard if it is Tarskian, nitary, and structural.
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 nite 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 fXig, if Xi is a formula.
De nition 4 (Paraconsistent logic). A Tarskian logic L is paraconsistent if it has a (primitive or de ned) negation : such that ; : 6`L for some formulas and in the language of L .
The most adequate manner to de ne the many-valued semantics of logic
is through a matrix. We introduce the de nition of the deterministic matrix,
also known as the logical matrix or simply as a matrix. In [
De nition 6 (Interpretation). Given a logic L in the language L, an interpretation 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 de ne the notion of validity in this type of semantics as follows: De nition 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(') 2 D , and we denote it as t j=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 de nition: De nition 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 j=L '.
If ' is a tautology in the logic L , we say that ' is an L -tautology. When logic is de ned via a many-valued semantics, it is usual to de ne the set of theorems of L as the set of tautologies obtained from the many-valued semantics, i.e. ' 2 L if and only if j=L '.
3 In this section, we present a summary of the state of the art of logic CG'3. Starting with the many-valued semantics de ned by Osorio et al. and ending with Kripke semantics of the CG03 logic as well as some important results proposed by Borja and Perez-Gaspar.
The logic CG03 was introduced in [
De nition 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) j=G03 '.
Lemma 1. Let ' be a formula in the language of CG03, then: j=CG03 ' if and only if for any Kripke model M for CG03 it holds that ' is e-valid. 1 We use the symbol j= to de ne the modeling relation and avoid confusion with the symbol j= that is used for tautologies.
3 In this section, we present an axiomatization for the CG03 logic. We begin by de ning a formal axiomatic theory whose language has four connective, bottom formula, conjunction, disjunction, and implication. Note that the connective disjunction is determined by the primitive connective.
Let CG03h be a formal axiomatic theory for CG03 logic de ned over the signature = f?; ^; !; :g, we de ne 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 . De nition 11 (CG03h). The logic CG03h is de ned over the language L the Hilbert calculus: Axiom schemas: by (
! ( ! ) Ax1 ! ( ! )) ! (( ! ) ! ( ! )) Ax2 ( ^ ) ! Ax3 ( ^ ) ! Ax4 ! ( ! ( ^ )) Ax5 ! ( _ ) Ax6 ! ( _ ) Ax7 ( ! ) ! (( ! ) ! ( _ ) ! ) Ax8 ( ! ) _ Ax9
_ : Ax10 :' ! (::' ! ) Ax11
! Ax12 Inference rule: !
MP De nition 12 (Derivation). Let [f'g L be a set of formulas. A derivation of ' from in CG03h is a nite 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 2 , 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 exists a derivation of ' from
in CG03h, denoted by in CG03h.
`CG03h ', if there
The following meta-theorems of CG03h will prove to be quite useful, their demonstrations are straightforward.
Proposition 1. The calculus CG03h satis es the following properties: (i) ; (ii) If ; (iii) If ;
i `CG03h `CG03h ' and `CG03h ' and ; : `CG03h ;
! (Deduction meta-theorem, DMT). `CG03h ' then ; _ `CG03h '.
`CG03h ' then `CG03h ' (Proof-by-cases).
Proof.
(i) To prove that a Hilbert calculus satis es DMT, it su ces 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.
De nition 13 (Valuations for CG03). A function v : L ! f0; 1; 2g is a valuation for CG03, or a CG03-valuation, if it satis es the following clauses: v(: ) = 0 when v( ) = 2 v( ^ ) 2 f1; 2g i v( ) 2 f1; 2g and v( ) 2 f1; 2g v( ! ) 2 f1; 2g i v( ) = 0 or v( ) = 2 or
v( ) = v( ) = 1 or v( ) = 2; v( ) = 1 The set of all such valuations will be designated by V CG03 .
For every [f'g L , the following semantical consequences relation w.r.t. the set V CG03 of CG03-valuations can be de ned:
j=CG03 ' if and only if, for every v 2 V CG03 ; if v( ) 2 f1; 2g for every 2 then v(') 2 f1; 2g: Theorem 2 (Soundness). For every [ f'g
L : If `CG03h ' then j=CG03 ': Proof. It su ces to verify that each axiom schema is a tautology in CG03 and if and are formulas such that v( ), v( ! ) 2 f1; 2g then v( ) 2 f1; 2g i.e. MP preserves tautologies.
The proof of completeness needs some de nitions and results related to Tarskian Logic, see de nition 3.
De nition 14 (Maximal set). For a given Tarskian logic L over the language L, let [ f'g L. The set is maximal non-trivial with respect to ' in L if 6`L ' but ; ` ' for any 2= . De nition 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 2 .
Lemma 2. Any set of formulas maximal non-trivial with respect to ' in L is closed, provided that L is Tarskian.
Proof. Straightforward from De nition 3 and De nition 14.
Theorem 3 (Lindenbaum-Los). Let L be a Tarskian and nitary logic over the language L. Let [ f'g 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 nitary because CG03h is de ned by a Hilbert calculus, so Theorem 3 holds. On the other hand, the following properties it holds: Lemma 3. If for every formulas is a maximal non-trivial set with respect to ' 2 CG03h, then
and , satis es the following properties: (i) (ii) ( (iii) ( (iv) `CG03h if and only if _ ) 2 if and only if ^ ) 2 if and only if 2 if and only if : 62 2 . 2 or 2 . 2 and 2 .
if and only if ::
Proof. The proof of each item can be seen in [
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) (' ^ : ' ^ ) ! (' ^ ) ) ) ) (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 2 L where is a maximal non-trivial set with respect to ' 2 CG03h. Then for all is veri ed:
8 0 i p 62 h(p) = < 1 i p 2 : 2 i p 2 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 by de nition.
= p, where p is a propositional variable, then a rmation holds Induction hypothesis. Assume that the statement is veri ed 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 62 ; 62 h( ) = 1 if and only if 2 ; 2 h( ) = 2 if and only if 2 ; 62
Note that it is su cient 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 rst condition on the right side of the statement holds for a formula, then the other two conditions are false and therefore h( ) 2= f1; 2g. 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 2 and 62 . Given that 2 by Lemma 3, : 62 . So 62 . On the other hand, we have that 62 by Lemma 3, : 2 . By Proposition 2(ii) and MP, we conclude : : 2 . II. Assume that h( ) = 1. Note that, this case is not veri ed, 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 62 and 62 . Given that 62 by Lemma 3, : 2 . So 2 . On the other hand, we have that 62 by Lemma 3, : 2 . By Proposition 2(ii) and MP, we conclude : : 2 .
Case2 implication. Let cases.
=
! , for some formulas , . We analyze three 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 2 , 2 and 62 , 62 . Given that 2 and 62 by Lemma 3, :: ^ : 2 , applying the Proposition 2(iii) and MP we get :( ! ) 2 . On the other hand, we have 2 and 62 by Lemma 3 we have ^ : 2 applying the Proposition 2(iv) and MP we get : ( ! ) 2 , i.e. ( ! ) 62 . (b) h( ) = 2; h( ) = 0. Note that and has less complexity than , then by induction hypothesis 2 , 62 and 62 , 62 . 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 2 , 62 and 2 , 2 . Given that 2 and 2 then by Lemma 3, ^ 2 , applying Proposition 2(vi) and MP we conclude that ! 2 . On the other hand, we have that 2 and 2 then ^ 2 by Lemma 3. Then applying Proposition 2(vii) and MP we obtain, ( ! ) 2 .
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 62 and 62 . Then : ^ : 2 . Then applying Proposition 2(viii) and MP we obtain, ( ! ) 2 , On the other hand, we have that : 2 , then applying Proposition 2(ix) and MP we obtain, : ( ! ) 2 i.e. ( ! ) 62 . (b) h( ) = 2. Note that has less complexity than , then by induction hypothesis 2 , 62 . Note that 2 , applying Ax1 and MP we obtain, :( ! ) 2 . On the other hand, : 2 , applying Proposition 2(x) and MP we obtain, : ( ! ) 2 i.e. ( ! ) 62 . (c) h( ) = 1; h( ) = 1. Note that and has less complexity than , then by induction hypothesis 2 , 2 and 2 , 2 . Given that 2 and 2 , then ^ 2 . Applying Proposition 2(vi) and MP we obtain, ( ! ) 2 . On the other hand, ( ^ ) 2 and applying Proposition 2(xi) and MP we obtain, : ( ! ) 2 i.e. ( ! ) 62 .
Case3 conjunction. Let cases.
=
^ , for some formulas , . We analyze three 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 62 and 62 . Given that 62 , then : 2 , applying Proposition 2(xii) and MP we obtain, :( ^ ) 2 . Therefore, ( ^ ) 62 . On the other hand, given that 62 and 62 , then : ^ : 2 , applying Proposition 2(xiii) and MP we obtain, : ( ^ ) 2 (b) h( ) = 0. Note that has less complexity than , then by induction hypothesis 62 and 62 . Given that 62 , then : 2 . Applying Proposition 2(xiv) and MP we obtain, :( ^ ) 2 , so ( ^ ) 2 . On the other hand, : 2 and 62 , then : ^ : 2 , applying Proposition 2(xv) and MP we obtain, : ( ^ ) 2 .
Therefore, ( ^ ) 62 .
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 2 , 2 and 2 , 2 . Given that 2 and 2 then ^ 2 . On the other hand 2 and 2 , then ^ 2 . Applying Proposition 2(xvi) and MP we obtain, ( ^ ) 2 . (b) h( ) = 1; h( ) = 2. Note that and by induction hypothesis 2 , 2 that and then has less complexity than , then
and 2 , 62 . Given 2 2 ^ 2 . On the other hand, given that 2 , 2 and : 2 then ^ ^ : 2 . Applying Proposition 2(xvii) and MP we obtain, ( ^ ) 2 . (c) h( ) = 2; h( ) = 1. Note that and has less complexity than , then by induction hypothesis 2 , 62 and 2 , 2 . 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 2 , 62 and 2 , 62 . Given that 2 and 2 then ^ 2 . On the other hand, : 2 and : 2 then : ^ : 2 . Applying Proposition 2(xix) and MP we obtain, : ( ^ ) 2 . Hence ( ^ ) 62 .
in CG03. The mapping v : L
L , with maximal non-trivial with respect to ' ! f0; 1; 2g de ned by: v( ) 2 f1; 2g if and only if 2 for all
2 L , is a valuation for CG03.
Proof. The demonstration is straightforward. It su ces prove that v satis es all the clauses of De nition 13
The completeness of CG03h is then an immediate consequence of Theorem 4 and Theorem 3.
Corollary 1 (Completeness of CG03h). For every [ f'g
L : If j=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 CG03valuation v, such that v[ ] f1; 2g as , but v(') = 0 as ' 62 . Therefore, 6j=CG03 ' and the theorem follows by contraposition. 5
The logic CG03 was rst developed by Osorio et al., in 2014 [
{ 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 Kalmar's technique, this proof is based on maximal theories concerning a sentence.