Kolmogorov problem on graphs

kolmogorov.txt

# Trying to think about a very modest generalization of the "Kolmogorov Puzzle" that
# dan piponi posted here: https://twitter.com/sigfpe/status/1474173467016589323

Consider a directed graph with vertices V and edges E. Loops and multiple edges are allowed.
All graphs we consider will have the same vertices, so we more or less identify a graph with
its set of edges.

For any graph G, we:

1) write G[x, y] for the set of edges from x to y in G.
2) write G+ for the graph with the same vertices as G, but whose edges
   are finite nonempty paths consisting of edges in G.
3) write G* for the graph that is the same as G+ but which also allows
   empty paths εₓ at every vertex x:V. The set of edges of G* is
   isomorphic to the edges of G+ disjoint union the vertices of G.
4) say a vertex v₀ ∈ V is G-productive if there's an infinite sequence
   of G-edges leading away from it: i.e. if there exists v₁, v₂, v₃
   and edges f₀ ∈ G[v₀,v₁], f₁ ∈ G[v₁,v₂], f₂ ∈ G[v₂,v₃], …
5) say H ⊆ G if H is a spanning subgraph of G; i.e. it has the same
   vertices, and a subset of its edges.


𝐓𝐡𝐞𝐨𝐫𝐞𝐦 [assuming classical logic]
Suppose every vertex in G is E-productive, and D ⊆ E+.
For any x:V, there exists a vertex v:V and an edge k : E*[x,v], such
that v is D-productive or (E+∖D)-productive.

𝐏𝐫𝐨𝐨𝐟
Let x and D be given.
Consider the proposition
    P = ∀y:V. ∀f : E*[x, y].
        ∃z:V. ∃g : E+[y, z].
        ∀w:V. ∀h : E+[z, w]. h ∈ D
Classically, either P is true or false.

In case P is true:

0) P(x, εₓ) gives us an existential witness z₀:V and an edge g₀ : E+[x, z₀].
1) P(z₀, g₀) gives us an existential witness z₁:V and an edge g₁ : E+[z₀, z₁].
2) P(z₁, g₀g₁) gives us an existential witness z₂:V and an edge g₂ : E+[z₁, z₂].
⋯
n+1) P(zₙ, g₀g₁⋯gₙ) gives us an existential witness zₙ₊₁:V and an edge gₙ₊₁ : E+[zₙ, zₙ₊₁].
⋯
etc.

The v that we provide to satisfy the conclusion of the theorem is z₀.
The k that we provide is g₀. We claim v is D-productive.
The sequence of edges that witnesses D-productivity is g₁, g₂, g₃,
…, because the last pair of universal quantifiers in P guarantees that
*any* path out of any of the vertices z₀, z₁, z₂, … belongs to D.

In case P is false: By DeMorgan,
   ¬P = ∃y:V. ∃f : E*[x, y].
        ∀z:V. ∀g : E+[y, z].
        ∃w:V. ∃h : E+[z, w]. h ∉ D

Let y and f be given by the existential. We now know the proposition
    Q = ∀z:V. ∀g : E+[y, z].
        ∃w:V. ∃h : E+[z, w]. h ∉ D

Proceed as follows:
0) Since y:V is E-productive, we know there's some z₀ and g₀ : E[y,z₀].
   Q(z₀, g₀) provides us with w₀:V and h₀ : E[z₀, w₀] with h₀ ∉ D
1) Q(w₀, g₀h₀) provides us with w₁:V and h₁ : E[w₀, w₁] with h₁ ∉ D
2) Q(w₁, g₀h₀h₁) provides us with w₂:V and h₂ : E[w₁, w₂] with h₂ ∉ D
⋯
n+1) Q(wₙ, g₀h₀h₁⋯hₙ) provides us with wₙ₊₁:V and hₙ₊₁ : E[wₙ, wₙ₊₁] with hₙ₊₁ ∉ D

The v that we provide to satisfy the conclusion of the theorem is z₀.
The k that we provide is fg₀. We claim z₀ is (E+∖D)-productive.
The sequence of edges that witness this productivity is h₀, h₁, h₂, ….
∎