Re: Bureaucracy and identity

Hello,

I think that this discussion on bureaucracy is 
very helpful, at least for me. My attitude, of 
course, is not that of trying to convince people 
of my point of view. Rather, I only try to make 
it clearer.

I'm sure we agree on everything if we clarify our 
positions enough, and I insist that it's very 
important that we have several different 
approaches to this problem. Actually, the more, 
the better.

This is not some sort of ecumenical speech: in 
most cases I think that a single personal point 
of view is more fruitful than a committee one, 
but in this case the problem is vague, and for 
this reason we better have different (converging) 
approaches.

At 19:54 +0100 23.3.05, Stéphane Lengrand wrote:
>>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'm not sure. Inference steps are natural 
>because they correspond more closely to human 
>reasoning, but the latter can be bureaucratic 
>and so far, sequentialising reasoning steps has 
>always been a source of bureaucracy. Proof-nets 
>are the typical formalism that gets rid of 
>bureaucracy precisely by blurring completely the 
>inference steps. If Wired Deduction gets rid of 
>it, though it is still based on inference steps, 
>I'd be extremely happy.
>Also, having a formalism close to human 
>reasoning might not be the first priority for 
>some people. For instance, I'd be much happier 
>to have a formalism suited for proof-search and 
>automatic reasoning.

I think we basically agree.

Just to clarify: I'm not looking for something 
that captures human reasoning. I think that we 
will actually have to go the opposite direction. 
There might be a `philosophical' reason for that, 
too: human reasoning is sequential!

However, we should ask for objects (derivations, 
nets) that are natural for human reasoning *as 
objects*. So, the way nets encode proofs is maybe 
not natural, but we can appeal to natural 
mathematical notions to describe them.

Commutativity is a typical example of this: it's 
not natural for humans to think in parallel, but 
it's natural to rotate pictures of parallel 
proofs. I think this makes the whole point, do 
you agree?

>>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. Actually, I'd say it's the very last. Here is my argument:
>
>I'd say that not only there is 
>formalism-bureaucracy and 
>deductive-system-bureaucracy, but there is also 
>logic-bureaucracy.
>There are some non-commutative logics after all. 
>In the case of AC, most of the languages used in 
>formalisms do not consider formulae modulo 
>equations. CoS does, but Natural deduction, 
>Sequent Calculus, or axiomatic Hilbert-style 
>systems do not. By that I do not mean it is 
>better not to do it.
>But in all those formalisms the fact that A/\B 
>is the same as B/\A is a theorem of the logic, 
>not an axiom as in CoS. Actually, there are lots 
>of other equivalences, and we do not want to 
>consider formulae modulo all of them. The thing 
>with AC is that not only the formulae are 
>equivalent but there is also a *type 
>isomorphism* between them. And the thing is that 
>I see no reason to have a special treatment for 
>AC and not for any random kind of type 
>isomorphism. Yes, because of the equations on 
>formulae, CoS identifies some type isomorphisms 
>(even the one between AxB->C and A->(B->C) ). 
>Considering formulae modulo AC breaks the 
>statndard representation as a tree, but 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.

Two things:

1) All of my arguments were inspired by and about 
classical logic. I agree with you that fancier 
logics might need a fancier attitude than mine 
for classical logic (but this wouldn't be 
impossible in my formalism!).

2) Your arguments are very syntactical (just a 
fact, neither good nor bad). Suppose there is no 
syntax (not even a language), only the semantic 
idea of classical logic, and you have to come up 
with a syntax. As soon as you decide to use 
grammars and strings, you introduce 
sequentialisation, which you wouldn't introduce 
if you decided to use graphs. Since this 
sequentialisation is *the very first* bureaucracy 
introduced, in my opinion this should be the very 
first to be thrown away. Of course, this only 
holds if one wants to stay true to the semantics 
and disregard the rest.

Of course, people see a computational (= 
syntactical) meaning of proofs, part of which has 
to do with type isomorphism. If you want to 
preserve (some of) that, than I agree with you 
that getting rid of AC might not be the starting 
point. However, in the case of type isomorphism, 
you're also committed to a specific kind of 
normalisation (cut elimination). What happens to 
your argument if you don't commit to that (as I 
don't do)?

As you know, I'm always skeptical of 
computational interpretations, and I think that 
Curry-Howard is mostly a coincidence. Anyway, I'm 
here to learn. As I said above, it's important 
that we keep distinct viewpoints.

>I think it is utopic to set as a task of the 
>formalism to remove every kind of 
>logic-bureaucracy that can ever come up in the 
>future.
>As you said yourself:
>
>>It is hopeless to try and define bureaucracy once and for all.
>
>That said, I think that if our formalism has all 
>the qualities that we dream of, and we have some 
>specific "plug-in" to deal with some 
>logic-specific bureaucracy such as AC, it's even 
>better!!

This is actually the case, and it's very simple. 
So, to recapitulate, suppose we adopt wired 
deduction, where associativity and commutativity 
are thrown away since the beginning because we 
work modulo AC. Suppose then that a logic comes 
which requires non-commutativity, like BV, or 
NEL, or Yetter's logic.

It's very simple! Since there are relations 
imposed on the wires, and these relations can 
very well be non-commutative, you keep your 
sequential information with you by just carrying 
with you the logical relations.

Associativity is only slightly trickier. If you 
really want to keep the associativity 
information, you need to build formulae *inside* 
the proof. For example, the formula A * (B * C) 
is `generated' inside a bigger derivation by

    A * (B * C)
    -----------
     A * true   .
     --------
       true

