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$".

notpossible if $\Gamma$ is empty. $\endgroup$withoutthe empty sequent, i.e., tautological. $\endgroup$doesn't make senseif $\Gamma$ is empty.) So for $\Gamma=\emptyset$ what I want to do is indeed impossible. What about for general $\Gamma$? $\endgroup$complete, i.e. you can prove from scratch anything that's true, and then went on. But they didn't care about proving things from other things. But mathematical logic is not my field so I don't know... $\endgroup$