We introduce a new 5-valued logic that we call N50 . This logic extends GLukG, a paraconsistent logic recently introduced [10]. We show that N50 is sound with respect to GLukG. GLukG paraconsistent logic has been investigated for a short period of time [5,10]. However, it has demonstrated important qualities for the study of other logics. It also has relevant attributes in knowledge representation [11]. Although, this work does not address this last point. On this paper, we investigate how to add a strong negation connective to GLukG logic. The logic that is of our interest is a 5-valued logic that is sound with respect to GLukG. In this case we use two kinds of negations, one is the strong negation represented by the symbol and the other one is the default negation represented by the : symbol. In the literature we can nd several logical extension, through a strong negation operator, but few of them are hardly paraconsistent logics satisfy a theorem of substitution, to see [3]. To summarize, the main contribution of the paper is the proposal of the paraconsistent 5-valued logic called N50 that satis es the following suitable properties: (1) It is a conservative extension of GLukG logic. (2) It satis es the substitution theorem. The structure of our paper is as follows. Section 2 describes the general background needed for the paper including the de nition of GLukG logic. On Section 3 we present a Hilbert-style axiomatization for GLukG which is a slight variation of the one presented in [10]. On Section 4 we present Theorem 4, our main result, which establishes that our logic N50 is a conservative extension of Nelson's N5. Finally, on Section 5 we present our conclusions and we address the future work.
meaning of such formulas in order to, nally, give a brief introduction to several of the logics that are relevant for the results of our later sections. 2.1
Syntax of formulas We consider a formal (propositional) language built from: an enumerable set L of elements called atoms (denoted a, b, c, . . . ); the binary connectives ^ (conjunction), _ (disjunction) and ! (implication); and the unary connective : (negation). Formulas (denoted , , , . . . ) are constructed as usual by combining these basic connectives together with the help of parentheses.
We also use $ to abbreviate ( ! ) ^ ( ! ) and to abbreviate ! . It is useful to agree on some conventions to avoid the use of so many parenthesis in writing formulas. This will make the reading of complicated expressions easier. First, we may omit the outer pair of parenthesis of a formula. Second, the connectives are ordered as follows: :; ^; _; !, and $, and parentheses are eliminated according to the rule that, rst, : applies to the smallest formula following it, then ^ is to connect the smallest formulas surrounding it, and so on.
A theory is just a set of formulas and, in this paper, we only consider nite theories. Moreover, if T is a theory, we use the notation LT to stand for the set of atoms that occur in the theory T , if T = f g we denote L . A literal l is either an atom or the negation of an atom. 2.2
Logic systems We consider a logic simply as a set of formulas that, moreover, satis es the following two properties: (i) is closed under modus ponens (i.e. if and ! are in the logic, then so is ) and (ii) is closed under substitution (i.e. if a formula is in the logic, then any other formula obtained by replacing all occurrences of an atom b in with another formula is still in the logic). The elements of a logic are called theorems and the notation `X is used to state that the formula is a theorem of X (i.e. 2 X). We say that a logic X is weaker than or equal to a logic Y if X Y , similarly we say that X is stronger than or equal to Y if Y X.
Hilbert style proof systems There are many di erent approaches that have been used to specify the meaning of logic formulas or, in other words, to de ne logics. In Hilbert style proof systems, also known as axiomatic systems, a logic is speci ed by giving a set of axioms (which is usually assumed to be closed by substitution). This set of axioms speci es, so to speak, the `kernel' of the logic. The actual logic is obtained when this `kernel' is closed with respect to the inference rule of modus ponens. The notation `X F for provability of a logic formula F in the logic X is usually extended within Hilbert style systems; given a theory T , we use T `X F to denote the fact that the formula F can be derived from the axioms of the logic and the formulas contained in T by a sequence of applications of modus ponens1. Recall that, in all these de nitions, the logic connectives are parameterized by some underlying logic, e.g. the expression `X (F1 ^ ^ Fn) ! F actually stands for `X (F1 ^X ^X Fn) !X F .
C! logic [
Pos1
Pos2
Pos3
Pos4
Pos5
Pos6
Pos7
Pos8
C!1
C!2
a ! (b ! a)
(a ! (b ! c)) ! ((a ! b) ! (a ! c))
a ^ b ! a
a ^ b ! b
a ! (b ! (a ^ b))
a ! (a _ b)
b ! (a _ b)
(a ! c) ! ((b ! c) ! (a _ b ! c))
a _ :a
::a ! a
Note that the rst 8 axioms somewhat constraint the meaning of the !, ^ and
_ connectives to match our usual intuition. It is a well known result that in any
logic satisfying axioms Pos1 and Pos2, and with modus ponens as its unique
inference rule, the Deduction Theorem holds [
Multivalued logics An alternative way to de ne the semantics for a logic is by the use of truth values and interpretations. Multivalued logics generalize the idea of using truth tables that are used to determine the validity of formulas in classical logic. The core of a multivalued logic is its domain of values D, where some of such values are special and identi ed as designated. Logic connectives (e.g. ^, _, !, :) are then introduced as operators over D according to the particular de nition of the logic.
An interpretation is a function I : L ! D that maps atoms to elements in the domain. The application of I is then extended to arbitrary formulas by mapping rst the atoms to values in D, and then evaluating the resulting expression in terms of the connectives of the logic (which are de ned over D). A formula is said to be a tautology if, for every possible interpretation, the formula evaluates to a designated value. The most simple example of a multivalued logic is classical logic where: D = f0; 1g, 1 is the unique designated value, and connectives are de ned through the usual basic truth tables. If X is any logic, we write j=X to denote that is a tautology in the logic X. We say that is a logical consequence of a set of formulas = f'1; '2; : : : ; 'ng (denoted by j=X ) if V ! is a tautology, where V stands for '1 ^ '2 ^ : : : ^ 'n.
Note that in a multivalued logic, so that it can truly be a logic, the implication connective has to satisfy the following property: for every value x 2 D, if there is a designated value y 2 D such that y ! x is designated, then x must also be a designated value. This restriction enforces the validity of modus ponens in the logic. The inference rule of substitution holds without further conditions because of the functional nature of interpretations and how they are evaluated.
Given a theory T , we de ne the negation of the theory :T as f:F j F 2 T g (the negation symbol is parameterized with respect to some given logic). For 1 We drop the subscript X in `X when the given logic is clear from the context. any pair of theories T and U , we use T `X U to state that T `X F for every formula F 2 U . 3
We present the Hilbert-style axiomatization of GLukG that is a slight
(equivalent) variant of the one presented in [
GLukG Logic has all the axioms of C! logic plus the following: := := (( ! ) ! ) ^ (( ! ) !
! (: ^ :: ). := ( ! ) ^ ( ! ).
). (: ! : ) $ (:: ! :: ) ::( ! ) $ (( ! ) ^ (:: ::( ^ ) $ (:: ^ :: ) ( ^ : ) ! ( ! ) ! :: )) 1. 2. 3.
_ $ E1 E2 E3
E4
Note that Classical logic is obtained from GLukG by adding to the list of
axioms any of the following formulas: !:: ; !(: ! ); (: !: )!( ! ).
It is shown in [
Theorem 1 ([
In this paper we consider the standard substitution, here represented with the usual notation: '[ =p] will denote the formula that results from substituting the formula for the atom p, wherever it occurs in '. Recall the recursive de nition: if ' is atomic, then '[ =p] is when ' equals p, and ' otherwise. Inductively, if ' is a formula '1#'2, for any binary connective #. Then '[ =p] will be '1[ =p]#'2[ =p]. Finally, if ' is a formula of the form :'1, then '[ =p] is :'1[ =p]. 3.1
Multivalued logic
It is very important to note that GLukG can also be presented as a multivalued
logic. Such presentation is given in [
In this paper we keep the notion G03 to refer to multivalued logic just de ned and we use the notion GLukG to refer as the Hilbert system de ned at the beginning of this section.
Theorem 2 (Substitution theorem for G03-logic [
Corollary 1 ([
We present N 50, a 5-valued logic. We will use the set of values f 2; 1; 0; 1; 2g. Valid formulas evaluate to 2. The connectives ^ and _ correspond to the min and max functions in the usual way. For the other connectives, the associated truth tables are as follows:
We have de ned 5 logical connectives, namely Nc := f!; ^; _; :; g. N formulas are built from these set of connectives. If always evaluates to the designated value then it is called a tautology.
Remark 1. Observed the following: 1: j= 2: j= 3: j= 4: j= 5: j= 6: j= ( ! ) $ ( ^ )$ ( _ )$ $ : : $ :: : ! : : ^ _ ^ : : : 7: j= : 8: j= 9: 2 10: 2 11: 2 : 12: 2 :
! ((: ! ((: ! ((: ! ((: ! ((: ! ((:
! ) ! ! ) ! : ): ! ) ! ): ! ) ! : ! ) ! : ! )! ): ): ): ):
What is important about this remark is that these formulae have the same
structure than those theorems of Nelson introduced previously in [
Theorem 3. Given and two formulae, then: 1. If and ! are tautologies, then is also a tautology.
2. If is a tautology, then :: is also a tautology.
Proof. The proof of 1 is straightforward; If and ! are tautologies, then they always evaluate to the designated value and, looking at the implication table given for N50 , we see that (since evaluates to 2) there is only one case in which ! evaluates to 2, and it is precisely when evaluates to 2. This concludes the proof of 1.
To prove 2, we see that if also evaluates to 2.
evaluates to 2, then ::
Note: N50 logic is in some way similar to N5 logic (see [
Theorem 4. N50 logic can express N5 logic.
Proof. It su ces to see that we can express the constant ? of N5 by the formula :a ^ ::a of N50 , where a is any formula. Hence, we can also express the : formula of N5 by ! ? in N50 .
Lemma 1. Let I be an interpretation (based on G03). Let JI be an interpretation (based on N50 ) de ned for every atom a as follows:
Then, for every GL-formula ,
JI (a) = JI ( ) =
I(a) if I(a) > 0
2 otherwise I( ) if I( ) > 0 < 0 otherwise Proof. The proof is by induction on the number n of ocurrences of !; ^; _; :; : if n = 0, is just an atom a, the proof is followed by de nition of JI . Assume now that lemma holds for all j n.
Case 1. is : . Then has fewer than n connectives. 1a. 0 < I( ) then I( ) = 2, hence I( ) = 1 or I( ) = 0. If I( ) = 1, by inductive hypothesis, we have that JI ( ) = I( ) = 1 so JI ( ) = JI (: ) = 2 = I( ): 1b. I( ) = 0, this subcase is analogous to subcase 1a.
Case 2. is ! . Then and have fewer than n connectives. 2a. 0 < I( ) then I( ) = 1 or I( ) = 2. i) Assume 1 = I( ), so I( ) = 2 and I( ) = 1. By inductive hypothesis, JI ( ) = I( ) = 2 and JI ( ) = I( ) = 1 thus JI ( ) = 1 = I( ). ii) If I( ) = 2 is worked analogously the previous subcase. 2b. I( ) = 0, we have by inductive hypothesis 0 < I( ) = JI ( ) and I( ) = JI ( ) < 0, so JI ( ) < 0.
Case 3. is ^ . Then and have fewer than n connectives. 3a. 0 < I( ) then by inductive hypothesis 0 < I( ) = minfI( ); I( )g = minfJI ( ); JI ( )g = JI ( ). 3b. I( ) 0 is similar to subcase 3a.
Finally, the case is _ is proved analogously.
A very important result is that N50 logic is a conservative extension of G03 logic, as the following theorem shows.
Theorem 5. For every GL-formula , is a tautology in N50 i in G03. is a tautology Proof. Suppose that is a tautology in G03, then by Theorem 1, is a theorem in GLukG. We proceed by induction on the length of the proof of . The base case is immediate from the fact that all GLukG axioms are tautologies in N50 . We suppose that any proposition, that has a proof with at most n steps, satis es the induction hypothesis.
Let be a proposition whose proof requires exactly n steps and let be B1; : : : ; Bn, a proof of . We are done if Bn = is a GLukG axiom. If is a Modus Ponens consequence, then by Theorem 3, if and ! are tautologies, then is tautology. This observation and the inductive hypothesis nish the proof.
For the other implication we suppose that is not a tautology in G03, then there exists an interpretation I (based on G03) such that I( ) 6= 2. By Lemma 1, there exists JI , an interpretation based on N50 , such that JI ( ) 6= 2. Hence, is not a tautology of N50 , as desired. 4.1
Substitution A particular feature of our N50 logic is that the symbol $ does not de ne a congruential relation on formulas, note that it can be the case that $ is a tautology, but $ doesn't. A particular example is the following: Take 1 to be (a ! b) and 2 to be a^ b. Clearly 1 $ 2 is a tautology, but 1$ 2 does not (take I(a) = I(b) = 1). This property also holds in N5.
Thus, when we refer to equivalence of formulas, we will have to be more precise and make some particular considerations. The term weak equivalence will mean that $ is a tautology. There is a stronger notion of equivalence of N-formulas, which we will call N50 -equivalence, and it holds when both $ and $ are tautologies. For this purpose, we de ne a new connective ,. We write , to denote the formula: ( $ ) ^ ( $ ). The reader can easily verify that $ is a tautology i for every valuation v, v( ) > 0 implies v( ) = v( ), while , is a tautology i for every valuation v, v( ) = v( ). This can be seen in the following truth tables: Theorem 6 (Basic Substitution theorem). Let , and let p be an atom. If , is a tautology then [ =p]$
Proof. If , is tautology then for every v, an N -valuation, v( ) = v( ) (see the comments at the end of the previous paragraph). Therefore, v( [ =p]) = [ =p]) so, v( [ =p] $ [ =p]) = 2.
To be able to apply standard substitution we require N50 -equivalence of formulas to hold. However, in certain cases this condition may be too strong. We are also interested in the particular cases where weak equivalence of formulas su ces for substituting. The rst such case is when substitution is not done inside the scope of a symbol.
Lemma 2. Let , and be N-formulas and let p be an atom such that p does not occur in within the scope of a symbol. If $ is a tautology then [ =p] $ [ =p] is a tautology.
Proof. It is of high importance to remember (see the comments at the end of the rst paragraph) that: $ is a tautology i for every valuation v, v( ) > 0 implies v( ) = v( ). By structural induction: Base case:
If = q, q an atom, we have: [ =p] $ [ =p] =
$ (q $ q if p 6= q if p = q; (hypothesis) therefore it is a tautology.
We suppose that the inductive case is satis ed: If = :'
By inductive hypothesis, for every N05-valuation, '[ =p] $ '[ =p] is a tautology. If 0 < v('[ =p]) then v(:'[ =p]) = v(:'[ =p]), therefore [ =p] $ [ =p] is a tautology.
Remark 2. If v('1) 0 and v('2)
0 implies v('1 ! '2) = 2 If = '1 ^ '2
Suppose that 0 < v(('1^'2)[ =p]) then, 0 < minfv('i[ =p])gi=1;2: Hence, by the inductive hypothesis v( i[ =p]) = v( i[ =p]) for i = 1; 2. Then v( [ =p]) = minfv('i[ =p])gi=1;2 = minfv('i[ =p])gi=1;2 = v( [ =p]). Therefore [ =p] $ [ =p] is a tautology. = '1 ! '2
Remember that by inductive hypothesis we have '1[ =p] $ '1[ =p] and '2[ =p] $ '2[ =p] are tautologies.
Suppose that 0 < v( [ =p]) = v('1[ =p] ! '2[ =p]).
We have two cases in which we can apply the inductive hypothesis: 1. v('1[ =p]) > 0 then by inductive hypothesis, we have v('1[ =p]) = v('1[ =p]), then 0 < v('2[ =p]), again by inductive hypothesis v('2[ =p]) = v('2[ =p]), therefore v('1[ =p] ! '2[ =p]) = v('1[ =p] ! '2[ =p]). 2. v('2[ =p]) > 0 then v('2[ =p]) = v('2[ =p]). Since '1[ =p] $ '1[ =p] and '2[ =p] $ '2[ =p] are tautologies, then we have that both '1[ =p] and '1[ =p] are negative or null (not necessarily in the same case). Finally v('1[ =p] ! '2[ =p]) = v('1[ =p] ! '2[ =p]). 4.2
Standard form We present the notion of a standard form of a formula.
De nition 1. We de ne the function S: N-formulae ! N-formulae as follows: If a is an atom and ' is an N-formula, then
S(a) = a; S(:a) = :a; S( a) = a; S( : ) = S(:: ); S(: ) = :S( );
S( ! ) = S( ) ! S( ); S( ^ ) = S( ) ^ S( ); S( ( ! )) = S( ) ^ S( S( ( ^ )) = S( ) _ S( S( ) = S( ): ); ); De nition 2 (Standard Form). An N-formula ' is said to be in standard form if S(') = '
Intuitively a formula is in standard form if it has all occurrences of the connective just in front of an atom.
Example 1. Take the formula ' := (a ! :b)^ S(') := a ^ b^ c. c. Then its standard form is Lemma 3. For any N-formula ', ' is a tautology in N50 i S(') is a tautology in N50 .
Proof. By structural induction: Base case: It is vacuously true.
We suppose that the inductive case is satis ed:
= :' is a tautology i ' evaluates to sis, 2 = :S(') = S( ).
2; 1; 0 or 1 i , by inductive hypothe= '1 ^ '2 is a tautology i '1 and '2 have the same value, by inductive hypothesis, S( ) = S('1) ^ S('2) is tautology.
If = '1 ! '2 is tautology, we have two cases: 1.- if '1 has any of the values 2; 1 or 0 then by inductive hypothesis also S('1) the same value; hence it does not matter the value of value S('2) and S( ) = S('1 ! '2) = S('1) ! S('2) is a tautology, and reciprocally 2.- if the value of '1 is 1 or 2 then '2 has the same value, respectively; hence, by the inductive hypothesis we have S( ) is tautology.
If = ' is a tautology then by remark 1 and the inductive hypothesis we have that S( ) is a tautology.
Finally, if = :' is a tautology, then S( ) = S( :') = S(::') = S('), but :' ! ' is a tautology, then ' is tautology, hence by inductive hypothesis S(') is a tautology. 5
We introduce a family of paraconsistent logics extended by a strong paraconsistent negation operator. We study one particular logic, that we call N50 , and we show that it is sound with respect to N-GLukG. For future work one can consider the formal construction of non-monotonic semantics based on N50 . This seems to be an easy task thanks to the experience of the construction of the answer set semantics based on N5 logic.