This would be distinct from the derivation ending in (A * B) * C.

In other words: associativity and commutativity 
are properties that I require for the 
*geometric*, *underlying* support. What you do 
above it, meaning what logical relations connect 
the wires, is the business of the deductive 
system, not of the formalism.

Is this convincing?

>>>What do you mean by *no equations*? In the 
>>>technical section you have equations for 
>>>associativity and commutativity.
>>
>>I mean no equations apart from those necessary to control bureaucracy.
>
>What else would we ever consider equations (such 
>horrible things) for? that's the least one can 
>ask, and the least you use them the better.

Again, it depends on the point of view. However, 
we agree that the least we use them, the better, 
so what I meant was `no equations apart from 
those STRICTLY necessary to control bureaucracy'.

>otherwise it's rather easy to define equivalence 
>classes of derivations in CoS,

It might be easy to define them, but very 
complicated to characterise them decently.

>and there you have your perfect formalism. What 
>we want is a formalism for canonical 
>representatives.

We ALSO want that, but we probably also want a 
formalism where more derivations than just the 
canonical representatives live, like formalisms 
A/B. In fact, as you and Kai show, for these 
formalisms term calculi are possible, and also 
elegant.

In fact, a possible plan is to go ahead with my 
deductive definition of system B, and then 
possibly show that your and Kai's system 
normalises formalism B proofs to canonical terms 
which, under AC, faithfully represent nonlinear 
wired deductions. This is 
bureaucracy-killing-normalisation, of course, not 
cut elimination or decomposition, or anything 
else.

Does it make any sense?

>>A PROBLEM WITH COMMUTATIVITY AND ASSOCIATIVITY
>>[...]
>
>Yes, that's exactly the problem Kaï and I 
>spotted, which made us put commutativity and 
>associativity as two-ways inference rules.
>Let me point at this stage that this decision is 
>completely orthogonal to having a deductive 
>system or a term formalism with typing rules. It 
>wouldn't be fair to disregard term syntaxes just 
>because we decided not to adress the AC 
>bureaucracy (though you may find other reasons 
>why doing so).

That was absolutely not my intention! As I told 
you already, I'm very sorry for giving you this 
impression.

I'm simply trying to show that there is also some 
value in looking at things from the geometric 
viewpoint.

>ABOUT WIRED DEDUCTION
>
>Just wanted to mention the fact that the way you 
>name the wires (whether it's with numbers or 
>whatever) is completely arbitrary so it 
>introduces exactly the same kind of bureaucracy 
>as alpha-conversion. Of course this has been 
>widely studied...

Well, clearly, you define identity modulo 
permutations of wires, I don't see any problem in 
this, I wouldn't call it bureaucracy.

>>2  COMPOSITION OF RULES
>>
>>This part needs to be completed. For now, 
>>suffice to say that we compose rules
>>like in the calculus of structures. Of course, it is possible to define more
>>geometric notions of compositions, like for formalism B.
>
>Well, that was actually the part I was waiting 
>for, where you explain how all the bureaucracy 
>is removed :-)
>I'd really like to see how you define 
>composition so that only canonical forms are 
>produced.

Just take CoS proofs, rewrite them by using wired 
rules instead of the standard ones, and then let 
the horizontal bars go up and down through the 
holes as they like.

It's a total triviality!! It's really an 
elementary school exercise: for every wire, what 
matters is the order of the logical relations 
that cross it. Collect this information for all 
the wires and you have your canonical proof.

Compare proofs modulo permutations of wires and 
you have your basic notion of identity.

If you want more sophisticated identity notions, 
than you need first to permute rules according to 
some specified set of permutation rules, and then 
repeat the procedure above.

Convinced? I didn't work at all on this specific 
notion, because it should be just an exercise, 
but, of course, if you find that something is 
unconvincing, or you have a difficult example, 
I'm interested...

>>3  CLASSICAL PROPOSITIONAL LOGIC
>>
>>*Proposition*   The _contraction_ rule
>>
>>       [P P]
>>    c_ ~|~^~ ,
>>        P
>>
>>is derivable for KSw.
>
>Let's be precise here. What you seem to prove is 
>that for all formula P, there is a derivation 
>from [ P P ] to P.
>the your contraction rule is rather a scheme of atomic rules.

Right.

>Nothing to do with what you call a local rule 
>having some kind of pipe, so you can't "permute" 
>it with some derivation operating on P (anyway, 
>the rule wouldn't be linear, and you forbid 
>that, which is a safe choice).

Right again. However, of course, you can permute 
contractions by rewriting derivations according 
to permutation rules (i.e., rules that tell you 
how to permute two instances of specific 
inference rules). So, if the particular 
bureaucracy you want to get rid of has to do with 
observing derivations modulo permutations of 
contractions, you can do that.

Of course, wired deduction doesn't offer you only 
canonical forms for this kind of bureaucracy. No 
formalism will ever offer you this for every 
possible kind of bureaucracy, we surely agree on 
this.

>Coming to linearity, I think I agree with Lutz: 
>I dislike the wired versions of atomic 
>contraction and rule ww. I see that this is how 
>you ensure linearity, but maybe we do not want 
>linearity of the wires.

Regarding ww, this is how I ensure minimality of 
rules. If you had the normal weakening, you would 
need some more rules. Specifically, you need a 
rule that creates a conjunction going up, 
something like

    (t f)
    -|-|- .
    [f f]

It's just an example, I don't know whether it 
works, but for sure, if you add enough of the 
right rules, it will work at some point (just add 
all the normal equations as rules, and you 
certainly have enough).

Of course, you might not want minimality of rules 
(actually, I don't care about that, I did the 
difficult exercise just because I wanted to make 
a secret test of subatomic logic!). In that case, 
no need to use strange rules.

Regarding contraction: you're right, it is for 
getting linearity. If you don't want linearity, 
just use the normal contraction. Everything else 
still works, including, of course, getting rid of 
basic bureaucracy.

I realise that I should have started presenting 
wired deduction in the nonlinear case, but I was 
too happy that it worked in the linear one, which 
is the one that is going to make categorists 
happy, I believe.

At 0:03 +0100 24.3.05, Stéphane Lengrand wrote:
>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.

I think formalism B is *much* simpler to market 
and explain than wired deduction to the 
non-esoteric proof theorist. I disagree on seeing 
duplication of information. If you present the 
slices and pipes intuition at the same time as 
inference rules, people will agree that there is 
no duplication of information, and it's such a 
simple definition (conceptually, on paper it's a 
bit of a bastard)!

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

Of course, we could. It just happens that in all 
the CoS systems the rules are separated the way I 
do in wired deduction. If there's a `deep' 
reason, I don't know. Actually, I have a clue (in 
subatomic logic), but I need some more work on 
that.

-Alessio