I am a student of graph theory and recently started learning mathematical logic.
If I am not wrong, any problem in the class Np-Complete can be represented as a SAT formula. As boolean formulas are a subset of first-order logic (FOL), any Np-complete problem can be represented as a problem of verifying an FO formula on some structure (eg. graphs).
Now, there is Courcelle's theorem that states, "every graph property definable in the monadic second-order (MSO) logic of graphs can be decided in linear time on graphs of bounded treewidth". That means some graph properties/ problems need MSO logic to be represented (3-colorability is often presented as an example).
My question is, for which type of graph problems MSO is indeed necessary? Also, can't we represent 3-colorability and all other Np-Complete problems on graphs in first-order logic?