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

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!

• I suppose $s$ is the successor function? Commented May 23, 2020 at 9:33
• Yes, it is the sucessor function Commented May 23, 2020 at 10:01
• In that case every natural number is definable in this theory. So we get an isolated 1-type for every natural number. Did you mean to ask about the isolated 1-types (plural)? Commented May 23, 2020 at 13:13
• Yes, i do mean plural. Commented May 23, 2020 at 13:15
• In that case my previous comment gave a hint about which 1-types are isolated (can you verify this?). Can there be any more? Commented May 23, 2020 at 13:17

## 1 Answer

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.