[FOM] Proof Identity

[Alessio Guglielmi]

Hello,

quick answers to Jon Cohen's remarks in 
<http://www.cs.nyu.edu/pipermail/fom/2005-December/009424.html>:


1) Jon suggests that natural deduction is as good as deep inference 
in removing the bureaucracy associated to rule permutations. This is 
(perhaps) true on the technical level, but false on the moral one. In 
fact, a proof in natural deduction strictly depends on the formula 
tree of its conclusion (more so than the sequent calculus).

There are less permutations simply because the formalism is more 
rigid, but this can hardly be considered a lack of bureaucracy. In 
deep inference, inference happens `at the same time' everywhere in a 
formula.

All that said, notice that not many logics have natural presentations 
in natural deduction, contrary to what happens in deep inference. In 
the case of natural deduction there's bureaucracy not only in proofs, 
but sometimes also in inference rules.


2) It's true that a coherence theorem gives you a natural definition 
of proof identity, however, this notion is only natural in the 
technical context you find yourself in. If you start from biased 
categorical models, you get biased proof identity notions. Such a 
fundamental question like proof identity should be addressed in the 
less technical way possible, I believe.


3) I don't think that deep inference proof theory should be distinct 
from categorical proof theory: quite the opposite! Deep inference is 
more categorical in spirit than any other formalism (Dominic Hughes 
gives an excellent account of this in the paper you also cite 
<http://boole.stanford.edu/~dominic/papers/di/di.pdf>, and there's a 
forthcoming PhD thesis by Richard McKinley).

However, I'm not sure that looking for coherence conditions is the 
best way to tackle the problem of identity of proofs. As Jon 
acknowledges, inference rules give rise to categorical structures, 
but not the converse. At least, I don't know examples of cases where 
this happened. Notice that I'm not speaking of the technical problem 
of mapping categorical constructions into rules, I'm speaking of the 
psychological and methodological problem of discovering the `right' 
rules.

The problem of proof identity depends on the shape of inference 
rules. In my opinion, it is more direct and fruitful to look at 
inference rules proof theoretically rather than through categorical 
constructions. Category theory, in this case, is useful in the 
background, more for avoiding moral mistakes than for providing 
inspiration. Since the problem of proof identity, at this time, 
requires more a definition than a technical solution, I would leave 
the technicalities of categorical constructions to the time when we 
are happy enough with the definitions.

Of course, there's plenty of technology available in categorical 
semantics for getting many proof identity notions (and publish many 
papers), but I think we should aim at a notion that can be explained 
to high school students.


Cheers,

-Alessio