Here's the informal part: I'm trying to get a better intuition about the differences between the standard model and the non-standard ones. Some people seem to be really good at imagining what non-standard models might look like. Models like the ultra-product $\mathbb{N}^\mathbb{N}$, while somewhat easy to have as a mental model, do a poor job of refuting sentences because of Łoś's theorem (thank you for pointing this out @qiaochu-yuan). The question through which I hope to improve my intuition is: is there a 'best' model with which to refute unprovable sentences? I expect the answer to the question as asked to be 'no', perhaps because there are two unprovable sentences that hold in the standard model but whose negations contradict each other, but I find it really hard to 'see' how any first order sentence fails to hold in any non-standard model and I certainly weren't able to come up with any such sentences (except by following Gödel's incompleteness result).
Here's the question:
Let $\mathbb{N}$ denote the standard (or prime) model of first order Peano Arithmetics ($PA$), that is: the least (w.r.t elementary embeddings) model such that $\mathbb{N}\vDash PA$. Is there a model $M\vDash PA$, i.e. one that satisfies Peano Arithmetics, but disagrees on every statement $\varphi$ not (dis)provable in $PA$? That is, is there an $M$ such that: $\forall \varphi.~\ PA \vdash \lnot\varphi ~\vee~ M\vDash \varphi ~\vee~ \mathbb{N}\vDash \varphi$
If the answer is yes, I realise this would still give me very little intuition about $M$, because of Tennenbaum's theorem (thank you to @noah-schweber for pointing this out). If the answer is not known, what about a finite set of models $M_1,\ldots,M_n$ s.t. $PA \vdash \lnot\varphi ~\vee~ M_1\vDash \varphi ~\vee \cdots \vee~ M_n\vDash\varphi$? (Completeness gives us a 'yes' for an infinite set of one model per formula.) If the answer is no, can we come up with a concrete set of true (in $\mathbb{N}$) first order formulas $\varphi_1,\ldots,\varphi_n$ such that none of them are disprovable, but their conjunction is disprovable?