Se ha identificado el lugar en el Henkin prueba de compactación donde la elección es utilizado, es decir, en la finalización de una arbitraria de la teoría de la $T$.
Si no desea utilizar la totalidad del Axioma de Elección, usted puede simplemente asumir que "cada primer orden de la teoría tiene una terminación" (llamar a este TC para la teoría de finalización) y seguir con su día. De hecho, esta suposición es estrictamente más débiles que los de CA.
Por lo general la gente no la frase de la asunción, en la forma en que lo hice como TC, en lugar de hablar acerca de la Booleano Primer Idea Teorema (BPIT) (o ultrafilter lema): Cada trivial álgebra de boole tiene un primer ideal (el complemento de la que es una de ultrafilter).
Pero BPIT es equivalente a la CT. Por qué? Bien, usted debe pensar en un álgebra Booleana como la codificación de un (proposicional) de la teoría, y un ultrafilter como la culminación de esa teoría.
BPIT $\to$ TC: Dada una teoría de la $T$, de forma que el Lindenbaum-Tarski álgebra $B_T$ de las sentencias de $T$ modulo comprobable de equivalencia de $T$. Asumiendo $T$ es consistente, $B_T$ es no trivial (es decir,$\top\neq \bot$), por lo que el uso de BPIT, hay un ultrafilter $U$$B_T$. Deje $T' = \{\varphi\mid [\varphi]\in U\}$ y compruebe que $T'$ es una constante en la finalización de $T$.
TC $\to$ BPIT: Dado un trivial álgebra Booleana $B$, vamos a construir una teoría de la $T_B$. Introducir un lenguaje que consta de un símbolo proposicional $P_b$ por cada elemento de a $b\in B$ (un proposicional es un símbolo de $0$-ary relación símbolo - es verdadera o falsa en un modelo - si no eres feliz permitiendo que estas en la lógica de primer orden, en lugar de tomar $P_b$ a ser un unario relación símbolo de un complemento de axiomas para $T_B$: $(\forall x\, P_b(x)) \lor (\forall x\, \lnot P_b(x))$).
Ahora para cada ecuación de la celebración en $B$, añada una relevante axioma $T_B$. Por ejemplo, si $a\lor b = c\land \lnot d$, añadir el axioma $P_a \lor P_b \leftrightarrow P_c \land P_d$ (o $\forall x\, P_a(x) \lor P_b(x) \leftrightarrow P_c(x) \land P_d(x)$ si usted está usando los predicados unarios).
La terminación de las $T'$ $T_B$ debe incluir $P_b$ o $\lnot P_b$ por cada $b\in B$. A continuación, $\{b\in B\mid P_b\in T'\}$ es un ultrafilter en $B$.
