Revisiting C1

Abstract

We show that logic C1 cannot be extended to a paraconsistent logic in which the substitution theorem is valid. We show with the help of an answer set programming (ASP) tool called clasp, that C1 is robust with respect to certain three valued paraconsistent logics with some desirable properties. In particular C1 is robust with respect to three-valued logic P2, a logic for which some of the De Morgan laws are valid.

Introduction

methodology sometimes could have limitations (see [ 8 ]), however it is useful to researchers interested in the study of logics, such as in our case.

One of the properties a logic can have and in which we are particularly interested is paraconsistency. Following Beziau [ 1 ], a logic is paraconsistent if it has a negation :, which is paraconsistent in the sense that a; :a 0 b, and at the same time has enough strong properties to be called a negation. Paraconsistent logics have important applications, speci cally [ 4 ] mention three applications in different elds: Mathematics, Arti cial Intelligence and Philosophy. In relation to the second one, the authors mention that in certain domains, such as the construction of expert systems, the presence of inconsistencies is almost unavoidable (see for example [ 11 ]). An application that has not been fully recognized is the use of paraconsistent logics in non-monotonic reasoning. In this sense [ 6,14 ] illustrate such novel applications. Thus, the research on paraconsistent logics is far from being over. A three-valued paraconsistent logic of particular interest to us is C1, which has been studied in [ 9 ].

In this paper, we present two results, rst we show that there is not paraconsistent logic that extends C1 and for which the substitution theorem holds, second we explain how to construct a program that obtains a paraconsistent three-valued logic, called P2 [ 3 ], such that the logic C1 is sound w.r.t. P2.

We take advantage of clasp since it allows us to de ne redundant constraints to de ne easily the primitive connectives as mathematical functions such as the _, :, ^, and !. For instance, in clasp we write

1fand(X; Y; Z) : v(Z)g1 v(X); v(Y ) instead of writing and(X; Y; Z) v(X); v(Z); v(Y ); not nothera(X; Y; Z). nothera(X; Y; Z) and(X; Y; Z1); Z! = Z1; v(X); v(Y ); v(Z); v(Z1). as we wrote in a preliminary work using DLV [ 16 ]. We also use the called conditions in clasp to de ne easily and brie y some constraints in our encoding. For instance, in clasp we write not f (X) : not sel(X) : v(X) instead of writing notf (1); f (2) as we wrote in [ 16 ]. Moreover in our clasp conditions we use not which is the negation as failure used in DLV.

Our paper is structured as follows. In section 2, we summarize some basic concepts and de nitions. In section 3, we show our results, a theorem and a clasp-encoding. Finally, in section 4, we present some conclusions. 2

Background

There are two ways to de ne a logic: by giving a set of axioms and specifying a set of inference rules; and by the use of truth values and interpretations. In this section we summarize each of them and we present some basic concepts and de nitions useful to understand this paper. 2.1

Hilbert style

In Hilbert style proof systems, also known as axiomatic systems, a logic is speci ed by giving a set of axioms and a set of inference rules. In these systems, it is common to use the notation ⊢X F for provability of a logic formula F in the logic X. In that case we say that F is a theorem of X.

We say that a logic X is paraconsistent if the formula (A ^ :A) ! B is not a theorem 2.

The relevance of logics for which the formula (A ^ :A) ! B is not a theorem, is that they are useful to de ne alternative semantics that can be applied in the study of non monotonic reasoning as we mentioned in the introduction section.

A very important property satis ed by many logics is the substitution theorem which we present now.

De nition 1. A logic X satis es the substitution theorem if: ⊢X $ 3 then ⊢X [ =p] $ [ =p] for any formulas , , and and any atom p that appear in where [ =p] denotes the resulting formula that is left after every occurrence of p is substituted by the formula .

