Guilt-Free Exponentials

Anna Patterson and Tom Costello

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

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

Abstract

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 “linear” property of linear logic.

The exponential is also used to embed intuitionistic logic in linear logic. Girard suggests 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 can be carried out in a logic which already contains all the structural rules of intuitionistic logic.

The logic of constructible falsity, N^{−}[2] , 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, ¬. Strong implication, A ⊸ B = A ⊃ B ∧ ¬B ⊃ ¬A, (written ⇒ in [3, 4]) and tensor, A ⊗ B = ¬(A ⊸ ¬B) are definable.

We add a new constant, I, 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^{−}. The new exponential, !, is defined as !A = A ∧ I.

This exponential ! 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.

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^{−}. A weak exponential ¡ is definable as ¡A = A ∨ ⊥, where ⊥ is another constant independent from 0, 1 and I. ⊥ was first introduced by Vakarelov[4]. ¡ 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 strong implication ⊸. However it is applied to the second argument via the rule A ⊸ ¡B. All four exponentials are distinct.

These two new units 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.

References

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

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

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

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

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