The Erdős–Hajnal property for a fixed forbidden induced subgraph $H$

Read-back of the definition ErdosHajnalConjectureFor.

The definition takes a type $W$ (any type, in any universe, possibly empty or infinite) and a simple graph $H$ on vertex set $W$ (a simple graph is an irreflexive, symmetric adjacency relation $\sim_H$ on $W$: no loops, no multiple edges). It produces the following proposition, written here in full:

Every binder and hypothesis, in order:

• $c$: there exists a real number $c$ with $0 < c$ (strict). No upper bound is imposed on $c$. The quantifier on $c$ comes before those on $V$ and $G$, so a single $c$ (depending only on $H$) must work for all $V$ and $G$ below.

• $V$: for every type $V$ in the lowest universe (ordinary sets) that is equipped with a finiteness structure; i.e. $V$ ranges over all finite vertex sets, the empty set included. No decidability or other assumptions are made on $V$.

• $G$: for every simple graph $G$ on vertex set $V$ (adjacency written $\sim_G$).

• Hypothesis $H \not\trianglelefteq G$: it is not the case that $H$ is inducingly contained in $G$. Here $H \trianglelefteq G$ means that there exists a graph embedding of $H$ into $G$, i.e. an injective map $f : W \to V$ such that for all $a, b \in W$: $f(a) \sim_G f(b)$ if and only if $a \sim_H b$. Equivalently, $G$ has an induced subgraph isomorphic to $H$. So the hypothesis says: $G$ contains no induced copy of $H$. (It is not the weaker statement "$G$ contains no subgraph isomorphic to $H$": a copy of $H$ in $G$ with extra edges among its vertices does not violate the hypothesis.)

• Conclusion: there exists a finite set $s$ of vertices of $G$ (any subset of the finite set $V$; $s$ may be empty) such that

  1. either $s$ is a clique of $G$, meaning: for all $u, v \in s$ with $u \ne v$, $u \sim_G v$ (every two distinct elements of $s$ are adjacent);
  2. or $s$ is a clique of the complement graph $\overline{G}$, whose adjacency is "$u \ne v$ and $u \not\sim_G v$"; i.e. for all $u, v \in s$ with $u \ne v$, $u \not\sim_G v$ — $s$ is an independent set of $G$;

  and, comparing real numbers,

where $|s|$ is the number of elements of $s$, $|V|$ is the number of vertices of $G$ (both cast from natural numbers to reals), the inequality is non-strict ($\ge$, not $>$), and $x^{c}$ is the real power with real exponent: for $x > 0$ it is $e^{c \ln x}$; for $x = 0$ and $c > 0$ it is $0^{c} = 0$. (Since $c > 0$ is required, the convention $0^0 = 1$ never comes into play.)

Edge cases silently included by the quantifiers:

• $V$ may be empty. Then $|V|^{c} = 0^{c} = 0$ and $s = \varnothing$ satisfies the conclusion, because $\varnothing$ is vacuously a clique of both $G$ and $\overline{G}$ and $0 \ge 0$.
• Any singleton $s = \{v\}$ is vacuously both a clique of $G$ and a clique of $\overline{G}$; so whenever $|V|^{c} \le 1$ (for instance $|V| = 1$, or $V$ empty) the conclusion is met by a singleton or by $\varnothing$.
• If $W$ is empty ($H$ has no vertices), the empty map is an embedding of $H$ into every $G$, so $H \trianglelefteq G$ always holds, the hypothesis $H \not\trianglelefteq G$ can never be satisfied, and the universally quantified part is vacuously true; the whole proposition then reduces to "there exists a real $c > 0$", which is true.
• If $W$ is infinite, no injective map $W \to V$ into a finite $V$ exists, so the hypothesis holds for every finite $G$ and the proposition asserts the conclusion for all finite simple graphs $G$ (on any finite vertex set).
• Nothing requires $H$ to be finite, nonempty, or connected; $H$ enters only through the hypothesis $H \not\trianglelefteq G$.