Proving a first order sentence is independent of Peano Axioms can be very difficult. An example of such a statement is the Paris-Harrington theorem:
http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem
Modular Arithmetic (MA) has the same axioms as first order Peano Arithmetic (PA) except $\forall x (Sx \ne 0)$ is replaced with $\exists x(Sx = 0)$. MA has arbitrarily large finite models based on modular arithmetic. It is easy to find a first order statement independent of MA. Find a finite model where the statement is true and a finite model where it is false. $0=1$ is independent of the axioms of MA because it is true in the smallest model, the trivial ring, and false in every other model.
I am looking for a statement, $P$, where there are arbitrarily large models where $P$ is true, arbitrarily large models where $P$ is false, and P is not independent of PA. Here are some examples:
These are only true in even size models:
$\exists x(x \ne 0 \land x+x = 0)$
$\forall x(x+x \ne S(0))$
$\exists x \forall y(x \ne y+y)$
This is only true in models of size $n^2+1$. I call these "complex" models because -1 is a square.
$\exists x(S(x*x)=0)$
Because these statements are independent of MA and not independent of PA we know the proof (or disproof) in PA must use the axiom $\forall x (Sx \ne 0)$. For example, proving $0 \ne 1$ requires this axiom.
