[Prev][Next][Index][Thread]

cut-elimination and combinatorics



Date: Sat, 4 Jan 92 16:02:01 +0100

 Trying to formalise the notion of "interaction sequence" in a
game-theoretic formulation of cut-elimination, I came out with
the following purely combinatorial statement. 


 DEFINITION: an INTERACTION SEQUENCE is a pair (S,f) such 
that S(0> empty, S(n) subset [0,n[, f(n) defined for n positive, 
and for all n

 S(n+1) = {n} u S(f(n)),    f(n+1) in S(n+1).



 LEMMA ("finiteness" of interaction sequences): 
 =====
 Given an interaction sequence (S,f)
 .either there exists an infinite sequence n(1) < n(2) < n(3) ... 
such that f(n(p+1)-1) = n(p) for all p, 
 .or there exists an infinite sequence n(1) < n(2) < n(3) ... 
such that f(n(p+1)) = n(p) for all p.



 (The proof is based on the remark that if f(m) = n, and m is not in the 
range of f, then for all k > m, S(k) and [n,m[ are disjoint.

 Intuitively, each positive integer n represent the index of a move in a game,
S(n) the set of index to which this move can answer, and f(n) the index
to which this move actually answers.)



 I would like to know if this statement, or a similar statement, is known
elsewhere in combinatorics. Many thanks in advance.