Streams and strings in formal proofs.
Streams are acyclic directed subgraphs of the logical flow graph of a proof representing bundles of paths with the same origin and the same end. The notion of stream is used to describe the evolution of proofs during cut-elimination in purely algebraic terms. The algebraic and combinatorial properties of flow graphs emerging from our analysis serve to elucidate logical phenomena. However, the full logical significance of the combinatorics, e.g. the absence of certain patterns within flow graphs, remains unclear.
Introduction
The analytical method which divides proofs into blocks, analyses them separately
and puts them together again, proved its failure: by "cutting up" it destroys
what it seeks to understand, that is the dynamics within proofs [CS97]. This
important point has been understood and emphazised by J-Y. Girard who, in
1987, introduced proof nets to study proofs as global entities and to study the way
that formulas interact in a proof through logical connectives. In 1991, another
notion of graph associated to proofs has been introduced by S. Buss [Bus91] for
different purposes (namely, as a tool to show the undecidability of k-provability)
and has been employed in [Car97, Car96, Car97a] to study dynamics in proofs.
This graph, called logical flow graph, traces the flow of occurrences of formulas
in a proof.
The combinatorics and the complexity of the evolution of logical flow graphs
of proofs under cut-elimination are particularly complicated and intruiging. An
overview can be found in [CS97] and a combinatorial analysis is developed in
[Car97b]. These difficulties constitute the main reason for looking at simpler
but well-defined subgraphs of logical flow graph and try to study their properties
and behavior in proofs.
We shall concentrate on streams (defined in Section 3). A stream represents
a bundle of paths traversing occurrences of the same atomic formula in a proof
and having the same origin and the same target. A proof is usually constituted
by several streams. They interact with each other because of logical rules and
share common paths because of contractions. There are cases where a bundle
of paths needs to be exponentially large in size like in the propositional cut-free
proofs of the pigeon-hole principle for instance (this is a consequence of [Hak85]
and a formal argument is found in [Car97c]), and the study of streams becomes
relevant for the study of complexity of sequent calculus proofs.
Our interest lies on the topological properties of streams. We shall be concerned
only with a rough description of logical paths in a stream. This description
will be based on axioms, cuts and contraction rules occurring in the
proof. Rules introducing logical connectives will not play any role. This simplified
treatment of logical paths allows for a description of proofs as strings
(Section 6), and for a natural algebraic manipulation of proofs (Sections 7 and
8). When logical flow graphs contain cycles, this description leads to precise relations
between proofs and finitely presented groups [Car98]. Here, we will only
look at proofs whose logical flow graph is acyclic and we shall develop a theory
which relates algebraic strings to streams. We prove that any stream can be
described by an algebraic string, and that for any string there is always a proof
with a logical flow graph which is a stream described by the string (Section 6).
Usually, several strings can describe the same stream. We shall characterise the
most compact and the most explicit ones (Sections 6).
In Section 8 we show that the transformation of streams during the procedure
of cut-elimination (Section 2.2) can be simulated by a finite set of rewriting
rules (Theorem 26). The notion of stream, though simple, is shown to
be very powerful at the computational level: Example 27 illustrates how, at
times, a purely algebraic manipulation of streams can completely describe the
proof transformation. Theorem 28 pinpoints how weak formulas in a proof influence
the complexity of streams during cut-elimination. Theorem 29 says that a
growth in complexity is either already "explicit" in a proof (i.e. a proof contains
a stream with large arithmetical value; this notion is defined in Section 7) or it
is due to purely global effects induced by local rules of transformation.
To conclude, let us mention that our algebraic analysis of proofs seems adequate
to approach the problem of the introduction of cuts in proofs, an important
topic in proof theory and automated deduction. It seems plausible that a
theory of the flow of information in a proof might lead to develop methods for
the introduction of cuts in proofs.
Basic notions and notation
In this section we briefly recall known concepts. For limitations of space, in
most cases, we shall refer the reader to the literature. Good sources are [Gir87a,
Tak87], and also [CS97].
2.1 Formal proofs
Formal proofs are described in the sequent calculus LK. This system is constituted
by axioms which are sequents of the form
any formula and \Gamma; \Delta are any collections of formulas, by logical rules for the
introduction of logical connectives and by two structural rules
Cut
Contraction
We shall extend LK with the rule
F -rule
where F is a unary predicate and   is a binary function. The F -rule is added
to LK because it allows to speak more directly about computations. It was
considered already in [Car97b, CS96a, Car96, CS97a].
In our notation, a rule is always denoted by a bar. The sequent(s) above
the bar is called antecedent of the rule and the sequent below the bar is called
consequent.
In the following we will frequently use the notion of occurrence of a formula in
a proof as compared to the formula itself which may occur many times. Notions
as positive and negative occurrence of a formula in a sequent are defined in
In an axiom the two formulas A are called distinguished formulas
and the formulas in \Gamma; \Delta are called side formulas. A formula A in \Pi which
has been introduced as a side formula in some axiom is called
A formal proof is a binary tree of sequents, where each occurrence of a
sequent in a proof can be used at most once as premise of a rule. The root
of the tree is labelled by the theorem, its leaves are labelled by axioms and its
internal nodes are labelled by sequents derived from one or two sequents (which
label the antecedents of the node in the tree) through the rules of LK and the
F -rule.
The height of a rule R in a proof \Pi is the distance between the consequent
of R and the root of the proof-tree describing \Pi.
At times we shall consider proofs \Pi which are reduced in the sense of [Car97b],
i.e. there are no superfluous redundancies in the proof which have been built
with the help of weak occurrences. More formally, no binary rule or contraction
rule is applied to a weak formula, no unary logical rule is applied to two weak
formulas and no occurrence in cut-formulas is weak. In [Car97b] it is shown that
given any proof, we can always find a reduced proof of the same end-sequent
which has a number of lines and symbols bounded by the ones of the original
proof.
2.2 Cut-elimination
In 1934 Gentzen proved the following result
Any proof in LK can be effectively transformed into a proof which
never uses the cut-rule. This works for both propositional and predicate
logic.
The statement holds for the extension of LK with the F -rule as well.
This is a fundamental result in proof theory and in [CS97] the reader can
find a presentation of its motivations and consequences. The computational
aspects of the theorem have been largely investigated but we are still far from an
understanding of the dynamical process which can occur within proofs [Car97,
Car96, Car97a]. After the elimination of cuts, the resulting proof may have
to be much larger than the proof with cuts. For propositional proofs, this
expansion might be exponential and for proofs with quantifiers, it can be super-
exponential, i.e. an exponential tower of 2's [Tse68, Ore79, Sta73, Sta78, Sta79].
We will not enter into the details of the steps of transformation of the procedure
of cut-elimination. The reader which is unfamiliar with them can refer
to [Gir87a] or [Tak87] (and also to [CS97] or to [Car97b]).
2.3 Logical flow graphs
As described in [Car97], one can associate to a given proof a logical flow graph
by tracing the flow of atomic occurrences in it. (The notion of logical flow graph
was first introduced by Buss in [Bus91] and a similar notion is due to Girard
and appeared in [Gir87]. Here we restrict Buss' notion to atomic formulas.)
We will not give the formal definition but we will illustrate the idea with an
example. Consider the two formal proofs below formalized in the language of
propositional logic and the sequences of edges that one can trace through them
cut
contraction
contraction
Each step of deduction manipulates formulas following a logically justified
rule, and precise links between the formulas involved in the logical step are
traced (the arrows indicated in the figures above represent some of these links).
Formulas in a proof correspond to nodes in the graph and logical links induced
by rules and axioms correspond to edges. As a side effect different occurrences
of a formula in a proof might be logically linked even if their position in the
proof is apparently very far apart. Between any two logically linked occurrences
there is a path. The graph that we obtain is in general disconnected and each
connected component corresponds to a different atomic formula in the proof.
The structure of the proof on the left is interesting because shows that paths
in a proof can get together through contraction of formulas, and the structure
on the right shows that cyclic paths might be formed.
The orientation on the edges of a logical flow graph is induced by natural
considerations on the validity of the rules of inference which we shall not discuss
here (see [Car97]). In the following we will not really exploit the direction of
the paths. We will use directions only to establish that a path starts and ends
somewhere. We might speak of a path going up or down, and of an edge being
horizontal, in case the edge appears in an axiom or between cut-formulas. These
latter will be called axiom-edges and cut-edges, respectively.
In the sequel, we call bridge any maximal oriented path that starts from a
negative occurrence, ends in a positive occurrence and does not traverse cut-
edges. The maximality condition implies that both the starting and ending
occurrences of a bridge should lie either in a cut-formula or in the end-sequent
of the proof.
A node of a logical flow graph is called a branching point if it has exactly
three edges attached to it. In a proof, branching points correspond to formulas
obtained by contraction or by a F :rule. We say that a node is a focussing
branching point if there are two edges oriented towards it. A node is called
defocussing branching point if the two edges are oriented away from it. A node
is called input vertex if there are no edges in the graph which are oriented
towards it. A vertex is called output vertex if there are no edges in the graph
which are oriented away from it. Input and output nodes are called extremal
points. In a proof, extremal points correspond to weak occurrences of formulas
and to occurrences of formulas in the end-sequent.
By a focal pair we mean an ordered pair (u; w) of vertices in the logical flow
graph for which there is a pair of distinct paths from u to w. We also require
that these paths arrive at w along different edges flowing into w.
Two logical flow graphs have the same topological structure if they can both
be reduced to the same graph by collapsing each edge between pairs of points
of degree at most 2 to a vertex.
The notions of bridge, focal pairs, topological structure, focussing and defo-
cussing point, input and output node have been introduced in [CS97a, Car97b]
where the reader can find properties and intuition.
A stream is an acyclic directed graph with one input vertex v and one output
vertex w. The pair (v; w) is called base of the stream. All other vertices in the
stream are not extremal.
If G is a directed graph, then a stream in G is a subgraph of G which is
a stream. A full stream in G based on (v; w) is a stream in G such that all
directed paths lying in G between v and w belong to the stream.
A substream of a stream is a subgraph of the stream that is based on a pair
(v; w), where v; w are nodes of the stream. A substream might have the same
base of the stream, but this is not required.
A stream of a proof \Pi is a stream in the logical flow graph of \Pi such that the
input and output vertices occur in the end-sequent of \Pi. A stream of a proof \Pi
is based on the pair of formulas (A; B), where A is a positive occurrence and B
is a negative occurrence.
In the simplest case, a stream of a proof is a bridge, but usually, the stream
of a cut-free proof will look (after stretching it) roughly as follows
input vertex
output vertex
where the bifurcation points correspond to the presence of contractions or F -
rules in a proof, the circles correspond to axiom-edges through which each path
has to pass, and the paths are oriented from left to right. In this way all
bifurcation points on the left hand side of the axiom-edges will correspond to
contractions on negative occurrences and the bifurcation points on the right will
correspond to contractions on positive occurrences or applications of F -rules.
If the proof contains cuts, a stream might be much more complicated. For
instance it might contain arbitrarily long chains of focal pairs as illustrated by
the following figure
output vertex
input vertex
where each horizontal edge (linking a focussing point to a defocussing point)
corresponds to a cut in the proof [Car97b]. It might also contain cyclic paths,
but we will not consider this situation here. The reader interested in cycles in
proofs can refer to [Car97c, Car97b, Car97a, Car96] for their combinatorics and
complexity.
Usually, a stream lying in an acyclic logical flow graph associated to a proof
and containing cuts, looks roughly as follows
where we see a chain of shapes similar to the one associated to cut-free proofs
but where single bridges are now allowed to take themselves this shape. As
usual, axioms lie along paths between the point where defocussing points end
and focussing points start to appear.
The following property of streams illustrates their regularity
Proposition 1 The number of focussing points in a stream is the same as the
number of its defocussing points.
Proof. The claim follows from a simple fact. Let P be an acyclic directed
graph which is connected, contains one input vertex, n focussing points and m
defocussing ones. Then, P has nodes. This is easily proved by
induction on the values of n; m by noticing that a defocussing node induces the
number of distinct output nodes to increase by 1, and a focussing node induces
the number of distinct output nodes to decrease by 1. From this we conclude
that if P is a stream, then exactly one input vertex and one
output vertex.4 Interaction of streams in proofs
A logical flow graph of a proof is a union of connected components. There might
be many of them, and typically, each component corresponds to a distinguished
atomic formula in the proof. Each component is a directed graph which has
input nodes as well as output nodes. When no cycles appear in a proof, this
is easy to check. To show the assertion in the general case, one needs to show
that cyclic logical flow graphs (e.g. graphs with several nested cycles) must have
incoming edges and outcoming ones. This follows from Theorems 25 and 54 of
[Car97b].
Each component is usually constituted by several streams as illustrated by
the graph on the left
x
x
x
which contains two streams, the first has base (x; y 1 ) and the second (x; y 2 ) (as
illustrated on the right).
Connected components and streams define two different types of interaction
in a proof:
1. distinct streams can share subgraphs (as in the example above) and can
influence one another. This interaction is analysed in [Car97b] through a combinatorial
study of cut-elimination.
2. different connected components belong to the same logical flow graph because
of logical connectives. The interaction between distinguished connected
components has been studied through the notion of proof-net by Girard, Lafont,
Danos, Regnier and many others. Girard's seminal paper [Gir87] introduces the
reader to the area. We shall skip here the numerous references.
In this paper we shall not address any question concerning interaction with
the exception of Section 8.
5 Strings and stream structures
In this section we introduce a language to represent a stream as a string formalized
in a language of three symbols b;  ; +, where b is a constant,   is the
binary operation of concatenation, and + is the binary operation of bifurcation.
We will also need two extra symbols (; ) to be used as separators. The language
will be called S and the words in S are simply called strings.
string is a word in the language Ssatisfying one of the following
conditions
i. b is a string
ii. if w are strings then w 1   w 2 is a string
iii. if w are strings then is a string.
Example 3 The string b corresponds to a stream which looks like a sequence
of edges. The diagrams below illustrate the behavior of the operations of concatenation
and of bifurcation + on streams. Obviously the pair of streams
that we consider in the diagrams below can be substituted by any other pair.
The topology of streams changes with the application of both operations since
new branching points are generated. Through concatenation we create sequences
of focal pairs and through bifurcation we create new focal pairs.
We define a first order theory whose axioms are universally quantified equations

Definition 4 A stream structure is an algebra of terms satisfying the following
axioms
A3
Axioms us that there is no topological change that can be
achieved by concatenating a bridge to a stream. Axioms A2; A2 0 can be illustrated
in terms of streams as follows
By the point of view of the input vertex, the structure of the two graphs is
identical. Namely, the number of paths going from the input vertex to the
output vertex remains unchanged for both graphs. Axioms A3 and A4 guarantee
that the topological structure of the stream is preserved by commutativity and
associativity of +. In fact, we shall be interested in streams up to isomorphism.
Definition 5 A stream structure is called associative when it satisfies
(associativity of   )
and it is called commutative when it satisfies
One can think of A1-A6 as universally quantified axioms over variables w,
stream structure is constituted by an abelian additive semi-group
and by a multiplicative part. The distributivity law holds. Notice also that
the operation of concatenation is not commutative in general and that in an
associative stream structure we do not distinguish substrings of the form (w 1
Since the operation of bifurcation is associative, in the following we will drop
parenthesis when not necessary. For instance, the word (w 1 will be
We will also use the shorthand notation w n instead of
times
and we will call n the multiplicity of w.
Proposition 6 The following properties are satisfied in any stream structure
1. w   wn
2. wn   wn
3. permutation -
Proof. To check the three properties it is a routine. Note that they correspond
to axioms A2; A3. They are derived from their corresponding axiom
with the help of A4.In a stream structure there are infinitely many non-equivalent strings. Namely,
for any two positive integers n; m, we have b n Therefore a stream structure
contains at least a countable number of non-equivalent terms.
Proposition 7 (Normalization) Let w be a string. For every stream struc-
ture, there is a unique integer k - 1 such that w is equivalent to b k in the stream
structure.
Proof. Let the height h(w) of a string w be defined as follows:
By induction on the height of the string w we show that there is a k such
that w is equivalent to b k .
If w is b then
If w is of the form w 1   w 2 then by induction hypothesis, w 1 is equivalent to
is equivalent to b l . Therefore w 1   w 2 is equivalent to b m   b l . On the
other hand, by property 2 in Proposition 6 and axiom A1 one derives
times
times
If w is of the form w 1 +w 2 then by induction hypothesis w are equivalent
to is equivalent to b m l and hence to
b m+l by axiom A6.
To show uniqueness, let us interpret the concatenation   as the operation
of multiplication on natural numbers, the bifurcation + as addition and the
constant b as the number 1. In this way, the model of natural numbers becomes
a natural model for the stream structure. In particular, given a string w there
is exactly one value k such that w is equivalent to b k . If this was not the case,
then the natural numbers could not be a model for the stream structure.Proposition 8 (Cancellation modulo torsion) The following properties are
satisfied in any stream structure
1. b   w
2. w 1
3. w   w
4. w 1
Proof. Properties are derived using axioms A1; To derive property
3 we apply Proposition 7 to the string w and observe that there is a positive
integer n such that w is equivalent to b n . Hence w   w
. By right distributivity (i.e. axiom
(where the right hand side contains n strings of the form b   w 1 ) and analogously
2 . Similarly, one shows property 4. In this case axioms A1 0 and
should be used instead.6 Strings and streams of proofs
To associate a string to a stream in a proof, we think of the logical flow graph
of the proof as being embedded in the plane, we read a bridge as the constant
b, we read a cut-edge as performing the operation of concatenation  , and we
express the nesting of bridges through the operation of bifurcation +.
Definition 9 A decomposition of an acyclic directed graph P is a set of streams
lying on P such that
1. each directed path in P belongs to exactly one of the streams P j ,
2. the input node of P j is an input node of P ,
3. the output node of P j is an output node of P .
If P is a graph lying in the logical flow graph of a proof \Pi, then the symbol
denotes the restriction of P to the logical flow graph of a subproof \Pi 0 of
\Pi.
\Pi be a proof whose last rule is applied to the subproofs
. (If the rule is unary, then consider \Pi 1 only.) A stream P is called
an extension of P is a stream of \Pi and fP is a decomposition
of
In Definition 10, if the last rule of \Pi is a cut, then the number of streams
n can be arbitrarily large. In fact, a stream P might pass through the cut-
formulas, back and forth, several times.
Definition 11 Let P be a stream of a proof \Pi. A string associated to a stream
P is built by induction on the height of the subproofs \Pi 0 of \Pi in such a way that
the following conditions are satisfied:
1. if \Pi 0 does not contain cuts, let fP be a decomposition of P - \Pi 0 .
Each string associated to P i is b m , where m is the number of distinguished
directed paths lying in P i ,
2. if the last rule of \Pi 0 is not a cut and it is applied to \Pi 1 ; \Pi 2 (if the rule
is unary, then consider \Pi be the decomposition of
. Then the decomposition of P - \Pi 0 is fP 0
l g where
(a)
i is an extension of P j and the string associated to P 0
w j is the string associated to P j , or
(b)
i is a stream obtained by the union of streams P 0
which
are extensions of P
and are based on the
same pair (v string associated to P 0
where w jr is the string associated to P jr , for
3. if the last rule of \Pi 0 is a cut applied to subproofs \Pi
is a decomposition of P - \Pi 1 and P - \Pi 2 , then the decomposition of P - \Pi 0
is fP 0
l g, where the P 0
i 's are all possible extensions of the streams
in such that
(a)
i is an extension of P and the string associated to P 0
i is
(possibly is the string associated to
(b)
i is a stream obtained by the union of streams P 0
where
each
jr is an extension of P jr and all the
jr are based on the same pair (v The string associated to P 0
is w 0
jr is w jr ;1  ;s is the string
associated to P jr ;s for
Let us now give a couple of examples to illustrate how streams of proofs can
be read as strings.
Example 12 Consider the stream of a proof
c
c
where a path starts on the left hand side of the picture, goes up until it reaches
a branching point. Two distinguished paths depart from this branching point,
they pass through two axioms in the proof and they rejoin into another branching
point to pass through a cut-edge, form a new bridge, pass through a second
cut-edge, go up into a new subproof, split once more, join once more and
end-up into the right hand side of the picture. The structure of this proof
can be described with different strings. For instance, the strings (b 2   b)   b 2 ,
(b   b)   (b   b)   b are
descriptions of the above structure. One can easily check that the three strings
are equivalent in a stream structure. In fact, the first and the second string are
equivalent by A2 0 and the second is equivalent to the third by A2.
Example 13 Consider two streams of proofs having the following form

where the height of a cut in the proof is reflected by the position of horizontal
edges in the graph. We read the stream on the left as (b   b)   b and the stream
on the right as b   (b   b). The parenthesis denote the height of a cut in a proof.
In this way the string (b   b)   b represents a cut between a subproof containing
a stream b   b and a second subproof containing a bridge. The representation of
b   (b   b) is symmetric.
string associated to a stream in a proof \Pi is compact if it is
determined as described in Definition 11, where we require that the streams P i
lying in decompositions fP relative to subproofs \Pi 0 of \Pi have distinct
bases (v
Given a stream of a proof, there is a unique compact string associated to it
(up to commutativity of +). This is because, for all subproofs \Pi 0 of \Pi, there is
only one stream P 0 (up to commutativity of +) which is defined as P - \Pi 0 on a
In Example 12, the string (b 2   b)   b 2 is compact. Compact strings are
a succinct way to represents streams. All other representations have larger
complexity, that is a larger number of symbols. Consider, for instance, a string
of the form w 1 describing a stream P of a proof based on (v; w).
If each w i describes a simple path in P based on (v; w), then w i is of the form
b. In this case we say that the string w 1
the stream P explicitly: all paths are described one by one. This description
is the most expensive in terms of the number of symbols and we refer to it as
explicit representation.
Proposition 15 Let \Pi be a cut-free proof. All the streams of \Pi are described
by strings of the form b n , where n is bounded by the number of axiom-edges of
\Pi.
Proof. The claim follows from Definition 11 (assertion 1) and the following
observation. Each path belonging to a stream passes through an axiom-edge
by definition. Suppose that more than one path belonging to the same stream
passes through the same axiom. These paths will pass through the pair of
distinguished formulas of the axiom but through distinct atomic occurrences.
Therefore there should be a moment along the proof, where the occurrences
need to identify (since a stream has one input vertex and one output vertex).
But the identification is impossible because of the subformula property which
holds for cut-free proofs.Remark 16 The cut-free proof of F (2)
which can be constructed
from axioms of the form F (t) ! F (t), the F -rule, and contractions on the left,
is an example of proof where the number n in Proposition 15 corresponds exactly
to the number of axioms in the proof. The logical flow graph of this proof is
a stream based on
)). Since distinguished formulas in axioms are
atomic and all of them are linked to the end-sequent, then the number of axioms
in the proof must coincide with the number of paths of the stream.
Remark 17 In proofs we can only compose and bifurcate bridges having the
same orientation. This justifies the fact that stream structures are not defined
to have a group on their additive part but simply an additive semi-group.
6.1 From strings to streams
We show that any string is associated to some stream of a proof.
Theorem For each string there is a proof with a stream described by the
string.
Proof. Let w be a string. We shall build a proof \Pi w whose end-sequent is
whose logical flow graph is a stream
associated to w. The construction is done by induction on the complexity of
the substrings.
If w is b then \Pi w is an axiom of the form F
If w is w 1   w 2 then by induction we know \Pi w1 and \Pi w2 . The end-sequents
of \Pi w1 and \Pi w2 are F
and g(x). By substituting the occurrences of the variable x in \Pi w2 with the term
f(x) we obtain a proof \Pi 0
w2 with end-sequent F (f(x)) ! F (g(f(x))), the same
logical structure as \Pi w2 and the same logical graph. (This is straightforward to
check.) Then, we combine with a cut on the formula F (f(x)) the proofs \Pi w1
and \Pi 0
w2 and obtain a proof of the sequent F (x) ! F (g(f(x))) whose associated
string is w 1   w 2 (by Definition 11).
If w is then by induction we know \Pi w1 and \Pi w2 . Their end-
sequents are of the form F
f(x) and g(x). We apply the F -rule to \Pi w1 and \Pi w2 to obtain a proof of
applying a contraction to the occurrences
F (x) on the left, we obtain the sequent F (x) ! F (f(x)   g(x)) and a proof with
associated string (by Definition 11).Remark 19 The proof \Pi constructed in Theorem is formalized in the extension
of the propositional sequent calculus with F -rules. Notice that there are no
occurrences in \Pi and that cuts are only on atomic formulas. In particular,
the proof \Pi is reduced. One might be unhappy with the presence of F -rules in
\Pi and might like to look for proofs in pure propositional logic. To find proofs
containing a required stream is not difficult once we allow an arbitrary use of
occurrences in \Pi. To find a propositional proof \Pi which is reduced is, on
the other hand, a very difficult task and it is not at all clear whether there is a
uniform algorithm that given a stream, returns a proof which contains it.
Remark 20 Theorem associates a stream to a given string. The proof
containing such a stream is not unique. Take for instance the following transformation
of streams due to the procedure of cut-elimination (the existence of
such transformations is proved in [Car97b])
where the contraction (on the proof on the left) lying above w is applied much
after the cut rule. The streams, before and after cut-elimination, are described
by the same string b   b also that this is the only
possible string describing the above structures. (The fact that the height of the
contraction above w is smaller than the height of the cut rule, plays a crucial
role here.)
6.2 Strings and topology of streams
Usually, proofs having streams with the same topology (i.e. the same display
of branching points), might have different strings associated to them. Take
for instance the following transformation of streams due to the procedure of
cut-elimination [Car97b]
where the proof on the left can be described by the strings b   b 2 and (b   b) 2 ,
but the proof on the right can only be described by (b   b) 2 . Also, consider the
following pair of streams
where the proof on the left is described by the strings b   b 2 and (b   b) 2 , and
the one on the right by b   (b
We say that a stream P in \Pi is minimal if for any subproof \Pi 0 of \Pi whose
end-sequent is combined with some cut-rule, the graph P - \Pi 0 does not contain
simple bridges as connected components.
Proposition be two minimal streams. If G 1 and G 2 have the
same topological structure then they are described by the same explicit strings.
Proof. Let G 1 be a stream for (v; w) and G 2 be a stream of (x; y). By
definition an explicit string for a stream is a bifurcation of strings which are
concatenations of b's and describe simple paths in the stream. Since G 1
have the same topological structure, the number of paths between v; w and
y must be the same, say n. In particular, the two streams are reduced by
hypothesis and therefore they have the same number of cut-edges lying along
each path. This is enough to conclude that if w is an explicit string
of G 1 then wn must also be a string of G 2 . Moreover, this string is
unique up to permutation of the components of the bifurcation operator.7 Arithmetical value of strings and complexity
If a proof contains cuts, then the compact descriptions for its streams might be
much shorter than the explicit ones. Let us illustrate this point with a concrete
example where the presence of a chain of focal pairs in a stream is described by
a compact string of size n, and by an explicit string of size 2 n .
Example 22 We look at a proof of F (2)
(This example is taken
from [Car97b].) There is no use of quantifiers and the formalization takes place
on the propositional part of predicate logic. Our basic building block is given
by
which can be proved for each j in only a few steps. (One starts with two copies
of the axiom F
combines them with the F -rule to get
Then one applies a contraction to the two occurrences of F
) on the left and
derives the sequent.) We can then combine a sequence of these proofs together
using cuts to get a proof of F (2)
in O(n) steps.
The logical flow graph for the proof of F (2)
looks roughly as
where the notation \Pi refers to the proofs of F (2)
). The
logical flow graph of each \Pi j contains two branches, one for the contraction of
two occurrences of F
) on the left, and another for the use of the F -rule on
the right. Along the graph we notice a chain of n pairs of branches which gives
rise to an exponential number of paths starting at F (2) and ending in F (2 2 n
There are no cycles in the proof and the logical flow graph of this proof is a
stream. The compact string associated to it is b 2   b 2  where each of the
corresponds to a focal pair in the graph. The explicit string is b 2 n
Can we detect a chain of focal pairs lying in a stream by reading its associated
string? To answer let us introduce some more notation. A string can always be
seen as a concatenation of strings either of the form b or w wn ,
wn are strings and n ? 1. For instance, take the string w of
the form (b   (b 2 +b   b 3 We say that are concatenated to
each other and we call them factors of w. A factor of the form w 1
is called non-trivial. The number of non-trivial factors of w is the index of w.
Proposition 23 Let P be a stream based on (v; w) and lying in the logical flow
graph of a proof \Pi. Let w be the string representing P . If w contains a substring
of index n then there is a chain of n focal pairs in the logical flow graph of \Pi.
Proof. Let P be a stream and w be the string associated to it. By Definition
11, any substring w 0 of w describes a stream lying in some subproof \Pi 0 of
\Pi. If w 0 has index n then w 0 is of the form w 1
are non-trivial factors, for
the substrings w correspond to streams lying in subproofs \Pi i linked
through cuts, and based on pairs
(in \Pi 0 the occurrences A are linked by a cut-edge). In particular, the
substrings
are of the form
By Definition 11, w
are strings associated to streams based
on the same pair (A; B). Therefore, there is at least a focal pair lying in the
subproof
(because
? 1). This means that in \Pi 0 we have a chain of focal
pairs which is defined by the cut-edges connecting the subproofs \Pi
and the focal pairs in the \Pi i j
's.As illustrated in Example 22, a chain of n focal pairs lying in a stream gives
rise to at least 2 n distinct paths. In Proposition 24, we show that the number
of paths in a stream can be computed precisely by means of an arithmetical
interpretation of strings. We say that the arithmetical value t(w) associated to
a string w is defined as follows: t(b) is 1, t(w 1
is
Proposition 24 Let w be a string associated to a stream P . Then the number
of directed paths from the input vertex to the output vertex of P is t(w).
Proof. This follows in a straightforward way from the interpretation between
streams and strings described in Example 3.Proposition 25 Let w be a string and w 0 be a substring of w. Then any substitution
of w 0 with a string w 00 where t(w string w   such that
Proof. The arithmetical term t(w) (once considered in its syntactical form)
contains the arithmetical subterm t(w 0 ). If we substitute the occurrence of t(w 0 )
with t(w 00 ) we shall obtain the arithmetical term t(w   ) whose value is t(w) since
cut-elimination
How does a stream of a proof evolve through the procedure of cut elimination?
A more general version of this question was addressed in [Car97, Car97b] where
the combinatorial operation of "duplication" on directed graphs was introduced
and used to analyse the combinatorics of the transformations induced by cut-
elimination. Here we would like to show that the evolution of streams can be
analysed through simple algebraic manipulations. We give a number of rewriting
rules and show that these rules describe the transformation.
The set of rewriting rules that we want to consider contains the computational
rules
wn wn
wn wn   w
wn \Gamma! w permutation -
which follow from the axioms A1-A3 and A5. Axiom A4 does not have a counter-part
here because from now on we shall consider only compact strings associated
to proofs. It also contains the local structural rule
which represents the possibility to duplicate the same substrings, and the global
structural rules
which cancel some of the substrings. It is clear that local and global structural
rules allow a string to grow and shrink. Theorem 26 shows how the process of
cut-elimination induces streams to shrink and grow. Notice that if w is a string
transformed by R6 into w 0 then t(w) ! t(w 0 ). If w is transformed in w 0 by R7 i ,
On the other hand, if any of the rules R1-R5
are used then
Before stating Theorem 26, we need to introduce some more definitions. A
reduction is a sequence of applications of rewriting rules that transforms a string
w into a string w 0 . An application of a rewriting rule s ! t to w replaces an
occurrence of the substring s in w with the substring t. A reduction of a string
is called final if it leads to a string of the form b n , for some n.
We say that a path in the logical flow graph of a proof is disrupted by a step
of cut-elimination when given two nodes of the path, after the transformation
there is no more path between them. A stream is disrupted when one of its
paths is disrupted. This notion was introduced in [Car97] where the reader can
find examples.
Theorem 26 Let \Pi be a proof and let w be the compact string associated to
some stream of \Pi. For any process of elimination of cuts which gives a cut-free
proof with n axioms, either there is a reduction of w to a string b m (where
through the rules R1-R7, or the stream is disrupted by some step of
elimination of cuts either on weak occurrences or on contractions.
Proof. The proof consists of checking that at each stage of the procedure
of cut-elimination, the deformation of streams in the proof is regulated by the
set of rules R1-R7. Namely, if w is a compact string associated to a stream
P in \Pi, and if \Pi 0 is the proof obtained by transforming \Pi through a step of
elimination of cuts, then there is a compact string associated to a stream in \Pi 0
which is obtained from w after rewriting one or several of its substrings with the
rules R1-R7. Notice that several substrings of w can be simultaneously affected
because several paths belonging to the same stream might be involved in the
transformation of the same cut.
We shall consider first the behavior of a stream P which passes through the
cut-formulas that are simplified by the step of the procedure.
Let us start by considering the elimination of a cut when one of the cut-
formulas is a distinguished occurrence in an axiom. There might be several
paths (of the stream P ) that pass through the distinguished occurrences and
each of these paths will be denoted b (in the string w) because of compactness.
This is shown by an easy chasing of Definition 11. If the axiom appears on the
left, then we use R1 to replace substrings b   w 0 with w 0 in w. If the axiom
appears on the right, then allows to replace substrings of the form w 0   b
with w 0 in w. Clearly the string that we obtain is compact.
If a cut is applied to formulas with non-trivial logical complexity, i.e. formulas
which are not atomic, then a directed path belonging to the stream might
pass through the same cut-formula several times and different portions of the
same path might behave differently. In particular, several directed paths belonging
to the stream might pass through the same cut-formulas. Their behavior
will be captured by a simultaneous applications of rules R1-R7 to substrings of
w which describe different portions of the stream involved in the transformation.
We shall start to consider the case where a cut is applied to two formulas
which are main formulas of two logical rules. Several situations might arise. Let
us suppose without loss of generality that the formulas are of the form A - B.
First, suppose that there is a substream lying in the stream that passes
through both A and B and that it is described by a substring (wA   wAB )   wB ,
where wA describes a substream passing through A in the cut-formula on the
right, wAB describes a substream passing through both the A and the B in the
cut-formula on the left, and wB describes a substream passing through B in
the cut-formula on the right. After cut-elimination, the substream is described
either by the string (wA   wAB )   wB or by the string wA   (wAB   wB ), depending
on the position of the cuts on A and B. In the first case no rewriting rule is
applied and the cut on A preceeds the cut on B; in the second case R5 is applied
and the cut on B preceeds the cut on A.
Second, suppose that there are paths of the stream that pass through exactly
one of the disjuncts. In this case the paths will be simply stretched but no change
in their description will take place.
These are the only two possible situations that might occur. Of course,
a path might pass through A and B several times, or wAB might describe a
stream passing through A and B on the cut-formula on the right, or the initial
substream might be described by wA   (wAB   wB ). It is easy to imagine all
combinations. The main point is that the treatment specified above adapts
easily to all other variants. In particular, rule R5 0 might be used instead of R5.
If a cut is applied to a formula A obtained from a contraction on two occurrences
then the procedure of cut-elimination yields a duplication of
a subproof and this creates quite intriguing situations.
We start to handle the simplest case. (This case is illustrated in Remark 20.)
Suppose that there is a substream lying in the stream that passes through the
cut-formula which lies on the proof that will be duplicated by the procedure.
Suppose also that the extremes of the substream do not both lie in the cut-
formula. Then, the stream has to pass through the sequent resulting from the
application of the cut rule because its extremes lie in the end-sequent. Let w 3 be
the substring describing the substream. Let w be the substreams passing
through the contraction formulas A 1 ; A 2 such that w 3   (w 1 +w 2 ) is a substring
describing the topology of this portion of the stream. After duplication of the
subproof the substring will be transformed into the substring (w 3   w 1 )+(w 3   w 2 )
and this is done by applying rules R2;
Suppose now that the substream above (i.e. the substream lying in the
stream that passes through the cut-formula which lies on the proof that will be
duplicated by the procedure) is such that both its extreme points belong to the
cut-formula. This case is the most intriguing. Let w 3 be the substring describing
the substream. After passing through the cut-edges, the stream will go up to
the contraction formulas A 1 ; A 2 and it will depart into four paths: two coming
from its input vertex, say w and two going towards its output vertex, say
It might be that not all the four paths belong to the stream and because
of this we shall handle different cases. We illustrate the transformation of the
portion of the stream in the following picture

input vertex
output vertex
input vertex
output vertex

where we think of the streams as being stretched.
If all four paths belong to the stream, the transformation is described by
rule R7 1 , where the paths w 1   w 3   w 2 and w 4   w 3   w 5 are lost. If w
belong to the stream, the transformation is described by R7 2 or R7 3 . The
cases where any three other paths are considered, is handled similarly. If w
or belong to the stream, then the substring is unaltered. If the paths
belong to the stream, then the stream will be disrupted and
the statement holds. This concludes the treatement of the contraction rule. (To
be precise, since the operation of bifurcation + is commutative, we might need
to use R3 to rearrange the order of the substrings of the form w
handling properly the contraction case.)
If two cuts are permuted, suppose that the stream passes through both pairs
of cut-formulas, say C be subproofs of \Pi to which a
cut on C applied and let \Pi 2 be the subproof whose last rule of inference is
a cut on D 1 ; D 2 . By Definition 11 a stream P 2 in \Pi 2 passing through
might be described either by a compact string of the form w 1  wn , or by
a compact string of the form (w 1;1
w 0 be a substring associated to a stream P 1 lying in \Pi 1 , passing through C 1
and connected by a cut-edge to P 2 . In the first case, w will contain a substring
of the form w wn ); then, we apply
(w 2  wn ). In the second case, w will contain a substring of the form
apply R5 and obtain
(w
If are contained in \Pi 1 , then rule has to be applied instead of
R2. If two cuts are permuted but the stream passes through only one of the
cut-formulas then no rule is applied.
If a cut is pushed upwards then it might happen that a contraction is pushed
below the height of the cut. This might imply that a branching point of the
stream (maybe several of them) will be pushed below a cut-edge and therefore
that the compact description of the stream might change. The new compact
description is obtained with the application of rules
In all cases treated above, the stream P passed through the cut-formulas
simplified by the step of the procedure. We shall consider now the case where
the stream does not pass through the pair of cut-formulas.
This is the case when one of the cut-formulas is weak. (Remember that the
extremes of a stream can only lie on the end-sequent.) Then the procedure of
cut-elimination will induce a disruption of the structure of the proof due to the
removal of a subproof. In case the stream passes through the subproof which is
removed, then the stream will be disrupted and the statement holds.
In case a stream passes through the side formulas of the antecedents of
a cut but not through their cut-formulas, its paths will be stretched and no
modification of the substrings is needed. The only exception is the contraction
case, where a substream passing through the side formulas of the subproof to
duplicate, might be duplicated while the subproof is duplicated. In this case,
rule R6 is used.
Let us notice that all along the proof one needs to verify that the string
associated to the proof \Pi 0 is compact. This is a straightforward verification and
we leave it to the reader.
To conclude, if the stream has not been disrupted then from Proposition 15
it follows that w has been reduced to a string b m where m is smaller than the
number of axioms in \Pi.Example 27 Consider the proof of the sequent F (2)
given in Example
22 and described by the compact string b 2   b 2   where the
terms b 2 are exactly n. We can calculate the exponential expansion of this proof
after cut-elimination through a purely algebraic manipulation of strings as we
shall show for namely for the string b 2   b 2   b 2   b 2 . For an arbitrary
n the approach is similar. By applying R4 to the substrings b 2   b 2 we get
(b apply R3 to all substrings b 2   b to get
(b   b (b   b and by R1 we
or in short b 4   b 4 . By applying
again R4; R3 and R1 we get
(b 4   (b 4   b
(b   b
(b   b
(b   b
(b   b
Note that b 16 is the minimum expected value for a cut-free proof computing
) from F (2). In fact the minimal tree of computation of F
branching points corresponding to 2
times F (2).
Theorem 28 Let \Pi be a proof of F
atomic cuts and no weak formulas. Let w i be the full compact string associated to
procedures of cut-elimination
transforming \Pi into \Pi 0 and w i into w 0
are simulated by R1-R5
and w 0
Proof. The proof \Pi has a very simple structure. Here are some properties:
1. the proof \Pi contains no logical rules and all formulas appearing in \Pi are
atomic. This is because cuts are defined on atomic formulas and formulas in
the end-sequent are atomic;
2. for any sequent in \Pi, exactly one formula lies on the right hand side of the
sequent. This follows from 1;
3. there are no contractions on the right in \Pi. This is because there are no
weak formulas and no logical rule can be applied on negative formulas in \Pi.
Properties 1-3 imply some properties of the flow graph of \Pi:
a. no path passes twice through the same cut-formula, since cut-formulas are
b. no path passes twice through the side formulas of a sequent used in a cut-
rule. This is because at any stage of the procedure, the sequents have the
and contractions are on the left only.
Therefore, if the cut-formula in the sequent is a positive occurrence of the form
are negative occurrences and no path
can start and end in them; if the cut-formula is a negative occurrence F (s j ),
for some there might be several paths passing through the side
formulas (in fact, all of them should pass through the formula on the right of
the sequent) but the proof where F occurs cannot be duplicated because
contractions can be applied only to negative formulas.
Properties a and b ensure that the rewriting rules R6 and R7 are not used
by the simulation. In particular R1-R5 are rewriting rules of the form p ! q
This implies that the final string w 0
i are of the form b n i where
\Pi be a proof of the sequent S such that the number of symbols
in S is n. If any cut-free proof \Pi 0 of S has 2 O(n) lines then
1. either there is a stream w in \Pi such that t(w) is 2 O(n) ,
2. or any process of cut-elimination from \Pi to \Pi 0 is simulated by R6.
Proof. If \Pi 0 has 2 O(n) lines then there is a stream b k in it where k is 2 O(n) .
This means that b k has been obtained from a string w in \Pi with or without the
help of R6. If R6 has not been used then the arithmetical value t(w) is at least
k since rules R1-R5 and R7 cannot augment it.Remark Rule R6 has a global effect. In fact, it does not concern the cut-
formulas involved in the step of elimination of cuts, but the structure of the
proof itself. It corresponds to the existence of a path in the proof which passes
twice through the side formulas of a subproof that is duplicated by the procedure
of cut-elimination.
Even if a proof might be such that no path passes twice through the side
formulas of a sequent applied to a cut-rule, during cut-elimination this property
might be lost. It is easy to check that permutation of cuts, contraction and
resolution of cut-formulas which are main formulas of logical rules, might produce
a proof which falsifies this property. Once the property is violated, rule
R6 might play a role in the transformation.
Remark 31 The expansion of \Pi 0 can be exponential with respect to the number
of sequents in \Pi, as in Example 22. This example shows that cuts on atomic
formulas can induce exponential complexity.
Problem To decide whether w 1 and w 2 can be reduced to the same string
k , for some k, by using rules R1-R5, can be done in polynomial time. In fact
can be polynomially reduced to some b k1 ; b k2 for some fixed k
and it is sufficient to check whether the values k 1 and k 2 are the same or not.
If we allow the rules R1-R7, does the question become NP -complete?



--R

The undecidability of k-provability
In Annals of Pure and Applied Logic
Some combinatorics behind proofs.
Cycling in proofs and feasibility.
Turning cycles into spirals.
Duplication of directed graphs and exponential blow up of proofs.
The cost of a cycle is a square.
Asymptotic cyclic expansion and bridge groups of formal proofs.
Looking from the inside and the outside.
Propositional proofs via combinatorial geometry and the search for symmetry.
Making proofs without modus ponens: An introduction to the combinatorics and complexity of cut elimination.
A graphic apology for symmetry and implicitness.
The relative efficiency of propositional proof systems.

Linear Logic.
Proof Theory and Logical Complexity.
The intractability of resolution.
Lower bounds for increasing complexity of derivations after cut elimination.
The lengths of proofs.
Structural Complexity of Proofs.
Bounds for proof-search and speed-up in predicate calculus
Lower bounds on Herbrand's Theorem.
Proof Theory.
Complexity of a derivation in the propositional calculus.
--TR
Linear logic
Graphic Apology for Symmetry and Implicitness
cut elimination;structure of proofs;proof complexity;duplication;cycles in proofs;directed graphs;logical flow graphs