[Prev][Next][Index][Thread]
kingdom of several formulas
Date: Thu, 12 Dec 91 15:39:59 +0100
To: Linear@cs.stanford.edu
Following discussions between V. Danos, G. Gonthier and I, we propose two formulas for computing k(F1,...,Fn), the
intersection of all subnets containing F1,...,Fn (see the penultimate message
of G. Bellin). In general F1,...,Fn are not conclusions of k(F1,...,Fn).
1. Let S be a switch of a given multiplicative proof-net R (hence S is an
acyclic and connected subgraph of R containing all formulas of R) and let the
Fi's be any formulas of R; then
k(F1,...,Fn) = union{k(F); F is in the smallest subtree of S
containing the Fi's}.
Same proof as for k(A PAR B) in the last letter of Danos.
2. We can also compute k(F1,...,Fn) by induction on n:
k(F1,...,Fn) = k(F1, F2) U k(F2,...,Fn).
To see that, notice that the union of two subnets of R with a non void
intersection is a subnet of R; thus the rhs of the equation is a subnet and,
by definition of kingdoms (k is the smallest subnet containing ...), it
contains k(F1,...,Fn); on the other hand k(F1, F2) and k(F2,...,Fn) are easily
seen to be included in k(F1,...,Fn).
3. Something else : a possible amendment to kingdom could be to define it
to be the smallest module (and not subnet) containing a given set of links.
Here we mean a module to be simply a subnet with hypotheses. Formulas given
so far are still appropriate.