Notes

1. a consistent 1st order theory K can be extended to a consistent negation-complete theory K'
Lindenbaum's lemma for 1st order theories
2. extend K to a theory K' that is also closed
3. show that k' has a model (Henkin interpretation)
Lindenbaum's lemma (45.10): K is a consistent 1st order theory, K' is a consistent negation-complete
extension K
let <c1, c2, c3...> be an enumeration of closed wffs in the language K
we define <k0, k1, k2...> as follows:
k0 is k
if ~cn+1 is not a theorem of kn, then kn+1 is kn + {Cn+1}
if ~cn+1 is a theorem of kn, then kn+1 is kn
let k00 be the theory that takes as axioms all the kii
k' is k00
a system S that has at least one closed term is closed iff for each formula A with just one free variable, if the result of substitution of a closed term for the free occurrences of the variable is a theorem, then ^[or]A is also a theorem