Finite models which break the theorem `every injective map is surjective' Consider the first order theory consisting of a single function $f$, and consider the theorem
$$ (\forall x,y: f(x) = f(y) \Rightarrow x = y) \Rightarrow (\forall x \exists y: f(y) = x) $$
which, translated into english, says that if $f$ is injective, then $f$ is surjective. This statement is certainly true for finite sets, arguing by means of cardinalities. But the theorem is false for infinite sets, which implies, since our axiom system is finite, there must be a finite model of the theory and a `function' which is injective but nor surjective. What is this model?
 A: There are a few things going on here.
First of all, the claim 

if a small enough axiom system is consistent, then there is a finite model of that theory.

is false: e.g the axiom "$f$ is injective but not surjective" in the language consisting of a single function symbol "$f$" has only infinite models. What is true is that any theory in first-order logic with arbitrarily large finite models has an infinite model - this is the compactness theorem, probably the most important basic result in model theory - but that's going the opposite way.
Second, and more relevantly, I think you are conflating two different expressions: a first-order sentence in a particular language, and a second-order sentence$^{*}$ which makes sense in any language.


*

*The statement "Every injective function is surjective" is expressible in second-order logic, and its models are exactly the finite$^{**}$ structures in whatever language we're working with (note that the statement itself doesn't use any nonlogical symbols, so it is expressible regardless of our language). However, it is not first-order expressible.

*The statement you've written is a first-order sentence in a particular language - namely, a language containing a unary function symbol symbol "$f$." Whether it is true or not in a given structure depends on how $f$ is interpreted in that structure; e.g. if we $\mathcal{A}$ be the structure with underlying set $\mathbb{N}$ and $f^\mathcal{A}$ being the function sending everything to $1$, then $\mathcal{A}$ satisfies your statement vacuously (since $f$ is not in fact injective). Less stupidly, we can have $f$ be the identity function. So just knowing that the underlying set of $\mathcal{A}$ is infinite does not tell you whether your statement is true or false in that structure, since that information alone doesn't tell you anything about what $f^\mathcal{A}$ looks like.

$^{*}$An annoyance: there are two ways to understand the phrase "second-order logic" - Henkin semantics and standard semantics. Henkin semantics for second-order expressions is just first-order logic in disguise; when I say "second-order logic," I mean the standard semantics. This is almost universally how the phrase is used, but occasionally you'll run into it being used the other way.
$^{**}$OK fine, strictly speaking its models are the Dedekind-finite sets, not just the finite sets; assuming (a tiny fragment of) the axiom of choice these are the same, but consistently with ZF (= set theory without choice) there are infinite, Dedekind-finite sets (it's even consistent that there are infinite sets that can't be split into two infinite pieces!). But this is really a side issue; I just mention it since it's an interesting technicality.
