Re: Bureaucracy and identity

At 13:14 +0100 16.3.05, Lutz Strassburger wrote:
> > I think there are two ways of tackling this problem:
> >
> > 1) We ask for purely technical properties to hold, like for example 
> > the non-collapsing of a categorical model, or the existence of 
> > canonical forms.
> >
> > 2) We start from the question of what `morally the same' means and 
> > go for that!
> >
> > The two ways are not mutually distinct (on the contrary!), however, 
> > I insist on the importance of the second one because I believe that 
> > the first approach should *follow* the second, and not the other 
> > way around.
>
> You have to be a bit more careful here. Of course you start by 
> meditating on what is `morally the same'. But as soon as you have 
> made up your mind, you need to translate that into some purely 
> technical properties that you want to hold. And only then you can go 
> for it.

Thanks for the advice!!

Anyway, I see that what I meant is not very clear. I was trying to 
avoid polemicising, but maybe I can be a bit more explicit.

For example, we know that there are several ways of making cut 
elimination confluent for classical logic. However, many of these 
methods are just technical stunts: you get confluence but what you do 
to get it *means nothing*.

In the war to bureaucracy, the danger is the same: I'm sure one can 
get canonical forms in thousands of different ways, especially with 
deep inference (which opens up many possibilities). However, I 
believe that only the notions that *mean something* will lead to 
further research, interesting developments, etc.

Of course, the question is what could this meaning be. I have no 
philosophical answers, but a rule of thumb could be that a given 
notion should have *at least two* completely different 
characterisations. For example: a deductive system and its associated 
term calculus, like in the Curry-Howard correspondence.

The same thing in other words: every time a `problem' (like `getting 
rid of bureaucracy') is not formally defined, there is a strong 
temptation to define it *after* one has found a technical solution. I 
think we should resist the temptation and set the bar (2) *before* 
making the jump (1). (In computer `science', where formalised 
problems don't abound as much as in mathematics, many people don't 
set the bar or set it after, and this of course is ridiculous, in my 
opinion.)

Enough said. Do we agree on this?

> > Do we agree that the *very first* source of bureaucracy in *all 
> > deductive systems* in *all formalisms* is associativity and 
> > commutativity (when present) in formulae?
>
> no.
> It certainly is bureaucracy. But not necessarily the "very first". 
> You simply lose importaint aspects if you take that for granted.

Which aspects? I might very slightly agree about associativity, but I 
feel I will never agree about commutativity. Give examples!

> > I mean, we do not want to distinguish formulae, and so proofs, just 
> > because of the order of associations, right?
>
> In principle yes. But I have my objections to putting this on a 
> higher level than "type A" or "type B" bureaucracy.

The plot thickens... Which objections?

> > Do we agree that *every* war to bureaucracy should start from this 
> > realisation?
>
> no.

So, what's the alternative? Suppose I have to write an introduction 
to the subject, what would you suggest?

> > Do we agree that the only practical way of dealing with 
> > commutativity is working under an equivalence relation that takes 
> > care of it?
>
> I am not so sure about this, maybe it is just a lack of 
> imagination... (although right now I cannot come up with a good 
> alternative)
>
> > (I guess that recognising this symmetry is the very first step 
> > towards a *geometric* understanding of proofs, and not doing it 
> > means abandoning all hopes for that goal.)
>
> which symmetry?

Commutativity.

> > Consider
> >
> >        E   C
> >     [  |   | ]
> >      [A B] A
> >   * ---------- .
> >       A [B A]
> >     [ |   |  ]
> >       D   F
> >
> > This is a derivation in formalism B in which two derivations are 
> > vertically composed by *, and we work under commutativity and 
> > associativity. The problem is that this is the only way I have in 
> > formalism B for representing (what I could graphically and 
> > imprecisely represent as)
> >
> >        E    C
> >     [  |    | ]
> >      [A B]  A
> >       |  \  |   .
> >       A  [B A]
> >     [ |    |  ]
> >       D    F
> >
> > However, the same derivation above could also stand for
> >
> >        E   C
> >        |   |
> >     [[A B] A ] ,
> >        |   |
> >        F   D
> >
> > and this of course is *morally different*!
> >
> > What can I do? Well, I could stop working under commutativity and 
> > associativity: this way I could easily distinguish between the two 
> > cases. However, if I drop commutativity and associativity, I get 
> > back all the bureaucracy in formulae, with a vengeance, because now 
> > this bureaucracy scales up to proof composition.
>
> I think the problem only appears because you put the 
> commutativity-and-associativity-bureaucracy on a higher level than 
> the type-A-bureaucracy and the type-B-bureaucracy. The problem would 
> disappear if you consider 
> commutativity-and-associativity-bureaucracy as a special case of 
> type-B-bureaucracy.

Example, please.

-Alessio