I'm working with only models satisfying a particular schema, using a result that from this schema we can deduce a theorem, and attempting to show this theorem holds in all such models. Can I do this even without having constructed an explicit (code of a) proof within the model that the assumed schema is true?
For completeness, showing a $\Delta_k$-separation schema holds is is the application I'm applying this question to: fix $k\in\mathbb N^+$, let $(L_\xi)_{\xi\in\textrm{Ord}}$ be the constructible hierarchy of sets, and let KP denote the fragment of ZFC called Kripke-Platek set theory. Consider the levels $L_\alpha$ which satisfy $KP+\Delta_k\textrm{-collection}$, KP augmented with the $\Delta_k$-collection schema. In Artigue-Isambert-Perrin-Zalc's "Some remarks on bicommutability" (1975, p.212) it's remarked that from $KP+\Delta_k\textrm{-collection}$ we can deduce $\Delta_k$-separation holds, using universal formulae both of these schemata can be axiomatized as single formulae so provability makes sense here. But I don't have a proof constructed within $L_\alpha$ of $KP+\Delta_k\textrm{-collection}$'s truth, I have only declared we chose $\alpha$ so that it's satisfied. Does this lack of a concrete subproof stop us from concluding $\Delta_k$-separation is proved in any such $L_\alpha$?
Some remarks: if we can't prove $\Delta_k$-separation in $L_\alpha$, I would be fine with its semantic truth. In particular, in Kranakis's paper "Reflection and partition properties of admissible ordinals" (1980, theorem 1.5(i)) a weaker-looking variant is given, that when $L_\alpha\vDash KP+\Sigma_k\textrm{-collection}$ then $L_\alpha$ also satisfies the $\Delta_k$-separation schema. Also, this idea of assuming a property ($\Delta_k$-collection) holds and deriving from it reminds me of an initial assumption in natural deduction.
My first question about "can we produce a proof" was not well-formed, I didn't specify the axioms from which to prove $\Delta_k\textrm{-separation}$.
For the second question, since we are only looking at models of $KP$ that also happen to satisfy $\Delta_k\textrm{-collection}$, I missed that we are quite literally looking at models of $KP+\Delta_k\textrm{-collection}$. Then since $\vdash$ for first-order logic is sound, if $KP+\Delta_k\textrm{-collection}\vdash\Delta_k\textrm{-separation}$, and $L_\alpha$ satisfies $KP+\Delta_k\textrm{-collection}$, then $L_\alpha$ satisfies $KP+\Delta_k\textrm{-separation}$. The part of natural deduction that this reminded me of turned out to be called the deduction theorem, which gives a bit more detail about the implication. Provability of $\Delta_k\textrm{-collection}\rightarrow\Delta_k\textrm{-separation}$ over $KP$ would entail that $KP+\Delta_k\textrm{-collection}\vdash\Delta_k\textrm{-separation}$, and then every model of $KP+\Delta_k\textrm{-collection}$ would also satisfies $KP+\Delta_k\textrm{-separation}$, again by soundness of $\vdash$.