Proof in sequent calculus without cut

Question

I met an exercise in Gaisi Takeuti, Proof Theory [Exercise 2.7, page 14].

How to construct a cut-free proof of$\ \forall xA(x)\rightarrow B\vdash \exists x(A(x)\rightarrow B)$, where A(a) and B are atomic and distinct.

Why A(a) and B are restricted to be atomic and distinct?

Answer 1

We have to note that :

$(∀x β → α) ↔ ∃x(β → α)$

is valid only with the assumption : $x$ not free in $\alpha$.

Thus - I think - when Takeuti "specify" that :

$A(a)$ and $B$ are atomic and distinct

we have to read it as meaning that they are not "schematic" formulae, but "fully indicated" ones.

I.e. $A(a)$ is (for example) $R_0^1(a_0)$, with $R_0^1$ a unary predicate letter, and thus $A(a)$ is an atomic formula with only $a$ free; thus $B$, being different from $A(a)$, has no free occurrences of $a$.

This fact is necessary for the use of $\forall$-right rule in the proof of the formula.