Re: Is cut semantical?

[categories <cat-dist@mta.ca>]

Date: Mon, 25 Aug 1997 08:46:46 -0700
From: Vaughan R. Pratt <pratt@cs.Stanford.EDU>


Just to clarify, my question was about proofs with cut, not about cut
itself, whose semantics is perfectly clear.  (I received a couple of
replies from people who merely answered the question in the subject
line, apparently without reading the message.)

The difficulty is that the standard semantics of cut as composition is
not injective, in that it erases the information as to the location of
the cut, as a nasty side effect of associativity.  I therefore do not
see how to attach semantical significance to proofs with cut, as
opposed to their cut-free counterparts where the situation is much
clearer.

This issue arises not just for the denotational semantics of proof but
its operational semantics as well.  In theorem-proving, proofs with cut
are in principle attractive because they can be quite short in
comparison to their cut-free counterparts.  In practice the difficulty
when backchaining of deciding where to put cuts, and what formula to
cut on, seems to make it much harder to find proofs with cut than
without.  Good decision methods are much easier to find for cut-free
logics.

Granted that making algorithmic sense of cut (in the context of a
proof) is hard enough, can one even make semantic sense of it *in that
context*?  That is, is there any bijection between proofs with cut and
some reasonable class of mathematical objects?

Presumably the class will not be closed under composition, at least not
of the associative kind.

Far from being the answer to my problem, composition is its root.

Vaughan Pratt