We present GLukG, a paraconsistent logic recently introduced. We discuss our motivation as well as interesting properties of this logic. We introduce a non-monotonic semantics based on GLukG.
It is well known that monotonic logics can be used to define nonmonotonic
semantics [
In this case the stable semantics gives no stable models. The sceptical version of
the stable semantics infers every formula in this example. This is also the case
for most of the traditional logic programming semantics in which inconsistency
might spoil the whole program. Most logics (at least classical logic and all
constructive intermediate logics) share the theorem (a ∧ ¬a) → b, meaning that in
the presence of an inconsistency (a ∧ ¬a) then one prove anything (such as the
unrelated formula b in this example). Paraconsistent logics reject this principle,
the do no not like to be destructive in the presence of inconsistent information.
To avoid this problem the stable semantics was generalized by [
We propose an approach that can be used by any paraconsistent logic stronger
or equal to Cω, the weakest paraconsistent logic introduced by da Costa himself.
We select however the paraconsistent logic GLukG because it is 3-valued and is
very expressive. GLukG can define the same class of functions as Lukasiewicz
3valued logic. In GLukG we can express very directly the strongest intermediate
logic (also known as the G¨odel’s 3-valued logic G3). This is important because
G3 is adequate to express the stable model semantics. However if we use the
original Cω we obtain similar interesting results. Moreover, GLukG can directly
express the GNM-S5 semantics [
The structure of our paper is as follows. Section 2 describes the general background of the paper including the definition of GLukG logic. In Section 3 we present our motivation of GLukG logic. This a contribution of this paper, because is the first time that it is explained how and why we came out with GLukG logic. In Section 4 we present an axiomatization of GLukG logic.
In Section 5 we discuss two main properties of GLukG logic that makes it interesting. In Section 6 we present our main contribution, namely the relation of GLukG logic and nonmonotonic reasoning. We also introduce a nonmonotonic semantics that can deal with inconsistent programs, that is our final contribution to this paper. Finally, in Section 7 we present the conclusions of the paper.
We assume that the reader has some familiarity with basic logic such as
chapter one in [
We first introduce the syntax of logic formulas considered in this paper. Then we present a few basic definitions of how logics can be built to interpret the meaning of such formulas in order to, finally, give a brief introduction to several of the logics that are relevant for the results of our later sections. 2.1
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 A, B, C, . . . ) are constructed as usual by combining these basic connectives together with help of parentheses. We also use A ↔ B to abbreviate (A → B) ∧ (B → A) 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, first, ¬ 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 finite 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 . A literal l is either an atom or the negation of an atom. A normal program is a set of formulas of the form α → x, where x is an atom and α is a conjunction of literals. When α is empty then formula α → x reduces to the atomic formula x. Normal programs are of particular interest in Logic Programming. 2.2
We consider a logic simply as a set of formulas that, moreover, satisfies the following two properties: (i) is closed under modus ponens (i.e. if A and A → B are in the logic, then so is B) and (ii) is closed under substitution (i.e. if a formula A is in the logic, then any other formula obtained by replacing all occurrences of an atom b in A with another formula B is still in the logic). The elements of a logic are called theorems and the notation `X A is used to state that the formula A is a theorem of X (i.e. A ∈ 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 different approaches that have been
used to specify the meaning of logic formulas or, in other words, to define
logics. In Hilbert style proof systems, also known as axiomatic systems, a logic is
specified by giving a set of axioms (which is usually assumed to be closed by
substitution). This set of axioms specifies, 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. Our presentation of our proof system of GLukG
logic follows the Hilbert style, see [
Cω logic [
Multivalued logics An alternative way to define 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 identified as designated. Logic connectives (e.g. ∧, ∨, →, ¬) are then introduced as operators over D according to the particular definition 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 first the atoms to values in D, and then evaluating the resulting expression in terms of the connectives of the logic (which are defined 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 = {0, 1}, 1 is the unique designated value, and connectives are defined through the usual basic truth tables. If X is any logic, we write |=X α to denote that α is a tautology in the logic X. We say that α is a logical consequence of a set of formulas Γ (denoted by Γ |=X α) if V Γ → α is a tautology.
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 ∈ D, if there is a designated value y ∈ 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. 3
One of the most well known semantics for NMR is the stable semantics. A semantics usually associates a set of two-valued models to a given theory. Consider the basic program B:
a ← ¬b.
B has 3 models, namely M1 = {a}, M2 = {b}, and M3 = {a, b}. Model M1 represents the function that evaluates atom a to true and atom b to false. Model M2 represents the function that evaluates atom b to true and atom a to false. Finally, model M3 represents the function that evaluates both atoms a, b to true. It turns out that only M1 is a stable model. Informally such rule reads as ’Normally a holds unless b is truth’. As we said in the introduction there are (contradictory) programs as P2 that gives no models. This lack of information is useless in many cases. Sometimes consistent programs (in classical logic) as program P1 also do not give models. Now, the stable semantics can be characterized using intuitionistic logic as follows. We can check each model and if it passes certain test, we consider it a stable model. Take M1, does it follows that ¬b, B `I a ? (where `I represents the inference relation using intuitionistic logic) The answer is of course ’yes’ and so M1 is a stable model of B. Take now M2, does it follows that ¬a, B `I b ? Well, it turns out that ¬a, B `I ¬¬b, but it can not infer b, so M2 is not a stable model. Let us be a little bit more technical.
Given a set of atoms M and when a theory, or logic program, T is clear by context we use the symbol Mf to denote the complementary set LT \ M . Moreover, given a theory T , we define the negation of the theory ¬T as the set {¬F | F ∈ T } (the negation symbol is parameterized with respect to some given logic). For any pair of theories T and U , using T `X U to state the fact that T `X F for every formula F ∈ U . If M is a set of atoms we also write T X M when: T `X M and M is a classical 2-valued model of T (i.e. atoms in M are set to true, and atoms not in M to false; the set of atoms is a classical model of T if the induced interpretation evaluates T to true).
atoms. M is a X-stable model of P if P ∪ ¬Mf X M .
We call weak completion the construction P ∪ ¬Mf X M just presented. If we use any constructive intermediate logic, we obtain the same class of X-stable models, namely the well known stable models. Intuitionistic logic is considered the weakest constructive intermediate logic, while G¨odel’s 3-valued logic G3 is the strongest constructive intermediate logic.
G3 can be presented as a multivalued logic. In this form it is defined through a 3-valued logic with truth values in the domain D = {0, 1, 2} where 2 is the designated value. The evaluation function of the logic connectives is then defined as follows: x ∧ y = min(x, y); x ∨ y = max(x, y); and the ¬ and → connectives are defined according to the truth tables given in Table 1. We write |= α to denote that the formula α is a tautology, namely that α evaluates to 2 (the designated value) for every valuation. We say that α is a logical consequence of a set of formulas Γ (denoted by Γ |= α if V Γ → α is a tautology.
Hence, We came up with a basic mathematical question. Can we use any other type of monotonic logic different to the constructive intermediate logics such that the following properties hold? 1. The logic should have the following desirable properties. It should satisfy the replacement and deduction theorems. It should be expressive enough. If possible it should be finitely axiomatizable and somehow close to some constructive logic. If possible the logic should be many-valued. 2. Definition 1 should give the same result to our basic program B as the stable semantics. More generally, it is convenient that for every stratified program our intended semantics should agree with the stable semantics. 3. Every stable model of a normal program should be an intended model of our semantics. Every intended model of a normal program in our semantics should be a classical minimal model. 4. The semantics should be expressive enough. 5. The semantics should be close to classical logic, namely if a normal program P infers a given atom x in classical logic then P and P ∪ x should have the same intended models.
We considered the above points only for pragmatical reasons. We did not
considered at first to be able to handled contradictory programs. The first partial
answer was that we could use modal logic S5 but representing as long as we use
¬ a for the definition of such negation operator, see [
G3 logic.
We present a Hilbert-style axiomatization of GLukG simpler than a previous one
presented in [
GLukG Logic has all the axioms of Cω logic plus the following:
E1 E2 E3 E4 (¬A → ¬B) ↔ (¬¬B → ¬¬A) ¬¬(A → B) ↔ ((A → B) ∧ (¬¬A → ¬¬B)) ¬¬(A ∧ B) ↔ (¬¬A ∧ ¬¬B) ((B ∧ ¬B) → (∼∼ A → A)
Note that Classical logic is obtained by adding any of the following list of axioms:
CL1 CL2 CL3
A → ¬¬A A → (¬A → B) (¬B → ¬A) → (A → B)
It is always useful to see that some strong inference rules hold in a given logic. In this sense, a simple but useful result is the following.
Theorem 1. Let Γ and Δ be two set of formulas. Let θ, θ1, θ2, α, and ψ be arbitrary formulas. Then the following basic properties hold. 1. Γ ` α implies Γ ∪ Δ ` α (monotonicity) 2. Γ ` α and Δ, α ` ψ then Γ ∪ Δ ` ψ (cut) 3. Γ, θ ` α iff Γ ` θ → α (deduction theorem) 4. Γ ` θ1 ∧ θ2 iff Γ ` θ1 and Γ ` θ2 ( ∧-rules) 5. Γ, θ ` α and Γ, ¬θ ` α iff Γ ` α (strong proof by cases)
It is very important to note that GLukG can also presented as a multivalued
logic. Such presentation is given in [
We present some useful theorems of GLukG logic. We can see for instance that
∼ behaves very much as a constructive negation. In fact it behaves exactly as the
negation operator of G3 logic. Note that of course ∼∼ α → α is not a theorem.
The reader can consult [
ON EX F1 F2 F3 F4 F5 F6 F7 G1 G2 G3 G4 G5 G6 G7 G8 ` ¬β ↔ ¬¬¬β ` ¬A → (¬¬A → B) `∼ α → (α → β) ` (α → β) → ((α→ ∼ β)→ ∼ α) ` (α → β) → (∼ β→ ∼ α) ` (∼∼ β∧ ∼ θ)→ ∼ (β → θ) `∼∼ θ→ ∼∼ (β → θ) ` β → (∼ θ→ ∼ (β → θ)) (∼∼ β∧ ∼∼ θ)→ ∼∼ (β ∧ θ) ∼ α → ¬α `∼ ¬θ→ ∼∼ θ. ` ¬¬θ→ ∼ ¬θ. ` ¬¬θ→ ∼∼ θ. `∼ θ → ¬¬ ∼ θ. ` ¬ ∼ θ→ ∼∼ θ. ` (∼∼ β ∧ ¬β) → ¬¬¬β.
`∼ β → ¬¬¬β. 4.2
The strategy of the proof for completeness is to follow the proof of completeness
for propositional classical logic given by Kalmar, see [
an associated formula Av as follows: 1. Av := ¬¬A, if v(A) = 2. 2. Av :=∼∼ A ∧ ¬A, if v(A) = 1. 3. Av :=∼ A, if v(A) = 0.
For a set Γ of formulas, we write Γv to denote the set of formulas {αv : α ∈ Γ }.
holds: Δv ` αv.
Proof. The proof is by induction on the size of α.
Base Case: α is an atomic formula, say p. Hence we need to show that pv ` pv, but this is immediately true.
Inductive step: Suppose that α is a non atomic formula. Then, we have 3 cases: (Case ¬) Suppose that α is of the form ¬β. By inductive hypothesis we know that Δv ` βv. We need to consider 3 subcases:
v(β) = 2. Hence Δv ` ¬¬β. Since v(α) = 0, we need to show that Δv `∼ α, that is Δv `∼ ¬β. It suffices to show that ` ¬¬β→ ∼ ¬β. But this can be verified with the help of Theorem 1 and Lemma 1.
v(β) = 1. Hence Δv ` (∼∼ β ∧ ¬β). Since v(α) = 2, we need to show that Δv ` ¬¬α, that is Δv ` ¬¬¬β. It suffices to show that ` (∼∼ β ∧ ¬β) → ¬¬¬β. But this can be verified with the help of Theorem 1 and Lemma 1.
v(β) = 0. Hence Δv `∼ β. Since v(α) = 2, we need to show that Δv ` ¬¬α, that is Δv ` ¬¬¬β. It suffices to show that `∼ β → ¬¬¬β. But this can be verified with the help of Theorem 1 and Lemma 1.
(Case →) Suppose that α is of the form β → θ. By inductive hypothesis we know that Δv ` βv, and Δv ` θv. We need to consider 6 subcases: v(β) = 0. Hence Δv `∼ β. Since v(α) = 2, we need to show that Δv ` ¬¬α, that is Δv ` ¬¬(β → θ). It suffices to show that `∼ β → ¬¬(β → θ). But this can be verified with the help of Theorem 1 and Lemma 1.
v(θ) = 2. Hence Δv ` ¬¬θ. Since v(α) = 2, we need to show that Δv ` ¬¬α, that is Δv ` ¬¬(β → θ) It suffices to show that ` ¬¬θ → ¬¬(β → θ). But this can be verified with the help of Theorem 1 and Lemma 1.
v(β) = 1, v(θ) = 0. Hence Δv `∼∼ β ∧ ¬β and Δv `∼ θ. Since v(α) = 0, we need to show that Δv `∼ α, that is Δv `∼ (β → θ). It suffices to show that ` ((∼∼ β ∧ ¬β)∧ ∼ θ)→ ∼ (β → θ). But this can be verified with the help of Theorem 1 and Lemma 1.
(Rest of cases of → and ∧) They carry out similarly and since each case is rather tedious we shall not include it here, however is straightforward, so its details are left to the reader.
1. ` ¬(A → ¬¬A) → ¬ ∼ A. 2. ` ¬(A → ¬¬A)→ ∼∼ A. 3. ` ¬(A → ¬¬A) → ¬A. 4. ` (¬A ∧ (A → ¬¬A))→ ∼ A.
Lemma 4. Γ, ¬¬α ` θ and Γ, (∼∼ α ∧ ¬α) ` θ and Γ, ∼ α ` θ implies Γ ` θ. Proof. Suppose (a) Γ, ¬¬α ` θ (b) Γ, (∼∼ α ∧ ¬α) ` θ (c) Γ, ∼ α ` θ.
By α → ¬¬α, α ` ¬¬α and (a) we get Γ, (α → ¬¬α), α ` θ.
By ¬(α→¬¬α) ` (∼∼ α∧¬α) (Lemma 3) and (b) we obtain Γ, ¬(α→¬¬α) ` θ. By ((α→¬¬α), ¬α) `∼ α (Lemma 3) and (c) we conclude Γ, (α→¬¬α), ¬α ` θ. From Γ, (α → ¬¬α), α ` θ and Γ, (α → ¬¬α), ¬α ` θ and basic logical manipulation, we get Γ, (α → ¬¬α) ` θ.
By Γ, (α → ¬¬α) ` θ and Γ, ¬(α → ¬¬α) ` θ and basic logical manipulation, we get Γ ` θ, as desired.
Proof. Case (a) This a straightforward proof by induction in the length of the proof. Of course one need to verify that every axiom is a tautology (this can be done by the help of a computer program) and that the rule of modus ponens preserves tautologies, which is a simple exercise.
Case (b) It follows by Lemma 4, Lemma 2, and a standard basic logical reasoning
as in [
In this section we present two main results of GLukG Logic, but first we present some definitions.
tory if there exists a formula α such that T ` α and T ` ¬α. Otherwise, we say that T is noncontradictory. We say that T is complete if for every formula α, T ` α or T ` ¬α. A theory T 0 is said to be an extension of a theory T if for every formula α, T ` α then T 0 ` α.
The two main results that help to understand better GLukG are the following. First, that GLukG can express Lukasiewicz 3-valued logic that is a well known expressive logic. Second, one expect that a noncontradictory theory can be extended to a noncontradictory and complete theory. All well known logics satisfy this property. We show that GLukG also satisfies it.
Proof. To express Lukasiewicz 3-valued logic we need to be able to define the corresponding negation and implication connectives. In fact, the original 3-valued system is based on these 2 connectives which are intended to generalize the negation and implication connectives of classical logic, see [20]. Negation of Lukasiewicz 3-valued logic is defined by ∼ A ∨ (∼∼ A ∧ ¬A ∧ A) and implication is defined by (A → B) ∨ (∼∼ A ∧ ¬A ∧ A). Note that Lukasiewicz 3-valued logic is usually defined with 0, 1/2, 1 values but instead we use 0, 1, 2 respectively.
We now move to prove the second property which is a a new result.
there exists a formula α such that T 6` α and T 6` ¬α. Then T ∪ {α} is noncontradictory or T ∪ {¬α} is noncontradictory.
Proof. Suppose (in order to obtain a proof by contradiction) that T ∪ {α} is contradictory and T ∪ {¬α} is contradictory. Then exist formulas β and θ such that T ∪ {α} ` β, T ∪ {α} ` ¬β, T ∪ {¬α} ` θ, T ∪ {¬α} ` ¬θ. Hence T ∪ {α} ` β ∧ ¬β and T ∪ {¬α} ` θ ∧ ¬θ.
Thus T ` α → (β ∧ ¬β) and T ` ¬α → (θ ∧ ¬θ). From this is not hard to see that T ` (β ∧ ¬β) ∨ (θ ∧ ¬θ). But it is easy to verify that ` ¬((β ∧ ¬β) ∨ (θ ∧ ¬θ)). So, T ` ¬((β ∧ ¬β) ∨ (θ ∧ ¬θ)). Hence T is contradictory obtaining a contradiction.
If we have a noncontradictory theory T and a formula α. We define T (α) = T ∪ {α} if T ∪ {α} is noncontradictory and otherwise T (α) = T ∪ {¬α}. By the above lemma, T (α) is noncontradictory.
Proof. Let β1, β2, . . . be an enumeration of all formulas based on the signature of T . Define a sequence T0, T1, . . . of theories defined as follows. T0 is T . Suppose that Tn is defined with n ≥ 0. If Tn does not decides βn+1, then let Tn+1 be Tn(βn+1), otherwise we let Tn+1 = Tn. Let Tω be the union of all Ti (i ≥ 0). One can prove that every Ti is noncontradictory by induction on i. The base case is by hypothesis (recall that T = T0 is noncontradictory) and the inductive step follows by Lemma 6. Then one can easily prove that Tω is noncontradictory. If Tω were contradictory the some Ti should be contradictory, but this is a contradiction. Also by construction Tω is complete. Hence T ω is a noncontradictory and complete extension of T , as desired.
The research community has long recognized the study of nonmonotonic
reasoning (NMR) as a promising approach to model features of commonsense reasoning.
On the other hand, monotonic logics have been successfully applied as a basic
building block in the formalization of nonmonotonic reasoning. The original idea
was to use well known modal logics and this idea can be traced back to [
More recently (in [
[
Based on all the previous work, [
Let as come back to Definition 1. If we use GLukG instead of G3, we obtain a
different semantics than the the well known stable semantics. Such semantics is
also equivalent to GNM-S5 [
Let us consider example P1 from the introduction. Clearly {a, b} is a GLukGstable model of P1. This is because {a, b} is a classical 2-valued model of P1 and P1 proves both a and b in GLukG logic.
Consider now example P2. Since P2 does not have 2-valued models then it does not have GLukG-stable models.
As a final example consider program P3: a ← ¬b.
This program has three 2-valued models, namely M1 = {a}, M2 = {b} and M3 = {a, b}. One can see that M1 is the unique GLukG-stable model of this program as follows. Note that ¬b, ¬b → a proves a in GLukG logic. Hence M1 is a GLukG-stable model of P3. M2 is not a GLukG-stable model of P3, since ¬a, ¬b → a does not prove b in GLukG logic. M3 is not a GLukG-stable model of P3, since ¬b → a does not prove {a, b} in GLukG logic.
In this subsection we introduce a nonmonotic semantics that can deal with
inconsistent programs. Our semantics is different to the one presented in [
Let us consider an example to explain what we have in mind with respect to a nonmonotic semantics that can deal with inconsistent programs. Consider again our program example P2: a→b, ¬a, and a. Then P2 does not have X-stable models, not matter the logic used.
We are interested in the definition of a semantics that can give the following set of literals as the unique output of P , namely {b, ¬a, a}.
Let P os(T ) denote the set of positive formulas of a given theory T . Let N eg(T ) denote the set of negative formulas of a given theory T .
N eg(M ) = LP \ N . (B) Otherwise, if P does not have GLukG-stable models then P has only one paraconsistent-GLukG stable model, namely the set of all literals than be proved from P using GLukG logic.
Following this approach, it turns out that {b, a, ¬a} is the unique paraconsistentGLukG stable model of our example P2. Consider again the basic program B: a ← ¬b.
Then B has one paraconsistent-GLukG stable model, namely M1 = {a, ¬b}. 7
We have given an axiomatization of GLukG based on Cω plus only 4 new axioms. For future work we consider two problems. The first one consists on determining wether or not GLukG is a maximal paraconsistent logic. It would be maximal if after adding any new axiom to GLukG that is not already a theorem we can prove (A ∧ ¬A) → B. The second problem consists on understanding in more detail how to take advantage of the paraconsistency flavor of GLukG in order to define a non-monotonic semantics that could deal properly with inconsistent programs. We provided already an initial idea in Definition 4 but future work must be done on this line of research. 19. C. Sakama and K. Inoue. Negation as failure in the head. Journal of Logic Programming, 35(1):39–78, 1998. 20. A. Urquhart. Many-valued logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol III, volume 3. D. Reidel Publishing Co., 1986.