Suppose we want to prove some $\Gamma \models \Delta$ in (first-order logic) sequent calculus LK. We start with the sequent $\Gamma \vdash \Delta$, and arbitrarily apply rules backward until we reach sequents that only contain atomic formulae. Then, either the sequents are axioms (e.g. $A \vdash A$), or not (e.g. $A \vdash B$).
Now, suppose that $\Gamma \models \Delta$. If we apply rules arbitrarily, are we guaranteed to always end up with axioms ($A \vdash A$)? Or can the order of application of rules change that outcome?
Another way of asking this: If at some point in the derivation we see a sequent with only atoms that is not an axiom (e.g. $A \vdash B$), can we immediately infer that $\Gamma \not\models \Delta$?
Is the outcome different if $\Gamma \models \Delta$ would only contain propositions, no predicates?
Thanks for the help :)
PS: Maybe this was a little unclear... Both $\Gamma$ and $\Delta$ can be one or more well-formed formulae.