Predicates that, if satisfied, can be satisfied simultaneously: looking for a reference Consider first-order logic with two unary predicate symbols $S$ and $S'$.  Call $S$ and $S'$ resolvable when the following property holds:
$$
((\exists x. S(x)) \land (\exists x.S'(x))) \quad\implies\quad \exists x. S(x)\land S'(x).
$$
With fewer brackets, using spacing:
$$
\exists x. S(x)\ \land\ \exists x.S'(x) \quad\implies\quad \exists x. S(x)\land S'(x).
$$
In words: $S$ and $S'$ are resolvable when if $S$ and $S'$ are satisfiable individually, then they are satisfiable together.
For example, fixing the domain to be natural numbers:

*

*Take $S(x)=\bot$.  Then $S$ and $S'$ are resolvable (for any $S'$) because the implication is trivially true.  It is easy to check that on a nonempty domain, every $S'$ is trivially resolvable with $\bot$.

*Take $S(x)=(x\text{ is odd})$ and $S'(x)=(x\text{ is even})$.  Then $S$ and $S'$ are not resolvable.  More generally, $S$ and $\neg S$ are never resolvable.

*Take $S=S'$.  Then $S$ and $S'$ are resolvable.  It is easy to check that every predicate is resolvable with itself.

*Take $S(x)$ to hold when "I like the number $x$" and $S'(x)$ to mean "You like the number $x$".  Then our taste in numbers is resolvable when if we both like some numbers, then there is some number that we both like.  This may or may not be valid: it will be valid for instance if $S$ and $S'$ range over possibly empty final segments of the natural numbers (i.e. $\varnothing$ or $[i,)$ for $i$ a natural number, just taking a maximum where this exists).

I don't recognise this property and do not recall having seen anything much like it.  I'm hoping to trace if it has been considered somewhere, and if so where.  So:
Question: Does anyone recognise this property, and have a pointer to a field of literature in which it has been studied?
 A: I am not aware of any interesting results about the property you are describing.
The following is not precisely what you are looking for, but maybe this will be helpful or interesting either way. You might think of it as an infinite analogue of what you are describing:
In model theory, a type in a model $M$ is a collection of formulas $t=\{\varphi_i(x) : i \in I\}$ with one free parameter $x$ in the language $L$ of $M$, such that for any finite subset $\{\varphi_{i_0}, \dots, \varphi_{i_n}\}\subseteq t$, the following is true:
$$M \models \exists x: \varphi_{i_0}(x) \land \dots \land \varphi_{i_n}(x)$$
I.e. any finite subset of $t$ is satisfiable. Now we call a type complete, if there exists some global witness, i.e. an element $x\in M$ such that $M\models \varphi_{i}(x)$ for every $i\in I$.
As an easy example of a type, which is not complete, consider the model $(\mathbb Q, <)$ in the language $L = \{<\}$, i.e, we are interested in statements about the linear order on $\mathbb Q$. Now we consider the following type given by $t= \{\varphi_q : q \in \mathbb Q\}$ where
$$\varphi_q (x) =\begin{cases} q < x & \text{ iff } q^2 < 2\\x < q & \text{ iff } q^2 > 2\end{cases}.$$
For any finite number of $q$'s this satisfiable as the order on $\mathbb Q$ is dense. If $t$ was complete, a global witness $x$ would necessarily be $\sqrt{2}$, because it has to be greater than any $q$ which is less than $\sqrt{2}$ but smaller than any $q$ which is greater than $\sqrt 2$. But $\sqrt 2\notin \mathbb Q$, hence $t$ is not complete.
As an example of a complete type, take an arbitrary model $M$ in any language $L$ and fix some $y\in M$, then take $t = \{\varphi(x) : M \models \varphi(y)\}$, this is trivially complete, as we defined $t$ to be set of formulas which hold for this $y$, so we may take $y$ as our global witness. This $t$ is know as the complete type of $y$.
A: As others have pointed out, this is not a validity of FOL, but I think you knew that. Either way, your formula is trivially true whenever the antecedent is false or the consequent is true. Another way that this could trivially be true is if both ∃xSx->∀ySy and ∃yTy->∀yTy are true.
