Re: Clarification on rule schemes

Dear all, dear sundry,

Just a brief addendum to what Alessio says, that I shall take in
a different direction.  He writes that:

	the most important principle is of course `to define
	connectives in isolation', meaning that you ask yourself
	how can you introduce the main connective of a formula,
	and then you try to come up with appropriate premises
	from which to conclude the desired conclusion. This works
	well for classical and intuitionistic logic, but not so
	well for linear and modal logics, and it doesn't work at
	all for some other logics like pomset logic. In linear
	logic, for example, the promotion rule does not obey this
	principle, because you define the `!' but you need to check
	for `?'s, so the `!' is not in isolation.

The above, known as Dosen's principle, is only one of a number of
holy cows we need to violate in order to get real progress in proof
theory.  Perhaps more contentiously, we need to recognise that
the subformula property is a nice, but superficial property that has
no non-accidental relationship to the fundamental notion of analytic
proof.  The ironically named "analytic cut" so beloved of lazy
workers in the ATP community ensures that proofs that bear it are
not analytic; the fact that one still can perform some weak kinds
of proof analysis in it's presence should not blind one to this
fact.  More importantly, in the presence of deep inference the
subformula property may be incompatible with the most revealing
presentations of proof analyticity.

Charles