[FOM] Boolean Rings : Commutative Rings :: Propositional Logic : A 'free' Logic?

[Vaughan Pratt]

On 5/19/2009 4:28 PM, Rex Butler wrote:
> Which brings me to my question.  Thinking of commutative rings as
> boolean rings without the identity x^2 = x, to what 'free' logical
> systems might commutative rings be associated with?

Since arithmetic negation (-x in the additive abelian group, as distinct 
from logical negation 1-x) is the identity operation in a Boolean ring, 
one could reasonably omit it from the generalization and ask about 
commutative rigs (rings without Negation), aka semirings.  Also in view 
of the naturality of not identifying "open the door and walk through it" 
with "walk through the door and open it," why not drop commutativity too?

De Morgan was arguably the first to take such a point of view, pointing 
out in his paper "On the Syllogism, no. {IV}, and on the logic of 
relations" in Trans. Cambridge Phil. Soc., 10, 331-358 (1860), six years 
after Boole's "The Laws of Thought," that composition of binary 
relations could be viewed as a form of conjunction.  This theme was 
subsequently developed by Peirce and Schroeder, and further abstracted 
to the variety RA of relation algebras by Tarski in the following century.

The earliest proposal I'm aware of to drop x^2 = x, Contraction, without 
also dropping commutativity is Girard's linear logic, presented as 
invited talks at LICS'86 (the first LICS, held in Cambridge MA) and a 
category theory conference in Boulder CO in 1987 (I attended both but 
utterly failed to grasp LL at either one) and published as a long and 
essentially unrefereed paper in TCS in 1987.  Whereas Relevance Logic 
had previously dropped Weakening, the rule that permits irrelevant 
hypotheses or "dead rats", Linear Logic was the first to drop 
Contraction as well, the rule that permits using a lemma twice without 
the obligation to prove it twice.

A couple of years later I started to see interesting connections between 
LL and the concurrency modeling my group was engaged in, mainly 
resulting from our need to distinguish ordinary and tensor product when 
generalizing from ordered time to metric time, in combination with a 
certain time-information or event-state duality that had first appeared 
in 1980 with the work of Nielsen, Plotkin, and Winskel on event 
structures.  Tightening up those connections over the following decade 
eventually led to the LICS'03 paper "Proof Nets for 
Multiplicative-Additive Linear Logic" by my research associates Rob van 
Glabbeek and Dominic Hughes, ACM Trans. Comp. Logic 6(4): 784-842 
(2005), where they gave the first satisfactory notion of proof net for 
MALL, linear logic with both multiplication (tensor) *and* addition (plus).

In MALL, multiplication distributes over addition but not conversely, 
unlike the situation for conjunction and disjunction in intuitionistic 
(and therefore Boolean) logic where disjunction distributes over 
conjunction.  (Confusingly LL also has par and times as the respective 
De Morgan duals of multiplication and addition.)

Girard's motivation for dropping Weakening and Contraction is that they 
interfere with the development of a natural algebra of proofs by 
identifying all proofs of Q from P, resulting in lattice theory (namely 
posets as opposed to categories) as the natural semantics of truth. 
This identification is hidden by the detailed "bureaucracy" (Girard's 
term) of traditional line-by-line proofs.  Some insight into the causes 
and limits of this identification can be had from the LICS'04 paper "On 
the Geometry of Interaction for Classical Logic" by Carsten Fuehrmann 
and David Pym, where they avoid this identification using an 
order-enriched version of classical logic (logic with weakening and 
contraction); see http://www.cs.bath.ac.uk/~pym/semclasspro.html for an 
applet illustrating their approach.

There is also noncommutative linear logic, some interest in which 
emerged around 1988, but the commutative version has tended to dominate 
in the applications of linear logic to both proof theory and concurrency 
modeling.

Vaughan Pratt