Fdtxjr

Let $sigma$ be a first-order language (signature) and let $mathcalA$ be a structure those signature is $sigma$ and those domain is $A$. A subset $Xsubset A$ is called definable in $mathcalA$ if there is a formula $phi$ over $sigma$ such that
$$forall a in A qquad ain X iff mathcalA models phi(a). $$

Let now $psi$ be a formula over $sigma$ with $5$ free variables. Set $Y_psi subset A$ to be a set of all $ain A$ such that there are two functions $F_1, F_2: Ato A$ with the property that for all $x, y in A$ it holds that $mathcalAmodelspsi(a, x, y, F_1(x), F_2(y)).$

Is it true that for all $mathcalA$ and for all $psi$ as above it holds that $Y_psi$ is definable in $mathcalA$?

Essentially my question is whether we can always simulate the following
$$forall x forall y exists f_1 exists f_2 mbox where $f_1$ depends only on $x$ and $f_2$ depends only on $y$ ldots $$
by a standard first-order formula.

One example when this is true is arithmetic, $mathcalA = langlemathbbN, +, cdot, <, =, 0, 1,rangle$. The point here is that definition of $Y_psi$:
$$exists F_1, F_2:mathbbNtomathbbN,, forall x forall y,, psi(a, x, y, F_1(x), F_2(y) )$$
in this case is equivalent to the following:
$$ forall l mbox there are two sequences $S^1, S^2$ of length $l$ s.t. forall x < l,forall y < l,, psi(a, x, y, S^1_x, S^2_y),$$
and the latter can be easily defined in $langlemathbbN, +, cdot, <, =, 0, 1,rangle$ using beta-function.

It remains unclear for me whether this is true for other structures.

Edit actually the proof with arithmetic is incorrect because I am implicitly using Konig's lemma which is false for trees with infinite branching.

No, we cannot do this.

I'll use a branching quantifier to express$^1$ "the universe is infinite" - by the compactness theorem, we can't do this in first-order logic. I'll then show how this gives an answer to the question you've asked, and then answer a secondary question implicit in your post. (And then there will be a footnote.)

Expressing infinitude

