PROOF THAT (P1) IS EQUIVALENT TO GIRARD'S `TECHNICAL CONDITION'
===============================================================
Recall Girard's technical condition (G), and condition (P1) from the
LICS paper:
(G) if v is a weight generated by the weights occurring in \Theta,
and x is a &-vertex, then v.~w(x) does not depend on p_x, where
w(x) is the weight of x and p_x is the eigenvariable of x.
(P1) for any &-resolution R of \Theta, exactly one linking of \Theta
is on R.
Here \Theta is a collection of slices \Theta(\phi), one for each
valuation \phi, such that \Theta(\phi) resolves &'s consistently with \phi,
ie, the additive resolution underlying \Theta(\phi) is a subgraph of
the &-resolution R(\phi) determined by \phi. (Recall that a valuation
is an assignment of 0 or 1 to each eigenvariable, ie, a choice of
right or left for each &.)
To prove (G) <=> (P1) we shall use the following stepping-stone
conditions. The first is the relaxation of (G) obtained by
restricting to weights of axiom links.
(G-AX)
if v the a weight of an axiom link of \Theta, and x is a &-vertex,
then v.~w(x) does not depend on p_x.
(SELF-INDEP)
no & depends on itself, ie, for all &-vertices x of \Theta,
w(x) does not depend on p_x.
(PRESENCE)
an axiom link z depends on a &-vertex x in a slice S only if
x is in S.
(Recall that z depends on x in \Theta(\phi) iff z is in \Theta(\phi)
but not in \Theta(\phi^x), where \phi^x is the valuation obtained from
\phi by toggling the 0/1 value of \phi(x).)
PROPOSITION
===========
(G) <=> (G-AX) and (SELF-INDEP) <=> (PRESENCE) <=> (P1)
Proof of (G) <=> (G-AX) and (SELF-INDEP)
-----------------------------------------
(G)=>(SELF-INDEP) follows by taking v=~w(L) in (G), and the fact that a
weight x depends on p iff ~x depends on p; (G)=>(G-AX) is trivial.
Conversely, (G-AX) and (SELF-INDEP) => (G) because, for any weight u not
depending on p, and any weights w and w',
(1) [w.u indep of p] and [w'.u indep of p] => (w|w').u indep of p
(2) [w.u indep of p] and [w'.u indep of p] => (w.w').u indep of p
(3) w.u indep of p => ~w.u indep of p
(NB x|y = "x or y", and ~w.u=(~w).u) In turn, (1) and (2) follow from
(a) [x indep p] and [y indep p] => x|y indep p
(b) [x indep p] and [y indep p] => x.y indep p
respectively, since (w.w').u = (w.u).(w'.u) and (w|w').u = (w.u)|(w'.u).
Finally, for (3), if ~w.u depends on p, then (w.u)|(~w.u) = (w|~w).u = u
depends on p, a contradiction.
Proof of (G-AX) and (SELF-INDEP) <=> (PRESENCE)
------------------------------------------------
We begin with an auxilary Lemma:
Lemma 1. If x is in \Theta(\phi) but not in \Theta(\phi^x), then some
axiom link depends on x in \Theta(\phi^x).
Proof of Lemma 1:
let y be the first vertex below x which is in both \Theta(\phi)
and \Theta(\phi^x); pick an axiom link above y.
Proof of (PRESENCE) => (SELF-INDEP):
x self-dependent
=> x in \Theta(\phi) but not \Theta(\phi^x)
=> (by Lemma 1) an axiom link depends on x in \Theta(\phi^x)
=> (by (PRESENCE)) x in \Theta(\phi^x), contradiction.
Proof of (G-AX) <=> (PRESENCE), given (SELF-INDEP).
Below is z an axiom link with weight v.
(G-AX)
<=>
v.~w(x) indep of p_x
<=>
all \phi. \phi(v.~w(x)) = \phi^x(v.~w(x))
<=>
all \phi. [z in \Theta(\phi) and x not in \Theta(\phi)] iff
[z in \Theta(\phi^x) and x not in \Theta(\phi^x)]
<=>
all \phi. x not in \Theta(\phi) implies
[z in \Theta(\phi) iff z \in \Theta(\phi^x)]
<=> (by (SELF-INDEP))
all \phi. x not in \Theta(\phi) implies z indep of x in \Theta(\phi)
<=> (contrapositive)
all \phi. z dep on x in \Theta(\phi) implies x in \Theta(\phi)
<=>
(PRESENCE)
Proof of (PRESENCE) <=> (P1)
----------------------------
(PRESENCE) => (P1). Existence follows immediately by definition of
\Theta as a set of slices \Theta(\phi)\subseteq R(\phi), one for each
valuation \phi. For uniqueness: suppose \lambda and \lambda' are
distinct linkings of \Theta, say from slices \Theta(\phi) and
\Theta(\phi'), with both \lambda and \lambda' on the same &-resolution R.
Claim: there exists a &-vertex x with \phi(x) not= \phi'(x), and x is
not in at least one of \Theta(\phi) or \Theta(\phi'). Proof of Claim:
pick any x such that \phi(x) not= \phi'(x) [exists, since \phi not=
\phi']; if x is not in R, then it is not in \Theta(\phi)\subseteq R,
as sought; if x is in R, then it cannot be in both \Theta(\phi) and
\Theta(\phi'), since R chooses (say) left for x, and one of
\Theta(\phi) and \Theta(\phi') chooses right (since \phi(x) not=
\phi'(x); QED Claim.
Without loss of generality, x is not in \Theta(\phi). Thus by
(PRESENCE), \Theta(\phi^x)=\Theta(\phi). Repeating this argument
for the remaining &-vertices on which \phi and \phi' differ,
we obtain \Theta(\phi')=\Theta(\phi), a contradiction.
(P1) => (PRESENCE). Suppose the axiom link z depends on x in
\Theta(\phi), and x is not in \Theta(\phi). Let \lambda be the
linking of \Theta(\phi), and let \lambda' be the linking of
\Theta(\phi^x) (distinct from \lambda, since z depended on x). Since
\Theta(\phi)\subset R(\phi) [by definition], and x is absent from
\Theta(\phi), we have also \Theta(\phi)\subseteq R(\phi'); thus both
\lambda and \lambda' fit on R(\phi'), contradicting (P1).
DJDH 2003/07/16