I have seen in at least two different places ([here](https://epub.ub.uni-muenchen.de/3843/1/3843.pdf), p. 183; and [here](http://www.mathematik.uni-muenchen.de/~aehlig/EST/rathjen2.pdf), 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$".



A derivation in Tait calculus
There's no *rule* that lets you get from a deduction of $\Gamma$ to a deduction of $\Gamma,\Delta$. However it's an easy lemma that, given a deduction of $\Gamma$, there is also a deduction of $\Gamma,\Delta$: go by induction on the deduction, adding $\Delta$ to every intermediate rule as well.


You might ask why it's defined this why, rather than including a weakening rule. (It is not, as your comment suggests, because proof theorists working with it didn't think hard about how proof systems work and what you might do with them.) The Tait calculus is optimized to be the right setting for cut-elimination proofs, so it's fairly minimal about what rules it has, and it's being especially parsimonious about how formulas get introduced, because cut-elimination proofs require a lot of accounting about where formulas first show up.


