Suggested improvements for the proof of Lindenbaum's lemma

[marethyu]

I have some thoughts on improving the proof for Lindenbaum's lemma. I am not sure if they can be approved if I make a pull request, so I am opening a discussion here first.

1. I found this paragraph quite hard to follow:

I think it is clearer if it is written this way:

From this, it follows that every finite subset $\Gamma'\subseteq\Gamma^\ast$ is a subset of $\Gamma_n$ for some $n\in\mathbb N$, since for each $B\in\Gamma'$ not already in $\Gamma_0$ is added at some stage $i$. If $n$ is the last one of these stages, then all $B\in\Gamma'$ are in $\Gamma_n$, i.e. $\Gamma'\subseteq\Gamma_n$.

2. The overall proof is a bit chunky to digest. I think the third and fourth paragraphs contribute to unnecessary bloat. Why can't we reuse the fact from the proof of lemma 12.6 that if $\Gamma^\ast$ is inconsistent, then $\Gamma_n$ is inconsistent for some $n$ to quickly finish the proof for $\Gamma^\ast$ is consistent?

[rzach]

The "fact" isn't proved in lemma 12.6, and what's done here is in fact the proof.

How about this for a rewrite:

From this, it follows that $\Gamma^\ast$ is consistent. Let $\Gamma' \subseteq \Gamma^\ast$ be finite. Each $B \in \Gamma'$ is also in $\Gamma_i$ for some $i$. Let $n$ be the largest among these. Since $\Gamma_i \subseteq \Gamma_n$ if $i < n$, every $B \in \Gamma'$ is also $\in \Gamma_n$, i.e., $\Gamma' \subseteq \Gamma_n$. Thus, every finite $\Gamma' \subseteq \Gamma^\ast$ is consistent. By Propositions 10.17 and 11.17, $\Gamma^\ast$ is consistent.

[marethyu]

Ah, I see. So, this lemma's proof contains the solution to the exercise from lemma 12.6's proof?

Yes, this rewrite is more clearer. I'd appreciate it if you update the proof with this new writeup.

[rzach]

Thanks!