[Prev][Next][Index][Thread]
Re: Mix Rule and Girardian Turnstile
Some counterintuitive obvious consequence of the "Mix" rule are:
1) -(A-oA)-o(B-oB). Hence the principle of variable-sharing which is
well known from the relevance literature (that A implies B only if A and
B share some propositional variable) is violated.
2) (A-oB) par (B-oA) becomes a theorem. This hints in the direction of
using Algebraic models in which the order relation is linear (but the
lack of contraction makes things more complicated).
I would like to use this opportunity to question the use of the name
"mix" here. This name was used for years by proof-theorticians for a
variant of the cut rule (equivalent to cut in the presence of the structural
rules). See the papers of Gentzen and the books of Kleene and Takeuti. Mixing
this with the rule discussed here is not a good idea. Relevance Logicians
have used the name "mingle" for this rule for many years (The system R-mingle
or RM in short is based on it). Another possible name is "combining".
Arnon Avron (aa@cauchy.stanford.edu)