Relative interpretations

In Kunen's Set theory (2011), he says that there is a finitistic proof that Con$(ZF^-)\implies$Con$(ZF)$. He also mentions elsewhere that if $\Theta$ is at least as strong as finitistic reasoning and we have a finitistic proof of Con$(\Lambda)\implies$Con$(\Gamma)$ then:

$\Theta \vdash$Con$(\Lambda)\implies$Con$(\Gamma)$

Now my question is when he says there is a finitistic proof of Con$(ZF^-)\implies$Con$(ZF)$, does he mean that $\Theta \vdash$Con$(ZF^-)\implies$Con$(ZF)$ for any $\Theta$ at least as strong as finitistic reasoning (like $BST^-$)?

My confusion is this: Understanding an Easy Relative Consistency Proof

Which leads me to believe that the $\Theta$ needs to be stronger than $BST^-$ in this particular case.

If this is the case, then what's the reason Kunen is not more clear on this point, ie why doesn't he explicitly say: "We have shown that $ZF^- \vdash$Con$(ZF^-)\implies$Con$(ZF)$"

Any help is appreciated, thanks!

-

Thanks for the reply. I've reread Andres' explanation again. So what he's saying is one way we can show $ZF^- \vdash$Con$(ZF^-)\implies$Con$(ZF)$ is by using the Completeness Theorem, and we can do so since basic model theory can be formalized in $ZF^-$ and so we can prove the Completeness Theorem in $ZF^-$. Or he says we can work in a weaker system $\Theta$ (such as $BST^-$ or one that can carry out finitistic reasoning?) and show that $\Theta\vdash$Con$(ZF^-)\implies$Con$(ZF)$ by the syntactic argument which he gives. Am I on the right path here? –  user52534 Sep 11 '13 at 21:28