Discarding the superscript for turnstile in Kleene's Introduction to Metamathematics [1952]

Question

In Kleene's IM page 149 the reader is asked to supply the details for the following two examples.

Example 5. Given $A(x) \vdash B$ and $A(x) \vdash \lnot B$ with x held constant, then $\vdash \lnot A(x)$ and $\vdash \forall x \lnot A(x)$.

Example 6. Given $A(x) \vdash^x B$ and $A(x) \vdash^x \lnot B$ with x not necessarily held constant, then $\vdash \lnot \forall x A(x)$.

I think that the proofs go roughly like below also see this question and answer:

For example 5:

1. $A(x) \vdash B$ - given
2. $A(x) \vdash \lnot B$ - also given
3. $\vdash \lnot A(x)$ - by negation introduction (on 1 and 2) page 99
4. $\lnot A(x) \vdash^x \forall x \lnot A(x)$ - by generality introduction page 99
5. $\vdash \lnot A(x) \vdash^x \forall x \lnot A(x)$ - from 3 and 4 we have this chain
6. $\vdash \forall x \lnot A(x)$ - from 5 (notice the lack/discharge of superscript, i.e. $\vdash$ instead of $\vdash^x$, that's one example of discharge)

For example 6:

1. $A(x) \vdash^x B$ - given
2. $\forall x A(x) \vdash A(x)$ - by generality elimination page 99
3. $\forall x A(x) \vdash A(x) \vdash^x B$ - from 1 and 2 we have this chain
4. $\forall x A(x) \vdash B$ - from 3 (notice the lack/discharge of superscript, that's the second example of discharge)
5. $\forall x A(x) \vdash \lnot B$ similarly from the other given deduction
6. $\vdash \lnot \forall x A(x)$ - by negation introduction (on 4 and 5)

The superscript was discharged twice:

• in step 6 for the proof of example 5
• in step 4 for the proof of example 6

What's the justification for this discharge of the superscript? (Or are there similarly simple proofs that don't involve this discharge?)

Answer 1

The superscript notation $\vdash^x$ is introduced by Kleene to keep track of the application of postulate Rule 9 and 12 with regards to the superscript variable $x$ for an assumption formula, when the deduced formula depends on the assumption. It is a bit ambiguous because it does not identify the assumption formula, but that's usually clear from context (e.g. when there is just one assumption formula). The reason for tracking is to ensure that we meet (or not meet) restrictions to rules, such as the deduction theorem, reductio ad aburdum, where they require that the discharged formula is not varied.

Now the definition for varied involves: an assumption, a variable free in the assumption, a dependent formula in a deduction and the application of Rule 9 or 12 for the variable, assumption to the dependent formula.

So the tracking via the superscript is not required, can be discharged, for some circumstances like:

• there is no assumption (step 6 example 5 above)
• the variable does not occur free (e.g. 4 in example 6 above, $x$ is not free in $\forall x A(x)$ because $\forall x$ bounds all free occurrences of $x$ in $A(x)$

In fact Kleene uses the discharge mechanism for the two circumstances above for Example 2 at step 2 and Example 3 at step 3 (IM same page 149)