Re: Bureaucracy and identity

Hi Alessio,

I think we (at least you and me) basically agree on the informal notions.

> BUREAUCRACY AND IDENTITY
>
> Do we agree that bureaucracy and identity of proofs are intimately related?

yes.

> There is no formal notion of bureaucracy, but I guess the consensus is that, 
> when two proofs are *morally the same*, but they differ in *inessential 
> details*, then this is due to *bureaucracy*.
>
> If this is so, we should conclude that eliminating bureaucracy should lead us 
> to eliminate the inessential details that blur the `sameness', i.e., 
> identity, of proofs.

yes.

> 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.

> In particular, the notion of identity should be related to the notion of 
> *inference step*, and I think that inference steps become sort of confused 
> both in categorical models and in term calculi. I think that by looking at 
> inference steps, we can get a better judgment of what is the same and what is 
> not.

I believe that this "confusion" is due to the bad presentation of 
categorical models and of term calculi. In the last years we have 
developed a lot of technology to improve the situation. But it has to be 
done! In principle it is all the same (it is like with these three blind 
man touching an elefant...). At some point in the future we will have the 
GUT of proof theory.

> HOW MANY KINDS OF BUREAUCRACY?
>
> Do we agree that we should not suppose that there is only one kind of 
> bureaucracy?

yes

> BUREAUCRACY IN THE FORMALISM AND IN THE DEDUCTIVE SYSTEM
>
> ...
>
> Do we agree?

I agree with what you said in that section.

> BUREAUCRACY IN FORMULAE
>
> 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.

> 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.

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

no.

> 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?

> A PROBLEM WITH COMMUTATIVITY AND ASSOCIATIVITY
>
> Working under associativity and commutativity is difficult. Actually, it is 
> also dangerous.
>
> The very first thing that Francois told me after seeing deep inference for 
> the first time was that I was going to have problems with the way I was using 
> equations. So far, there was no problem, but I do have a serious problem now, 
> in the war to bureaucracy.
>
> This is actually not a problem in the technical sense (point 1 above) but it 
> is a problem in a moral sense (point 2), so it's indeed serious!

I don't see the distinction between the two.

> 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.

> In the next email I'll show you a solution to the problem.

In the next mail I'll comment on that.

-Lutz