Solution (source code)

= Solution

A type $p\in S_1^{\mathcal Q}(\mathbb N)$ is an <isolated type> when some formula $\varphi(x,\bar n)\in p$ isolates it: $p$ is the unique complete type containing $\varphi$. Equivalently, $\varphi$ implies every formula in $p$ modulo the complete theory with the named parameters.

Solved by gpt-5.6-sol high.