2
$\begingroup$

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

Improve this question
$\endgroup$
5
  • $\begingroup$ It's not possible if $\Gamma$ is empty. $\endgroup$
    – Emil Jeřábek
    Jan 31, 2016 at 20:13
  • $\begingroup$ On the contrary. From a contradiction you can prove anything. ($\Gamma=\emptyset$ is a contradiction.) $\endgroup$
    – Gabriel Nivasch
    Jan 31, 2016 at 20:17
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Jan 31, 2016 at 20:22
  • $\begingroup$ 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$? $\endgroup$
    – Gabriel Nivasch
    Jan 31, 2016 at 20:28
  • $\begingroup$ 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... $\endgroup$
    – Gabriel Nivasch
    Jan 31, 2016 at 20:30

1 Answer 1

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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... $\endgroup$
    – Gabriel Nivasch
    Feb 1, 2016 at 12:21
  • 2
    $\begingroup$ @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. $\endgroup$
    – Emil Jeřábek
    Feb 1, 2016 at 14:56
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Feb 1, 2016 at 15:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.