I have seen in at least two different places (here, p. 183; and here, last slide) the Tait calculus defined the following way.
Here $\Gamma$ denotes a set of formulas $\{A_1, \ldots, A_k\}$, which is to be interpreted as the disjunction "$A_1 \vee \cdots \vee A_k$"; and "$\Gamma, A$" is shorthand for $\Gamma \cup \{A\}$.
The rules are as follows:
$$\frac{}{\Gamma,\neg A,A}$$
$$\frac{\Gamma,A\qquad\Gamma,A'}{\Gamma,A\wedge A'}$$
$$\frac{\Gamma,A}{\Gamma,A\vee A'}$$
$$\frac{\Gamma,A}{\Gamma,A'\vee A}$$
$$\frac{\Gamma,A(x)}{\Gamma,\forall x A(x)} \qquad\text{$x$ not free in $\Gamma$}$$
$$\frac{\Gamma,A(t)}{\Gamma,\exists x A(x)} \qquad\text{$t$ a term}$$
$$\frac{\Gamma,\neg A \qquad \Gamma,A}{\Gamma}$$
My question is as follows: I want to prove that from $\Gamma$ one can derive "$\Gamma,A$" for arbitrary $A$. (Meaning, it should be possible to add arbitrary additional formulas to a given conjunction.) However, I haven't been able to do such a derivation from the above rules.
I can prove the following: If you can derive $\Gamma$, you could have as well derived "$\Gamma,A$" (since you could have added $A$ from the beginning). But this is weaker than getting from $\Gamma$ to "$\Gamma,A$".