Talk:Compactness Theorem/Proof using Henkin Construction

Henkin does the witness extension and maximal extension simultaneously, as this is necessary for the witness part anyway. I propose we put that theorem under the combined name Henkin Construction, and use that for Gödel's Completeness Theorem, making this page redundant (since we have Compactness Theorem/Proof using Gödel's Completeness Theorem). Ideally we would also have a version of Gödel's Completeness Theorem which didn't use Axiom of Choice, only Boolean Prime Ideal Theorem or equivalent, but I still need to find a good source for that. --CircuitCraft (talk) 00:47, 14 March 2023 (UTC)