Logical derivations without instantiation rules

Question

I'm trying to, through sequent calculus, prove some derivations without any instantiation rules, but I keep getting stuck. Take, for example, \begin{align} &\text{All basketball players are tall}\\ &\text{Kyrie is a basketball player}\\ &\rule{6cm}{0.2mm}\\ &\text{Kyrie is tall} \end{align}

Let $Bx$ be "x is a basketball player", $Tx$ be ''x is tall", and let the constant $k$ denote Kyrie.

I'd have $\forall x (\text{~B}x\lor Tx)$ and $Bk$, but I'm not sure how I'd use the rules of sequence calculus to

A) Introduce these statements meaningfully (aka not just writing $\forall x (\text{~B}x\lor Tx) \implies \forall x (\text{~B}x\lor Tx)$ and now just being stuck with this statement on the right)

and

B) How to actually use that $Bk$ and $\forall x (\text{~B}x\lor Tx)$ together imply $Tk$, without using an instantiation rule.

Edit: The allowed rules

Answer 1

In Sequent Calculus there are no "instantiation rules".

With the specific set of rules of BBJ, Computability and Logic, page 170, we have to play with the negation sign.

Starting from axioms: $Bk ⇒ Bk$ and $Tk ⇒ Tk$, we apply $(\text R 2_b)$ to get $\lnot Bk, Bk ⇒$ and then $(\text R 4)$ to get:

$\lnot Bk \lor Tk, Bk ⇒ Tk$.

Then $(\text R 2_a)$ to get $Bk ⇒ \lnot (\lnot Bk \lor Tk), Tk$, followed by $(\text R 5)$ and $(\text R 2_b)$ again to conclude with:

$\lnot \exists x \lnot (\lnot Bx \lor Tx), Bk ⇒ Tk$.

As per page 169: "It will be convenient in this chapter to work with a version of first-order logic in which the only logical symbols are $\lnot, \lor, ∃, =$, that is, in which $\land$ and $∀$ are treated as unofficial abbreviations."

Thus, we have to replace $\lnot \exists \lnot$ with $\forall$ and it is done.