I am asked to write formally the Soundness theorem for predicate FOL. I write it. Could you check it and see if I stated correctly or not?
Theorem
FOL is sound respect to the proposed test theory $(A_1,A_2,A_3,A_4,A_5,MP,$ Generalization rule), i.e. $$\vdash_{FOL}\phi\implies\vDash_{FOL}\phi$$
where $\vdash$ denotes theorem, $\vDash$ denotes a formula it's valid under every interpretation, $A_i$ are the axioms $(A_1,A_2,A_3$ are the same as in propositional logic).