the compactness theorem is equivalent to the ultrafilter lemma, which in turn is essentially equivalent to the statement that Arrow's impossibility theorem is false if the number of voters is allowed to be infinite.

Well, I can confirm that I think that that's super cool!

the compactness theorem is independent of ZF

As wuncidunci says, that's only true if you allow uncountable languages. I can't think of many cases off the top of my head where you would really want that... countable is usually enough.

Also: more evidence that the higher model theory of first-order logic is highly dependent on set theory!