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

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?

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*}
• I think, to be more pedantic, we should express $F$ to be a binary predicate satisfying the axioms of a function, e.g. $\forall x \exists ! y : F(x,y)$, then injectivity would look like $\forall x_1 x_2 y_1 y_2 : (F(x_1,y_1)\wedge F(x_2,y_2)\Rightarrow y_1=y_2\Rightarrow x_1=x_2)$. But I guess we can always make this shortcut and in fact quantify over function symbols. Anyways, this is the idea I was looking for, tyvm. Jul 13, 2023 at 10:26
• Yes you're right, what you wrote is better, for some reason when I briefly skimmed through the pdf I thought they allowed this kind of shortands but that's not the case and now I see that $X$ and $F$ having the same arity is kind of confusing. Jul 13, 2023 at 11:15