# A derivation in Tait calculus

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

• It's not possible if $\Gamma$ is empty. Jan 31 '16 at 20:13
• On the contrary. From a contradiction you can prove anything. ($\Gamma=\emptyset$ is a contradiction.) Jan 31 '16 at 20:17
• No, you can't, in this calculus. It's a trivial induction on the length of derivation: all premises of all rules contain at least one formula, hence the only sequents you can derive from the empty sequent is itself, and sequents already derivable without the empty sequent, i.e., tautological. Jan 31 '16 at 20:22
• Now I see what you meant. (I thought you were saying that what I want to do doesn't make sense if $\Gamma$ is empty.) So for $\Gamma=\emptyset$ what I want to do is indeed impossible. What about for general $\Gamma$? Jan 31 '16 at 20:28
• I get the feeling that people just bothered proving that this calculus is 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... Jan 31 '16 at 20:30

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 wrote (as I also did), that given a deduction of $\Gamma$ there is also a deduction of $\Gamma,\Delta$. Well, now this does not seem so clear to me. If you add $\Delta$ too early, free instances of $x$ in it might interfere with the $\forall$ rule. For example, if you can derive $\forall x\ x+ x \ge x$, it's not clear you can also derive $x\ge 7, \forall x\ x+ x \ge x$. But anyway, this is a side point. I'm trying to understand Buchholz and Wainer's proof of the limitations of Peano Arithmetic; and if I have more questions I'll come back and ask... Feb 1 '16 at 12:21
• @GabrielNivasch: The argument indeed needs to deal with variables in a more subtle way, but this is not too difficult. Basically, you first rename eigenvariables in the proof so that they do not conflict with $\Delta$, and then add $\Delta$ to each sequent. Feb 1 '16 at 14:56
• Hmm. What I said applies when the $\forall$-rule is stated as $\Gamma,A(u)\mathrel/\Gamma,\forall x\,A(x)$, such as in Rathjen’s slides. I don’t think the weakening rule is admissible in full generality in the calculus where the eigenvariable $u$ is required to be $x$, as you stated it in the question. Feb 1 '16 at 15:00