> That’s more about non-categoricity/compactness/Lowenheim–Skolem. As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice,

> That’s more about non-categoricity/compactness/Lowenheim–Skolem. As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice, but the proof of the two Godel theorems does not. That would make a difference for people who are doubtful about the axiom of choice.