Re: Bureaucracy and identity

Hi,

actually, I did have the slight feeling that not addressing the AC bureaucracy put you off the term 
syntax approach, and I'm glad if I was wrong. I just wanted to clarify anyway the fact that a term 
formalism does not make the problem more difficult.
We think it makes the systems very clean, logic-independent, and using a background that is 
well-known. But I also admit that it would be interesting to hide the syntax part and just show the 
"purely logical" aspect. Maybe that's what wired deduction is. To be honest, I'm much more enthused 
about it than Formalism B in earlier presentations, where inference rules act on derivations, thus 
unnecessarily duplicating information.

> One more thing: I agree that pipes and tubes should be the same thing (I guess they're both 
> realisations of that idea Stephane and I discussed in Paris at the end of Michel's workshop, 
> right?). I prefer the word `pipe' because it reminds me of when I was young and smoking pot, 
> instead of taking the underground, but that's all.

Yes, that's the realisation of those ideas, and I think I even prefer "pipes" to "tubes", though I 
never tried such smoking.

Question about wired deduction:
Is there any reason why separating atomic rules from local rules? Why can't we have some rules that 
both manipulate pipes and wires?

Stéphane

PS: Typos and paragraphs I'd like to rephrase:

> The thing with AC is that not only the formulae are equivalent but there is also a *type 
> isomorphism* between them. And I see no reason to have a special treatment for AC and not for 
> other type isomorphisms. It is true that, thanks to equations on formulae, CoS identifies some 
> type isomorphisms (even the one between AxB->C and A->(B->C) ), and considering formulae modulo AC 
> breaks the statndard representation as a tree.
> The trouble is that some day, someone will come up with a fancy logic and some 
> never-heard-of type
> isomorphisms that make the equivalence clases of formulae look like weird 
> mathematical objects
> (why not cycles, for instance?), and all the work we'll have done for AC might just not work 
> there.

[...]

> > I mean no equations apart from those necessary to control bureaucracy.
>  What else would we ever consider equations (such horrible things) for? The less you use them, the 
> better.


> It will motivate sub-atomic stuff even more.