Consider the sentence $$(*)quadexists xforall y_1exists_y_1z_1forall y_2exists_y_2z_2[z_1not=xwedge z_2not=xwedge(y_1not=y_2iff z_1not=z_2)]$$ (as it will turn out, this can be simplified a bit, but I think the way I've written it is clearer). Here "$exists_overlineab$" means that $b$ depends only on the tuple $overlinea$.

I claim that for every structure $mathcalA$, we have $$mathcalAmodels(*)iffmathcalAmbox is infinite.$$ One direction is easy: if $mathcalA$ is infinite, there is an injection $i$ from $mathcalA$ to itself which is not a surjection. Pick some $ainmathcalAsetminus im(i)$ to be our $x$ and use $i$ to choose our $z$s ($z_1=i(y_1), z_2=i(y_2)$).

The other direction is the interesting one: why can't $(*)$ have finite models? To establish this, we need to do some analysis of $(*)$.

Moving to second-order logic, $(*)$ is equivalent to the sentence $$(**)quadexists x, F,Gforall y_1,y_2[F(y_1)not=xwedge G(y_2)not=xwedge (y_1not=y_2iff F(y_1)not=G(y_2))].$$ Here $F,G$ are our "strategies" for picking $z_1,z_2$ respectively; the dependence of $z_k$ only on $y_k$ $(kin1,2)$ is reflected in the inputs each function takes.

Suppose $mathcalAmodels(**)$. Pick appropriate witnesses to this: some $ainmathcalA$ and some specific functions $U,V:mathcalArightarrowmathcalA$ such that

• $(i)$ for every $c_1,c_2inmathcalA$ we have $U(c_1)not=anot=V(c_2)$, and




• $(ii)$ for every $d_1,d_2inmathcalA$ we have $U(d_1)=V(d_2)iff d_1=d_2$.

(Of course, such witnesses won't be unique, but so what?)

Our first observation is that from $(ii)$ we get a huge amount of information about $U$ and $V$. Namely, the following two facts:

• 
  $U$ and $V$ are the same function. Suppose otherwise. Then for some $dinmathcalA$ we have $U(d)not=V(d)$. Now take $d_1=d_2=d$ and note that this shows that $(ii)$ above fails.

I'll now use "$W$" to refer to this function, in order to avoid apparent asymmetry.

• 
  The function $W$ is injective. Suppose otherwise. Then we have some $d_1,d_2inmathcalA$ such that $d_1not=d_2$ but $W(d_1)=W(d_2)$; remembering that $U=W=V$, we get that $d_1not=d_2$ but $U(d_1)=V(d_2)$, again contradicting point $(ii)$ above.

Our second observation is simpler: clause $(i)$ tells us that the function $W$ must not have $a$ in its image.

So putting this all together, we've concluded:

If $mathcalAmodels(*)$, then there is an injection from $mathcalA$ to itself which is not a surjection.

But this can only happen if $mathcalA$ is infinite! So we're done.

From satisfaction to definability

This doesn't really answer your question, which was about definable sets rather than classes of models. But this is just a quick hop away.

Let $mathcalN$ be a nonstandard model of PA with standard part $S$. Then $S$ is clearly undefinable in first-order logic, but it is definable via $(*)$: it's the set of elements whose corresponding initial segments satisfy $neg(*)$.

• This last bit deserves an explanation. First-order logic allows relativization: given a structure $mathcalS$ and a definable substructure $mathcalXsubseteqmathcalS$, for each sentence $varphi$ there is a sentence $varphi^mathcalX$ such that $$mathcalSmodelsvarphi^mathcalXiffmathcalXmodelsvarphi;$$ $varphi^mathcalX$ is gotten by "relativizing" quantifiers, e.g. replacing "$exists x(psi(x))$" with "$exists x(xinmathcalSwedgepsi(x))$." In fact relativization is a bit broader than what I've described, but ignore that for now.
  

Of course, the above assumes $Con(PA)$; what if we don't want to assume that? Well, we're still in luck. Take as our structure $mathcalA$ a set with an equivalence relation such that $(i)$ there are infinitely many infinite classes and $(ii)$ for every finite $n$ there is a finite class with $>n$ elements. It's a standard exercise to show that the set of elements whose classes are infinite is not definable, but it is definable using $(*)$. And this argument can be appropriately formulated and proved in very weak systems - in particular, much weaker than even PA itself.

More definability: the natural numbers

One point that you've raised, which the above doesn't address, is what happens in the structure $mathcalN=(mathbbN; +,times)$:

Is there a branching-quantifier definable subset of $mathcalN$ which isn't first-order definable?

The answer is no - $mathcalN$ can "first-orderize" branching quantifiers - but the proof is a bit subtle. The obstacle of course is that we want to quantify over functions (= strategies), but first-order logic doesn't let us do that, and the failure of Konig's lemma (as you've correctly observed) means that we can't just look at "finite pieces" of functions.

Getting around this obstacle takes two observations:

• The first observation is that for every specific branching-quantifier-formula $varphi$, there is some $n$ such that for every tuple $overlinea$ such that $varphi(overlinea)$ holds we have a witness to $varphi(overlinea)$ which is $Sigma_n$-definable; so to tell whether $varphi(overlinea)$ holds we just need to search over the $Sigma_n$-definable functions.




• The second observation lets us do exactly that. While Tarski showed that truth in $mathcalN$ is not definable in $mathcalN$, we nonetheless have that the set of true $Sigma_n$-formulas is definable for every specific $n$. This lets us search over $Sigma_n$-definable functions, for each specific $n$. Combined with the previous key point, we get the desired result.

Now, this isn't a proof, since each of the two facts above is definitely nontrivial, but in the interests of length I won't sketch their proofs here; if you're interested, I recommend asking a further MSE question (and I'll answer it myself if I have the time).

$^1$The axiom of choice

Wait, what now?

Well, I've used the following claim:

A set is infinite iff there is a non-surjective injection from the set to itself.

This actually isn't provable in ZF (= set theory without choice) alone; the left-to-right direction can fail, and counterexamples are called "infinite Dedekind-finite sets."

However, this isn't really a problem: we still have that every model of $(*)$ must be Dedekind-infinite, and that's enough - ZF alone proves that there is no sentence which is true in exactly the Dedekind-infinite structures. I chose to assume the axiom of choice since I think the situation is a bit easier to understand if we initially assume that infinite sets "work properly" - in particular, it's easier to think about the compactness theorem when you don't have to worry about choice.