Proving equivalence of two notions of an acyclic graph over graphs of arbitrary size I'm trying to show that a simple proof calculus for a first-order theory of a strict partial order ($<$ and propertyless constant symbols) is compact without using the compactness of first-order logic. The axioms for a strict partial order are $\forall a b c \mathop. (a < b \land b < c \to a < c)$ and $\forall a \mathop. \lnot (a < a)$. For the moment I am restricting attention to quantifier-free, connective-free, and variable-free propositions like $a < b$ where $a$ and $b$ are constant symbols. However, because the compactness of this restricted theory falls right out of the compactness of first-order logic more generally, I am certain that this theory is compact.
In order to show this, I want to reframe the problem using elementary graph theory. I'm close to a solution, but I'm not sure how to get the transfinite induction to work right. How do you prove the infinite case?
I want to show that two definitions of being an acyclic graph are equivalent for graphs of any size.

*

*A graph $G$ does not contain a $k$-cycle for any $k \in \mathbb{N}$.

*For every edge $E = (u, v)$, there exists a red-blue vertex coloring of $G$ so that there are no blue-to-red edges and $E$ is red-to-blue.

Metaphorically, blue is true; red is false; edges from true to false are bad.
Call a graph that is acyclic according to the first definition (1)-acyclic and a graph that is acyclic according to the second definition (2)-acyclic.
Graphs have directed edges and self-loops permitted. A self-edge doesn't have a coloring of the kind in condition (2) because the same vertex can't be both red and blue.
For finite graphs, the equivalence is pretty clear. If your finite graph $G$ contains a cycle in it, then picking any edge in the cycle and making it red-to-blue will force one of the edges in the cycle to be blue-to-red.
Similarly, for a finite graph, if a consistent coloring can be extended from an edge $E$ to the rest of the graph, then $E$ can't be part of a $k$-cycle. If this holds for all edges $E$ then the whole graph is acyclic.
Okay, so far, so good. Now let's consider infinite graphs.
Every (1)-cyclic graph is (2)-cyclic. Suppose there's a $k$-cycle. Pick one of its edges, there is no consistent coloring where that edge is red-to-blue.
It is harder to show that every (1)-acyclic graph is (2)-acyclic.
I have the start of an argument.
I intend to show that $G$ is 2-acyclic by choosing an arbitrary edge $E$ and showing that we can construct a consistent coloring starting at $E$ and extending outwards to the component containing $E$.
Pick a graph $G$. Suppose that it is (1)-acyclic, or equivalently that it has no $k$-cycles for any finite $k$.
If $G$ contains a self-edge then we're done because $G$ isn't (1)-acyclic.
Suppose $G$ has no self-edges.
If $G$ contains no edges at all, then it is (1)-acyclic and (2)-acyclic.
Suppose $G$ has at least one edge.
Consider a partial coloring of the graph $G$ with no colors applied to any vertices. Let's call this partial coloring step 0.
Pick an edge $E$ arbitrarily and make it red-to-blue. Additionally, color every vertex outside the connected component containing $E$ blue, arbitrarily. Call this step 1.
Okay, now suppose $\kappa = \lambda + 1$ is a successor ordinal. Let step $\kappa$ be the partial coloring associated by making every vertex with an edge to a red vertex red and every vertex with an edge from a blue vertex blue.
Okay, now suppose $\kappa$ is a limit ordinal. Take the union of all the previous partial colorings.
Let $\kappa$ be an ordinal that is in bijection with the vertices of $G$.
Define the coloring $\pi$ as $\bigcup_{\alpha < \kappa} [\text{step $\alpha$}]$ associated with the edge $E$.
The union of an arbitrary collection of partial colorings with no blue-to-red edges has no blue-to-red edges, therefore none of the steps involved in the construction of $\pi$ introduced a blue-to-red edge. Therefore there are no blue-to-red edges.
Because our starting edge $E$ was chosen arbitrarily, $G$ is (2)-acyclic.
I'm not convinced by this transfinite construction. The argument that each of the steps preserved this property, therefore the whole object has this property feels a little weak. The construction also seems fragile. I added the additional restriction in bold, that everything outside the connected component containing $E$ is made blue arbitrarily, after finishing the proof, and I'm not certain there aren't other gaps. What is the correct way to make this kind of transfinite argument?

Changes

*

*2022-01-14: Fix up the labels of $(1) \implies (2)$, as suggested by Misha Lavrov in the comments.

 A: Transfinite induction is not necessary, because all paths in graphs are finite.
Suppose that our graph has no cycles. Let $(u,v)$ be an arbitrary edge. Then color each vertex $w$:

*

*blue, if there is a $v-w$ walk in the graph (equivalently, if there is a $v-w$ path);

*red, otherwise.

For any edge $(x,y)$, if $x$ is blue, then appending $y$ to the $v-x$ walk gives a $v-y$ walk, so $y$ is also blue. Therefore there are no blue-red edges.
If $u$ is blue, then the implied $v-u$ path can be turned into a cycle by adding a final step along edge $(u,v)$. We assumed there were no cycles, so $u$ must instead be red, and therefore $(u,v)$ is a red-blue edge.
This proves that every $(1)$-acyclic graph is $(2)$-acyclic.

The inductive argument in the question is not too different - it is more complicated to say "color $w$ blue if there is a $v-w$ walk and red if there is a $w-v$ walk" but it achieves the same purpose and that's what every step of the induction is doing: after step $k$, we will have done this for all walks of length less than $k$.
In fact, after we have done all the finite steps, we have colored every vertex we are going to color recursively (and so nothing happens in steps $\omega+1$, $\omega+2$, and so forth). This is why transfinite induction is not necessary. If there are still any doubts, here is a quick proof sketch: suppose that vertex $y$ gets colored blue in step $\omega+1$, due to an edge $(x,y)$ where $x$ was blue after the limit step $\omega$. Then $x$ was actually colored blue in some finite step $k$, because the coloring in step $\omega$ is just the union of colorings done in the finite steps. However, that means we would have already colored $y$ blue in step $k+1$: we do not need to wait infinitely long to color $y$. (The case for red vertices is symmetric.)
The vertices that need to be colored by a separate rule are those with no incoming edge from any blue vertex and no outgoing edge to any red vertex. I color them all red, but it's fine to also color them all blue: all we want is that there is no blue-red edge between two of them.
Note, however, that these are not precisely "vertices outside $E$'s connected component". I assume this means "weakly connected component" because the strongly connected components are all isolated vertices. But there can be vertices in the same weakly connected component which the induction would not color: for example, a vertex with no incoming edges, and an outgoing edge to $v$.
