Finite choice property

Hello,

I think we need to be clearer about our way to 
cope with the subformula property (SFP). The 
problem is that, from the point of view of 
marketing, it's too weak to say that `we have a 
weaker property than the subformula one, but what 
we have has the same features'.

So, especially in view of the survey paper we are 
working at, I propose formally to introduce a new 
notion, which we could call the *finite choice 
property*:

*** Definition   We say that a formal system S 
has the *finite choice property* (FCP) if, for 
every inference rule r in S and for every 
structure (or sequent, or formula) T, the set of 
instances of r whose conclusion is T is finite.

Clearly, SFP => FCP but FCP /=> SFP (loosely 
speaking, the first implication works if SFP is 
carefully defined, but that is usually the case, 
at least in propositional logic). Then, we can 
claim that what people really want is FCP, which 
is more general than SFP, and so why not using a 
more general formalism than one with SFP?

Please give me feedback on this, and don't trust 
me on the choice of words, etc. I think this is 
important.

Please also consider the following alternative.

The notion I just defined is top-down asymmetric, 
as SFP is. It might be worthy to consider an 
alternative definition of FCP which makes justice 
of CoS's top-down symmetry (for convenience, I 
define this notion only for CoS, but it's obvious 
how to modify it for other formalisms):

*** Definition   We say that a formal system S 
has the *upwards finite choice property* (UFCP) 
if, for every inference rule r in S and for every 
structure T, the set of instances of r whose 
conclusion is T is finite.

*** Definition   We say that a formal system S 
has the *downwards finite choice property* (DFCP) 
if, for every inference rule r in S and for every 
structure T, the set of instances of r whose 
premise is T is finite.

*** Definition   We say that a formal system S 
has the *finite choice property* (FCP) if it has 
UFCP and DFCP.

In this case, what matters for provability is 
UFCP. We can't normally claim FCP for classical 
logic, because identity and weakening violate it. 
Of course, normal systems at least have the 
identity rule, so it looks like getting FCP is 
desperate, and so it's not worthy to introduce 
the notion this complicated way.

On the other hand, it might be nice to have DFCP 
handy for *refutations*, meaning that if one day 
we decide to use CoS as a unifying formalism also 
for refutations, then it might be nice to have a 
symmetric notion of finite choice. For this 
reason, it might be worthy to start on the right 
foot in this matter. (By the way, in subatomic 
proof theory FCP always holds, but this is still 
science-fiction.)

So, what do you think?

One more thing. What do you think about this new entry for the FAQ page?

*** Question   Your `cut-free´ systems don't have 
the subformula property! Are you crazy?

*** Answer   No. Our cut-free systems enjoy the 
finite choice property, which means that given a 
conclusion, every inference rule yields a finite 
set of possible premises. This is the essence of 
the subformula property. Technically speaking, 
the subformula property is meaningless for our 
systems (and so they don't enjoy it). The reason 
is our abolishing the distinction between formula 
and sequent, i.e., the distinction between object 
and meta (or judgmental, structural) level in 
derivations.

Ciao,

-Alessio