[Prev][Next][Index][Thread]
re:braids in linear logic
Date: Wed, 13 May 92 12:36:45 EDT
To: linear@cs.stanford.edu
This is a followup to my previous note, Braids in Linear Logic. I
would like to clarify some points, as well as correct an error.
First, regarding nets for braided mLL. Since this will be a
noncommutative logic with some additional inference rules, the
appropriate version of net to begin with are the two-sided nets of M.
Abrusci defined in JSL 56. These are a two sided version of the
Danos-Regnier nets. So, there will be premises, as well as conclusions.
Axiom links will be drawn as lines from A to A, signifying the
deduction A entails A. There will also be introduction and elimination
links for each of the connectives. Then, these links are augmented
with the twisted links mentioned in the previous note.
Regarding crossed G-Sets, I should have mentioned that tensor is
product, with | | given by |(x,y)|=|x||y|. Maps of crossed
G-Sets are maps of G-sets such that |f(x)|=|x|.
Finally, the statement that crossed G-Sets distinguish all unequal
deductions is false, when G is an abelian group. However, the first
part of the theorem is correct. I apologize for the error.
Rick Blute