[FOM] Proof Identity
Alessio Guglielmi
Lists at Alessio.Guglielmi.name
Thu Dec 8 13:28:50 EST 2005
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
More information about the FOM
mailing list