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