I've been reading through the following proof of compactness theorem:


One thing that struck me is that this proof seems to require language L to be countable, e.g. in Lemma 3, where it's enumerated. As far as I know countability of language is not a requirement, and, weirdly, in Theorem 10 uncountable language L' is used.

I'm quite confident this proof method can be applied to well-orderable language, by applying transfinite induction where it's required, but well-orderability of every set is equivalent to full AC, which is stronger than BPIT, which I heard compactness is equivalent to.

My questions are: can this proof be actually applied to uncountable languages (give or take minor modifications)? If not, can anyone give me a link to proof of this general fact?

Thanks in advance!

  • $\begingroup$ I think there are at least two or three threads about compactness theorem being equivalent to BPIT. Have you bothered looking them up? $\endgroup$ – Asaf Karagila Aug 12 '14 at 17:36
  • $\begingroup$ @AsafKaragila I considered linking the OP to another thread about this, but surprisingly I couldn't find one that spells out the point I wanted to make, that an ultrafilter on a Boolean algebra is the same as a completion of a theory (except for Hans Stricker's answer here which just links to a book). So I decided to that writing a new answer would be worthwhile. $\endgroup$ – Alex Kruckman Aug 12 '14 at 17:49
  • $\begingroup$ @Alex: And I've voted your answer. But there are also one and two and three and four threads (and maybe more) about compactness and the BPI, many of which include references to papers and books that may or may not contain an answer to this question. $\endgroup$ – Asaf Karagila Aug 12 '14 at 18:34

You've identified the one place in the Henkin proof of compactness where choice is used, namely in completing an arbitrary theory $T$.

If you don't want to use the full Axiom of Choice, you can simply assume "every first-order theory has a completion" (call this TC for theory completion) and move on with your day. Indeed, this assumption is strictly weaker than AC.

Usually people don't phrase the assumption in the way I did as TC, instead they talk about the Boolean Prime Idea Theorem (BPIT) (or ultrafilter lemma): Every nontrivial Boolean algebra has a prime ideal (the complement of which is an ultrafilter).

But BPIT is equivalent to TC. Why? Well, you should think of a Boolean algebra as encoding a (propositional) theory, and an ultrafilter as a completion of that theory.

BPIT $\to$ TC: Given a theory $T$, form the Lindenbaum-Tarski algebra $B_T$ of sentences of $T$ modulo provable equivalence from $T$. Assuming $T$ is consistent, $B_T$ is nontrivial (i.e. $\top\neq \bot$), so using BPIT, there is an ultrafilter $U$ on $B_T$. Let $T' = \{\varphi\mid [\varphi]\in U\}$ and check that $T'$ is a consistent completion of $T$.

TC $\to$ BPIT: Given a nontrivial Boolean algebra $B$, we'll build a theory $T_B$. Introduce a language consisting of one propositional symbol $P_b$ for each element $b\in B$ (a propositional symbol is a $0$-ary relation symbol - it's either true or false in a model - if you're not happy allowing these in first-order logic, instead take $P_b$ to be a unary relation symbol an add axioms to $T_B$: $(\forall x\, P_b(x)) \lor (\forall x\, \lnot P_b(x))$).

Now for each equation holding in $B$, add a relevant axiom to $T_B$. For example, if $a\lor b = c\land \lnot d$, add the axiom $P_a \lor P_b \leftrightarrow P_c \land P_d$ (or $\forall x\, P_a(x) \lor P_b(x) \leftrightarrow P_c(x) \land P_d(x)$ if you're using unary predicates).

A completion $T'$ of $T_B$ must include $P_b$ or $\lnot P_b$ for each $b\in B$. Then $\{b\in B\mid P_b\in T'\}$ is an ultrafilter on $B$.

  • $\begingroup$ Where in the proof are you adding the Henkin witnesses ? $\endgroup$ – Rene Schipperus Aug 12 '14 at 17:37
  • $\begingroup$ I'm just addressing the step where we complete the (Henkinized) theory, since this is the only place choice is used. The rest of the proof is just the usual Henkin proof. $\endgroup$ – Alex Kruckman Aug 12 '14 at 17:40
  • $\begingroup$ Yes but how do you Henkinize the theory ? For each formula $\varphi$ of the theory with constants you need to chose a constant $c$ and add the formula $\exists \varphi(x)\rightarrow \varphi(c)$ so that the theory is consistent. $\endgroup$ – Rene Schipperus Aug 12 '14 at 17:44
  • $\begingroup$ There's no use of choice hiding there. Just introduce a constant for each formula of the relevant form. $\endgroup$ – Alex Kruckman Aug 12 '14 at 17:46
  • $\begingroup$ We don't need to enumerate the formulas to do this, and we're not "choosing" the new constants from some infinite pool, we're just introducing them. $\endgroup$ – Alex Kruckman Aug 12 '14 at 17:51

Just well order the language in the order type of an uncountable cardinal. The argument is exactly the same using transfinite induction.

See the answer of Alex and some of the discussion, I add here how to Henkinize the theory without choice. Let $T_0=T$ be a theory in the language $\mathcal{L}_0$ and let $$T_1=T_0\cup \{ \exists \varphi(x) \rightarrow c_{\varphi} |\varphi \in \mathcal{L}_0\}$$ where $c_{\varphi}$ are new constants $\mathcal{L}_1=\mathcal{L}_0 \cup \{c_{\varphi} |\varphi \in \mathcal{L}_0\}$ and in general $$T_{n+1}=T_n\cup \{ \exists \varphi(x) \rightarrow c_{\varphi} |\varphi \in \mathcal{L}_n\}$$ let and
$$\mathcal{L}_{n+1}=\mathcal{L}_n \cup \{c_{\varphi} |\varphi \in \mathcal{L}_n\}$$

Then $\cup T_n$ will be a consistent theory with Henkin witnesses. Now extend to a complete theory using whatever technology you want.

  • $\begingroup$ But to well order any uncountable cardinal we need full power of AC. I've heard that Boolean prime ideal theorem (or equivalently ultrafilter lemma), strictly weaker than AC, is enough to prove general compactness theorem. If that claim is false, please correct me now. $\endgroup$ – Wojowu Aug 12 '14 at 15:58
  • $\begingroup$ Yes, its true compactness is weaker, but I guess you need a different proof, you are using the Henkin witness proof I suppose. $\endgroup$ – Rene Schipperus Aug 12 '14 at 16:02
  • $\begingroup$ No need to use a different proof, see my answer. $\endgroup$ – Alex Kruckman Aug 12 '14 at 17:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.