Proof of Consistency Expansion (First Order Logic - Completeness)

[rybla]

In content/first-order-logic/completeness/henkin-expansions.tex, there is a proposition:

If $\Gamma$ is consistent in $\Lang L$ and $\Lang L'$ is obtained from $\Lang L$ by adding !!a{denumerable} set of new !!{constant}s $\Obj d_0$, $\Obj d_1$, \dots, then $\Gamma$ is consistent in~$\Lang L'$.

which doesn't have a proof. I think it should, although perhaps it could be an exercise (doesn't seem like it should be a very involved proof though).

[rzach]

Ah yes, true. The proof depends on the proof system used, so there should be corresponding propositions (with proof left as exercise) in each of the proof system chapters.