I learned that an $n$-type $\pi$ over a theory $T$ is isolated if there exists a formula $\varphi(x_1,\ldots,x_n)$ such that $T \cup \exists \bar x \varphi$ is coherent and $T\vdash \forall \bar x (\varphi(x) \Rightarrow \psi(x))$ for all $\psi$ in $\pi$.
It seems to me that this says that $\pi$ is basically "finite": if a finite set of formulas $\varphi_i$ implies all the formulas in the type, then taking the conjunction of this set isolates $\pi$. Is this the way to apprehend isolated types?
For example, if $\pi$ is the complete 2-type $tp^{\mathbb C}(1,e)$, $\pi$ expresses all we can say about how $1$ and $e$ relates to each other in the language of rings, right? I think this is not isolated, but I don't know how to prove it formally. However, if $\pi$ is $tp^{\mathbb C}(1, \sqrt 2)$, then it seems to me that $y^2 - 2x$ isolates $\pi$, am I right?
Anyway, I don't have any intuition about what types really are. I would really appreciate any hints on how to apprehend them and how to use them!
First: why do we have types? Because first-order logic is notoriously 'bad' with infinity.
Given any specific formula $\varphi(x)$ and a complete theory $T$ in some language $\mathscr{L}$, we either have $T \vdash \exists x\varphi(x)$ or $T \vdash \lnot \exists x\varphi(x)$. Whether or not any given formula has a realization in a model is entirely determined by the theory of the model. Of course, the same is true for any finite combination of formulas.
But what if we took an infinite collection of formulas? In general, the theory will tell you nothing about whether or not there is a common realization - unless your collection was not really infinite, meaning there is some single formula which implies each one in your set. More often, the existence of a common realization will depend on your specific choice of model.
A type is just a maximal consistent set of formulas in some fixed number of variables. Of course, every type will have lots of redundant formulas: you'll have every tautology, and every possible conjunction of formulas (though the maximality makes this worth it). In isolated types, everything is essentially redundant except for one formula (which implies everything else).
What would you do with types? Sometimes, you want to construct models of theories which either realize or omit a specific set of sentences - this happens a lot, and it's annoying to have to make the same compactness argument every time. It also provides an extremely useful way of comparing nonisomorphic models of a given theory, and counting how close those models are to being 'full'.