Couple of questions from Takeuti's Proof Theory book

Question

I am reading Gaisi Takeuti's Proof Theory (Second Edition, Dover), and I have a couple of questions:

I) Right after the first (1.1.) definition, the author says that "In any case it is essential that each set of variables is infinite...". Why is that, i.e., what happens if the number of variables is finite?

II) Definition 1.6. (p. 8) defines (fully) indicated term. I find it very confusing. What is the difference between a non-indicated and an indicated term? Can there be a term in a formula that is not indicated?

III) Why is there a need for a proof using induction of Proposition 1.7. (p. 8)? The proposition says:

If $A(a)$ is a formula (in which $a$ is not necessarily fully indicated), and $x$ is a bound variable not occurring in $A(a)$, then $\forall x A(x)$ and $\exists x A(x)$ are formulas.

Shouldn't this follow from the definition of the formula; more precisely of $\forall x A$ and $\exists x A$?

Thank you for the answers.

Answer 1

Regarding I), the "potential supply" of variables must be "unlimited", basically for two reason :

• in order to be able to build formulae satisfiable in domain with any finite number of elements;

• in order to avoid problems with substitution; if an attempted substitution can cause problems due to the "clash" with existing quantifiers, an unlimited supply of variables can gives us the certainty of finding a "new" one not already occurring into the formula.

Regarding II), we can consider the formula $B := (x=0)$ and the term $0$. Then we get $A := B[^x_0] := (0=0)$ by replacement of the term $0$ in place of the free variable $x$.

In $A$, the term $0$ is not fully-indicated, because it is not true that "every occurrence of [the term] $t$ [in $A$] is obtained by such a replacement".

---

---

Regarding III), I'm perplexed ...

We have to take into account the "role" of indicated variables; see the quantifier rules [page 10] :

Consider :

2.5 : the rule for $\forall$-right; we have that the "move" from $F(a)$ to $\forall x F(x)$ is applied with $a$ fully indicated. This means that we have to replace all occurrences of $a$ in $F(a)$ with $x$ [e.g. from $(a=a)$ to $\forall x(x=x)$].

Consider instead :

2.6 : the rule for $\exists$-right; now in the "move" from $F(t)$ to $\exists x F(x)$ "not every $t$ in $F(t)$ is necessarily indicated". This means that we can "remove" from $F(t)$ only some and not all occurrences of $t$ [e.g. from $(t=t)$ to $\exists x(x=t)$].

If we step back to Def.1.3 [page 6] of quantified formulae, we have that they are built-up from e.g. $A := (a=0)$, to $A' := A[^a_x] := (x=0)$, to $\exists xA' := \exists x(x=0)$,

"where $A'$ is obtained from $A$ by writing $x$ in place of $a$ at each occurrence of $a$ in $A$."

In conclusion, I think that the "perplexing" Prop.1.7 [page 8] is aimed to license us to "remove" the above "snytactical" restriction; if we stay with Def.1.3, a formula like $\exists x (x=a)$ cannot be "produced" from : $(a=a)$ [see Def.1.2, page 6 : "every free variable is a term"].