[Prev][Next][Index][Thread]
Re: 2 questions re: mapping from IL to ILL
-
To: types
-
Subject: Re: 2 questions re: mapping from IL to ILL
-
From: pratt@cs.Stanford.EDU
-
Date: Tue, 08 Sep 92 17:34:02 EDT
-
In-Reply-To: Your message of Tue, 01 Sep 92 19:11:15 +0100. <9209011828.AA11418@Ghoti.Stanford.EDU>
-
Sender: meyer@theory.lcs.mit.edu
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.