Complete isolated 1-types of the theory $Th(\mathbb{N}, s, P)$

Question

So I wish to describe the complete isolated 1-types of the theory $Th(\mathbb{N}, s, P)$. Where $P$ is the parity (even, odd unary predicate) and $s$ is the successor function. This is an exercise from my lecture notes; The difficulty I'm facing here "applying" the abstract notion of types, and isolation on something concrete (the lack of examples in the notes also doesn't help). Thus I hope with this (simple) example, it can help me in tackling similar questions.

Helps and insights is appreciated.

Cheers!

Answer 1

Every natural number is definable in this theory. For example, $0$ is defined by the formula $zero(z)$ as follows: $$ \forall x(z \neq s(x)). $$ Then we can define $1$ as the successor of 0, i.e. the $y$ such that $$ \exists z(zero(z) \wedge y = s(z)). $$ Continuing this process shows that every natural numbers is definable in $\operatorname{Th}(\mathbb{N}, s, P)$.

Changing the notation a bit, let $\varphi_n(x)$ be the formula that defines $n$. Then this formula isolates the 1-type of $n$. These must be the only isolated 1-types, because no other 1-type is realised in the model $(\mathbb{N}, s, P)$.

---

If that last argument went too quickly, here is it in more detail. The idea is that every isolated type must be realised in every model of the theory (assuming the theory is complete). To see this, let $p(x)$ be isolated by a formula $\psi(x)$. Then either $\exists x \psi(x)$ or $\neg \exists x \psi(x)$ must be a consequence of the theory. Since $\psi(x)$ isolates a type it must be consistent, so $\exists x \psi(x)$ must be a consequence of the theory. Any realisation of $\psi(x)$ will be a realisation of $p(x)$, so every model must realise $p(x)$.

---

Note that in all of this the $P$ does not really play a role.