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?


1 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*} $$

  • 1
    $\begingroup$ 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. $\endgroup$ Jul 13, 2023 at 10:26
  • $\begingroup$ 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. $\endgroup$
    – pasthec
    Jul 13, 2023 at 11:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.