Re: Clarification on rule schemes

On Wed, 5 May 2004, Charles Stewart wrote:

> 
> 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.  

Just a clarification:
I think you talk about different principles. Alessio says that logical 
rules (rules which introduce logical connectives) should exhibit only one 
connective (but possibly more than one occurrence). In other words, the 
introduction of a connective should not depend on the presence of 
different connectives (I think Wansing already named this principle). 
Dosen´s principle is on a higher level: in a given framework, whatever the 
logic, logical rules should be uniquely defined. So, alternative logics 
(i.e. logics that share the same connectives) should differ only on their 
structural rules.

Phiniki