1: \begin{proof}[Proof sketch]

2: %% We need to prove that there exists a sequent

3: %% $\Gamma\vdash\Delta$ which is provable in

4: %% CLKID$^\omega$, but becomes unprovable once

5: %% the cut rule is removed from the calculus.

6: %% Consider the sequent 

7: %% $ \vdash \forall k\ \mbox{\it nat}\,k \rightarrow 

8: %% \mbox{\it tplus}\ k\,0\,k$,

9: %% whose cyclic proof is given in 

10: %% Figure~\ref{tpluscyclicproof}. 

11: %% In the absence of the cut rule,

12: %% this sequent leads to the infinite 

13: %% derivation tree,

14: %% depicted in Figure~\ref{tpluscutfreeattempt},

15: %%  with the property that for each

16: %% node, exactly one rule is applicable.

17: %% Thus, our sequent has a unique derivation tree,

18: %% which is infinite and does not constitute a

19: %% valid CLKID$^\omega$ proof.

20: 

21: %% To obtain a rigorous proof of the theorem, we would need

22: %% to prove first the following two lemmas.

23: %% \bigskip

24: 

25: %% \begin{lemma}

26: %% For any natural number $\alpha$,

27: %% the sequent $\vdash {\it tplus}\,(S^\alpha\,0)\,0\,(S^\alpha\,0)$

28: %% has a unique CLKID$^\omega$ proof.

29: %% \end{lemma}

30: %% \bigskip

31: 

32: %% \begin{lemma}

33: %% For any natural number $\alpha$, the 

34: %% sequent ${\it nat}\,k\vdash{\it

35: %%   tplus}\,(S^\alpha\,k)\,0\,(S^\alpha\,k)$

36: %% has a unique, infinite derivation tree

37: %% in CLKID$^\omega$.

38: %% \end{lemma}

39: %% \bigskip

40: 

41: %% \noindent

42: %% Both lemmas are immediately proved by induction on $\alpha$ (the

43: %% second proof will make use of the first lemma). The theorem

44: %% can then be obtained as a corollary of the second lemma.

45: %% \end{proof}

46: