The standard approach to second-order axiom systems

Question

This is a very basic question, but for some reason I couldn't find an answer elsewhere on the Internet.

Suppose we have an axiom system $A$ written in the language of second-order logic. In order to prove that $A$ entails a theorem $\phi$, we generally proceed as follows. Fix a structure $M$ such that $M$ satisfies $A$, and prove that $M$ satisfies $\phi$, and thereby conclude that $A$ entails $\phi$.

Is this correct?

Answer 1

Edit:After reading Peter Smith answer below I think I should add some specifications. In the following answer I've interpreted your "Fix a structure $M$ such that $M$ satisfies $A$" as "we prove that for a generic structure $M$ that satisfies $A$". In case you meant that we find just one structure which is models of both $A$ and $\phi$ then the conclusion is false.

The answer depends if whether you're considering syntactic or semantic entailment. In the second case the answer is yes, by definition, in the second case the answer is no, or to be exact it depends on the semantic you're considering. If you're dealing with the standard semantic the answer is no because second order logic is incomplete, if you use semantics like Henkin semantic then the answer become again yes, because with this semantic second order logic is complete.

Answer 2

First, $A$ need not be categorical. So showing that $M$ satisfies $A$ and satisfies $\varphi$ won't in that case tell us much about semantic entailments (other than that $A \nvDash \neg\varphi$).

And even if we show that every model that satisfies $A$ satisfies $\varphi$ that doesn't tell us about theorems, assuming we are using a second order language with the standard ('full') semantics. It can be the case that $A \vDash \varphi$, i.e. $\varphi$ is true in every model which makes all the sentences in $A$ true, even though $A \nvdash \varphi$, where $\vdash$ indicates deducibility in the relevant proof system.

A nice example is when $A$ is the standard formulation of second-order Peano Arithmetic $\mathsf{PA_2}$, and $\varphi$ is its canonical Gödel sentence $\mathsf{G_2}$. Since second-order PA is categorical, any sentence which is arithmetically true (i.e. true in the standard model of $\mathsf{PA_2}$) is true in all its models (as the models are all isomorphic). So $\mathsf{PA_2} \vDash \mathsf{G_2}$, since the canonical Gödel sentence is true, but not $\mathsf{PA_2} \vdash \mathsf{G_2}$ since it is a Gödel sentence.