Exercises

April 24 Lecture CS 358, Spring 1995

1. Show permutability for ℘. More specifically, show that if there is a cut-free proof of a sequent ⊢ Γ, A℘B (in the standard one-sided system), then there is a cut-free proof of this sequent whose last rule is

\frac{⊢ Γ, A, B}{⊢ Γ, A℘B}

2. Show that permutability (as in the previous exercise) fails for tensor (⊗).

3. Consider the fragment of linear logic with 1, ⊥, ⊗, ℘ only. Define the weight H(A) of any formula inductively by

\begin{aligned}H(1) & = & 1 \\ H(⊥) & = & 0 \\ H(A℘B) & = & H(A) + H(B) \\ H(A⊗B) & = & H(A) + H(B) − 1 \end{aligned}

Show that if A is provable, then H(A) = 1.

4. Find a linear formula A over 1, ⊥, ⊗, ℘ that is not provable but has weight H(A) = 1.