# What can we prove with infinite graphs that we cannot prove without them?

I asked the following question on CSTheory.SE and was advised that this site might be a more appropriate place for it. Below the line you find the slightly edited question, the original one is here.

This is a follow-up question to this one about infinite graphs.

Answers and comments to that question list objects and situations which are naturally modeled by infinite graphs. But there are also numerous (combinatorial) theorems about infinite graphs (see chapter 8 in Diestel's book) of which, for example, König's infinity lemma is a famous one.

Now I have the following question: What can we prove with such theorems about infinite graphs that we cannot prove without them? Or more specifically, what is an example where we model something as an infinite graph, then invoke a theorem about infinite graphs, and in the end have proved something about the original problem -- without knowing how to prove it otherwise?

-
It seems difficult to make precise what it means to say a theorem is about infinite graphs. In set theory, everything is a set, and a set is just a (directed) graph. A slightly more precise question is: what interesting properties of finite graphs cannot be proved in Peano arithmetic? – Colin McQuillan Sep 13 '12 at 14:47
@ColinMcQuillan: You're quite right and I was struggling explaining what I actually mean. Since I don't know much about logic I couldn't express it any better. So thanks for making it more precise. – Gregor Sep 13 '12 at 14:57

The Paris-Harrington theorem is a statement about finite graphs which cannot be proved in Peano arithmetic, but can be proved using the axiom of countable choice and an argument about red-blue colourings of the complete graph on $\mathbb{N}$.