> By the compactness theorem this is guaranteed to work.

I think you mean completeness, but essentially yes.

In this case I meant compactness - if a statement follows from your (possibly infinite set of) axioms then it follows from a finite subset of them. But you can skin the cat in many ways, yeah (proof theory vs model theory way of looking at it I guess).