[Prev][Next][Index][Thread]

Re: 2 questions re: mapping from IL to ILL

To: linear@cs.stanford.edu
Date: 01 Sep 92 22:46:48 PDT (Tue)
Received: from Ghoti.Stanford.EDU by theory.lcs.mit.edu (5.65c/TOC-1.2S) 
	id AA06476; Tue, 08 Sep 92 17:23:42 EDT

>The first question concerns the mapping
>	| A -> B |   ==>   !| A | -o | B |
>I can't see why this isn't
>        | A -> B |   ==>   !( !| A | -o | B |)

Then it wouldn't follow that -> was intuitionistic implication.  In
particular you couldn't show A->(B->C) = (B&A)->C.  With the first
mapping this follows via
	A->(B->C) = !A-o(!B-oC) = (!B@!A)-oC = !(B&A)-oC = (B&A)->C.
With your mapping you get stuck thus:
	A->(B->C) = !(!A-o!(!B-oC)) = ?

(By A=B I mean constructive equivalence, i.e. isomorphism, of A and B
rather than their identity.  Nonconstructive equivalence would settle
for independent proofs of A|-B and B|-A, constructive equivalence adds
the further requirement that these proofs compose via cut to yield the
standard (identity) proofs of A|-A and B|-B.)

>or
>        | A -> B |   ==>   !| A | -o !| B |

Similar problem:
	A->(B->C) = !A-o!(!B-o!C) = ?

>The second question concerns
>        | A x B |   ==>   | A | & | B |
>Here, I thought it would be
>        | A x B |   ==>   !( !| A | & !| B |)
>as the projected component would occur more than once too.

A&B is already intuitionistic conjunction.  Your translation would turn
it into linear conjunction (tensor product), via !(!A&!B) = !!A@!!B.

>Oh - and also, is it ever possible to have
>       A -o !B

Sure, it's a wff.

>and, if so, what does it mean?

If you mean are there any properties specifically of this juxtaposition
of operations, I would be surprised to see any.  Model theoretically,
this is the question of what maps are there from algebra A into the
free algebra F(UB).  Whereas maps FA->B from a free algebra correspond
1-1 to maps A->UB in the underlying CCC, maps to a free algebra don't
get to take advantage of the freeness.

	Vaughan Pratt






   Linear Moderator's Note: 

   If you are happy with nonconstructive equiv., 
   (only interested up to "o-o" ("-o" and "o-"))
   then your proposed translations are OK, but
   use more "!"'s (are somewhat more sloppy) than 
   necessary.  

                 !B |- !B     C |- C
                 !B -o C, !B |- C
   !A |- !A      !(!B-oC), !B |- C
   !A-o!(!B-oC), !A, !B |- C
   !(!A-o!(!B-oC)), !A, !B |- C
   !(!A-o!(!B-oC)), (!A & !B), !B |- C
   !(!A-o!(!B-oC)), (!A & !B), (!A & !B) |- C
   !(!A-o!(!B-oC)), !(!A & !B), !(!A & !B) |- C
   !(!A-o!(!B-oC)), !(!A & !B) |- C
   !(!A-o!(!B-oC)) |- !(!A & !B) -o C
   !(!A-o!(!B-oC)) |- !(!(!A & !B) -o C)


       !A |- !A       !B |- !B
   !A, !B |- !A   !A, !B |- !B
   !A, !B |- !A & !B
   !A, !B |- !(!A & !B)     C |- C
   !(!A & !B) -o C, !A, !B |- C
   !(!(!A & !B) -o C), !A, !B |- C
   !(!(!A & !B) -o C), !A |- !B-oC
   !(!(!A & !B) -o C), !A |- !(!B-oC)
   !(!(!A & !B) -o C) |- !A-o!(!B-oC)
   !(!(!A & !B) -o C) |- !(!A-o!(!B-oC)) 

   These proofs have extra "!" steps.

   For all of these reasons, Girard's original translation is
   preferred.  However, there are asymmetric translations
   (where a formulas translation depends on its context) 
   that don't use any "!"s at all.  
   See: Patrick Lincoln, Andre Scedrov, and Natarajan Shankar
   ``Linearizing Intuitionistic Implication'', Proc. 6th 
   {IEEE} Symp. on Logic in Computer Science,Amsterdam, NL, 1991.

   pdl.