# Property of finite structure inexpressibiliy in first-order logic

I want two show that a certain property $u$ of some finite structure is not definable in first-order logic.

Is the following reasoning correct?

Let $\mathcal{S}$ denote a finite structure. Further, we can "transform" $\mathcal{S}$ to another finite structure $\mathcal{S'}$ (through some kind of bijection).

We already know that a property $p$ of $\mathcal{S}$ is not definable in first-order logic. Now we assume that $u$ is definable by a sentence $\varphi$. Further, we can show that $$\mathcal{S'} \models \varphi \iff \mathcal{S} \text{ has property } p.$$

That this prove that property $u$ of $\mathcal{S}$ of is not definable in first-order logic?

-
I think you need your map (between $\mathcal{S}$ and $\mathcal{S}'$ to be an isomorphism; maybe just a homomorphism. – Quinn Culver Nov 5 '12 at 12:37

The basic idea is in these two answers was the following: First assume that some first order formula $\varphi ( \bar{x} )$ defines yur relation/function/whatever in the structure $\mathcal{N}$ you are interested in. Then you want to apply an automorphism of $\mathcal{N}$ to show that there are $\bar{a}$ in the universe of $\mathcal{N}$ such that looking at things in one direction you have that $\mathcal{N} \models \varphi ( \bar{a} )$, but looking at it from another direction you get that $\mathcal{N} \models \neg \varphi ( \bar{a} )$. (One direction will come from the definition of property in question, the other from the fact that automorphisms of $\mathcal{N}$ must preserve first-order properties.)
In the two examples I have linked to, there were not enough automorphisms of the structures we were really interested in. We then went to elementary extensions of these structures, which are rich in automorphisms, and show that similar contradictory consequences hold. We went to elementary extensions because if $\varphi ( \bar{x} )$ is supposed to define a relation with certain first-order properties in $\mathcal{N}$, then it must also define a relation with the same first-order properties in every elementary extension of $\mathcal{N}$.