What can we prove with infinite graphs that we cannot prove without them?
Here's an example from distributed computing:



1 Background

1.1 Asynchronous Shared Memory Model

Let's consider a collection of distributed nodes that communicate using
shared memory variables. There is an adversary that controls when a node take steps 
and when to deliver messages. The computation is asynchronous, i.e., the 
adversary can delay the steps of nodes for any (finite) amount of time.
You can think of a step of a node as a state transition of its local 
automaton (according to the algorithm) where the next state is determined 
by the current state and the observations of the node since the last step.

1.2 Safety and Liveness

When formally reasoning about the properties of an asynchronous algorithm, 
we distinguish between safety and liveness properties. Informally, a 
safety property can be interpreted as a guarantee that something "bad" 
never happens. (E.g., for mutual exclusion, a safety property would be 
that no two nodes enter the critical section  simultaneously.) Liveness, 
on the other hand, can be interpreted as "something good will eventually 
happen", e.g.: every node eventually terminates. 

To formalize safety, we consider the infinite set ${M}$ of all possible 
executions of all possible algorithms, taking into account all possible 
choices of the adversary. An execution is an infinite sequence of steps.  We can define a metric on $M$ by taking the distance between two distinct 
runs $\alpha,\beta \in M$ to be $2^{-n}$ where $n$ is the first index where $\alpha$ and $\beta$ differ.

A safety property $S$ corresponds to some nonempty set $P\subseteq M$ that 
is closed in the sense that the limit of an infinite 
sequence of runs in $P$ cannot be in $M\setminus P$. So once we know that some property is a safety property, it is sufficient to show that this property holds on finite prefixes.



Applying Koenig's Infinity Lemma

It's not always straightforward to see whether a specific property is a 
safety property: Consider the implementation of read/write atomic objects 
on top of basic shared memory variables. Such an implementation should handle requests and their responses in a way that makes them look as if they happen at some instant in time and don't violate their order of invocation. (Due to the asynchronous operation, the actual duration between request and response might be nonzero.) Atomicity is also known as Linearizability. Section 13.1 of [A] gives a proof that Atomicity is a safety property. The proof uses Koenig's lemma to show that the limit of any infinite sequence of executions (each of which satisfies Atomicity) also satisfies Atomicity. 

[A] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.