Представление доказательств раскрашенными графами и гипотеза Хадвигера

Цветной граф — это граф, дуги которого раскрашены в некоторые цвета. Раскрашенный граф – это граф, вершины которого раскрашены в некоторые цвета. Если $M$ – множество цветных (или раскрашенных цветных) графов порядка $k$ и $G$ – цветной (или раскрашенный цветной) граф, то будем говорить, что $G$ $M$-правилен (или $M$ – правильно раскрашен), если все его подграфы порядка $k$ принадлежат $M$.
Мы покажем, как по любой формуле $p$ исчисления предикатов первого порядка построить конечное множество $B_p$ цветных графов порядка 3 и конечное множество $C_p$ раскрашенных цветных графов порядка 2 такие, что $\vdash p$ тогда и только тогда, когда существует $B_p$ – правильный цветной граф, не допускающий $C_p$ – правильной раскраски.
Гипотеза Хадвигера (ГХ). Если ни один подграф графа без петель $G$ не стягиваем к полному графу порядка $n$, то вершины $G$ можно раскрасить в $n-1$ цвет так, что соседние вершины раскрашены в различные цвета.
Мы построим формулу $X$ исчисления предикатов первого порядка такую, что ГХ эквивалентна $\rceil\vdash X$. Таким образом, ГХ сводится к ГХ${}_1$: если все подграфы порядка 3 цветного графа $G$ принадлежат $B_X$, то $G$ $C_X$ – правильно раскрашиваем.
Здесь $B_X$ и $C_X$ – конкретные конечные множества цветных графов порядка 3 и раскрашенных цветных графов порядка 2 соответственно. Библ. – 5 назв.