headers
Alessio Guglielmi | 8 Jul 2005 20:24
Picon
Favicon

Re:Back to computability logic

At 19:26 -0400 28/6/05, Giorgi Japaridze wrote:
>Hello everyone. About a year ago we have collectively attempted but
>failed to axiomatize various fragments of computability logic. Finding
>good deductive systems for computability logic has been on the problems
>list of the main CoS webpage since then. I see a light at the end of
>the tunnel in the paper advertised below.  Its last paragraph kinda
>contains a marriage proposal to CoS, so I'd be curious to know how the
>other party feels before going any farther.
>
>The preprint is available at http://arxiv.org/abs/math.LO/0506553

Hi Giorgi and everybody,

I didn't answer before because I was away from email, but I managed 
to print your paper before leaving and I'm enthusiastic about this 
new development, despite only having a superficial reading of it 
(sorry for that, I couldn't really find the time).

However, I think I know enough to say that your notion of sharing is 
elegant and new, and I'm very intrigued by your ability to deal with 
binary tautologies. This logic reminds me a bit of pomset logic, in 
the sense of being a very hard nut to crack. Pomset logic led us to 
deep inference; if binary tautologies do something similar it would 
be fantastic, I think. I encourage everybody to read this paper and 
share opinions. It `smells' good to me.

The question now is whether one can do proof theory with the cirquent 
calculus. I cannot say I understand your system (with my guts, I 
mean), but I'll play with it as soon as I can. Unfortunately, it 
won't be very soon, because I'm relocating. If anybody finds
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 8 Jul 2005 20:40
Picon
Favicon

Re:Back to computability logic

and, by the way, I agree with everything you say about linear logic 
in your paper.

LL is a hybrid, because it tries to do something non-classical by 
using an inherently classical underlying syntax. It is still an 
interesting logic and it has been important, because it has a complex 
proof theory and because proof nets are a very nice idea.

However, it made its time, I think. Unfortunately, there are many 
?logicians who invested a lot in that, they'll be hard to convince.

Ciao,

-Alessio
Permalink | Reply | 501 comments |
headers
Yves Guiraud | 22 Jul 2005 15:50
Picon
Favicon

New paper announcement

Hi to all the frogs readers,

I hope that the workshop in Lisbon was fine. On that topic, for people 
interested, I've just finished an extended version of the paper Lutz has 
presented for me there (thanks again!).

It is still called "The three dimensions of proofs" and is located at the 
following adress (the short one is still available):

http://iml.univ-mrs.fr/~guiraud/recherche/cos1.pdf

Any comments are welcome!

Ciao and enjoy the summer holidays,

Yves
Permalink | Reply | 0 comments |
headers
Giorgi Japaridze | 24 Jul 2005 06:38
Favicon

Re: Back to computability logic

Hi Alessio and everybody.

I do not check my mail very often in these summer days, either. 
And I could not make it to Lisbon, unfortunately. Thank you for your comments. 

. Question: how does cut elimination for CL5 look like? 
. Of course, one has to design a cut rule, but I guess 
. the obvious degeneration of your and-introduction would 
. do fine.

Yes, it'd be interesting to look into this. At this point all I know 
(semantically) is that the system is closed under the standard version 
of cut ;-)

A few typos (one perhaps misleading) have been corrected in the paper. 
The new version is at the same URL: 
http://arxiv.org/abs/math.LO/0506553

Ciao,
Giorgi
Permalink | Reply | 501 comments |
headers
Alessio Guglielmi | 26 Jul 2005 14:34
Picon
Favicon

Red and blue (again)

Hello Dale and batrachianologists,

a few years ago Dale mentioned to me this phenomenon: if you paint 
connectives in the sequent calculus in red and blue, you can often 
prove their equivalence. For example, if you have red conjunction &-R 
and blue conjunction &-B, subjected to the same rules, then you can 
prove that

    F  &-R  G   <->   F  &-B  G  .

In linear logic, this works for all connectives but not for the 
modalities: differently coloured modalities are independent, they 
aren't equivalent.

We discussed this thing a few times already, also on Frogs, but I 
never resolved to write down a couple of paragraphs. So, since the 
thing resurfaced again at Dale's talk in Lisbon, I wrote a quick note 
with my point of view: 
<http://iccl.tu-dresden.de/~guglielm/p/AG15.pdf>.

In brief: this phenomenon is another artifact of the sequent calculus.

The first thing I have to say is that colouring connectives in red 
and blue is a purely syntactic thing, not necessarily connected to 
any meaningful semantics. Still, I agree that the relation of this 
with equivalence is interesting.

Second: my immediate reaction would be that if two things only are 
distinguished by the colour, but they behave the same, they must BE 
the same! So, this seems to me a (rare) case in which semantics
(Continue reading)

Permalink | Reply | 25 comments |
headers
Francois Lamarche | 26 Jul 2005 15:08
Picon
Favicon

SD05: it's over!

Greetings to everybody,

Now that Structures and Deduction 2005 has been over for a week, we've 
had some nice feedback from several people who were there and it seems 
we are not completely deluded in thinking it was a successful meeting!

It was a success because of all you people, and we would like to thank 
you:

-- the ICALP grand organizers, Luis and Luis, the workshop organizers, 
Antonio and Vasco, our own designated all-around fixer, Francisco, and 
all their supporting staff. The task was enormous, and you managed an 
operation that *ran amazingly smoothly*, and was always on schedule! We 
even saw some of you in the audience!

-- the two invited speakers, who gave us talks that fit *perfectly* 
with our intended scope.

-- the PC and referees, in particular those who weren't in Lisbon. You 
committment and seriousness gave us a refereeing and selection process 
which was worthy of an international conference. And kudos to Andrei 
Voronkov for the top-notch software that helped us doing that.

-- the authors, most of whom managed to fit the technicalities of their 
papers into a format that *communicated* their ideas, and permitted the 
kind of immediate feedback that we were hoping for.

-- the participants, who created the lively atmosphere we had, and 
sparked all these great discussions.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rajeev.Gore | 27 Jul 2005 01:10
Picon
Picon

Re:Red and blue (again)


Hi Alessio,

> If differently coloured connectives are all reduced to the SAME meta
> level (the classical one), then, OF COURSE, one gets equivalence.
> And, OF COURSE, equivalence is missing when there is no meta level
> corresponding to the connectives, like in the case of linear logic
> modalities.

Yes, this was one of the motivating reasons for Wansing's display
calculus for modal logic: it could derive equality of blue boxes and
red boxes.

> So, the sequent calculus is only apparently half-adequate to deal
> with the situation, and I guess the same is true with every
> formalism which commits to a fixed meta level, like hypersequents
> and the display calculus.

Not sure what you mean here Alessio. What is wrong with translating
into a fixed meta level ? The problem with traditional sequent calculi
is that they have no meta-level connective for box at all. Thus the
red-box right rule has to look for red-boxes in the antecedent so it
can construct the corresponding premise. But when faced with 
  [blue] p |- [red] p 
as a conclusion, it gets confused, and it can't construct 
  p |- p
from this situation.

Raj
(Continue reading)

Permalink | Reply | 6 comments |
headers
Jon Cohen | 27 Jul 2005 03:19
Picon
Picon

Re: Red and blue (again)

Hi,

First, there's a slight mistake in the note - it uses the lattice style
introduction rule on the right and the monoid style rule on the left.
This breaks cut elimination...

More to the point, I don't see the issue here. We need to remember a
couple of quirks of CoS - namely that it is a one sided calculus and
that [,] takes the place of comma (since we are working on the right).
If you introduce two colours of [,], then this is, as you say, just the
same as introducing two colours of comma. How to distinguish between two
"colours" of branching? Going up a proof, it is obvious. Coming down, it
just means that we have two conjunctions to choose from - just like if
we have access to both lattice and monoidal conjunction (and are working
in linear logic where they are distinct notions). This issue does not
arise in CoS because it keeps track of the type of branching by using
different colours for (,). This is even clear when one asks how to
introduce (,) in a CoS proof...

Your argument against SC seems to hinge on the fact that it cannot show
two colours of exponentials to be equivalent. However, when moving to
CoS you only dealt with the classical connectives. Can CoS prove the
equivalence of {!}A and <!>A? Here, the different braces indicate the
different colours. If so, then this is quite worrying!

It is not always desirable for different coloured modalities to be the
same. For instance, in, say, basic tense logic Kt, we have a modality
for each of future and past. We certainly don't want them to come out to
be equivalent. Here, the fact that the modalities are different has
*everything* to do with the logic. But this is just the same as if we
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 27 Jul 2005 10:10
Picon
Favicon

Re:Red and blue (again)

At 09:10 +1000 27/7/05, Rajeev.Gore@... wrote:
>>So, the sequent calculus is only apparently half-adequate to deal 
>>with the situation, and I guess the same is true with every 
>>formalism which commits to a fixed meta level, like hypersequents 
>>and the display calculus.
>
>Not sure what you mean here Alessio. What is wrong with translating 
>into a fixed meta level ? The problem with traditional sequent 
>calculi is that they have no meta-level connective for box at all.

There is nothing wrong, technically, in translating into a fixed meta 
level. However, what is the point in asking the question about 
equivalence of differently coloured connectives, when the meta level 
is fixed? I mean, instead of saying

    red-box = blue-box

plain and simple, one says

    red-box = meta-box   &   blue-box = meta-box   ->   red-box = blue-box .

I say: what the  <at> %#$???

Perhaps we agree that new logics are needed with very different 
semantics from classical logic. If we want to deduce and compute in 
these logics, we need a syntax which is as neutral as possible 
regarding semantics. In this perspective, keeping a fixed meta level 
is a methodological and strategical mistake, because it limits the 
possibilities tremendously.
(Continue reading)

Permalink | Reply | 5 comments |
headers
Rajeev.Gore | 28 Jul 2005 01:42
Picon
Picon

Re:Red and blue (again)


> There is nothing wrong, technically, in translating into a fixed meta 
> level. However, what is the point in asking the question about 
> equivalence of differently coloured connectives, when the meta level 
> is fixed? I mean, instead of saying
> 
>     red-box = blue-box
> 
> plain and simple, one says
> 
>     red-box = meta-box   &   blue-box = meta-box   ->   red-box = blue-box .
> 
> I say: what the  <at> %#$???

Agreed.

> Perhaps we agree that new logics are needed with very different 
> semantics from classical logic. If we want to deduce and compute in 
> these logics, we need a syntax which is as neutral as possible 
> regarding semantics. In this perspective, keeping a fixed meta level 
> is a methodological and strategical mistake, because it limits the 
> possibilities tremendously.

Absolutely.

> Asking the colour question means asking a purely syntactic question 
> related to the `interaction' of subformulae in a proof. This means 
> forgetting about the semantics (and associated notion of equivalence) 
> and trying to reconstruct it in part. If you do so by resorting to a 
> meta level that keeps with it the old classical equivalence, then
(Continue reading)

Permalink | Reply | 4 comments |

Gmane