On an explicit model for $\mathbf Q$ with the negation of the axiom of induction I've been thinking for a while about non standard models of Robinson Arithmetic (here on out referred to as $\mathbf Q$), specifically ones in which induction ($\mathbf{AI}$) fails. This could happen in two ways: (1) $\mathbf Q$ is left as is without induction and non standard models are analysed on it, and (2) we add the negation of $\mathbf{AI}$ to $\mathbf Q$ (a system which I've quirkly named Hume Arithmetic) and search for a model on it.
On this post I'll mainly focus on the latter approach. $\neg \mathbf{AI}$ implies that there exists a formula with a free variable $P$ such that $P(0) \wedge \forall x (P(x) \rightarrow P(x'))$ is true but $\forall x P(x)$ does not hold. I've been thinking for a few months about this on and off but can't seem to find any model that could satisfy $\neg \mathbf{AI}$, much less a specific formula. I know one must exist because for $\mathbf{Q}$ and $\mathbf{PA}$ to be different systems then $\mathbf{AI}$ has to be contingent in $\mathbf{Q}$.
Any help with ways to find such a model? And I know this might sound silly, but if you're going to give an explicit answer on a model can you add a spoiler warning? I realise that with my current skills and understanding I can't solve this but I'd still love to give it a try for myself, even if it's with a little help!
 A: Great question!
In my opinion, the simplest nonstandard model of $Q$ consists of polynomials (in one variable). Specifically, let $\mathfrak{P}$ be the set consisting of all integer-coefficient polynomials in the variable $x$ with positive leading coefficient ... and also the zero polynomial. With successor, addition, and multiplication defined in the obvious way, $\mathfrak{P}$ forms a model of $Q$, and this is easy to check.
(At this point it's also a good idea to check that a couple other obvious ideas don't work: e.g. the set of all polynomials with integer coefficients does not yield a model of $Q$.)
This is a really pretty structure, and something it's not hard to care about. But I claim that induction breaks in it ... really really badly in fact! You said you didn't want spoilers, so I've hidden the full answer below, but here's a hint: think about parity (even vs. odd).

 The key idea is that, while every natural number is either even or odd, it doesn't make a whole ton of sense to ask whether the polynomial "$x$" is even or odd. This motivates the following counterexample to induction in $\mathfrak{P}$: look at the property $EoO(a)$ = "Either for some $b$ we have $S(b+b)=a$, or for some $b$ we have $b+b=a$." It's easy to check that in $\mathfrak{P}$, $(i)$ not every element satisfies $EoO$, but $(ii)$ 0 does satisfy EoO and $(iii)$ if $a$ satisfies $EoO$ then $S(a)$ also satisfies $EoO$. So this does in fact constitute a failure of induction in $\mathfrak{P}$.


Incidentally, you've had a huge bit of luck here in your choice of $Q$ specifically.
There are lots of theories between $Q$ and PA, generally of the form [ordered semiring axioms] + [some fragment of the whole induction scheme]. For example, the theory I$\Sigma_1$ consists of the ordered semiring axioms together with the induction scheme for $\Sigma_1$ formulas. This is an attractive theory in a lot of contexts, and - like $Q$ - the gap between it and PA is measured by induction. But there is an important sense in which $Q$ is tame in a way that I$\Sigma_1$ isn't: namely, Tennenbaum's theorem. The theory I$\Sigma_1$ has no "easily describable" nonstandard models, so while you could ask the same question about I$\Sigma_1$ you couldn't get quite as snappy an answer.
In general, Tennenbaum's theorem explains a conspicuous gap in the literature: why, in all the discussion of incompleteness of PA, are there no analyses of specific interesting nonstandard models of PA? The answer is that Tennenbaum largely rules out this possibility. This also helps motivate $Q$: Robinson found a theory which is weak enough to have lots of interesting, easily-describable, and very different models while also being strong enough to be subject to Godel's incompleteness theorem.
