Challenge!

Here is a cute problem for you to think about.

Take the fragment of the sequent calculus for propositional logic over one propositional variable that consists of only the rules of weakening and contraction on the left and the right. That is, if the variable is x, then we start from x|-x and all we can do is add an x on either side or delete an x from one side, provided there are at least 2 x's on that side.

A theorem, T, of the system is just something that is derivable using the above rules. The depth of a theorem is the number of inferences in a proof of minimal length for T. For example, x,x |- x,x has depth 2, since the shortest proof is something like:

x |- x
--------
x,x |- x
--------
x,x |- x,x

The challenge is to give precise answers to the following...

Challenge 1 (easy): How many theorems are there of depth n in the above system?
Challenge 2 (trickier): How many theorems of depth n are there when we add cut to the above system?

Note that in the presense of cut, the depth of a proof, P, is defined to be the maximal length of a branch of P and the depth of a theorem, T, is defined to be the minimum depth over all proofs of T.

Also, note that we use an "additive" cut. That is, if we cut V |- x,W and X,x |- Y, we get V,X |- W,Y. Of course, in our case, the letters V,W,X and Y stand for multisets of our propositional variable (x).

If you do not know what cut is, or are rusty on formal proofs in general, then see this post.