As examples of axiomatic systems, we present three logics: the positive logic [ 12 ], the C! logic which is a paraconsistent logic de ned by daCosta [ 5 ], and C1 logic [ 9 ]. In Table 1 we present a list of axioms, the rst eight of them de ne positive logic. C! logic is de ned by the axioms of positive logic plus axioms C!1 and C!2. C1 logic is de ned by the axioms of C! plus the following two axioms: :1: B◦ ! ((A ! B) ! ((A ! :B) ! :A)) :2: A◦ ^ B◦ ! (A ^ B)◦ ^ (A _ B)◦ ^ (A ! B)◦ where B◦ = :(B ^ :B). 2 For any logic X that contains Pos1 and Pos2 (axioms of positive logic de ned in Table 1) among its axioms and Modus Ponens as its unique inference rule, the formula (A ^ :A) ! B is a theorem if and only if A; :A ⊢X B. 3 Here we use the notation ⊢X to indicate that the formula that follows is a theorem or a tautology depending on how the logic is de ned. 2.2

Multi-valued logics

An alternative way to de ne a logic is by the use of truth values and interpretations. Multi-valued logics generalize the idea of using truth tables to determine the validity of formulas in classical logic. The core of a multi-valued logic is its domain of values D, where some of such values are special and identi ed as designated or select values. Logic connectives (e.g. ^, _, !, :) are then introduced as operators over D according to the particular de nition of the logic, see [ 10 ].

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). It is understood in general that, if I is an interpretation de ned on the arbitrary formulas of a given program P , then I(P ) is de ned as the function I applied to the conjunction of all the formulas in P . A formula F is said to be a tautology, denoted usually by j= F if, for every possible interpretation, the formula F evaluates to a designated value. The simplest example of a multi-valued logic is classical logic where: D = f0; 1g, 1 is the unique designated value, and the connectives are de ned through the usual basic truth tables.

Note that in a multi-valued 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.

As an example of a multi-valued logic, we present the well known paraconsistent logic P2 [ 3 ] (also called Cive), a three-valued logic that is relevant in this work. The truth values of logic P2 are in the domain D = f0; 1; 2g where 1 and 2 are the designated values. The ^, _, !, and : connectives are de ned according to the truth tables given in Table 2. An interesting theoretical question that arises in the study of logics is whether a given logic satis es the substitution theorem [ 15 ]. It is well known that there are several paraconsistent logics for which that theorem is not valid [ 2 ]. We show that logic C1 can not be extended to a paraconsistent logic in which the substitution theorem is valid. In order to do this we provide a de nition and some results. De nition 2. A logic X satis es the weak substitution property if: then ⊢X : $ : . ⊢X $ Theorem 1. [ 13 ] Any logic stronger than C! satis es the weak substitution property iff satis es the substitution property.

The rst result of our paper is that C1 can not be extended to a paraconsistent logic in which the substitution theorem holds.

Theorem 2. Any extension of logic C1 to a logic where the substitution theorem holds, is not paraconsistent.

Proof. It is easy to see that a; :a ⊢ (a ^ :a) $ a.

By substitution theorem we have a; :a ⊢ :(a ^ :a) $ :a,

but a; :a ⊢ :a, therefore a; :a ⊢ :(a ^ :a).

We also know by an instance of axiom :1 that ⊢ :(a ^ :a) ! ((:b ! a) ! ((:b ! :a) ! ::b))), then by using modus ponens in the previous line a; :a ⊢ ((:b ! a) ! ((:b ! :a) ! ::b))), now we use Pos1 and modus ponens and a; :a ⊢ (:b ! a), therefore by usung modus ponens again ⊢ (:b ! :a) ! ::b, we also have a; :a ⊢ (:b ! a). then a; :a ⊢ ::b, using C!2 ::b ⊢ b.

Finally, we have a; :a ⊢ b.

This last line shows that paraconsistency does not hold. ⊔⊓

Our second result is based on an ASP encoding. ASP has been used to develop different approaches in the areas of planning, logical agents and arti cial intelligence. However, as far as the authors know, it has not been used as a tool to study logics. Here we use ASP to represent axioms and the inference rule Moduls Ponens in clasp in order to

nd three-valued logics that are paraconsistent and for which the axioms of C1 are tautologies.

In what follows, we explain how to construct a program that obtains three

C1+, and then for larger family that de ne the logic P2.

valued logics such that the logic C1 is sound w.r.t. them. We use this program repeatedly, rst for the axioms of C1 and then for the axioms of a logic called

Based on a set of values, and a subset of values corresponding to the property of being select, the clasp-encoding constructs the adequate truth tables for the connectives of a multi-valued logic that makes all instances of the axioms of the given logic select. These truth tables are built in such a way that Modus Ponens preserves the property of being select. The encoding also includes the adequate conditions that each connective of the logic should satisfy, such as the arity, and the uniqueness; the de nition of Modus Ponens; and all of the axioms of the logic. It is worth mentioning that all of the axioms are encoded as constraints. When each axiom is encoded as a constraint, the elimination of those assignment values of the logic connectives for which the axioms are not select, is guaranteed.

Now we present the clasp-encoding, to search for three-valued logics for which logic C1 is sound by extending C1 with the addition of desirable properties represented in terms of axioms. We present the encoding of one of the axioms of C1, the encoding of the other axioms is similar. The encoding uses the values 0, 1, and 2 to create the truth tables for the connectives of the logic. The select value are 1 and 2 4. Thus, for any assignment of the values 0, 1 and 2 to the statements letters of a formula F , the tables determine a corresponding value for F . If F always takes the values 1 and 2, F will be called select. Furthermore, is a propositional program. As usual in ASP, we take for granted that programs with predicate symbols are only an abbreviation of the ground program. The encoding corresponds to the program Pval [ Pprim [ Pdef [ PAx [ Ppar that we present below. We want to remark that Pdef includes all the de ned connectives of the C1 logic, PAx includes the axioms of C1 logic.

Pval : ><8>: sv%%e(ST0l(;er11lu)e;:t2sche)t:l(vv2aa)ll:uuees:0:0; 1; 2 Pprim : >>><>>8>: :11%%:ffiP:inmmergippm(llX(iieXt;siZ;,vY)en;:oZcvto),(nZ:onv)rg(e,Z1cat)nigv1dev,s(.X..v)(:X); v(Y ): Pdef : PAx : Ppar : 8 % B◦ >< bl(X; Z) neg(X; X1); and(X; X1; Y ); neg(Y; Z):

%Modus Ponens >: impl(X; Y; Z); sel(X); sel(Z); not sel(Y ); v(X); v(Y ); v(Z): >: : : : 8 %Axioms of C1 >< %A1 : A ! (B ! A)

impl(B; A; Z); impl(A; Z; R); v(R); not sel(R): { %Paraconsistency: (A ^ :A) ! B is not a theorem.

eval(R) neg(A; A1); and(A; A1; L); impl(L; B; R); v(R):

not eval(X) : not sel(X) : v(X):

We can see that the paraconsistency property is encoded as a constraint in Ppar. This means that in case of obtaining answer sets they must satisfy the paraconsistency property.

When we execute the clasp-encoding , we obtain 8192 answer sets. Each of them corresponds to an adequate set of truth tables for the connectives of a paraconsistent three-valued logic that make logic C1 sound. These 8192 three-valued logics really represent 4096 different three-valued logics because of isomorphisms created by the two designated values.

It is always convenient to look for logics as close to classical logic as possible, then we go one step further to obtain an extension proposed by Beziau for which certain De Morgan laws are valid. In this sense, if we replace the axiom :2 in C1 by the following stronger axiom, called :3, then we obtain logic C1+ [ 9 ]:

A◦ _ B◦ ! (A ^ B) ◦ ^(A _ B) ◦ ^(A ! B)◦ 4 We choose two designated values because we already know that when running the same program with the option of one designated value it does not return any logic.

When we implement this replacement in the clasp-encoding and we execute it, we obtain 8 answer sets. Each of them corresponds to an adequate set of truth tables for the connectives of a three-valued logic that is sound with respect to the C1+ logic and satis es the paraconsistency property. These 8 three-valued logics really represent 4 different three-valued logics because of isomorphisms created by the two designated values.

Now, if we add the following two axioms to C1+ logic (A _ B)◦ (A ! B)◦ and we add their implementation in the clasp-encoding , we obtain 2 answer sets, each of them corresponds to an adequate set of truth tables for the connectives of a three-valued logic thats make logic P2 [ 3 ] sound and satis es the paraconsistency property. These two three-valued logics are isomorphic due to the symmetry generated by the two designated values. 4

Conclusions

ASP have been used to develop different approaches in the areas of planning, logical agents and arti cial intelligence. However, as far as the authors know, it has not been used as a tool to study logics. We provide a clasp-encoding that can be used to obtain paraconsistent multi-valued logics. We also proved that C1 logic can not be extended to a paraconsistent logic where the substitution theorem holds.

References

1. J. Y. Beziau . The paraconsistent logic Z. A possible solution to jaskowski's problem . Logic and logical philosophy , 15 : 99 { 111 , 2006 .

2. W. A. Carnielli and J. Marcos . Limits for paraconsistent calculi . Notre Dame Journal of Formal Logic , 40 ( 3 ): 375 { 390 , 1999 .

3. W. A. Carnielli and J. Marcos . A taxonomy of C-Systems . In Paraconsistency: The Logical Way to the Inconsistent , Proceedings of the Second World Congress on Paraconsistency (WCP 2000 ), number 228 in Lecture Notes in Pure and Applied Mathematics , pages 1 { 94 . Marcel Dekker , Inc., 2002 .

4. N. C. A. da Costa , J.-Y. Beziau, and O. A. S. Bueno . Aspects of paraconsistent logic . Logic Journal of the IGPL , 3 ( 4 ): 597 { 614 , 1995 .

5. N. C. A. daCosta. On the theory of inconsistent formal systems (in Portuguese) . PhD thesis , Curitiva: Editora UFPR , Brazil, 1963 .

6. M. J. O. Galindo , J. R. A. Ram rez, and J. L. Carballido . Logical weak completions of paraconsistent logics . J. Log. Comput. , 18 ( 6 ): 913 { 940 , 2008 .

7. M. Gelfond and V. Lifschitz . The Stable Model Semantics for Logic Programming . In R. Kowalski and K. Bowen, editors, 5th Conference on Logic Programming , pages 1070 { 1080 . MIT Press, 1988 .

8. K. G odel. Uber unabhangigkeitsbeweise im aussagenkalkul(sobre pruebas de independencia en el calculo conectivo) . In ergebnisse eines mathematischen kolloquiums , ed. by k. menger, num. 4 ( 1931 -32), pages 9 - 10 .

9. J.-Y. Beziau . Logiques construites suivant les methodes de dacosta . Logique et Analyse , 33 : 259 { 272 , 1990 .

10. E. Mendelson. Introduction to Mathematical Logic. Wadsworth, Belmont, CA, third edition, 1987 .

11. V. S. S. N. da Costa . Paraconsistent logics as a formalism for reasoning about inconsistent knowledge bases . Arti cial Intelligence in Medicine , 1 : 167 { 174 , 1989 .

12. M. Osorio and J. L. Carballido . Brief study of G'3 logic . Journal of Applied Non-Classical Logic , 18 ( 4 ): 475 { 499 , 2008 .

13. M. Osorio , J. L. Carballido , and C. Zepeda . An application of clasp in the study of logics . In J. P. Delgrande and W. Faber, editors, LPNMR , volume 6645 of Lecture Notes in Computer Science, pages 278 { 283 . Springer, 2011 .

14. M. Osorio , J. A. Navarro , J. Arrazola , and V. Borja . Logics with common weak completions . Journal of Logic and Computation , 16 ( 6 ): 867 { 890 , 2006 .

15. D. van Dalen. Logic and Structure . Springer, Berlin, second edition, 1980 .

16. C. Zepeda , J. L. Carballido , A. Mar n , and M. Osorio . Answer set programming for studying logics . In Special Session MICAI 2009. Ed. IEEE Computer Society , pages 153 { 158 , Puebla , Mxico. ISBN: 13 978 - 0 - 7695 -3933-1.