A strong negation in da Costa's Cn systems can be naturally extended from the strong negation (¬∗) of C1. In [1] Newton da Costa proved the conectives {→, ∧, ∨, ¬∗} in C1 satisfy all schemas and inference rules of classical logic. In the following paper we present a proof that all logics in the Cn herarchy also behave classically as C1. This result tell us the existance of a common property among the paraconsistent family of logics created by da Costa.
According to the authors in [
A common misconception related to paraconsistent logics is the confusion
between triviality and contradiction. A theory T is trivial when any of the
sentences in the language of T can be proven. We say that a theory T is
contradictory if exists a sentence α in the language of T such that T proves α and
¬α. Finally, a theory T is explosive if and only if T is trivial in the presence of
a contradiction. We can see that contradictoriness and triviality are equivalent
if and only if for the underlying logic the law of explosion is valid [
Paraconsistent logics were born in two different ways. In 1948, Jaskowski
gave the following conditions that any paraconsistent logic should satisfy [
Also, in 1963, we can find a new approach given by da Costa, who independently defined a set of conditions that a paraconsistent logic should satisfy.
These conditions are the following: dC1. In these calculi the principle of non-contradiction, in the form ¬(α ∧ ¬α), should not be a valid schema; dC2. From two contradictory formulae, α and ¬α, it would not in general be possible to deduce any arbitrary formula β; dC3. It should be simple to extend these calculi to corresponding predicate calculi; dC4. They should contain the most part of the schemata and rules of the classical propositional calculus which do not interfere with the first conditions.
Nowadays we can find paraconsistent logics applications in many fields such
as informatics, physics, medicine, etc. From Minsky’s comment we can see that
paraconsistent ideas are an approach in Artificial Intelligence [
In physics the authors in [
In the literature we can find many proper paraconsistent logics [
Finding a strong negation in the Cn herarchy is interesting because we can
collapse a fragment of these logics into classical logic, that is, we can have a
translation which provides an embedding of classical logic into any logic of this
Cn system. This fact is mentioned in many papers [
The organization of this document is as follows: In Section 2 we present basic background in logic, including definitions of some basic properties (monotonicity, cut-elimination, deduction theorem) of the paraconsistent logic Cω that we are going to work with. In Section 3 we present a inductive proof about the classical behavior of the strong negation defined in the Cn systems. Finally, in Section 4, we present some conclusions about the proof presented.
We first introduce the syntax of logical 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. 2.1
Logic Systems We consider a formal (propositional) language built from: an enumerable set L of elements called atoms (denoted a, b, c, ...); the binary connectives ∧ (conjuntion), ∨ (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 (α → β) ∧ (β → α). Finally, it is useful to agree on some conventions to avoid the use of many parenthesis when writing formulas in order to make easier the reading of complicated expressions. First, we may omit the outer pair of parenthesis of a formula. Second, the connectives are ordered as follows: ¬, ∧, ∨, →, ↔, 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.
We consider a logic simply as a set of formulas that (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 also 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. α ∈ 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 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 under 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 some given inference rules which include Modus Ponens. The notation `X α for provability of a logic formula α in the logic X is usually extended within Hilbert style systems; given a theory Γ , we use Γ `X α to denote the fact that the formula α can be derived from the axioms of the logic and the formulas contained in Γ by a sequence of applications of the inference rules.
As a example of a Hilbert style system we present next a logic that is relevant for our work.
Cω [
Note that the first 8 axiom schemata somewhat constrain the meaning of the
→, ∧ and ∨ connectives to match our usual intuitions. It is a well known result
that in any logic satisfying Pos1 and Pos2, and with Modus Ponens as its unique
inference rule, the deduction theorem holds [
Theorem 1. Let Γ and Δ be two sets of formulas. Let θ, θ1, θ2, α and ψ be arbitrary formulas. Let ` be the deductive inference operator of Cω. Then the following basic properties hold. 1. Γ ` α → α (identity theorem) 2. Γ ` α implies Γ ∪ Δ ` α (monotonicity) 3. Γ ` α and Δ, α ` ψ then Γ ∪ Δ ` ψ (cut) 4. Γ, θ ` α if and only if Γ ` θ → α (deduction theorem) 5. Γ ` θ1 ∧ θ2 if and only if Γ ` θ1 and Γ ` θ2 (∧ - rules) 6. Γ, θ ` α and Γ, ¬θ ` α if and only if Γ ` α (strong proof by cases) 3
Strong negation in Cn systems We will start giving some basic definitions in order to understand concepts needed in the Cn hierarchy.
Definition 1. ( [
In fact αo can be seen as a modal operator to the formula α that captures the idea of consistency/well - behavior in C1.
Definition 2. ( [
For the careful reader should not confuse α0 with αo. Basically αn represents n applications of the consistency operator (o) to the formula α, and α(n) represents a conjunction of α1, . . . , αn.
Definition 4. ( [
Also, we can see that in Cn, the axiom Cn1 can be replaced by the axiom schema (β ∧ ¬β ∧ β(n)) → α. Intuitively from Cn2 we see that α(n) propagates the what we call n-consisteny in Cn. Finally we define a strong negation in both C1 and Cn.
Definition 5. ( [
Base case (n = 1). By Definition 2 we have that `Cω ¬(α1) ↔ ¬(αo). Also by Definition 1, `Cω ¬(αo) ↔ ¬(¬(α ∧ ¬α)), we can expand the last formula to `Cω ¬(α1) ↔ ¬(¬(α ∧ ¬α)). We can use axiom schema ¬¬α → α to prove `Cω ¬(α1) → α ∧ ¬α, which is by axiom schema Pos3 we have `Cω ¬(α1) → α. From this we apply deduction theorem to obtain ¬(α1) `Cω α as desired.
Inductive step. We assume by induction hypothesis that ¬(αn) `Cω α holds. Accordingly to Definition 2 we have that `Cω ¬(αn+1) ↔ ¬(αn)o, which in fact is `Cω ¬(αn)o ↔ ¬¬(αn ∧ ¬(αn)). From this is easy to prove that ¬(αn+1) `Cω ¬(αn), and with the inductive hypothesis we have that ¬(αn+1) `Cω α. tu
Proof. We can see that αn `Cω α ∨ αn. On the other hand, due to Lemma 1 we have that ¬(αn) `Cω α, therefore ¬(αn) `Cω α ∨ αn. Applying strong proof by cases we have that `Cω α ∨ αn. tu
1.
Proof. By induction on n.
Base case (n = 1). From Lemma 1 we have that `Cω α ∨ αo holds when n = Inductive step. We assume by induction hypothesis that `Cω α ∨ α(n) holds. We know from Lemma 2 that `Cω α ∨ αn+1. Thus `Cω (α ∨ α(n)) ∧ (α ∨ αn+1). Applying the distributive law to the last formula we have that `Cω α ∨ (αn+1 ∧ α(n)), which in fact it is by definition `Cω α ∨ α(n+1). tu Theorem 2 (Excluded Middle). In Cω, we have that `Cω α ∨ ¬(n)α
`Cω (α ∨ ¬(n)α) ↔ (α ∨ (α ∧ α(n))) `Cω (α ∨ ¬((nn))αα)) ↔↔ (αα∨∨α¬(nα)) ∧ (α ∨ α(n)) `Cω (α ∨ ¬ Therefore it is only necessary to check that α ∨ α(n) holds, but accordingly to the Lemma 3 this is true. tu
The next two theorems follows from a similar proof in [
Theorem 3 (Reductio Ad Absurdum). In Cn we have that:
(Γ ∪ {α} `Cn β), (Γ ∪ {α} `Cn ¬β), (Γ ∪ {α} `Cn β(n)) ⇒ Γ `Cn ¬α Proof. Using Deduction Theorem we can prove the following from the hypothesis given: Γ `Cn α → β(n), Γ `Cn α → β and Γ `Cn α → ¬β. By the transitive rule and the axiom schema `Cn β(n) → ((α → β) → ((α → ¬β) → ¬α)) we have that Γ `Cn α → ((α → β) → ((α → ¬β) → ¬α)). By the application of Modus Ponens twice we have that Γ `Cn α → ¬α. From this, using theorem `Cn ¬α → ¬α (as an instance of Identity theorem), and axiom schemas `Cn α ∨ ¬α and `Cn (α → ¬α) → ((¬α → ¬α) → ((α ∨ ¬α) → ¬α)) we can conclude that Γ `Cn ¬α. tu Theorem 4 (Explosive Principle). In Cn we have that:
`Cn α → (¬(n)α → β) Proof. According to the strong negation definition we have that: α, ¬(n)α, ¬β `Cn ¬α ∧ α(n), therefore α, ¬(n)α, ¬β `Cn ¬α and α, ¬(n)α, ¬β `Cn α(n). Also we have that α, ¬(n)α, ¬β `Cn α. By the theorem 3 is easy to prove that α, ¬(n)α `Cn ¬¬β. Cn contains the axiom schemata ¬¬α → α, which it let us prove that α, ¬(n)α `Cn β. Finally, applying two times deduction theorem to the last formula we have that `Cn α → (¬(n)α → β). tu Theorem 5. The connectives {→, ∧, ∨, ¬(n)} in Cn satisfy all the axiom schemata and inference rules in classical propositional calculus.
Proof. Any logic in Cn extends the positive logic axioms from Cω. Then, it is
only necessary observe that the following axiom (¬(n)α → ¬(n)β) → (β → α)
holds in Cn
1. ¬(n)α → ¬(n)β
2. β
3. β → (¬(n)β → α)
4. ¬(n)β → α
5. ¬(n)α → α
6. α → α
7. (α → α) → ((¬(n)α → α) → ((α ∨ ¬(n)α) → α))
8. (¬(n)α → α) → ((α ∨ ¬(n)α) → α)
9. (α ∨ ¬(n)α) → α
10. α ∨ ¬(n)α
11. α
12. (¬(n)α → ¬(n)β), β `Cn α
13. (¬(n)α → ¬(n)β)(n`)Cβn) β→→(βα→ α)
14. `Cn (¬(n)α → ¬
The presented work gives general ideas how to possibly extend a property in C1
to Cn, mainly using inductive proofs. We know that all logics in the Cn system
are strictly weaker than C1 [