# The standard approach to second-order axiom systems

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?

-
By "fix a structure $M$" you meant considering a generic structure $M$? – Giorgio Mossa Jan 30 '13 at 16:49
Yeah. I just meant "let $M$ be an arbitrary structure such that..." – goblin Jan 30 '13 at 17:17

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.

-

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.

-
@ineff is speedy -- and dead right! But you might like the added example here. – Peter Smith Jan 30 '13 at 15:34
Thanks for the reply. I was under the impression that usually, we forgo specifying a proof system for $A$ (which will necessarily be incomplete) by using a set theory (typically ZFC) instead. How does this gel with the answer given? – goblin Jan 30 '13 at 15:45
@user18921 You wrote in your question about theorems, and theorems are conclusions deduced is some proof-system or other. So you do need implicitly or explicitly to specify one if you are to ask questions about theorems. – Peter Smith Jan 30 '13 at 15:50
Perhaps the issue is the there are two meanings of "entails": semantic entailment and syntactic entailment. These do not coincide for full second-order semantics but the correspond for first-order (Henkin) semantics. – Carl Mummert Jan 30 '13 at 17:35
@CarlMummert But doesn't talk of entailing a theorem require the syntactic interpretation? – Peter Smith Jan 30 '13 at 18:04