I would like to know why the relation: R(x,y) iff x independent from y (i.e: tp(x/y) doesn't fork over the empty set) is type definable in stable theory?
Thanks to the helper.
First, the relation $R(x,y)$ as you defined it is in general not type-definable (although it is definable in any $\aleph_0$-categorical theory, since it is invariant). Indeed, take any stable structure in which $X = \mathrm{acl}(\emptyset)$ is infinite, and take any sequence $(a_n) \subseteq X$ without repetitions. Then we have $R(a_n,a_n)$ for all $n$, but in an ultra-power, if $a = [a_n]$ (the class of the sequence modulo the ultra-filter) then $a \notin \mathrm{acl}(\emptyset)$, so $\neg R(a,a)$. This happens, for example, in the theory of algebraically closed fields, which is as stable as you can get.
Second, for any fixed $b$, the relation $R(x,b)$ is type-definable: $$ R(x,b) = \{ \neg \varphi(x,b) \colon \text{the formula } \varphi(x,b) \text{ forks over } \emptyset \}. $$ I stated this over the empty set, as in the question, but the same is true over an arbitrary parameter set.
The problem is that as $b$ varies, the property "$\varphi(x,b)$ forks over $\emptyset$" varies in a non type definable fashion, so you really must know $b$
Work in a large saturated model, $\mathcal M.$ Things like $x$ and $y$ are not assumed to be singletons. They may be tuples.
First, I want to be careful about just what the question says. To say that this relation is type definable would mean that as a subset of $\mathcal M^2,$ the set of points satisfying the relation is the intersection of definable sets in $\mathcal M^2.$
Lets use the following characterization of forking - everything is over the empty set, but I want to assume that the types are stationary. $a$ forks with $b$ if $tp(a/b)$ represents a new formula. In a stable theory, types are definable, that is, fix a formula $\psi(x,y)$ and consider the set of parameters $c$ so that $b \models \psi (x,c).$ Definability of types says that this is a definable set. In fact, it is a boolean combination of instances of $\psi .$
So, for each new formula that $a$ might represent over $b,$ we can simply tell, definably. Intersecting over the set of all potential new formulas which $a$ might represent gives a type-definable subset of $\mathcal M^2.$
Maybe someone else can comment: is there a way to get around stationarity in a simple manner? Maybe one should just do things over the algebraic closure of the empty set and somehow go back down? Am I just being silly? (I am used to working over models, not over the empty set...)