It is!? Does anyone know a proof of Compactness that doesn’t use completeness as a lemma?
There’s actually a direct one on ProofWiki. It’s constructive, even, sort of. (Roughly: take the ultraproduct of all the models of the finite subsets with a suitable choice of ultrafilter.) If you’ve worked with ultraproducts at all, and maybe if you haven’t, this proof is pretty intuitive.
As Qiaochu_Yuan points out, this is equivalent to the ultrafilter lemma, which is independent of ZF but strictly weaker than the Axiom of Choice. So, maybe it’s not that intuitive.
There’s actually a direct one on ProofWiki. It’s constructive, even, sort of. (Roughly: take the ultraproduct of all the models of the finite subsets with a suitable choice of ultrafilter.) If you’ve worked with ultraproducts at all, and maybe if you haven’t, this proof is pretty intuitive.
As Qiaochu_Yuan points out, this is equivalent to the ultrafilter lemma, which is independent of ZF but strictly weaker than the Axiom of Choice. So, maybe it’s not that intuitive.
That’s really beautiful, thanks.