Exponentials as Projections from Paraconsistent Logics

Anna Patterson and Tom Costello

Computer Science Department, Stanford University, Stanford, CA 94305,

             Email {annap,costello}@cs.Stanford.EDU

Abstract

Classical or intuitionistic logic can be recaptured from a paraconsistent logic. We consider operations that map a part of N^{−}, a paraconsistent logic, to intuitionistic logic.

Girard [1] introduces an operator !_{l} called an exponential, to add structural rules to linear logic^{1}. A formula !_{l}A can be replicated or discarded. Thus the exponential removes the “linearity”, the notion that assumptions should only be used once, from linear logic.

The exponential is also used to embed intuitionistic logic in linear logic. Girard shows that intuitionistic implication A ⊃ B can be represented as !_{l}A ⊸_{l} B.

We suggest that these two uses can be separated. We look at how the second transformation, embedding intuitionistic implication, can be carried out in a paraconsistent logic, N^{−}, where N^{−} allows assumptions to the used arbitrarily many times.

An abstract definition of a Girard exponential ! in category theory is a co-monad ⟨!, ϵ: ! → id, δ: ! →!^{2}⟩, where ! distributes through the additive conjunction to yield the multiplicative conjunction.

These observations lead us to believe that an abstract definition of an exponential is that of a logic translator, or an operator which reduces the logic to some underlying fragment of that logic.

We show that a Girard exponential, that is a co-monad where ! distributes through the additive conjunction, can be added as a new operator to the logic N^{−}. N^{−} is the system N without the consistency notion φ ∧ ¬φ ⊃ ψ. N^{−} is a conservative extension of intuitionistic logic.

1We use subscript l to denote operators from linear logic.

The logic of constructible falsity, N^{−}[2, 3] , adds an involutory negation ¬ to intuitionistic logic. This negation asserts the existence of a counterexample to a formula, not merely that the truth of a formula implies contradiction. N^{−} contains the intuitionistic connectives ∧, ∨, ⊃ and ∼, as well as the new involutory negation, ¬. Substitutable implication, A ⊸ B = A ⊃ B ∧ ¬B ⊃ ¬A, (written ⇒ in [5, 6]) and tensor, A ⊗ B = ¬(A ⊸ ¬B) are definable such that (A ⊗ B) ⊸ C = A ⊸ (B ⊸ C).

We add a new constant I, overdefined, to N^{−} which is the unit for tensor ⊗ and is distinct from the other constants, falsity, 0, and truth,

1. I is not definable in N^{−} but can be axiomatized as ϕ ⊃ I, ¬I ≡ I. When a proposition is overdefined it is both “true” and “false”.

Therefore the negation of overdefined, I is itself, and every formula implies it. The new exponential, !, is defined as !A = A ∧ I.

This exponential forms an idempotent co-monad ⟨!, ϵ: ! → id, δ: ! → !^{2}⟩ where ! arises as the co-unit of the co-Kleisli construction applied to this co-monad and as such obeys !1 = I, !(A ∧ B) = !A ⊗ !B, and ! !A = !A, the characteristic equations of Girard’s exponential. Further, intuitionistic implication is definable as !A ⊸ B using this new exponential and substitutable implication.

Linear logic contains two exponentials, !_{l} and ?_{l}, which are DeMorgan duals. Adding I to N^{−}, gives us two dual exponentials, ! and ?, related by ?A = ¬!¬A.

More exponentials can be added to N^{−} using the constant for undefined, ⊥. A weak exponential ¡ is definable as ¡A = A ∨ ⊥, where ⊥ is a constant independent from 0, 1 and I and ⊥ is not definable in N^{−}. ⊥ was first studied by Vakarelov[6] where it was axiomatized as ¬⊥ ≡ ⊥ and ⊥ ⊃ ϕ.

The weak exponential ¡ is an idempotent monad which arises as the unit of the Kleisli construction. ¡ also obeys ¡I = 1, ¡(A ⊗ B) = ¡ A ∧ ¡ B and ¡ ¡ A = ¡A. The dual exponential ¿ is definable as, ¿A = ¬¡¬A.

The weak exponential also extracts intuitionistic implication from substitutable implication ⊸. However ¡ is applied to the second argument via the rule A ⊸ ¡B. All four exponentials are distinct. It is notable that A ⊸ ¡ B is not equivalent to !A ⊸ B.

The addition of the two units ⊥ and I complete N^{−}, in the sense that there is a representation theorem for N^{−} with these additional units with respect to H × H^{op} where H is a Heyting algebra. This naturally completes N^{−} so that every point in the algebra H × H^{op} is representable as an equivalence class of interderivable formulas.

This shows that we can naturally divide the exponential construction of Girard into two parts, one that deals with “linearity” or counting the occurrences of assumptions, and a second that captures the embedding of a intuitionistic logic in a paraconsistent logic.

References

[1] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[2] David Nelson. Constructible falsity. Journal of Symbolic Logic, 14:14–26, 1949.

[3] David Nelson and Ahmad Almukdad. Constructible falsity and inexact predicates. Journal of Symbolic Logic, 49(1):231–233, March 1984.

[4] A. Patterson and T. Costello. Guilt-free exponentials. Bulletin of the Association of Symbolic Logic. Winter Meeting of the ASL, 1997.

[5] H. Rasiowa. An algebraic approach to nonclassical logics. North-Holland, 1974.

[6] D. Vakarelov. Notes on N-lattices and constructive logic with strong negation. Studia Logica, XXXVI(1-2):109–126, 1977.