How to express that a graph has Independent set of size at least $n/2$ in $\exists SO$

Question

I am looking to provide a formula saying "A graph with $n$ vertices has an independent set $X$ of size at least $n/2$" in existentional second order logic.

(This is exercise 1.2. from Libkin's Elements of Finite Model Theory (see here for online pdf, page 10 of the book (or 23 in the pdf)).

I can express that $X$ is an independent set as follows (assume that our vocabulary containts just one binary relational symbol $E$ for the edge relation):

$$ \exists X (\forall x\forall y : X(x) \wedge X(y) \Rightarrow \neg E(x,y)) $$ However, how to express that $X$ is of size at least $n/2$?

There is a simillar example with bipartite subgraph with at least $m/2$ edges ($m$ is the number of total edges) in the same exercise.

E: For the bipartite subgraph, in fact, this is true in general, so a formula like $\forall x\colon x=x$ would describe all graphs that have bipartite subgraph with at least $m/2$ edges, however, is it expressible really as it is -- without knowing that it is in fact valid for all graphs?

Any hints?

Answer 1

One way to see it is to notice that asking for $|X|\ge n/2$ is the same as asking that $X$ is bigger than $V(G)\setminus X$, which can be witnessed by an injection from $V(G)\setminus X$ to $X$. Thus, the property can be expressed in the following way:

$$ \begin{align*} |X|\ge n/2 &\iff |V\setminus X|\le|X| \\ &\iff \exists F: V\setminus X \hookrightarrow X \\ &\iff \exists F \left(\ \forall x\forall y: F(x)\neq F(y)\ \wedge\ \forall x: \neg X(x)\implies X(F(x))\ \right) \end{align*} $$