Proof soundness of a Hilbert Style Calculus This is more a question about checking if my understanding of the topic is adequate. If you want to proof the soundness of a syntactic Hilbert style calculus, i.e. showing that $\Delta\vdash\alpha \Rightarrow \Delta\models\alpha$, would it be enough to prove the axioms and rules as semantic tautologies, as this implies the preservation of the semantic truth in the considered system.
So showing for all axioms $\phi_i$ that $\models\phi_i$ and for all rules of the form $\phi_0,\dots ,\phi_n\vdash\psi$ that $\models (\bigwedge_{k=0}^{n}\phi_k)\rightarrow\psi$?
 A: Your understanding is correct, but note that it is restricted to classical logic. More generally, we can consider a formal system to consist of rules that specify what statements can be deduced. We can separately define semantics that specify which statements are true (in a given world), and we say that a world satisfies a statement if the statement is true in that world. Then we say that a formal system is sound iff it only deduces statements that are satisfied by all worlds. If the formal system permits an initial axiom set, then it is sound iff from the axioms it only deduces statements that are satisfied by all worlds that satisfy the axioms.
(Conventionally we use the term "structure" for a world, and "model of the axioms" for a world that satisfies the axioms.)
If each rule is of the form "If you can deduce every statement in $S$, then you can deduce every statement in $T$." where $S,T$ are collections of statements, then we can define that a rule is truth-preserving (for the chosen semantics) iff any world that satisfies $S$ also satisfies $T$. Then we can easily prove that any formal system with truth-preserving rules is sound. Note that it is crucial that the formal system only deduces statements that are explicitly allowed by the rules, namely the collection of deducible statements is the collection generated by the rules from the axioms, or equivalently the minimal collection that includes the axioms and is closed under the rules.
Now if we apply this directly to your question, what we need to show is that for each rule of the form $φ_{1..n} \vdash ψ$, every structure that satisfies all of $φ_{1..n}$ also satisfies $ψ$. Symbolically we would prove $φ_{1..n} \vDash ψ$. This is equivalent to your formulation only because of the specific semantics of classical logic, whereas some other logics may not have the same semantics for "$\to$", even if they still have a Hilbert-style calculus.
