On lovely pairs and the \((\exists y\in P)\) quantifier (Q817964)

Recall that a simple theory is low if for any formula \(\varphi(x,y)\) and \(z\) the condition that \(\varphi(.,y)\) forks over \(z\) is type-definable (in \(y,z\)). The authors define the theory to be weakly low if for any complete finitary type tp\((a/B)\) and formula \(\varphi(x,y,z)\) (with parameters in \(B\)) there is some formula \(\psi(y)\) with parameters in \(Ba\) true for any \(b\) independent of \(a\) over \(B\) iff \(\varphi(a,b,.)\) does not fork over \(Bb\). In particular a low theory is weakly low. An elementary pair \(P\prec M\) is said to eliminate the quantifier \(\exists y\in P\) if for every formula \(\varphi(x,y,z)\) and \(a\in M\) there is a formula \(\psi(x,w)\) and \(b\in M\) such that for all \(c\in P\) there is \(d\in P\) with \(M\models\varphi(c,d,a)\) iff \(M\models\psi(c,b)\). This condition is equivalent to quantifier-elimination of the structure \(P\) in the language where we have relations for all traces of \(M\)-definable subsets. A pair \(P\prec M\) is \(\kappa\)-lovely, if for all \(A\) of cardinality less than \(\kappa\) and all types \(p\) over \(A\) some non-forking realization of \(p\) over \(A\cup P\) is realized in \(M\), and if \(p\) does not fork over \(P\cap A\), then it is realized in \(P\). For stable theories, lovely pairs are precisely Poizat's beautiful pairs. [\textit{I. Ben-Yaacov, A. Pillay} and \textit{E. Vassiliev}, ``Lovely pairs of models'', Ann.\ Pure Appl.\ Logic 122, 235--261 (2003; Zbl 1030.03026)]. The authors show that a simple theory is weakly low iff some/any lovely pair eliminates \(\exists y\in P\); in this case \(P\) with the induced structure from \(M\) is also simple. If the theory is low, the elimination is uniform. Finally, it is shown that \textit{E. Casanovas'} example [``The number of types in simple theories'', Ann.\ Pure Appl.\ Logic 98, 69--86 (1999; Zbl 0939.03039)] of a simple non-low theory is weakly low; the authors give a variant which isn't.