Clarifications on proof of compactness theorem

Question

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

http://www.princeton.edu/~hhalvors/teaching/phi312_s2013/compactness.pdf

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!

Answer 1

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$.

Answer 2

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.