[proofplan]
Enumerate all $L$-sentences and build an increasing chain of consistent theories by deciding one sentence at a time. At each stage, if adding the next sentence preserves consistency, add it; otherwise add its negation, and prove that this second choice must preserve consistency. The union of the chain is consistent because every formal contradiction uses only finitely many premises. Since every sentence is eventually decided, the union is complete, and completeness plus consistency gives maximal consistency.
[/proofplan]
[step:Enumerate the sentences and define the recursive extension]
Since $L$ is countable, the set of $L$-sentences is countable. Choose a sequence $(\varphi_n)_{n \in \mathbb{N}}$ of $L$-sentences such that every $L$-sentence appears at least once in the sequence. Here $\mathbb{N}$ denotes the set of positive integers, and $\mathbb{N}_0 := \{0\} \cup \mathbb{N}$ denotes the set of nonnegative integers. We write $\bot$ for a contradiction, and for a set $\Gamma$ of $L$-sentences and an $L$-sentence $\chi$, the notation $\Gamma \vdash \chi$ means that there is a formal proof of $\chi$ from premises in $\Gamma$ in classical first-order logic.
Define an increasing sequence $(T_n)_{n \in \mathbb{N}_0}$ of $L$-theories recursively. Set $T_0 := T$. Suppose $T_n$ has been defined and is consistent. Define
\begin{align*}
T_{n+1}
:=
\begin{cases}
T_n \cup \{\varphi_{n+1}\}, & \text{if } T_n \cup \{\varphi_{n+1}\} \text{ is consistent},\\
T_n \cup \{\neg \varphi_{n+1}\}, & \text{otherwise}.
\end{cases}
\end{align*}
We will prove that every $T_n$ is consistent.
[guided]
The construction follows the usual decision procedure for a Lindenbaum extension. We list the sentences as $\varphi_1,\varphi_2,\dots$ and then decide them one at a time. Here $\mathbb{N}$ denotes the positive integers, $\mathbb{N}_0 := \{0\} \cup \mathbb{N}$ denotes the nonnegative integers, $\bot$ denotes a contradiction, and $\Gamma \vdash \chi$ means that the $L$-sentence $\chi$ has a formal proof from the set $\Gamma$ of premises in classical first-order logic.
The initial theory is
\begin{align*}
T_0 := T.
\end{align*}
By hypothesis, $T_0$ is consistent. Now assume that $T_n$ is already defined and consistent. We look at the next sentence $\varphi_{n+1}$. If adding $\varphi_{n+1}$ keeps the theory consistent, we add it:
\begin{align*}
T_{n+1} := T_n \cup \{\varphi_{n+1}\}.
\end{align*}
If adding $\varphi_{n+1}$ makes the theory inconsistent, we instead add its negation:
\begin{align*}
T_{n+1} := T_n \cup \{\neg \varphi_{n+1}\}.
\end{align*}
The point of the next step is to justify that this second option is safe. It is not enough to define the sequence; we must prove that the construction never destroys consistency.
[/guided]
[/step]
[step:Show that the recursive construction preserves consistency]
We prove by induction on $n \in \mathbb{N}_0$ that $T_n$ is consistent. The base case is the hypothesis that $T_0 = T$ is consistent.
Assume $T_n$ is consistent. If $T_n \cup \{\varphi_{n+1}\}$ is consistent, then $T_{n+1}$ is consistent by definition. It remains to handle the case in which $T_n \cup \{\varphi_{n+1}\}$ is inconsistent. We claim that $T_n \cup \{\neg \varphi_{n+1}\}$ is then consistent.
Suppose, toward a contradiction, that $T_n \cup \{\neg \varphi_{n+1}\}$ is also inconsistent. Since formal derivations use only finitely many premises, there exist finite subsets $\Gamma, \Delta \subset T_n$ such that
\begin{align*}
\Gamma \cup \{\varphi_{n+1}\} &\vdash \bot,\\
\Delta \cup \{\neg \varphi_{n+1}\} &\vdash \bot.
\end{align*}
By the classical first-order [Deduction Theorem](/theorems/1452), applied to the displayed derivation from $\Gamma \cup \{\varphi_{n+1}\}$, the first derivation gives
\begin{align*}
\Gamma \vdash \neg \varphi_{n+1},
\end{align*}
and by the same metatheorem applied to the displayed derivation from $\Delta \cup \{\neg \varphi_{n+1}\}$, the second gives
\begin{align*}
\Delta \vdash \neg\neg \varphi_{n+1}.
\end{align*}
Using the classical double-negation elimination rule, we get
\begin{align*}
\Delta \vdash \varphi_{n+1}.
\end{align*}
Since $\Gamma \cup \Delta \subset T_n$, the theory $T_n$ derives both $\varphi_{n+1}$ and $\neg \varphi_{n+1}$, hence derives a contradiction. This contradicts the consistency of $T_n$. Therefore $T_n \cup \{\neg \varphi_{n+1}\}$ is consistent, so $T_{n+1}$ is consistent in all cases.
By induction, $T_n$ is consistent for every $n \in \mathbb{N}_0$.
[guided]
We prove consistency of every stage by induction.
The base case is immediate from the hypothesis:
\begin{align*}
T_0 = T
\end{align*}
is consistent.
Now assume that $T_n$ is consistent. If $T_n \cup \{\varphi_{n+1}\}$ is consistent, then the construction sets
\begin{align*}
T_{n+1} = T_n \cup \{\varphi_{n+1}\},
\end{align*}
so there is nothing further to prove in that case.
The only delicate case is the alternative branch: suppose $T_n \cup \{\varphi_{n+1}\}$ is inconsistent. We must prove that adding $\neg \varphi_{n+1}$ is consistent. Assume the contrary, namely that $T_n \cup \{\neg \varphi_{n+1}\}$ is also inconsistent.
Inconsistency means that a contradiction is formally derivable. Because formal proofs are finite objects, each such derivation uses only finitely many premises from the theory. Hence there are finite subsets $\Gamma, \Delta \subset T_n$ such that
\begin{align*}
\Gamma \cup \{\varphi_{n+1}\} &\vdash \bot,\\
\Delta \cup \{\neg \varphi_{n+1}\} &\vdash \bot.
\end{align*}
The first derivation says that assuming $\varphi_{n+1}$ together with $\Gamma$ leads to contradiction. Applying the classical first-order Deduction Theorem to that derivation gives
\begin{align*}
\Gamma \vdash \neg \varphi_{n+1}.
\end{align*}
The second derivation says that assuming $\neg \varphi_{n+1}$ together with $\Delta$ leads to contradiction. Applying the same Deduction Theorem to that derivation gives
\begin{align*}
\Delta \vdash \neg\neg \varphi_{n+1}.
\end{align*}
By the classical double-negation elimination rule,
\begin{align*}
\Delta \vdash \varphi_{n+1}.
\end{align*}
Since both $\Gamma$ and $\Delta$ are subsets of $T_n$, the theory $T_n$ proves both $\varphi_{n+1}$ and $\neg \varphi_{n+1}$. Thus $T_n$ proves a contradiction, contradicting the inductive hypothesis that $T_n$ is consistent.
Therefore, if adding $\varphi_{n+1}$ is inconsistent, adding $\neg \varphi_{n+1}$ must be consistent. This completes the induction.
[/guided]
[/step]
[step:Take the union and prove it is consistent]
Define
\begin{align*}
T^* := \bigcup_{n=0}^{\infty} T_n.
\end{align*}
Then $T \subset T^*$ because $T = T_0 \subset T^*$.
We prove that $T^*$ is consistent. Suppose, toward a contradiction, that $T^*$ is inconsistent. Then there is a finite subset $\Sigma \subset T^*$ such that
\begin{align*}
\Sigma \vdash \bot.
\end{align*}
For each sentence $\sigma \in \Sigma$, choose an index $n_\sigma \in \mathbb{N}_0$ such that $\sigma \in T_{n_\sigma}$. Since $\Sigma$ is finite, the integer
\begin{align*}
N := \max\{n_\sigma : \sigma \in \Sigma\}
\end{align*}
is well-defined. The sequence $(T_n)_{n \in \mathbb{N}_0}$ is increasing, so $\Sigma \subset T_N$. Hence $T_N \vdash \bot$, contradicting the consistency of $T_N$. Therefore $T^*$ is consistent.
[guided]
We now pass from the finite-stage theories to their union:
\begin{align*}
T^* := \bigcup_{n=0}^{\infty} T_n.
\end{align*}
Because $T_0 = T$ and the sequence is increasing, we have $T \subset T^*$.
The key point is that consistency survives the union. Suppose the union were inconsistent. Then there would be a formal proof of contradiction from premises in $T^*$. Formal proofs are finite, so only finitely many premises from $T^*$ are actually used. Let $\Sigma \subset T^*$ be this finite set of premises, so
\begin{align*}
\Sigma \vdash \bot.
\end{align*}
Each sentence $\sigma \in \Sigma$ entered the construction at some finite stage, so choose $n_\sigma \in \mathbb{N}_0$ with $\sigma \in T_{n_\sigma}$. Since $\Sigma$ is finite, the maximum
\begin{align*}
N := \max\{n_\sigma : \sigma \in \Sigma\}
\end{align*}
exists. Because the theories are nested,
\begin{align*}
T_0 \subset T_1 \subset T_2 \subset \cdots,
\end{align*}
every sentence in $\Sigma$ belongs to $T_N$. Thus the same finite derivation of contradiction is already a derivation from $T_N$, contradicting the consistency of $T_N$.
So $T^*$ is consistent.
[/guided]
[/step]
[step:Use the enumeration to show that every sentence is decided]
Let $\psi$ be an arbitrary $L$-sentence. Since $(\varphi_n)_{n \in \mathbb{N}}$ enumerates all $L$-sentences, choose $k \in \mathbb{N}$ such that $\psi = \varphi_k$.
At stage $k$, the construction adds either $\varphi_k$ or $\neg \varphi_k$ to $T_k$. Hence either
\begin{align*}
\psi \in T^*
\end{align*}
or
\begin{align*}
\neg \psi \in T^*.
\end{align*}
Since $T^*$ is consistent, it cannot contain both $\psi$ and $\neg \psi$. Therefore, for every $L$-sentence $\psi$, exactly one of $\psi$ and $\neg \psi$ belongs to $T^*$.
[guided]
Let $\psi$ be any $L$-sentence. The enumeration was chosen so that every $L$-sentence occurs somewhere in the sequence, so there is an index $k \in \mathbb{N}$ with
\begin{align*}
\psi = \varphi_k.
\end{align*}
At the recursive stage that decides $\varphi_k$, the construction adds either $\varphi_k$ or its negation $\neg \varphi_k$ to the next theory in the chain. Since every later $T_n$ is contained in the union $T^*$, this gives either
\begin{align*}
\psi \in T^*
\end{align*}
or
\begin{align*}
\neg \psi \in T^*.
\end{align*}
The consistency of $T^*$ rules out the possibility that both occur: if both $\psi$ and $\neg \psi$ belonged to $T^*$, then $T^*$ would formally derive a contradiction in classical first-order logic. Thus each $L$-sentence is decided by $T^*$, and exactly one of $\psi$ and $\neg \psi$ belongs to $T^*$.
[/guided]
[/step]
[step:Conclude maximal consistency]
It remains to prove maximality. Let $S$ be a consistent $L$-theory such that $T^* \subset S$. Suppose, toward a contradiction, that $T^* \subsetneq S$. Choose a sentence $\theta \in S \setminus T^*$.
By the previous step, exactly one of $\theta$ and $\neg \theta$ belongs to $T^*$. Since $\theta \notin T^*$, we have $\neg \theta \in T^*$. Because $T^* \subset S$, this implies $\neg \theta \in S$. But also $\theta \in S$, so $S$ is inconsistent, contradicting the assumption that $S$ is consistent.
Thus no proper consistent $L$-theory extends $T^*$. Hence $T^*$ is maximally consistent, contains $T$, and decides every $L$-sentence. This proves the Lindenbaum Extension Lemma.
[guided]
We now verify that the consistent theory $T^*$ is maximal among consistent $L$-theories. Let $S$ be a consistent $L$-theory satisfying
\begin{align*}
T^* \subset S.
\end{align*}
To prove maximality, we must show that this inclusion is equality. Suppose instead that it is proper. Then there is an $L$-sentence $\theta$ such that
\begin{align*}
\theta \in S \setminus T^*.
\end{align*}
The previous step says that $T^*$ decides every $L$-sentence exactly once. Applying that result to $\theta$, and using $\theta \notin T^*$, we obtain
\begin{align*}
\neg \theta \in T^*.
\end{align*}
Since $T^* \subset S$, this implies
\begin{align*}
\neg \theta \in S.
\end{align*}
But by the choice of $\theta$, we also have $\theta \in S$. Therefore $S$ contains both $\theta$ and $\neg \theta$, so $S$ is inconsistent in classical first-order logic. This contradicts the assumption that $S$ is consistent.
Hence no proper consistent $L$-theory extends $T^*$. We have already shown that $T \subset T^*$ and that $T^*$ is consistent. Therefore $T^*$ is a maximally consistent $L$-theory extending $T$, which is the desired conclusion.
[/guided]
[/step]