It is perhaps well-known that ideas from mathematical logic (esp. model theory) can help solve problems in "main-stream" mathematics, e.g. using ideas from model theory to solve problems in algebraic geometry. However, all of those examples seem quite advanced.
Is there an accessible example of using logical ideas to solve problems in other areas of mathematics (including theoretical computer science)? I'm going to give a lecture to undergraduates and would really like to highlight this to them, and ideally the examples would be easily explainable to someone with only basic mathematical training.
The De Bruijn-Erdős theorem seems like a good candidate, its statement only involves graphs, which computer science students with no abstract algebra exposure should also be familiar with.
The chromatic number of a graph $G$, denoted $\chi(G)$, is the least number of colours needed to colour the vertices of the graph in a way such that every edge has endpoints of different colours. The De Bruijn-Erdős theorem states that, given a graph $G$, if $\chi(H)\leq k$ for every finite subgraph $H\subseteq G$, then $\chi(G)\leq k$.
This theorem (and its version for hypergraphs) can be proved by a straightforward application of the compactness theorem for first order order logic, although this was not the first proof given historically