[FOM] Boolean Rings : Commutative Rings :: Propositional Logic : A 'free' Logic?
Vaughan Pratt
pratt at cs.stanford.edu
Thu May 21 15:58:02 EDT 2009
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
More information about the FOM
mailing list