The theory of a model of a theory that knows all formulas true in almost all its models We are in first order logic world.
Let $\sigma$ be a finite signature and $T$ a consistent theory of $\sigma$.
Due to Löwenheim–Skolem theorem, we can consider the $\underline{set}$ of all at most countable models of $T$ up to elementary equivalance(does not change what formulas hold).
Let $\mu$ be a nonprincipial ultrafilter of it, denote by $\Omega^T_\mu$ the ultraproduct of
all those models  with respect to $\mu$.
Clearly, the theory of $\Omega^T_\mu$ are formulas that are true for almost all with respect to $\mu$ models of $T$.
In particular, this theory, call it $T(\Omega^T_\mu)$, has $T$ as a subset.
My questions are:


*

*Does the equality $T(\Omega^T_\mu)=T$ hold?

*Does it depend on $\mu$? Is the intersection over all $\mu$ equal to $T$?

*If they are not equal, what the difference means? Furthemore, we could consider a sequance of theories $T\subset T(\Omega^T_\mu) \subset T(\Omega^{T(\Omega^T_\mu)}_{\mu'})\subset\ldots$. Does it stabilize?

*Does $T(\Omega^T_\mu)$ complete $T$ in any nice sense?


I suspect that all those questions are classical and already answered, but I do not know where
to look for them. Just before pandemia I have finished my first course on mathematical logic and I have been wondering about this object since then.
 A: In this answer, I will basically repeat things that zeb said in their nice answer, but arranged differently (in a way that might or might not be more clear). 
Let $\text{Mod}_{\leq \aleph_0}(T)$ be the "set" of all at most countable models of $T$. Your question is a bit ambiguous about what this means - I'll come back to that later. Morally, picking an ultrafilter on $\text{Mod}_{\leq \aleph_0}(T)$ is the same as picking a completion of $T$. 
In one direction, if you pick an ultrafilter $\mu$ on $\text{Mod}_{\leq \aleph_0}(T)$, you can take the complete theory of the ultraproduct, $T(\Omega^T_\mu)$ in your notation. This is a complete theory, and it contains $T$, so it's a completion of $T$. 
In the other direction, given a completion $T\subseteq T'$, for each sentence $\varphi\in T'$, consider the set of models $M_\varphi = \{M\in \text{Mod}_{\leq \aleph_0}(T)\mid M\models \varphi\}$. Then $F_{T'} = \{M_\varphi\mid \varphi\in T'\}$ has the finite intersection property, so we can extend it to an ultrafilter. And moreover for any ultrafilter $\mu$ extending $F_{T'}$, we have $T(\Omega^T_\mu) = T'$, by Łoś's Theorem. 
But now there's a subtlety here: You want $\mu$ to be a non-principal ultrafilter.
If by $\text{Mod}_{\leq \aleph_0}(T)$, you mean a set of isomorphism representatives for the models of $T$, so this set contains just one copy of each model of $T$ up to isomorphism, then if $T'$ has only one (at most countable) model (i.e. if it's the theory of a finite structure, or if it's $\aleph_0$-categorical), then the ultrafilter $\mu$ you get by the above construction will be principal. That is, picking a non-principal ultrafilter on $\text{Mod}_{\leq \aleph_0}(T)$ picks a completion of $T$, but we never get a completion that is $\aleph_0$-categorical or the theory of a finite structure. Worse, if $T$ already has only finitely many (at most countable) models up to isomorphism, then there is no non-principal ultrafilter on $\text{Mod}_{\leq \aleph_0}(T)$ - this corresponds to the fact that $T$ has no completion with more than one (at most countable) model. 
These issues go away if $\text{Mod}_{\leq \aleph_0}(T)$ contains infinitely many copies of each model up to isomorphism (e.g. if it's more like the proper class of all at most countable models of $T$). Then when we extend $F_{T'}$ to an ultrafilter $\mu$, we can always make sure $\mu$ is non-principal. 
So the answer to your questions are: 
(1) $T(\Omega_\mu^T) = T$ if and only if $T$ is already complete.
(2) Yes, it definitely depends on $\mu$ (unless $T$ is complete). If you remove the restriction that $\mu$ be non-principal, the intersection of all theories of the form $T(\Omega^T_\mu)$ is $T$. If you require $\mu$ to be non-principal, this intersection is the set $T_{\text{cof}}$ of all sentences which are in all but finitely many models in $\text{Mod}_{\leq \aleph_0}(T)$. If $\text{Mod}_{\leq \aleph_0}(T)$ contains infinitely many copies of each model up to isomorphism (e.g. if this "set" is actually the proper class of all at most countable models of $T$), then again $T_{\text{cof}} = T$. 
(3) The "difference" consists of moving from $T$ to a completion. The chain stabilizes after the first step, i.e. $T(\Omega_\mu^T) = T(\Omega_{\mu'}^{T(\Omega_\mu^T)})$, since $T(\Omega_\mu^T)$ is already complete.
(4) Yes, $T(\Omega_\mu^T)$ is a completion of $T$. 
A: The theory of $\Omega_{\mu}^T$ will automatically be a complete theory which extends the original theory $T$, just because it is the theory of a particular model, and every statement is either true or false in any particular model. It will usually contain more than just the statements that are true in all but finitely many of the models of $T$.
If your original theory $T$ has a statement $\phi$ which is true in infinitely many countable models and false in infinitely many other countable models, then it is easy to construct an ultrafilter $\mu$ which contains the set of models where $\phi$ holds, and to construct another ultrafilter $\mu'$ which contains the set of models where $\phi$ fails (since any filter is contained in an ultrafilter). So $\phi$ will hold in $\Omega_{\mu}^T$ but not in $\Omega_{\mu'}^T$.
For example, the first order theory $N$ of the natural numbers (Peano arithmetic) is known to have infinitely many non-isomorphic models which contain (non-standard) numbers encoding proofs of contradictions in Peano arithmetic, as well as infinitely many non-isomorphic models which do not contain numbers encoding proofs of contradictions in Peano arithmetic, so you can construct ultrafilters $\mu, \mu'$ such that $\Omega_{\mu}^N$ is a model of Peano arithmetic which asserts the inconsistency of Peano arithmetic, while $\Omega_{\mu'}^N$ is a model of Peano arithmetic which asserts the consistency of Peano arithmetic.
Edit: A stronger observation than the above is this. Suppose $T'$ is any extension of the theory $T$ such that $T'$ has infinitely many nonisomorphic countable models. Then there is a non-principal ultrafilter $\mu$ such that $\Omega_{\mu}^T$ is a model of $T'$. Again, to prove this you just start with the filter generated by complements of singletons and by the set of models of $T'$, and complete it to an ultrafilter.
